VTechWorks staff will be away for the Memorial Day holiday on Monday, May 27, and will not be replying to requests at that time. Thank you for your patience.

Show simple item record

dc.contributor.authorZhang, Liangen_US
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_US
dc.publisherVirginia Techen_US
dc.rightsI hereby certify that, if appropriate, I have obtained and attached hereto a written permission statement from the owner(s) of each third party copyrighted matter to be included in my thesis, dissertation, or project report, allowing distribution as specified below. I certify that the version I submitted is the same as that approved by my advisory committee. I hereby grant to Virginia Tech or its agents the non-exclusive license to archive and make accessible, under the conditions specified below, my thesis, dissertation, or project report in whole or in part in all forms of media, now or hereafter known. I retain all other ownership rights to the copyright of the thesis, dissertation or project report. I also retain the right to use in future works (such as articles or books) all or part of this thesis, dissertation, or project report.en_US
dc.subjectBounded Model Checkingen_US
dc.subjectFormal Verificationen_US
dc.titleDesign Verification for Sequential Systems at Various Abstraction Levelsen_US
dc.contributor.departmentElectrical and Computer Engineeringen_US
dc.description.degreePh. D.en_US
thesis.degree.namePh. D.en_US
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen_US
thesis.degree.disciplineElectrical and Computer Engineeringen_US
dc.contributor.committeechairHsiao, Michael S.en_US
dc.contributor.committeememberLu, Guo-Quanen_US
dc.contributor.committeememberShimozono, Mark M.en_US
dc.contributor.committeememberMartin, Thomas L.en_US
dc.contributor.committeememberTront, Joseph G.en_US

Files in this item


This item appears in the following Collection(s)

Show simple item record