Advertisement

SAT-Based Image Computation with Application in Reachability Analysis

  • Aarti Gupta
  • Zijiang Yang
  • Pranav Ashar
  • Anubhav Gupta
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)

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.

Keywords

Conjunctive Normal Form Reachability Analysis Partial Assignment Symbolic Model Check Conjunctive Normal Form Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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.Google Scholar
  2. 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.Google Scholar
  3. 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.Google Scholar
  4. 4.
    R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug. 1986.CrossRefGoogle Scholar
  5. 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.Google Scholar
  6. 6.
    J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking. In Proceedings of the 28th Design Automation Conference, pages 403–407, June 1991.Google Scholar
  7. 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.CrossRefGoogle Scholar
  8. 8.
    G. Cabodi, P. Camurati, and S. Quer. Improving the efficiency 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.CrossRefGoogle Scholar
  9. 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 VerificationMethods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 365–373, June 1989.Google Scholar
  10. 10.
    M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:201–205, 1960.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    D. Geist and I. Beer. Efficient 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.Google Scholar
  12. 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.Google Scholar
  13. 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.CrossRefGoogle Scholar
  14. 14.
    J. P. Marques-Silva. Search Algorithms for Satisfiability Problems in Combinational Switching Circuits. PhD thesis, EECS Department, University of Michigan, May 1995.Google Scholar
  15. 15.
    J. P. Marques-Silva and. A. Sakallah. Grasp: A new search algorithm for satisfiability. In Proceedings of the International Conference on Computer-Aided Design, pages 220–227, Nov. 1996.Google Scholar
  16. 16.
    J. P. Marquez-Silva. Grasp package. http://algos.inesc.pt/~jpms/software.html
  17. 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.Google Scholar
  18. 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.Google Scholar
  19. 19.
    R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. In International Workshop for Logic Synthesis, May 1995. Lake Tahoe, CA.Google Scholar
  20. 20.
    F. Somenzi et al. CUDD: University of Colorado Decision Diagram Package. http://vlsi.colorado.edu/~fabio/CUDD/
  21. 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.Google Scholar
  22. 22.
    P. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining decision diagrams and SAT procedures for efficient 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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Aarti Gupta
    • 1
  • Zijiang Yang
    • 1
  • Pranav Ashar
    • 1
  • Anubhav Gupta
    • 1
  1. 1.NEC USA CCRLPrinceton

Personalised recommendations