- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- An effective guidance strategy for abstraction-guided...
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
An effective guidance strategy for abstraction-guided simulation de Paula, Flavio M
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 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.
Item Metadata
Title |
An effective guidance strategy for abstraction-guided simulation
|
Creator | |
Publisher |
University of British Columbia
|
Date Issued |
2007
|
Description |
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.
|
Genre | |
Type | |
Language |
eng
|
Date Available |
2011-03-11
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
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.
|
DOI |
10.14288/1.0051996
|
URI | |
Degree | |
Program | |
Affiliation | |
Degree Grantor |
University of British Columbia
|
Campus | |
Scholarly Level |
Graduate
|
Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
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.