Show simple item record

dc.contributor.authorHu, Weien_US
dc.date.accessioned2011-02-14en_US
dc.date.accessioned2014-03-14T20:31:21Z
dc.date.available2011-02-14en_US
dc.date.available2014-03-14T20:31:21Z
dc.date.issued2011-02-01en_US
dc.date.submitted2011-02-03en_US
dc.identifier.otheretd-02032011-141047en_US
dc.identifier.urihttp://hdl.handle.net/10919/31121
dc.description.abstractVerification, as opposed to Testing and Post-Silicon Validation, is a critical step for Integrated Circuits (IC) Design, answering the question â Are we designing the right function?â before the chips are manufactured. One of the core areas of Verification is Equivalence Checking (EC), which is a special yet independent case of Model Checking (MC). Equivalence Checking aims to prove that two circuits, when fed with the same inputs, produce the exact same outputs. There are broadly two ways to conduct Equivalence Checking, simulation and Formal Equivalence Checking. Simulation requires one to try out different input combinations and observe if the two circuits produce the same output. Obviously, since it is not possible to enumerate all combinations of different inputs, completeness cannot be guaranteed. On the other hand, Formal Equivalence Checking can achieve 100% confidence. As the number of gates and in particular, the number of flip-flops, in circuits has grown tremendously during the recent years, the problem of Formal Equivalence Checking has become much harder â A recent evaluation of a general-case Formal Equivalence Checking engine [1] shows that about 15% of industrial designs cannot be verified after a typical sequential synthesis flow. As a result, a lot of attention on Formal Equivalence Checking has been drawn both academically and industrially. For years Combinational Equivalence Checking(CEC) has been the pervasive framework for Formal Equivalence Checking(FEC) in the industry. However, due to the limitation of being able to verify circuits only with 1:1 flip-flop pairing, a pure CEC-based methodology requires a full regression of the verification process, meaning that performing sequential optimizations like retiming or FSM re-encoding becomes somewhat of a bottleneck in the design cycle [2]. Therefore, a more powerful framework â Sequential Equivalence Checking (SEC)â has been gradually adopted in industry. In this thesis, we target on Sequential Equivalence Checking by finding efficient yet powerful group of relationships (invariants) among the signals of the two circuits being compared. In order to achieve a high success rate on some of the extremely hard-to-verify circuits, we are interested in both two-node and multi-node (up to 4 nodes) invariants. Also we are interested in invariants among both flip-flops and internal signals. For large circuits, there can be too many potential invariants requiring much time to prove. However, we observed that a large portion of them may not even contribute to equivalence checking. Moreover, equivalence checking can be significantly helped if there exists a method to check if a subset of potential invariants would be sufficient (e.g., whether two-nodes are enough or multi-nodes are also needed) prior to the verification step. Therefore, we propose two sufficiency-based approaches to identify useful invariants out of the initial potential invariants for SEC. Experimental results show that our approach can either demonstrate insufficiency of the invariants or select a small portion of them to successfully prove the equivalence property. Our approaches are quite case-independent and flexible. They can be applied on circuits with different synthesis techniques and combined with other techniques.en_US
dc.publisherVirginia Techen_US
dc.relation.haspartHu_W_T_2011.pdfen_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.subjectInvariant filteringen_US
dc.subjectAssume and Verifyen_US
dc.subjectBoolean Satisfiability(SAT)en_US
dc.subjectSequential Equivalence Checking(SEC)en_US
dc.titleSufficiency-based Filtering of Invariants for Sequential Equivalence Checkingen_US
dc.typethesisen_US
dc.contributor.departmentElectrical and Computer Engineeringen_US
thesis.degree.nameMaster of Scienceen_US
thesis.degree.levelmastersen_US
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen_US
dc.contributor.committeechairHsiao, Michael S.en_US
dc.contributor.committeememberShukla, Sandeep K.en_US
dc.contributor.committeememberSchaumont, Patrick Roberten_US
dc.identifier.sourceurlhttp://scholar.lib.vt.edu/theses/available/etd-02032011-141047/en_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record