Title page for ETD etd-07282003-144744


Type of Document Master's Thesis
Author Chandrasekar, Kameshwar
Author's Email Address kachandr@vt.edu
URN etd-07282003-144744
Title ATPG based Preimage Computation: Efficient Search Space Pruning using ZBDD
Degree Master of Science
Department Electrical and Computer Engineering
Advisory Committee
Advisor Name Title
Hsiao, Michael S. Committee Chair
Armstrong, James R. Committee Member
Ha, Dong Sam Committee Member
Keywords
  • ATPG
  • Preimage
  • Model Checking
  • Equivalence Checking
  • ZBDD
Date of Defense 2003-07-28
Availability unrestricted
Abstract
Preimage 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.

Files
  Filename       Size       Approximate Download Time (Hours:Minutes:Seconds) 
 
 28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access 
  thesis_kamesh.pdf 254.27 Kb 00:01:10 00:00:36 00:00:31 00:00:15 00:00:01

Browse All Available ETDs by ( Author | Department )

dla home
etds imagebase journals news ereserve special collections
virgnia tech home contact dla university libraries

If you have questions or technical problems, please Contact DLA.