CMU-CS-85-100Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-85-100
Michael Browne, Edmund Clarke, David Dill, Bhubaneswar Mishra December 1984 Unavailable Electronically
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. 18 pages
| |

Return to:
SCS
Technical Report Collection This page maintained by reports@cs.cmu.edu |