Strategies for SAT-Based Formal Verification

Simple item page
dc.contributor.authorVimjam, Vishnu Chaithanyaen
dc.contributor.committeechairHsiao, Michael S.en
dc.contributor.committeememberHa, Dong Samen
dc.contributor.committeememberShukla, Sandeep K.en
dc.contributor.committeememberBrown, Ezra A.en
dc.contributor.committeememberBuehrer, R. Michaelen
dc.contributor.departmentElectrical and Computer Engineeringen
dc.date.accessioned2014-03-14T20:07:02Zen
dc.date.adate2007-02-13en
dc.date.available2014-03-14T20:07:02Zen
dc.date.issued2007-01-29en
dc.date.rdate2007-02-13en
dc.date.sdate2007-01-31en
dc.description.abstractVerification of digital hardware designs is becoming an increasingly complex task as the designs are incorporating more functionality, becoming complex and growing larger in size. Today, verification remains a bottleneck in meeting time-to-market requirements and consumes more than 70% of the overall design-costs. Traditionally, verification has been done using simulation-based approaches, where a set of appropriate test-stimuli is used by the designer. As the designs become more complex, however, simulation-based techniques often fail to capture corner-case errors. Furthermore, unless exhaustively tested, these approaches do not guarantee the correctness of a system with respect to its specifications. As a consequence, formal methods for design verification have been sought after. In formal verification, the conformance of a design to a given set of specifications is proven mathematically, thereby leaving no room for unexplored search spaces. Despite the exponential time/memory complexities often involved within the formal approaches, they have shown promise in capturing subtle bugs, which were missed otherwise. In this dissertation, we focus on Boolean Satisfiability (SAT) based formal verification, which has gained tremendous importance in the recent past. Importantly, SAT-based approaches often alleviate the memory explosion problem, which had been a bottleneck of the traditional symbolic (Binary Decision Diagram based) approaches. In SAT-based techniques, the set of verification tasks are converted into a set of Boolean formulae, which are checked for satisfiability using a SAT solver. These problems are often NP-complete and are prone to an explosion in the required run-time. To overcome this, we propose novel strategies which utilize both structural and logical information of a sequential circuit. In particular, we devise techniques to extract non-trivial invariants of a design, strengthen properties such that they can be proven faster and interleave bounded reachability analysis with bounded model checking. We provide the necessary algorithms and implementation details in order to automate the proposed techniques. Experiments conducted on a variety of benchmark circuits show that orders of magnitude improvement in overall run-times can be achieved via our techniques compared to the existing state-of-the-art SAT-based approaches.en
dc.description.degreePh. D.en
dc.identifier.otheretd-01312007-121134en
dc.identifier.sourceurlhttp://scholar.lib.vt.edu/theses/available/etd-01312007-121134/en
dc.identifier.urihttp://hdl.handle.net/10919/26078en
dc.publisherVirginia Techen
dc.relation.haspartvimjam_phd_dissertation.pdfen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectATPGen
dc.subjectEquivalence Checkingen
dc.subjectSATen
dc.subjectModel Checkingen
dc.subjectBDDen
dc.subjectLearningen
dc.titleStrategies for SAT-Based Formal Verificationen
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:
vimjam_phd_dissertation.pdf
Size:
1003.04 KB
Format:
Adobe Portable Document Format
Download

Collections

Doctoral Dissertations