Forward model checking techniques oriented to buggy designs
- 1 January 1997
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10923152,p. 400-404
- https://doi.org/10.1109/iccad.1997.643567
Abstract
Forward model checking is an efficient symbolic model checking method for verifying realistic properties of sequential circuits and protocols. We present the techniques that modify the order of state traversal on forward model checking, and that dramatically improve average CPU time for finding design errors. A failing property has to be checked again and again to analyze the bug until it is corrected. The techniques, therefore, can have significant impacts on actual verification tasks. We use a modified regular//spl omega/-regular expression to represent a set of illegal state transition sequences of an FSM. It makes the problem clear and gives us a sense of depth-first traversal, not on the state space, but on the property.Keywords
This publication has 9 references indexed in Scilit:
- Symbolic model checking: 1020 States and beyondPublished by Elsevier ,2004
- CTL model checking based on forward state traversalPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Bug identification of a real chip design by symbolic model checkingPublished 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
- Efficient generation of counterexamples and witnesses in symbolic model checkingPublished by Association for Computing Machinery (ACM) ,1995
- Symbolic Model CheckingPublished by Springer Nature ,1993
- Software for Analytical Development of Communications ProtocolsAT&T Technical Journal, 1990
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986