Advertisement

SWORD: A SAT like Prover Using Word Level Information

  • Robert Wille
  • Görschwin Fey
  • Daniel Große
  • Daniel Große
  • Stephan Eggersglüß
  • Rolf Drechsler
Chapter
Part of the IFIP International Federation for Information Processing book series (IFIPAICT, volume 291)

Solvers for Boolean Satisfiability (SAT) are state-of-the-art to solve verification problems. But when arithmetic operations are considered, the verification performance degrades with increasing data-path width. Therefore, several approaches that handle a higher level of abstraction have been studied in the past. But the resulting solvers are still not robust enough to handle problems that mix word level structures with bit level descriptions. In this paper, we present the satisfiability solver SWORD – a SAT like solver that facilitates word level information. SWORD represents the problem in terms of modules that define operations over bit vectors. Thus, word level information and structural knowledge become available in the search process. The experimental results show that on our benchmarks SWORD is more robust than Boolean SAT, K*BMDs or SMT.

Keywords

Module Variable Auxiliary Variable Finite State Machine Conjunctive Normal Form Word Level 
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.

References

  1. 1.
    Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Comp. 35 (1986) 677–691MATHCrossRefGoogle Scholar
  2. 2.
    Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans. on CAD 21 (2002) 1377–1394Google Scholar
  3. 3.
    Davis, M., Logeman, G., Loveland, D.: A machine program for theorem proving. Comm. of the ACM 5 (1962) 394–397MATHCrossRefGoogle Scholar
  4. 4.
    Eén, N., Sörensson, N.: An extensible SAT solver. In: SAT 2003. Volume 2919 of LNCS. (2004) 502–518Google Scholar
  5. 5.
    Bryant, R., Chen, Y.A.: Verification of arithmetic functions with binary moment diagrams. In: Design Automation Conf. (1995) 535–541Google Scholar
  6. 6.
    Drechsler, R., Becker, B., Ruppertz, S.: K*BMDs: A new data structure for verification. In: European Design & Test Conf. (1996) 2–8Google Scholar
  7. 7.
    Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: ASP Design Automation Conf. (2002) 741–746Google Scholar
  8. 8.
    Thathachar, J.: On the limitations of ordered representations of functions. In: Computer Aided Verification. Volume 1427 of LNCS., Springer Verlag (1998) 232–243Google Scholar
  9. 9.
    Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Design Automation Conf. (2003) 425–430Google Scholar
  10. 10.
    Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Computer Aided Verification. Volume 3114 of LNCS. (2004) 175–188Google Scholar
  11. 11.
    Dutertre, B., Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Computer Aided Verification. Volume 4114 of LNCS. (2006) 81–94Google Scholar
  12. 12.
    Dutertre, B., L.Moura: The YICES SMT Solver. (2006) Available at http://yices.csl.sri.com/.
  13. 13.
    Huang, C.Y., Cheng, K.T.: Using word-level ATPG and modular arithmetic constraint-solving techniques for assertion property checking. IEEE Trans. on CAD 20 (2001) 381–391Google Scholar
  14. 14.
    Marques-Silva, J., Sakallah, K.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. on Comp. 48 (1999) 506–521CrossRefMathSciNetGoogle Scholar
  15. 15.
    Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conf. (2001) 530–535Google Scholar
  16. 16.
    Goldberg, E., Novikov, Y.: BerkMin: a fast and robust SAT-solver. In: Design, Automation and Test in Europe. (2002) 142–149Google Scholar
  17. 17.
    Parthasarathy, G., Iyer, M., Cheng, K.T., Wang, L.C.: An efficient finit-domain constraints solver for circuits. In: Design Automation Conf. (2004) 212–217Google Scholar
  18. 18.
    Novikov, Y., Brinkmann, R.: Foundations of hierarchical SAT-solving. In: Int’l Workshop on Boolean Problems. (2004) 103–141Google Scholar
  19. 19.
    Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7 (1960) 506–521CrossRefGoogle Scholar
  20. 20.
    Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, Part 2. (1968) 115–125 (Reprinted in: J. Siekmann, G. Wrightson (Ed.), Automation of Reasoning, Vol. 2, Springer, Berlin, 1983, pp. 466–483.).Google Scholar
  21. 21.
    Mano, M.M., Kime, C.R.: Logic and Computer Design Fundamentals. 3rd edn. Pearson Education (2004)Google Scholar
  22. 22.
    Höreth, S.: Compilation of optimized OBDD-algorithms. In: European Design Automation Conf. (1996) 152–157Google Scholar
  23. 23.
    Herbstritt, M.: wld: A C++ library for decision diagrams, Institute of Computer Science, Albert-Ludwigs-University, Freiburg im Breisgau. (2000) http://ira.informatik.uni-freiburg.de/software/wld.
  24. 24.
    Wille, R., Groβe, D.: Fast exact Toffoli network synthesis of reversible logic. In: Int’l Conf. on CAD. (2007) 60–64Google Scholar

Copyright information

© Springer-Verlag US 2009

Authors and Affiliations

  1. 1.Institute of Computer ScienceUniversity of BremenBremenGermany

Personalised recommendations