Symbolic model checking for sequential circuit verification
- 1 April 1994
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
- Vol. 13 (4) , 401-424
- https://doi.org/10.1109/43.275352
Abstract
The temporal logic model checking algorithm of Clarke, Emerson, and Sistla (1986) is modified to represent state graphs using binary decision diagrams (BDD's) and partitioned transition relations. Because this representation captures some of the regularity in the state space of circuits with data path logic, we are able to verify circuits with an extremely large number of states. We demonstrate this new technique on a synchronous pipelined design with approximately 5/spl times/10/sup 120/ states. Our model checking algorithm handles full CTL with fairness constraints. Consequently, we are able to express a number of important liveness and fairness properties, which would otherwise not be expressible in CTL. We give empirical results on the performance of the algorithm applied to both synchronous and asynchronous circuits with data path logic.<>Keywords
This publication has 17 references indexed in Scilit:
- Symbolic model checking: 1020 States and beyondPublished by Elsevier ,2004
- Verifying pipelined hardware using symbolic logic simulationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Implicit state enumeration of finite state machines using BDD'sPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Don't care minimization of multi-level sequential logic networksPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A unified framework for the formal verification of sequential circuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Sequential circuit verification using symbolic model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Representing circuits more efficiently in symbolic model checkingPublished by Association for Computing Machinery (ACM) ,1991
- Formal hardware verification by symbolic ternary trajectory evaluationPublished by Association for Computing Machinery (ACM) ,1991
- A Method for Symbolic Verification of Synchronous CircuitsPublished by Elsevier ,1991
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986