Advertisement

Implicative Simultaneous Satisfiability and Applications

  • Zurab Khasidashvili
  • Alexander Nadel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7261)

Abstract

This paper proposes an efficient algorithm for the systematic learning of implications. This is done as part of a new search and restart strategy in the SAT solver. We evaluate the new algorithm within a number of applications, including BMC and induction with invariant strengthening for equivalence checking. We provide extensive experimental evidence attesting to a speedup of one and often two orders of magnitude with our algorithm, on a representative set of industrial and publicly available test suites, as compared to a basic version of invariant strengthening. Moreover, we show that the new invariant strengthening algorithm alone performs better than induction and interpolation, and that the absolutely best result is achieved when it is combined with interpolation. In addition, we experimentally demonstrate the superiority of an application of our new algorithm to BMC.

Keywords

Model Check Problem Instance Equivalence Check Satisfying Assignment Bound Model Check 
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.
    Abramovici, A., Breuer, M.A., Friedman, A.D.: Digital Systems Testing and Testable Design. Computer Science Press (1990)Google Scholar
  2. 2.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Biere, A., Heule, M., Van Maaren, H., Walsh, T.: Handbook of Satisfiability. IOS Press (2009)Google Scholar
  4. 4.
    Bjesse, P., Claessen, K.: SAT-Based Verification without State Space Traversal. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 372–389. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  5. 5.
    Bjesse, P., Boralv, A.: DAG-aware circuit compression for formal verification. In: ICCAD 2004 (2004)Google Scholar
  6. 6.
    Brand, D.: Verification of large synthesized designs. In: ICCAD 1993 (1993)Google Scholar
  7. 7.
    Case, M.L., Mishchenko, A., Brayton, R.K., Baumgartner, J., Mony, H.: Invariant-strengthened elimination of dependent state elements. In: FMCAD 2008 (2008)Google Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)Google Scholar
  9. 9.
    Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. ENTCS 89(4) (2003)Google Scholar
  10. 10.
    van Eijk, C.A.J.: Sequential equivalence checking without state space traversal. In: DATE 1998 (1998)Google Scholar
  11. 11.
    Fraer, R., Ikram, S., Kamhi, G., Leonard, T., Mokkedem, A.: Accelerated verification of RTL assertions based on satisfiability solvers. In: HLDVT 2002 (2002)Google Scholar
  12. 12.
    Huang, S.-Y., Cheng, K.-T.: Formal Equivalence Checking and Design Debugging. Kluwer (1998)Google Scholar
  13. 13.
    Khasidashvili, Z., Nadel, A., Palti, A., Hanna, Z.: Simultaneous SAT-Based Model Checking of Safety Properties. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) HVC 2005. LNCS, vol. 3875, pp. 56–75. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  14. 14.
    Kroening, D., Strichman, O.: Decision Procedures. EATCS. Springer (2008)Google Scholar
  15. 15.
    Kuehlmann, A.: Dynamic Transition Relation Simplification for Bounded Property Checking. In: ICCAD 2004 (2004)Google Scholar
  16. 16.
    Kuehlmann, A., Krohm, F.: Equivalence checking using cuts and heaps. In: DAC 1997 (1997)Google Scholar
  17. 17.
    Kunz, W., Pradhan, D.K.: Recursive learning: An attractive alternative to the decesion tree for test generation in digital circuits. In: ITC 1992 (1992)Google Scholar
  18. 18.
    McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  19. 19.
    Mishchenko, A., Chatterjee, S., Brayton, R., Een, N.: Improvements to combinational equivalence checking. In: ICCAD 2006 (2006)Google Scholar
  20. 20.
    Mony, H., Baumgartner, J., Mishchenko, A., Brayton, R.: Speculative reduction-based scalable redundancy identification. In: DTAE 2009 (2009)Google Scholar
  21. 21.
    Nadel, A.: Generating Diverse Solutions in SAT. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 287–301. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  22. 22.
    Nordström, J.: Stålmarck’s Method Versus Resolution: A Comparative Theoretical Study. Stockholm University (2001)Google Scholar
  23. 23.
    Sheeran, M., Singh, S., Stålmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  24. 24.
    Sheeran, M., Stälmarck, G.: A tutorial on Stälmarck’s method of propositional proof. Formal Methods In System Design 16(1) (2000)Google Scholar
  25. 25.
    Silva, P.M., Sakallah, K.: Robust search algorithms for test pattern generation. In: FTCS (1997)Google Scholar
  26. 26.
    Strichman, O.: Accelerating bounded model checking of safety properties. Formal Methods in System Design 24 (2004)Google Scholar
  27. 27.
    Whittemore, J., Kim, K., Sakallah, K.: SATIRE: A new incremental satisfiability engine. In: DAC (2001)Google Scholar
  28. 28.
    Wieringa, S.: On incremental satisfiability and bounded model checking. In: DIFTS (2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Zurab Khasidashvili
    • 1
  • Alexander Nadel
    • 1
  1. 1.Intel CorporationHaifaIsrael

Personalised recommendations