Title :
Forward model checking techniques oriented to buggy designs
Author :
Iwashita, H. ; Nakata, T.
Author_Institution :
Fujitsu Labs. Ltd., Kawasaki, Japan
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 :
finite state machines; formal verification; logic CAD; logic testing; sequential circuits; symbol manipulation; tree searching; CPU time; FSM; buggy designs; depth-first traversal; design errors; finite state machine; forward model checking techniques; illegal state transition sequences; protocols; sequential circuit verification; state traversal; symbolic model checking method; Sequential logic circuit testing;
Conference_Titel :
Computer-Aided Design, 1997. Digest of Technical Papers., 1997 IEEE/ACM International Conference on
Conference_Location :
San Jose, CA, USA
Print_ISBN :
0-8186-8200-0
DOI :
10.1109/ICCAD.1997.643567