Open Collections

An effective guidance strategy for abstraction-guided simulation

University of British Columbia

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 blowup, 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 promise has yet to be realized, as the performance of previous work has been unreliable — sometimes great, sometimes poor. The problem is the guidance strategy. In this thesis, we first develop a platform to enable flexible exploration of abstraction-guided simulation — different guidance heuristics and formal tools are easily inserted — while providing the capacity, speed, and Verilog compatibility of a leading industry-standard (logic-simulation) tool, Synopsys VCS. Then, we start by exploring some greedy heuristics and find that they tend to perform poorly, adding too much search overhead for limited ability to escape dead ends (local optima). Based on these experiments, we propose a new guidance strategy, which pursues a more global search and is better able to avoid getting stuck. Experimental results 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.

Text

2011-03-11

For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.

http://hdl.handle.net/2429/32341

Computer Science

University of British Columbia

Graduate