Computer Science Department
School of Computer Science, Carnegie Mellon University
Automatic Verification of Sequential Circuits Using Temporal Logic
Michael Browne, Edmund Clarke, David Dill, Bhubaneswar Mishra
The verification system uses a simple and efficient algorithm, called a Model Checker . The algorithm works in two steps: in the first step, it builds a labeled state-transition graph; and in the second step, it determines the truth of a temporal formula with respect to the state-transition graph. We discuss two different techniques that we have implemented for automatically generating the state-transition graphs: The first involves extracting the state graph directly from the circuit by simulation. The second obtains the state graph by compilation from an HDL specification of the original circuit. Although these approaches are quite different, we believe that there are situations in which each is useful.