Type of Document Master's Thesis Author Chandrasekar, Kameshwar Author's Email Address email@example.com 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
- Model Checking
- Equivalence Checking
Date of Defense 2003-07-28 Availability unrestricted 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.
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
If you have questions or technical problems, please Contact DLA.