Mining constraints for Testing and Verification

Simple item page
dc.contributor.authorWu, Weixinen
dc.contributor.committeechairHsiao, Michael S.en
dc.contributor.committeememberLiu, Yiluen
dc.contributor.committeememberHuang, Chaoen
dc.contributor.departmentElectrical and Computer Engineeringen
dc.date.accessioned2014-03-14T20:31:09Zen
dc.date.adate2009-02-06en
dc.date.available2014-03-14T20:31:09Zen
dc.date.issued2009-01-20en
dc.date.rdate2009-02-06en
dc.date.sdate2009-01-28en
dc.description.abstractWith the advances in VLSI and System-On-Chip (SOC) technologies, the complexity of hardware systems has increased manifold. The increasing complexity poses serious challenges to the digital hardware design. Functional verification has become one of the most expensive and time-consuming components of the current product development cycle. Today, design verification alone often surpasses 70% of the total development cost and the situation has been projected to continue to worsen. The two most widely used formal methods for design verification are Equivalence Checking and Model Checking. During the design phase, hardware goes through several stages of optimizations for area, speed, power, etc. Determining the functional correctness of the design after each optimization step by means of exhaustive simulation can be prohibitively expensive. An alternative to prove functional correctness of the optimized design is to determine the design's functional equivalence with respect to some golden model which is known to be functionally correct. Efficient techniques to perform this process is known as Equivalence Checking. Equivalence Checking requires that the implementation circuit should be functionally equivalent to the specification circuit. Complexities in Equivalence Checking can be exponential to the circuit size in the worst case. Since Equivalence Checking of sequential circuits still remains a challenging problem, in this thesis, we first address this problem using efficient learning techniques. In contrast to the traditional learning methods, our method employs a mining algorithm to discover global constraints among several nodes efficiently in a sequential circuit. In a Boolean satisfiability (SAT) based framework for the bounded sequential equivalence checking, by taking advantage of the repeated search space, our mining algorithm is only performed on a small window size of unrolled circuit, and the mined relations could be reused subsequently. 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 these problems are alleviated. We also propose a pseudo-functional test generation method based on effective functional constraints extraction. We use mining techniques to extract a set of multi-node functional constraints which consists of illegal states and internal signal correlation. Then the functional constraints are imposed to a ATPG tool to generate pseudo functional delay tests.en
dc.description.degreeMaster of Scienceen
dc.identifier.otheretd-01282009-222714en
dc.identifier.sourceurlhttp://scholar.lib.vt.edu/theses/available/etd-01282009-222714/en
dc.identifier.urihttp://hdl.handle.net/10919/31056en
dc.publisherVirginia Techen
dc.relation.haspartThesis.pdfen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectLearningen
dc.subjectSimulationen
dc.subjectSATen
dc.subjectMulti-node Constrainten
dc.subjectMiningen
dc.titleMining constraints for Testing and Verificationen
dc.typeThesisen
thesis.degree.disciplineElectrical and Computer Engineeringen
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen
thesis.degree.levelmastersen
thesis.degree.nameMaster of Scienceen

Files

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

Collections

Masters Theses