Activity-based refinement for abstraction-guided simulation

Semi-formal verification tools are gaining popularity because of their ability to balance the performance of logic simulators with the goal-focused capabilities of formal verification. Within this domain, abstraction-based simulation is a technique that has been proposed in several research works and has also emerged in a few commercial solutions. Abstraction-based simulation performs reachability analysis on a design abstraction to gather approximate information on the distance of each design state from a goal state, and then uses this information in a guided search by the logic simulator. Unfortunately, so far, the quality of the abstraction has been the weakest link in this semi-formal solution, because of its impact in enabling a simulator to reach a verification goal. This paper presents a novel solution for abstraction refinement that operates in an abstraction-based simulation framework. Our solution collects switching activity information during simulation and determines how to modify and improve an abstraction based on analysis of this information. By using refinement, the original abstraction crafted by the tool is no longer a critical aspect of the semi-formal search. Instead, initially the abstraction may be weak, improving over time to enable the simulator to reach the goal state.