Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking

Model checking is an automatic technique for verifying sequential circuit designs and protocols. An efficient search procedure is used to determine whethe or not the specification is satisfied. If it is not satisfied, our technique will produce a counter-example execution trace that shows the cause of the problem. We describe an efficient algorithm to produce counter-examples 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 specifications.