On dynamic switching of navigation for semi-formal design validation

Abstraction-guided simulation is a promising semi-formal framework for design validation. Unlike previously proposed approaches that utilized potentially costly abstraction-refinement for altering the abstraction when encountering hard corner cases, in this paper, a novel and low-cost method is proposed. The search begins with an initial abstraction and dynamically switches guidance to a new, different abstract model when it becomes apparent that the current model does not provide a sufficiently detailed map of the state space to advance the search towards the target. We automatically and efficiently identify those state variables that influence the circuitpsilas transition towards the target state using binary resolution, and these variables are used to create new abstractions on-the-fly during the search. The new abstractions provide a fine-grained abstract view of local segments of the concrete state space, which the stimuli generator uses to navigate towards the hard-to-reach target state. Experimental results show that our method is scalable and highly effective in reaching hard-to-reach states.