Advertisement

DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems

  • Malay K Ganai
  • Aarti Gupta
  • Pranav Ashar
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)

Abstract

We present a SAT-based model checking platform (DiVer) based on robust and scalable algorithms that are tightly integrated for verifying large scale industry designs. DiVer houses various SAT-based engines each targeting capacity and performance issues inherent in verifying large designs. The engines with their respective roles are as follows: Bounded Model Checking (BMC) and Distributed BMC over a network of workstations for falsification, Proof-based Iterative Abstraction (PBIA) for model reduction, SAT-based Unbounded Model Checking and Induction for proofs, Efficient Memory Modeling (EMM) and its combination with PBIA in BMC for verifying embedded memory systems with multiple memories (with multiple ports and arbitrary initial state). Using several industrial case studies, we describe the interplay of these engines highlighting their contribution at each step of verification. DiVer has matured over 3 years and is being used extensively in several industry settings. Due to an efficient and flexible infrastructure, it provides a very productive verification environment for research and development.

References

  1. 1.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  2. 2.
    McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)Google Scholar
  3. 3.
    Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)CrossRefGoogle Scholar
  4. 4.
    Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of DAC (1999)Google Scholar
  5. 5.
    Sheeran, M., Singh, S., Stalmarck, G.: Checking Safety Properties using Induction and a SAT Solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  6. 6.
    Ganai, M., Aziz, A.: Improved SAT-based Bounded Reachability Analysis. In: Proceedings of VLSI Design Conference (2002)Google Scholar
  7. 7.
    Ganai, M., Zhang, L., Gupta, A., Ashar, P., Yang, Z.: Efficient Approaches for Bounded Model Checking. US Patent Application 2003-0225552, Filed on May 30 (2002)Google Scholar
  8. 8.
    McMillan, K.: Applying SAT methods in Unbounded Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 250. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  9. 9.
    McMillan, K., Amla, N.: Automatic Abstraction without Counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    McMillan, K.: 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
  11. 11.
    Gupta, A., Ganai, M., Wang, C., Yang, Z., Ashar, P.: Abstraction and Bdds Complement SAT-Based BMC in DiVer. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 206–209. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    Ganai, M., Gupta, A., Ashar, P.: Distributed SAT and Distributed Bounded Model Checking. In: Proceedings of CHARME (2003)Google Scholar
  13. 13.
    Gupta, A., Ganai, M., Ashar, P., Yang, Z.: Iterative Abstraction using SAT-based BMC with Proof Analysis. In: Proceedings of ICCAD (2003)Google Scholar
  14. 14.
    Ganai, M., Gupta, A., Ashar, P.: Efficient Modeling of Embedded Memories in Bounded Model Checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 440–452. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  15. 15.
    Ganai, M., Gupta, A., Ashar, P.: Efficient SAT-based Unbounded Model Checking Using Circuit Cofactoring. In: Proceedings of ICCAD (2004)Google Scholar
  16. 16.
    Gupta, A., Ganai, M., Ashar, P.: Lazy Constraints and SAT Heuristics for Proof-based Abstraction. In: Proceedings of VLSI Design (2005)Google Scholar
  17. 17.
    Ganai, M., Gupta, A., Ashar, P.: Verification of Embedded Memory Systems using Efficient Memory Modeling. In: Proceedings of DATE (2005)Google Scholar
  18. 18.
    Kuehlmann, A., Ganai, M., Paruthi, V.: Circuit-based Boolean Reasoning. In: Proceedings of DAC (2001)Google Scholar
  19. 19.
    Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of DAC (2001)Google Scholar
  20. 20.
    Ganai, M., Zhang, L., Ashar, P., Gupta, A.: Combining Strengths of Circuit-based and CNF-based Algorithms for a High Performance SAT Solver. In: Proceedings of DAC (2002)Google Scholar
  21. 21.
    Ganai, M., Kuehlmann, A.: On-the-fly Compression of Logical Circuits. In: Proceedings of IWLS (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Malay K Ganai
    • 1
  • Aarti Gupta
    • 1
  • Pranav Ashar
    • 1
  1. 1.NEC Laboratories AmericaPrincetonUSA

Personalised recommendations