Forward image computation with backtracing ATPG and incremental state-set construction
Pages 254 - 259
Abstract
Image computation is a fundamental step in formal verification of sequential systems, including sequential equivalence checking and symbolic model checking. Since conventional Reduced Ordered Binary Decision Diagram (ROBDD) based methods can potentially suffer from memory explosion, there has been a growing interest in using Automatic Test Pattern Generation (ATPG) / Boolean Satisfiability (SAT) based techniques in recent years. While ATPG has been successful for computing pre-image, image computation presents a very different set of problems. In this paper, we present a novel backtracing-based ATPG technique for forward image computation. We carefully alter the ATPG engine to compute the image cubes and store them incrementally in a Zero-Suppressed Binary Decision Diagram (ZBDD). In order to improve the efficiency of image computation, we propose three heuristics: (i) gate-observability based decision selection heuristics to accelerate ATPG, (ii) search-state based learning techniques supported with a proof for correctness, and (iii) on-the-fly state-set minimization techniques to reduce the size of computed image set. Experimental results on ISCAS '89 and ITC '99 benchmark circuits show that we can achieve orders of magnitude improvement over OBDD-based and SAT-based techniques.
References
[1]
P. A. Abdulla, P. Bjesse, and N. Eén. Symbolic Reachability Analysis based on SAT-solvers. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems, pages 411--425, 2000.]]
[2]
Bin Li, M. S. Hsiao and S. Sheng. A Novel SAT All-solutions Solver for Efficient Preimage Computation. In Proceedings of Design, Automation and Test in Europe, pages 272--277, 2004.]]
[3]
F. Brglez. On Testability of Combinational Networks. In Proceedings of International Symposium on Circuits and Systems, pages 221--225, 1984.]]
[4]
K. Chandrasekar and M. S. Hsiao. ATPG-based Preimage Computation: Efficient search space pruning with ZBDD. In Proceedings of High-Level Design Validation and Test Workshop, pages 117--122, 2003.]]
[5]
K. Chandrasekar and M. S. Hsiao. Decision Selection and Learning for an 'all-solutions ATPG engine'. In Proceedings of International Test Conference, pages 607--616, 2004.]]
[6]
S. Chang, W. Jone, and S. Chang. TAIR: Testability Analysis by Implication Reasoning. IEEE Transactions on Computer Aided Design, 19(1):152--160, January 2000.]]
[7]
N. Eén and N. Sörensson. An Extensible SAT-solver. In Proceedings of SAT, pages 502--518, 2003.]]
[8]
J. Giraldi and M. L. Bushnell. Search state equivalence for redundancy identification and test generation. In Proceedings of International Test Conference, pages 184--193, 1991.]]
[9]
L. H. Goldstein. Controllability/Observability Analysis of Digital Circuits. IEEE Transactions on Circuits and Systems, 26:685--693, September 1979.]]
[10]
The VIS Group. VIS: A System for Verification and Synthesis. In Proceedings of Computer Aided Verification, pages 428--432, 1996.]]
[11]
A. Gupta, A. Gupta, Z. Yang, and P. Ashar. Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation. In Proceedings of Design Automation Conference, pages 536--541, 2001.]]
[12]
A. Gupta, Z. Yang, P. Ashar, and A. Gupta. SAT-based Image Computation with Application in Reachability analysis In Proceedings of Formal Methods in Computer-Aided Design, pages 354--371, 2000.]]
[13]
A. Gupta, Z. Yang, P. Ashar, L. Zhang, and S. Malik. Partition-based Decision Heuristics for Image Computation using SAT and BDDs. In Proceedings of International Conference on Computer Aided Design, pages 286--292, 2001.]]
[14]
S.-Y. Huang, K.-T. Cheng, K.-C. Chen, C.-Y. Huang, and F. Brewer. AQUILA: An Equivalence Checking System for Large Sequential Designs. IEEE Transactions on Computers, 49(5):443--464, May 2000.]]
[15]
S. Minato. Zero-suppressed BDDs for Set Manipulation in Combinatorial Problems. In Proceedings of Design Automation Conference, pages 272--277, 1993.]]
[16]
H.-J. Kang and I.-C. Park. SAT-based Unbounded Symbolic Model Checking. In Proceedings of Design Automation Conference, pages 840--843, 2003.]]
[17]
A. Gupta, M. K. Ganai and P. Ashar. Efficient SAT-based Unbounded Symbolic Model Checking using Circuit Cofactoring'. In Proceedings of International Conference on Computer Aided Design, pages 510--517, 2004.]]
[18]
K. L. McMillan. Applying SAT Methods in Unbounded Symbolic Model Checking. In Proceedings of Computer Aided Verification, pages 250--264, 2002.]]
[19]
K. L. McMillan. Interpolation and SAT-based Model Checking. In Proceedings of Computer Aided Verification, pages 1--13, 2003.]]
[20]
A. Mishchenko. Extra v 2.0: Software library extending CUDD. In http://www.ee.pdx.edu/~alanmi/research/extra.htm.]]
[21]
A. Mishchenko. An Introduction to Zero-suppressed Binary Decision Diagrams. In http://www.ee.pdx.edu/~alanmi/research.]]
[22]
I.-H. Moon, G. D. Hachtel, and F. Somenzi. Border block Triangular Form and Conjunction Schedule in Image Computation. In Proceedings of Formal Methods in Computer-Aided Design, pages 73--90, 2000.]]
[23]
I.-H. Moon, J. H. Kukula, K. Ravi, and F. Somenzi. To Split or to Conjoin: The Question in Image Computation. In Proceedings of Design Automation Conference, pages 23--28, 2000.]]
[24]
S. Seth, L. Pan, and V. D. Agrawal. PREDICT: Probabilistic Estimation of Digital Circuit Testability. In Proceedings of Fault Tolerant Computing Symposium, pages 220--225, 1985.]]
[25]
S. Sheng and M. Hsiao. Efficient Preimage Computation using a Novel Success-driven ATPG. In Proceedings of Design, Automation and Test in Europe, pages 822--827, 2003.]]
[26]
F. Somenzi. CUDD: CU Decision Diagram Package 2.4.0. In http://vlsi.colorado.edu/~fabio/CUDD/, 2004.]]
[27]
P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining Decision Diagrams and SAT Procedures for Efficient symbolic model checking. In Proceedings of International Conference on Computer Aided Verification, pages 124--138, 2000.]]
Index Terms
- Forward image computation with backtracing ATPG and incremental state-set construction
Recommendations
Disjunctive image computation for software verification
Existing BDD-based symbolic algorithms designed for hardware designs do not perform well on software programs. We propose novel techniques based on unique characteristics of software programs. Our algorithm divides an image computation step into a ...
The image computation problem in hybrid systems model checking
HSCC'07: Proceedings of the 10th international conference on Hybrid systems: computation and controlIn this paper, we analyze limits of approximation techniques for (non-linear) continuous image computation in model checking hybrid systems. In particular, we show that even a single step of continuous image computation is not semidecidable numerically ...
The Compositional Far Side of Image Computation
ICCAD '03: Proceedings of the 2003 IEEE/ACM international conference on Computer-aided designSymbolic image computation is the most fundamental computationin BDD-based sequential system optimization and formal verification.In this paper, we explore the use of over-approximationand BDD minimization with donýt cares during image computation.Our ...
Comments
Information & Contributors
Information
Published In
April 2005
518 pages
Copyright © 2005 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 17 April 2005
Check for updates
Author Tags
Qualifiers
- Article
Conference
Acceptance Rates
Overall Acceptance Rate 312 of 1,156 submissions, 27%
Upcoming Conference
GLSVLSI '25
- Sponsor:
- sigda
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 233Total Downloads
- Downloads (Last 12 months)3
- Downloads (Last 6 weeks)1
Reflects downloads up to 07 Mar 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in