Applications of Hierarchical Verification in Model Checking

Robert Beers, Rajnish Ghughal, and Mark Aagaard

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


The linear temporal model checker that we use provides sound decomposition mechanisms within a purely model checking environment. We have exploited these mechanisms to successfully verify a wide spectrum of circuits. This paper describes a variety of the decomposition strategies that we have used as part of a multi-year industrial formal verification effort. The strategies generally use structural decomposition and cone-of-influence reductions to transform the verification of a single, large property into the verification of a number of smaller properties. We have also exploited symmetry to write parameterized properties that we verify over regular structures such as arrays.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:39
Start Conference Manager
Conference Systems