Sciweavers

Share
ICCAD
2005
IEEE

Transition-by-transition FSM traversal for reachability analysis in bounded model checking

9 years 7 months ago
Transition-by-transition FSM traversal for reachability analysis in bounded model checking
Abstract— In bounded model checking (BMC)-based verification flows lack of reachability constraints often leads to false negatives. At present, it is daily practice of a verification engineer to identify the missing reachability constraints by manually inspecting the design code and by analyzing counterexamples. This, unfortunately, requires a lot of effort and is prone to errors. We propose an algorithm to determine reachability constraints automatically. The proposed approach applies to a design style where the operation of the design is controlled by a main FSM which can easily be extracted from the RTL description of the circuit. The algorithm decomposes and analyzes the state space of the circuit by considering transitions of the main FSM. Experimental results show that the proposed method can considerably reduce the manual work of verification engineers.
Minh D. Nguyen, Dominik Stoffel, Markus Wedler, Wo
Added 16 Mar 2010
Updated 16 Mar 2010
Type Conference
Year 2005
Where ICCAD
Authors Minh D. Nguyen, Dominik Stoffel, Markus Wedler, Wolfgang Kunz
Comments (0)
books