An Effective Guidance Strategy for Abstraction-Guided Simulation ∗ ABSTRACT

Despite major advances in formal verification, simulation continues to be the dominant workhorse for functional verification. Abstraction-guided simulation has long been a promising framework for leveraging the power of formal techniques to help simulation reach difficult target states (assertion violations or coverage targets): model checking a smaller, abstracted version of the design avoids complexity blow-up, yet computes approximate distances from any state of the actual design to the target; these approximate distances are used during random simulation to guide the simulator. Unfortunately, the performance of previous work has been unreliable — sometimes great, sometimes poor. The problem is the guidance strategy. Because the abstract distances are approximate, a greedy strategy will get stuck in local optima. Previous works expanded the search horizon to try to avoid dead-ends. We explore such heuristics and find that they tend to perform poorly, adding too much search overhead for limited ability to escape dead-ends. Based on these experiments, we propose a new guidance strategy, which pursues a more global search and is better able to avoid getting stuck. Experiments show that our new guidance strategy is highly effective in most cases that are hard for random simulation and beyond the capacity of formal verification