Skip to main content
SpringerLink
Log in

*BMDs can delay the use of theorem proving for verifying arithmetic assembly instructions

  • Conference paper
  • First Online:
Formal Methods in Computer-Aided Design (FMCAD 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1166))

Included in the following conference series:

Abstract

We address the problem of formally verifying arithmetic instructions of microprocessors implemented by microprograms that contain loops. We try to avoid theorem proving techniques using a new symbolic representation: Binary Moment Diagrams (*BMDs).

In order to use *BMDs for verifying sequential circuits as well as microprograms, we extend this representation and define several bit-vector level operators. This extension is then integrated into an automatic verification system. We illustrate the paper with examples and we discuss power and weakness of *BMDs.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Arditi. Formal verification of microprocessors: a first experiment with the Coq proof assistant. Technical Report RR-96-31, Université de Nice-Sophia Antipolis. Laboratoire I3S, May 1996.

    Google Scholar 

  2. L. Arditi and H. Collavizza. An object-oriented framework for the formal verification of processors. In European Conference on Object-Oriented Programming, volume 952 of LNCS, 1995.

    Google Scholar 

  3. L. Arditi and H. Collavizza. Towards verifying VHDL descriptions of processors. In European Design Automation Conference with EURO-VHDL, 1995.

    Google Scholar 

  4. P. J. Ashenden. The VHDL Cookbook. Public Domain, Dept. Computer Science, University of Adelaide, South Australia, first edition, July 1990.

    Google Scholar 

  5. D. L. Beatty and R. E. Bryant. Formally verifying a microprocessor using a simulation methodology. In31st ACM/IEEE Design Automation Conference, 1994.

    Google Scholar 

  6. J. Bern, C. Meinel, and A. Slobodová. Efficient OBDD-based boolean, manipulation in CAD beyond current limits. In 32nd ACM/IEEE Design Automation Conference, 1995.

    Google Scholar 

  7. R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug. 1986.

    Google Scholar 

  8. R. E. Bryant. Binary decision diagrams and beyond: Enabling technologies for formal verification. In IEEE Internationl Conference on Computer-Aided Design, 1995.

    Google Scholar 

  9. R. E. Bryant and Y.-A. Chen. Verification of arithmetic functions with binary moment diagrams. Technical Report CMU-CS-94-160, School of Computer Science, Carnegie Mellon University, June 1994.

    Google Scholar 

  10. R. E. Bryant and Y.-A. Chen. Verification of arithmetic circuits with binary moment diagrams. In 32nd ACM/IEEE Design Automation Conference, 1995.

    Google Scholar 

  11. J. Burch. Using BDDs to verify multipliers. In 28th ACM/IEEE Design Automation Conference, 1991.

    Google Scholar 

  12. J. Burch, E. Clarke, K. McMillan, and D. Dill. Sequential circuit verification using symbolic model checking. In 27th ACM/IEEE Design Automation Conference, 1990.

    Google Scholar 

  13. J. Burch and D. Dill. Automatic verification of pipelined microprocessor control. In Computer-Aided Verification, volume 818 of LNCS, 1994.

    Google Scholar 

  14. E. Clarke, M. Fujita, and X. Zhao. Hybrid decision diagrams, overcoming the limitations of MTBDDs and BMDs. In IEEE Internationl Conference on Computer-Aided Design, 1995.

    Google Scholar 

  15. E. Clarke, K. McMillan, X. Zhao, M. Fujita, and H.-Y. Yang. Spectral transforms for large Boolean functions with application to technology mapping.In 30th ACM/IEEE Design Automation Conference, 1993.

    Google Scholar 

  16. E. C. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. In ACM Symposium on Principles of Programming Languages, 1992.

    Google Scholar 

  17. A. Cohn. A proof of correctness of the Viper microprocessor: the first level. In VLSI Specification, Verification and Synthesis. Kluwer Acad. Publ., Jan. 1987.

    Google Scholar 

  18. F. Corella. Automatic high-level verification against clocked algorithmic specifications. In 11th International Conference on Computer Hardware Description Languages and their Applications. Elsevier Science Publishers B.V., 1993.

    Google Scholar 

  19. Cornes, Courant, Filliâtre, Huet, Manoury, MŨnoz, Murthy, Parent, Paulin-Mohring, SaÏbi, and Werner. The Coq Proof Assistant. Reference Manual. Version 5.10. Technical report, INRIA Rocquencourt-CNRS-ENS Lyon, 1996.

    Google Scholar 

  20. O. Coudert, C. Berthet, and J.-C. Madre. Verification of synchronous sequential machines based on symbolic execution. In Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, 1989.

    Google Scholar 

  21. R. Drechsler, B. Becker, and S. Ruppertz.K*BMDs: a new data structure for verification. In European Design and Test Conference, 1996.

    Google Scholar 

  22. M. Gordon. Proving a computer correct using LCF-LSM hardware verification system. Technical Report 42, Computer Laboratory, The University of Cambridge, Sept. 1983.

    Google Scholar 

  23. A. Gupta. Formal hardware verification methods: a survey. Formal Methods in System Design, 1(2/3):151–238, Oct. 1992.

    Google Scholar 

  24. K. Hamaguchi, A. Morita, and S. Yajima. Efficient construction of binary moment diagrams for verifying arithmetic circuits. In IEEE Internationl Conference on Computer-Aided Design, 1995.

    Google Scholar 

  25. R. Hojati and R. K. Brayton. Automatic datapath abstraction in hardware systems. In Computer-Aided Verification, volume 939 of LNCS, 1995.

    Google Scholar 

  26. A. D. Hu, D. L. Dill, A. J. Drexler, and H. C. Yang. Higher-level specification and verification with BDDs. In Computer-Aided Verification: Fourth International Workshop, volume 663 of LNCS, 1992.

    Google Scholar 

  27. W. Hunt Jr. FM8501: a Verified Microprocessor. PhD thesis, Institute for Computing Science, University of Texas at Austin, 1986.

    Google Scholar 

  28. J. Joyce. Multi Level Verification of Microprocessor-Based Systems. PhD thesis, University of Cambridge, Computer Laboratory, 1989.

    Google Scholar 

  29. Y.-T. Lai and S. Sastry. Edge-valued binary decision diagrams for multi-level hierarchical verification. In 29th ACM/IEEE Design Automation Conference, 1992.

    Google Scholar 

  30. S. Rajan, N. Shankar, and M. Srivas. An integration of model checking with automated proof checking. In Computer-Aided Verification, volume 939 of LNCS, 1995.

    Google Scholar 

  31. M. K. Srivas and S. P. Miller. Applying formal verification to a commercial microprocessor. In International Conference on Computer Hardware Description Languages, 1995.

    Google Scholar 

  32. P. J. Windley. Formal modeling and verification of microprocessors. IEEE Transactions on Computers, 44(1), Jan. 1995.

    Google Scholar 

  33. Z. Zhu, J. Joyce, and C. Seger. Verification of the Tamarack-3 microprocessor in a hybrid verification environment. In Higher Order Logic Theorem Proving and Its Applications. 6th International Workshop, volume 780 of LNCS, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université de Nice, Sophia Antipolis, France

    Laurent Arditi

  2. Laboratoire I3S, CNRS, ura 1376

    Laurent Arditi

Authors
  1. Laurent Arditi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mandayam Srivas Albert Camilleri

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Arditi, L. (1996). *BMDs can delay the use of theorem proving for verifying arithmetic assembly instructions. In: Srivas, M., Camilleri, A. (eds) Formal Methods in Computer-Aided Design. FMCAD 1996. Lecture Notes in Computer Science, vol 1166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0031798

Download citation

  • DOI: https://doi.org/10.1007/BFb0031798

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61937-6

  • Online ISBN: 978-3-540-49567-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation