Skip to main content
SpringerLink
Log in

An Object-Oriented Framework for the Formal Verification of Processors

  • Conference paper
  • First Online:
ECOOP’95 — Object-Oriented Programming, 9th European Conference, Åarhus, Denmark, August 7–11, 1995 (ECOOP 1995)

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

Included in the following conference series:

Abstract

We propose an object-oriented approach for the formal verification of processors. This approach has been validated on significant applications. It is based on a class hierarchy that provides the basic components to describe processors at any abstraction level, and to specify verifications to execute.

The originality of our method is to combine an object-oriented model (to ensure genericity) and a computer algebra verification system (to ensure efficiency). Computer experiments with our framework clearly shown three main advantages: processor descriptions are very easy to write down, the core of the verification system is generic so it may be applied without any modification to different processors, and last, the proof times are very short compared with previous approaches.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 74.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. F. Anceau. The Architecture of Microprocessors. Addison-Wesley Publishing Company, 1986.

    Google Scholar 

  2. L. Arditi and H. Collavizza. Binary moment diagrams for verifying loops in microprocessor instructions. Technical report, Laboratoire I3S, Université de Nice-Sophia Antipolis, Nov. 1994.

    Google Scholar 

  3. L. Arditi and H. Collavizza. Towards verifying VHDL descriptions of processors. Technical report, Laboratoire I3S, Université de Nice — Sophia Antipolis, Jan. 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. G. Bracha and W. Cook. Mixin-based inheritance. In European Conference on Object Oriented Programming / Object-Oriented Programming Systems, Languages and Applications, October 1990.

    Google Scholar 

  6. M. L. Coe and P. J. Windley. Microprocessor verification: A tutorial. Technical Report LAL-92-10, Laboratory for Applied Logic, Brigham Young University, Provo, Utah, 1992.

    Google Scholar 

  7. A. Colin. A proof of correctness of the Viper microprocessor: the first level. In G. Birtwhistle and P. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 27–71, Calgary, Canada, Jan. 1987. Kluwer Acad. Publishers.

    Google Scholar 

  8. E. Gallesio. STklos: a Scheme object oriented system dealing with the TK toolkit. In Xhibition 94, San Jose, Jul. 1994. ICS.

    Google Scholar 

  9. M. Gordon. HOL, a machine oriented formulation of higher order logic. Technical Report 68, University of Cambridge, Computer Laboratory, 1985.

    Google Scholar 

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

    Article  Google Scholar 

  11. W. A. Hunt Jr. Microprocessor design verification. Journal of Automated Reasoning, 5(4):429–460, Dec. 1989.

    Article  Google Scholar 

  12. J. J. Joyce. Formal verification and implementation of a microprocessor. In G. Birtwhistle and P. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 129–157, Calgary, Canada, Jan. 1987. Kluwer Acad. Publishers.

    Google Scholar 

  13. B. Meyer. Object-Oriented Software Construction. Prentice Hall International, 1988.

    Google Scholar 

  14. A. Paepcke. Object-oriented programming: the CLOS perspective. MIT press, 1993.

    Google Scholar 

  15. J. Pulou, J. Rainard, and P. Thorel. Microprocesseur à test intégré MTI — description fonctionnelle et architecture. Technical Report NT/CNS/CC/59, CNET, Grenoble, Jan. 1987.

    Google Scholar 

  16. J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, and W. Lorensen. Object-oriented Modeling and Design. Prentice Hall, 1991.

    Google Scholar 

  17. R. Sekar and M. Srivas. Equational techniques. In G. Birtwistle and P. Subrahmanyam, editors, Current Trends in Hardware Verification and Automatic Theorem Proving, pages 173–217, New-York, 1989. Springer-Verlag.

    Google Scholar 

  18. M. Srivas and M. Bickford. Formal verification of a pipelined microprocessor. IEEE Software, 7(5):52–64, Sept. 1990.

    Article  Google Scholar 

  19. V. Stavridou. Formal Methods in Circuit Design. Number 37 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1993.

    Google Scholar 

  20. G. L. Steele Jr. Common Lisp the Language. Digital Press, second edition, 1990.

    Google Scholar 

  21. P. J. Windley. The Formal Verification of Generic Interpreters. PhD thesis, University of California, Division of Computer Science, 1990.

    Google Scholar 

  22. Z. Zhu, J. Joyce, and C. Seger. Verification of the Tamarack-3 microprocessor in a hybrid verification environment. In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic Theorem Proving and Its Applications. 6 th Int. Work. HUG’93, volume 780 of LNCS, pages 253–266, Vancouver, Canada, Aug. 1993. Springer-Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire I3S, CNRS-URA 1376, Université de Nice — Sophia Antipolis, 650, Route des Colles, B.P. 145, 06903, Sophia Antipolis Cédex, France

    Laurent Arditi & Hélère Collavizza

Authors
  1. Laurent Arditi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hélère Collavizza
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Keio University, 3-14-1 Hiyoshi, Kohoku-ku, Yokohama, 223, Japan

    Mario Tokoro

  2. Rank Xerox Research Centre, 6 Chemin de Maupertuis, F-38240, Meylan, France

    Remo Pareschi

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Arditi, L., Collavizza, H. (1995). An Object-Oriented Framework for the Formal Verification of Processors. In: Tokoro, M., Pareschi, R. (eds) ECOOP’95 — Object-Oriented Programming, 9th European Conference, Åarhus, Denmark, August 7–11, 1995. ECOOP 1995. Lecture Notes in Computer Science, vol 952. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49538-X_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-49538-X_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60160-9

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation