Toward diagrammability and efficiency in event-sequence languages |
| |
Authors: | Kathi Fisler |
| |
Affiliation: | (1) Department of Computer Science, WPI, Worcester, MA, USA |
| |
Abstract: | Many industrial verification teams are developing suitable event-sequence languages for hardware verification. Such languages
must be expressive, designer friendly, and hardware specific, as well as efficient to verify. While the formal verification
community has formal models for assessing the efficiency of an event-sequence language, none of these models also accounts
for designer friendliness. We propose an intermediate language for event sequences that addresses both concerns. The language
achieves usability through a correlation to timing diagrams; its efficiency arises from its mapping into deterministic weak
automata. We present the language, relate it to existing event-sequence languages, and prove its relationship to deterministic
weak automata. These results indicate that timing diagrams can become more expressive while remaining more efficient for symbolic
model checking than LTL. |
| |
Keywords: | Timing diagrams Property-specification languages Weak automata |
本文献已被 SpringerLink 等数据库收录! |
|