Logical errors in sequential circuit designs and communication protocols are an important problem for system designers. They can delay getting a new product on the market or cause the failure of some critical device that is already in use. My research group has developed a verification method called temporal logic model checking for this class of systems. In this approach specifications are expressed in a propositional temporal logic, while circuits and protocols are modeled as state--transition systems. An efficient search procedure is used to determine automatically if a specification is satisfied by some transition system. The technique has been used in the past to find subtle errors in a number of non-trivial examples.

During the last few years, the size of the state-transition systems that can be verified by model checking techniques has increased dramatically. By representing transition relations implicitly using Binary Decision Diagrams (BDDs), we have been able to check some examples that would have required 10^20 states with the original algorithm. Various refinements of the BDD-based techniques have pushed the state count up to 10^100. By combining model checking with various abstraction techniques, we have been able to handle even larger systems. For example, we have used this technique to verify the cache coherence protocol in the IEEE Futurebus+ Standard. We found several errors that had been previously undetected. Apparently, this is the first time that formal methods have been used to find nontrivial errors in an IEEE standard.

Additional information can be found in the CMU Model Checking home page.