Model checking synchronous timing diagrams

Abstract

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.