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

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.