Show simple item record

dc.contributor.authorGoel, Nehaen_US
dc.date.accessioned2017-04-04T19:49:39Z
dc.date.available2017-04-04T19:49:39Z
dc.date.issued2010-07-30en_US
dc.identifier.otheretd-08102010-204533en_US
dc.identifier.urihttp://hdl.handle.net/10919/76840
dc.description.abstractIntegrated circuit design has progressed significantly over the last few decades. This increasing complexity of hardware systems poses several challenges to the digital hardware verification. Functional verification has become the most expensive and time-consuming task in the overall product development cycle. Almost 70\% of the total verification time is being consumed by design verification and it is projected to worsen further. One of the reasons for this complexity is the synthesis and optimization (automated as well as manual) techniques used to improve performance, area, delay, and other measures have made the final implementation of the design very different from the golden (reference) model. Determining the functional correctness between the reference and implementation using exhaustive simulation can almost always be infeasible. An alternative approach is to prove that the optimized design is functionally equivalent to the reference model, which is known to be functionally correct. The most widely used formal method to perform this process is equivalence checking. The success of combinational equivalence checking (CEC) has contributed to aggressive combinational logic synthesis and optimizations for circuits with millions of logic gates. However, without powerful sequential equivalence checking (SEC) techniques, the potential and extent of sequential optimization is quite limited. In other words, the success of SEC can unleash a plethora of aggressive sequential optimizations that can take circuit design to the next level. Currently, SEC remains extremely difficult compared to CEC, due to the huge search space of the problem. Sequential Equivalence Checking remains a challenging problem, in this thesis we address the problem using efficient learning techniques. The first approach is to mine missing multi-node patterns from the mining database, verify them and add those proved as true during the unbounded SEC framework. The second approach is to mine powerful and generalized Boolean relationships among flip-flops and internal signals in a sequential circuit using a data mining algorithm. In contrast to traditional learning methods, our mining algorithms can extract illegal state cubes and inductive invariants. These invariants can be arbitrary Boolean expressions and can help in pruning a large don't-care space for equivalence checking. The two approaches are complementary to each other in nature. One computes the subset of illegal states that cannot occur in the normal function mode and the other approach mines legal constraints that represent the characteristics of the miter circuit and can never be violated. These powerful relations, when added as new constraint clauses to the original formula, help to significantly increase the deductive power for the SAT engine, thereby pruning a larger portion of the search space. Likewise, the memory required and time taken to solve the SEC problem is alleviated.
dc.language.isoen_USen_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.subjectInductive invariantsen_US
dc.subjectImplicationsen_US
dc.subjectData Miningen_US
dc.subjectFormal verificationen_US
dc.subjectFinite state machinesen_US
dc.titleMining Multinode Constraints and Complex Boolean Expressions for Sequential Equivalence Checkingen_US
dc.typeThesisen_US
dc.contributor.departmentElectrical and Computer Engineeringen_US
dc.description.degreeMaster of Scienceen_US
thesis.degree.nameMaster of Scienceen_US
thesis.degree.levelmastersen_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.committeememberAbbott, A. Lynnen_US
dc.contributor.committeememberRamakrishnan, Narenen_US
dc.type.dcmitypeTexten_US
dc.identifier.sourceurlhttp://scholar.lib.vt.edu/theses/available/etd-08102010-204533/en_US
dc.date.sdate2010-08-10en_US
dc.date.rdate2016-09-30
dc.date.adate2010-08-13en_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record