Efficient generation of counterexamples and witnesses in symbolic model checking

Model checking is an automatic technique for verifying sequential circuit designs and protocols. An ecient search procedure is used to determine whether or not the specication is satised. If it is not satised, our technique will produce a counterexample execution trace that shows the cause of the problem. We describe an ecient algorithm to produce counterexamples and witnesses for symbolic model checking algorithms. This algorithm is used in the SMV model checker and works quite well in practice. We also discuss how to extend our technique to more complicated specications.