Design Verification for Sequential Systems at Various Abstraction Levels

Simple item page
dc.contributor.authorZhang, Liangen
dc.contributor.committeechairHsiao, Michael S.en
dc.contributor.committeememberLu, Guo-Quanen
dc.contributor.committeememberShimozono, Mark M.en
dc.contributor.committeememberMartin, Thomas L.en
dc.contributor.committeememberTront, Joseph G.en
dc.contributor.departmentElectrical and Computer Engineeringen
dc.date.accessioned2014-03-14T20:06:57Zen
dc.date.adate2005-01-31en
dc.date.available2014-03-14T20:06:57Zen
dc.date.issued2005-01-27en
dc.date.rdate2005-01-31en
dc.date.sdate2005-01-28en
dc.description.abstractWith 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.en
dc.description.degreePh. D.en
dc.identifier.otheretd-01282005-102938en
dc.identifier.sourceurlhttp://scholar.lib.vt.edu/theses/available/etd-01282005-102938/en
dc.identifier.urihttp://hdl.handle.net/10919/26053en
dc.publisherVirginia Techen
dc.relation.haspartdissertation_v3.pdfen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectBounded Model Checkingen
dc.subjectFormal Verificationen
dc.subjectSATen
dc.subjectSimulationen
dc.subjectATPGen
dc.titleDesign Verification for Sequential Systems at Various Abstraction Levelsen
dc.typeDissertationen
thesis.degree.disciplineElectrical and Computer Engineeringen
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen
thesis.degree.leveldoctoralen
thesis.degree.namePh. D.en

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
dissertation_v3.pdf
Size:
815.15 KB
Format:
Adobe Portable Document Format
Download

Collections

Doctoral Dissertations