More Web Proxy on the site http://driver.im/

Article

SAT-Based Image Computation with Application in Reachability Analysis

Authors:

Anubhav GuptaAuthors Info & Claims

FMCAD '00: Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design

Pages 354 - 371

Published: 01 November 2000 Publication History

Abstract

Image computation finds wide application in VLSI CAD, such as state reachability analysis in formal verification and synthesis, combinational verification, combinational and sequential test. Existing BDD-based symbolic algorithms for image computation are limited by memory resources in practice, while SAT-based algorithms that can obtain the image by enumerating satisfying assignments to a CNF representation of the Boolean relation are potentially limited by time resources. We propose new algorithms that combine BDDs and SAT in order to exploit their complementary benefits, and to offer a mechanism for trading off space vs. time. In particular, (1) our integrated algorithm uses BDDs to represent the input and image sets, and a CNF formula to represent the Boolean relation, (2) a fundamental enhancement called BDD Bounding is used whereby the SAT solver uses the BDDs for the input set and the dynamically changing image set to prune the search space of all solutions, (3) BDDs are used to compute all solutions below intermediate points in the SAT decision tree, (4) a fine-grained variable quantification schedule is used for each BDD subproblem, based on the CNF representation of the Boolean relation. These enhancements coupled with more engineering heuristics lead to an overall algorithm that can potentially handle larger problems. This is supported by our preliminary results on exact reachability analysis of ISCAS benchmark circuits.

References

[1]

P. A. Abdulla, P. Bjesse, and N. Een. Symbolic reachability analysis based on SAT-solvers. In Tools and Algorithms for the Analysis and Construction of Systems (TACAS) , 2000.

Digital Library

[2]

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Analysis and Construction of Systems (TACAS) , volume 1579 of Lecture Notes in Computer Science , 1999.

Digital Library

[3]

R. K. Brayton et al. VIS: A system for verification and synthesis. In R. Alur and T. Henzinger, editors, Proceedings of the Internation Conference on Computer-Aided Verification , volume 1102 of Lecture Notes in Computer Science , pages 428- 432, June 1996.

Digital Library

[4]

R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers , C-35(8):677-691, Aug. 1986.

Digital Library

[5]

J. Burch and V. Singhal. Tight integration of combinational verification methods. In Proceedings of the International Conference on Computer-Aided Design , pages 570-576, 1998.

Digital Library

[6]

J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more eficiently in symbolic model checking. In Proceedings of the 28th Design Automation Conference , pages 403-407, June 1991.

Digital Library

[7]

J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design , 13(4):401-424, Apr. 1994.

Digital Library

[8]

G. Cabodi, P. Camurati, and S. Quer. Improving the eficiency of BDD-based operators by means of partitioning. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems , 18(5):545-556, May 1999.

Digital Library

[9]

O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines using symbolic execution. In Proceedings of the Internatiocal Workshop on Automatic Verification Methods for Finite State Systems , volume 407 of Lecture Notes in Computer Science , pages 365-373, June 1989.

Digital Library

[10]

M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM , 7:201-205, 1960.

Digital Library

[11]

D. Geist and I. Beer. Eficient model checking by automatic ordering of transition relation partitions. In Proceedings of the Internation Conference on Computer-Aided Verification , volume 818 of Lecture Notes in Computer Science , pages 299- 310, 1994.

[12]

A. Gupta and P. Ashar. Integrating a Boolean satisfiability checker and BDDs for combinational verification. In Proceedings of the VLSI Design Conference , Jan. 1998.

Digital Library

[13]

T. Larrabee. Test pattern generation using Boolean satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems , 11(1):4-15, Jan. 1992.

Digital Library

[14]

J. P. Marques-Silva. Search Algorithms for Satisfiability Problems in Combinational Switching Circuits . PhD thesis, EECS Department, University of Michigan, May 1995.

[15]

J. P. Marques-Silva and K. A. Sakallah. Grasp: A new search algorithm for satisfiability. In Proceedings of the International Conference on Computer-Aided Design , pages 220-227, Nov. 1996.

Digital Library

[16]

J. P. Marquez-Silva. Grasp package. http://algos.inesc.pt/~jpms/software.html.

[17]

I.-H. Moon, J. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the Design Automation Conference , pages 23-28, June 2000.

Digital Library

[18]

A. Narayan, A. J. Isles, J. Jain, R. K. Brayton, and A. Sangiovanni-Vincentelli. Reachability analysis using partitioned ROBDDs. In Proceedings of the International Conference on Computer-Aided Design , pages 388-393, 1997.

Digital Library

[19]

R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Eficient BDD algorithms for FSM synthesis and verification. In International Workshop for Logic Synthesis , May 1995. Lake Tahoe, CA.

[20]

F. Somenzi et al. CUDD: University of Colorado Decision Diagram Package. http://vlsi.colorado.edu/~fabio/CUDD/.

[21]

