Skip to main content
SpringerLink
Log in

ΜSPEED: a system for the specification and verification of microprocessors

  • Conference paper
  • First Online:
STACS 92 (STACS 1992)

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

Included in the following conference series:

  • 127 Accesses

Abstract

ΜSPPED is a system for the specification of micro-processor behaviour at the assembly language level and micro-sequence level. Starting from a user-friendly interface, the description is built according to a functional model inspired from the denotational semantics of programming languages. The verification consists in the correspodence between the functions obtained at the two levels.

work partly supported by CNET #883 B09 10 790 9245 CNS, and “CHARME” BRA #3216

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

References

  1. Borrione, Camurati, Paillet, Prinetto: “A functional approach to formal hardware verification: The MTI experience”, Proc. IEEE ICCD'88, Port Chester, New York. October 1988.

    Google Scholar 

  2. Borrione, Pierre, Salem: “Formal verification of VHDL descriptions in Boyer-Moore: first results”, 1st European Conference on VHDL Methods, Marseille, France, 4–7 Sept. 1990.

    Google Scholar 

  3. Bickford, Srivas: “Verification of a Pipelined Microprocessor Using Clio”, Proc. Work. on “Hardware Specification, Verification and Synthesis: Mathematical Aspects”, Cornell University, Ithaca, USA, July 1989

    Google Scholar 

  4. Cohn: “A Proof of Correctness of the Viper Microprocessor: The First Level”, in Proc. “VLSI Specification, Verification and Synthesis”, Calgary, Canada, Jan. 1987.

    Google Scholar 

  5. Collavizza: “Functional Semantics of Microprocessors at the Micro-program level and Correspondence with the Machine Instruction level”, Proc IEEE EDAC Glasgow, Scotland, 12–15 March, 1990.

    Google Scholar 

  6. Camurati, Prinetto: “Formal verification of hardware correctness: an introduction”, Proc. IFIP 8th Int. Conf. CHDL, Amsterdam, April 1987 (North Holland)

    Google Scholar 

  7. Hunt: “FM8501: A Verified Microprocessor”, Technical Report 47, Institute for Computing Science. University of Texas at Austin, Feb. 1986.

    Google Scholar 

  8. Paillet: “Functional Semantics of Microprocessors at the Machine Instruction Level”, Proc. 9th IFIP Int. Conf. CHDL, Washington D.C., USA, June 89 (North Holland)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université de Provence, 3 Place Victor Hugo, 13331, Marseille, France

    H. Collavizza

Authors
  1. H. Collavizza
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Alain Finkel Matthias Jantzen

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Collavizza, H. (1992). ΜSPEED: a system for the specification and verification of microprocessors. In: Finkel, A., Jantzen, M. (eds) STACS 92. STACS 1992. Lecture Notes in Computer Science, vol 577. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55210-3_218

Download citation

  • DOI: https://doi.org/10.1007/3-540-55210-3_218

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-46775-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation