ATPG based Preimage Computation: Efficient Search Space Pruning using ZBDD

Simple item page
dc.contributor.authorChandrasekar, Kameshwaren
dc.contributor.committeechairHsiao, Michael S.en
dc.contributor.committeememberArmstrong, James R.en
dc.contributor.committeememberHa, Dong Samen
dc.contributor.departmentElectrical and Computer Engineeringen
dc.date.accessioned2014-03-14T20:42:07Zen
dc.date.adate2003-08-06en
dc.date.available2014-03-14T20:42:07Zen
dc.date.issued2003-07-28en
dc.date.rdate2012-06-22en
dc.date.sdate2003-07-28en
dc.description.abstractPreimage Computation is a fundamental step in Formal Verification of VLSI designs. Conventional OBDD-based methods for Formal Verification suffer from spatial explosion, since large designs can blow up in terms of memory. On the other hand, SAT/ATPG based methods are less demanding on memory. But the run-time can be huge for these methods, since they must explore an exponential search space. In order to reduce this temporal explosion of SAT/ATPG based methods, efficient learning techniques are needed. Conventional ATPG aims at computing a single solution for its objective. In preimage computation, we must enumerate all solutions for the target state during the search. Similar sub-problems often occur during preimage computation that can be identified by the internal state of the circuit. Therefore, it is highly desirable to learn from these search-states and avoid repeated search of identical solution/conflict subspaces, for better performance. In this thesis, we present a new ZBDD based method to compactly store and efficiently search previously explored search-states. We learn from these search-states and avoid repeating subsets and supersets of previously encountered search spaces. Both solution and conflict subspaces are pruned based on simple set operations using ZBDDs. We integrate our techniques into a PODEM based ATPG engine and demonstrate their efficiency on ISCAS '89 benchmark circuits. Experimental results show that upto 90% of the search-space is pruned due to the proposed techniques and we are able to compute preimages for target states where a state-of-the-art technique fails.en
dc.description.degreeMaster of Scienceen
dc.identifier.otheretd-07282003-144744en
dc.identifier.sourceurlhttp://scholar.lib.vt.edu/theses/available/etd-07282003-144744/en
dc.identifier.urihttp://hdl.handle.net/10919/34218en
dc.publisherVirginia Techen
dc.relation.haspartthesis_kamesh.pdfen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectATPGen
dc.subjectPreimageen
dc.subjectModel Checkingen
dc.subjectEquivalence Checkingen
dc.subjectZBDDen
dc.titleATPG based Preimage Computation: Efficient Search Space Pruning using ZBDDen
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_kamesh.pdf
Size:
248.31 KB
Format:
Adobe Portable Document Format
Download

Collections

Masters Theses