Forward Model Checking Techniques Oriented to Buggy Designs

Abstract

Forward model checking is an efficient symbolic model checking method for verifying realistic properties of sequential circuits and protocols. In this paper, 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/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.