Model Checking Synchronous Timing Diagrams

Nina Amla, E. Allen Emerson, Robert P. Kurshan and Kedar S. Namjoshi

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


Model checking is an automated approach to the formal verification of hardware and software. To allow model checking tools to be used by the hardware or software designers themselves, instead of by verification experts, the tools should support specification methods that correspond closely to the common usage. For hardware systems, timing diagrams form such a commonly used and visually appealing specification method. In this paper, we introduce a class of synchronous timing diagrams with a syntax and a formal semantics that is close to the informal usage. We present an efficient, decompositional algorithm for model checking such timing diagrams. This algorithm has been implemented in a user-friendly tool called RTDT (the Regular Timing Diagram Translator). We have applied this tool to verify several properties of Lucent's PCI synthesizable core.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:38
Start Conference Manager
Conference Systems