RTDT: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams

Model Checking is an automated approach to formal verification of hardware and software. It is desirable for model checkers to allow common, visually appealing specifications. To this end, we introduce a class of synchronous timing diagrams with a semantics that corresponds to common usage. We present an efficient, decompositional algorithm for model checking, implemented in a user-friendly tool, RTDT, which we have applied to the verification of Lucent's F-Bus interface.