Please watch out for the latex superscripts!!  --Ed


Symbolic Model Checking "With" and "Without" BDDs

Edmund M. Clarke, Jr.
School of Computer Science
Carnegie Mellon University


Logical errors in finite-state concurrent systems such as sequential
circuit designs and communication protocols are an important problem
for computer scientists. They can delay getting a new product on the
market or cause the failure of some critical device that is already in
use.  {\em Temporal logic model checking} is an automatic verification
technique 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 past decade, 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), it is possible 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, even larger systems can be handled. For
example, this technique has been used to verify the cache coherence
protocol in the IEEE Futurebus+ Standard.  Several errors were found
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.

Although model checking is already useful for verifying many circuit
and protocol designs that arise in industry, additional research is
needed to exploit the full power of this method.  For example, a new
technique called {\em bounded model checking} has been developed that
uses fast propositional decision procedures like GRASP and
Stahlmarck's algorithm instead of BDDs to handle even larger examples.
The new technique has been used to verify twenty one complex circuits
from the Power PC Microprocessor.  Traditional model checking
techniques based on BDDs were only able to handle one of the circuits
we tried.