I will first introduce Synchronous Regular Timing Diagrams (SRTDs), which is a graphical way of specifying synchronous properties. I will present the efficient linear-time model checking algorithms for SRTDs. These algorithms have been implemented in a tool called RTDT. I will describe how we used RTDT and the model checker COSPAN to verify that Lucent's PCI Interface Core satisfied timing diagrams found in the PCI Local Bus specification. I will present verification results that demonstrate that our model checking approach is more efficient than previous approaches.

Next, I will outline a well studied approach to ameliorating the state explosion problem, called assume-guarantee reasoning. In the assume-guarantee paradigm: each component guarantees certain sub-properties based on assumptions about the other components. I will discuss the difficulties in applying this method, foremost among them is that a non-trivial amount of manual effort is required to derive the assumptions and decompose the property. I will then present a new proof rule for assume-guarantee reasoning, which generalizes several earlier rules. I will show how to apply it, in a fully automated manner, to properties specified as synchronous timing diagrams. Our experiments with applying this method have yielded promising results, showing substantial reductions in the space requirements for model checking.