H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit state enumeration of finite state machines using BDDs. In Proceedings of the International Conference on Computer-Aided Design , pages 130-133, 1990.

[22]

P. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining decision diagrams and SAT procedures for eficient symbolic model checking. In Proceedings of the Internation Conference on Computer-Aided Verification , volume 1855 of Lecture Notes in Computer Science , pages 124-138, 2000.

Digital Library

Cited By

He FGao YYin L(2018)Efficient software product-line model checking using induction and a SAT solverFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6048-712:2(264-279)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s11704-016-6048-7
Toda TSoh T(2016)Implementing Efficient All Solutions SAT SolversACM Journal of Experimental Algorithmics10.1145/297558521(1-44)Online publication date: 4-Nov-2016
https://dl.acm.org/doi/10.1145/2975585
(2015)Logic analysis and optimization with quick identification of invariants through one time frame analysisProceedings of the 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2015.7340476(102-107)Online publication date: 1-Sep-2015
https://dl.acm.org/doi/10.1109/MEMCOD.2015.7340476
Show More Cited By

Recommendations

Improvements in SAT-based Reachability Analysis for Timed Automata
Concurrency Specification and Programming (CS&P 2003)

The paper deals with the problem of checking reachability for timed automata. In order to check reachability of a~state satisfying some property, first the transition relation of a timed automaton is unfolded iteratively to some depth and encoded as a ...
Improvements in SAT-based Reachability Analysis for Timed Automata
Concurrency Specification and Programming (CS&P 2003)

The paper deals with the problem of checking reachability for timed automata. In order to check reachability of a~state satisfying some property, first the transition relation of a timed automaton is unfolded iteratively to some depth and encoded as a ...
A modular CNF-based SAT solver
SBCCI '10: Proceedings of the 23rd symposium on Integrated circuits and system design

The state-of-the-art SAT solvers, such as Chaff [11], zChaff [18], BerkMin [5], and Minisat [2] usually share the same core techniques, for instance: the watched literals structures conflict clause recording and non-chronological backtracking. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FMCAD '00: Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design

November 2000

537 pages

ISBN:3540412190

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 November 2000

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

28
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

He FGao YYin L(2018)Efficient software product-line model checking using induction and a SAT solverFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6048-712:2(264-279)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s11704-016-6048-7
Toda TSoh T(2016)Implementing Efficient All Solutions SAT SolversACM Journal of Experimental Algorithmics10.1145/297558521(1-44)Online publication date: 4-Nov-2016
https://dl.acm.org/doi/10.1145/2975585
(2015)Logic analysis and optimization with quick identification of invariants through one time frame analysisProceedings of the 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2015.7340476(102-107)Online publication date: 1-Sep-2015
https://dl.acm.org/doi/10.1109/MEMCOD.2015.7340476
Lin CWan LChen D(2014)C-MineProceedings of the 51st Annual Design Automation Conference10.1145/2593069.2593107(1-6)Online publication date: 1-Jun-2014
https://dl.acm.org/doi/10.1145/2593069.2593107
Lin CLiu LVasudevan SAyala JJones AMadden PCoskun A(2013)Generating concise assertions with complete coverageProceedings of the 23rd ACM international conference on Great lakes symposium on VLSI10.1145/2483028.2483088(185-190)Online publication date: 2-May-2013
https://dl.acm.org/doi/10.1145/2483028.2483088
Brauer JKing AKriener J(2011)Existential quantification as incremental SATProceedings of the 23rd international conference on Computer aided verification10.5555/2032305.2032322(191-207)Online publication date: 14-Jul-2011
https://dl.acm.org/doi/10.5555/2032305.2032322
Ward DSomenzi FHassoun S(2006)Decomposing image computation for symbolic reachability analysis using control flow informationProceedings of the 2006 IEEE/ACM international conference on Computer-aided design10.1145/1233501.1233662(779-785)Online publication date: 5-Nov-2006
https://dl.acm.org/doi/10.1145/1233501.1233662
Gupta AGanai MWang C(2006)SAT-Based verification methods and applications in hardware verificationProceedings of the 6th international conference on Formal Methods for the Design of Computer, Communication, and Software Systems10.1007/11757283_5(108-143)Online publication date: 22-May-2006
https://dl.acm.org/doi/10.1007/11757283_5
Ganai MGupta AAshar PJoyner WMartin GKahng A(2005)Beyond safetyProceedings of the 42nd annual Design Automation Conference10.1145/1065579.1065773(738-743)Online publication date: 13-Jun-2005
https://dl.acm.org/doi/10.1145/1065579.1065773
Chandrasekar KHsiao MLach JQu GIsmail Y(2005)Forward image computation with backtracing ATPG and incremental state-set constructionProceedings of the 15th ACM Great Lakes symposium on VLSI10.1145/1057661.1057723(254-259)Online publication date: 17-Apr-2005
https://dl.acm.org/doi/10.1145/1057661.1057723
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents