Advertisement

Abstract BDDs: A Technique for Using Abstraction in Model Checking

  • Edmund Clarke
  • Somesh Jha
  • Yuan Lu
  • Dong Wang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)

Abstract

We propose a new methodology for exploiting abstraction in the context of model-checking. Our new technique uses abstract BDDs as its underlying data structure. We show that this technique builds a more refined model than traditional compiler-based methods proposed by Clarke, Grumberg and Long. We also provide experimental results to demonstrate the usefulness of our method. We have verified a pipelined carry-save multiplier and a simple version of the PCI local bus protocol. Our verification of the PCI bus revealed a subtle inconsistency in the PCI standard. We believe this is an interesting result by itself.

Keywords

Abstract BDDs Model checking abstraction 

References

  1. 1.
    R. E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation”, IEEE Trans. on Comput., Vol. C-35, No. 8, pp. 677–691, Aug. 1986.zbMATHCrossRefGoogle Scholar
  2. 2.
    J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill, “Symbolic Model Checking for Sequential Circuit Verification”, IEEE Trans. on CAD of Integrated Circuits and System, Vol.13, No.4, pp.401-424, 1994.Google Scholar
  3. 3.
    E. M. Clarke, E. A. Emerson, and A. P. Sistla, “Automatic verification of finitestate concurrent system using temporal logic”, Proceedings of the Tenth Annual ACM Symposium on Principles of Programming Languages (POPL), January, 1983.Google Scholar
  4. 4.
    E. M. Clarke, R. Enders, T. Filkorn and S. Jha, “Exploiting Symmetry in Temporal Logic Model Checking”, Formal Methods in System Design 9(1/2):77–104, 1996.CrossRefGoogle Scholar
  5. 5.
    E. M. Clarke and O. Grumberg and H. Hiraishi and S. Jha and D. E. Long and K. L. McMillan and L. A. Ness, “Verification of the Futurebus+ Cache Coherence Protocol”, Formal Methods in System Design 6(2):217–232, 1995.CrossRefGoogle Scholar
  6. 6.
    E. M. Clarke, O. Grumberg, D. E. Long, “Model Checking and Abstraction”, ACM Transactions on Programming Languages and System (TOPLAS), Vol. 16, No. 5, pp. 1512–1542, Sept. 1994.Google Scholar
  7. 7.
    E. A. Emerson and A. P. Sistla, “Symmetry and Model Checking”, Formal Methods in System Design 9(1/2):105–130, 1996.CrossRefGoogle Scholar
  8. 8.
    P. Godefroid, D. Peled, and M. Staskauskas, “Using Partial Order Methods in the Formal Verification of Industrial Concurrent Programs”, ISSTA'96 International Symposium on Software Testing and Analysis, pp. 261–269, San Diego, California, USA, 1996. ACM Press.Google Scholar
  9. 9.
    J. L. Hennessy, D. A. Patterson, Computer Architecture: A Quantitative Approach, second edition, 1996. Morgan Kaufman Press.Google Scholar
  10. 10.
    C. N. Ip and D. L. Dill, “Better Verification Through Symmetry”, Formal Methods in System Design 9(1/2):41–76, 1996.Google Scholar
  11. 11.
    S. Jha, Y. Lu, M. Minea, E. M. Clarke, “Equivalence Checking using Abstract BDDs”, Intl. Conf. on Computer Design (ICCD), 1997.Google Scholar
  12. 12.
    Shinji Kimura, “Residue BDD and Its Application to the Verification of Arithmetic Circuits”, 32nd Design Automation Conference (DAC), 1995.Google Scholar
  13. 13.
    D. E. Long, “Model Checking, Abstraction and Compositional Verification”, School of Computer Science, Carnegie Mellon University publication CMU-CS-93-178, July 1993.Google Scholar
  14. 14.
    K. L. McMillan, “Symbolic Model Checking: An Approach to the State Explosion Problem”. Kluwer Academic Publishers, 1993.Google Scholar
  15. 15.
    D. Peled, “Combining Partial Order Reduction with on-the-fly model-checking”, Journal of Formal Methods in System Design, 8(1):39–64.Google Scholar
  16. 16.
    PCI SGI, “PCI Local Bus Specification”, Production Version Revision 2.1, June 1, 1995.Google Scholar
  17. 17.
    Kavita Ravi, Abelardo Pardo, Gary D. Hachtel, Fabio Somenzi, “Modular Verification of Multipliers”, Formal Methods in Computer-Aided Design, pp. 49–63, Nov. 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Edmund Clarke
    • 1
  • Somesh Jha
    • 1
  • Yuan Lu
    • 1
  • Dong Wang
    • 1
  1. 1.Carnegie Mellon UniversityPittsburghUSA

Personalised recommendations