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.
