An Effective Guidance Strategy for Abstraction-Guided Simulation

Flavio M. de Paula, Alan J. Hu

ACM/IEEE Design Automation Conference, 2007.

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.