Towards Diagrammability and Efficiency in Event Sequence Languages

Industrial verification teams are actively 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 account 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.

• Type: Conference
• Year: 2003
• Where: CHARME
• Authors: Kathi Fisler
• Keywords: CHARME 2003, Deterministic Weak Automata, Event Sequence Languages, Hardware, Suitable Event Sequence