| Type of Document |
Dissertation |
| Author |
Zhang, Liang
|
| Author's Email Address |
liang@vt.edu |
| URN |
etd-01282005-102938 |
| Title |
Design Verification for Sequential Systems at Various Abstraction Levels |
| Degree |
PhD |
| Department |
Electrical and Computer Engineering |
| Advisory Committee |
| Advisor Name |
Title |
| Michael S. Hsiao |
Committee Chair |
| G. Q. Lu |
Committee Member |
| Joseph G. Tront |
Committee Member |
| Mark Shimozono |
Committee Member |
| Thomas L. Martin |
Committee Member |
|
| Keywords |
- Bounded Model Checking
- Formal Verification
- SAT
- Simulation
- ATPG
|
| Date of Defense |
2005-01-27 |
| Availability |
unrestricted |
Abstract
With the ever increasing complexity of digital systems, functional verification has become a daunting task to circuit designers. Functional verification alone often surpasses 70% of the total development cost and the situation has been projected to continue to worsen. The most critical limitations of existing techniques are the capacity issue and the run-time issue. This dissertation addresses the functional verification problem using a unified approach, which utilizes different core algorithms at various abstraction levels. At the logic level, we focus on incorporating a set of novel ideas to existing formal verification approaches. First, we present a number of powerful optimizations to improve the performance and capacity of a typical SAT-based bounded model checking framework. Secondly, we present a novel method for performing dynamic abstraction within a framework for abstraction-refinement based model checking. Experiments on a wide range of industrial designs have shown that the proposed optimizations consistently provide between 1-2 orders of magnitude speedup and can be extremely useful in enhancing the efficacy of existing formal verification algorithms. At the register transfer level, where the formal verification is less likely to succeed, we developed an efficient ATPG-based validation framework, which leverages the high-level circuit information and an improved observability-enhanced coverage to generate high quality validation sequences. Experiments show that our approach is able to generate high quality validation vectors, which achieve both high tag coverage and high bug coverage with extremely low computational cost.
|
| Files |
| Filename |
Size |
Approximate Download Time
(Hours:Minutes:Seconds)
|
| 28.8 Modem |
56K Modem |
ISDN (64 Kb) |
ISDN (128 Kb) |
Higher-speed Access |
| |
dissertation_v3.pdf |
834.71 Kb |
00:03:51 |
00:01:59 |
00:01:44 |
00:00:52 |
00:00:04 |
|
