Modelling bit vectors in HOL: The word library | SpringerLink
Skip to main content
Springer Nature Link
Log in

Modelling bit vectors in HOL: The word library

  • Conference paper
  • First Online:
Higher Order Logic Theorem Proving and Its Applications (HUG 1993)

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

Included in the following conference series:

Abstract

The bit vector is one of the fundamental data objects in hardware specification and verification. The modelling of bit vectors is a key to the success of a hardware verification project. This paper describes a pragmatic approach to modelling bit vectors in higher-order logic and an implementation as a system library in the HOL theorem prover. In this approach, bit vectors are represented using a polymorphic type. Restricted quantifications are used to simulate dependent types to model the sizes of the vectors. The library consists of many theorems asserting the basic properties of the bit vectors and some useful tools for reasoning about them. Examples showing the effective use of the library are described.

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.

Similar content being viewed by others

References

  1. R. J. Boulton. A HOL semantics for a subset of ELLA. Technical Report 254, University of Cambridge Computer Laboratory, 1992.

    Google Scholar 

  2. A. J. Camilleri. Executing behavioural definitions in higher order logic. Technical Report 140, University of Cambridge Computer Laboratory, 1988.

    Google Scholar 

  3. A. Cohn. A proof of correctness of the VIPER microprocessor: the first level. Technical Report 104, University of Cambridge Computer Laboratory, January 1988.

    Google Scholar 

  4. A. Cohn. A proof of correctness of the VIPER microprocessor: the second level. Technical Report 134, University of Cambridge Computer Laboratory, May 1990.

    Google Scholar 

  5. A. Cohn and M. J. C. Gordon. A machanized proof of correctness of a simple counter. Technical Report 94, University of Cambridge Computer Laborartory, July 1986.

    Google Scholar 

  6. M. J. C. Gordon. Hardware verification by formal proof. Technical Report 74, University of Cambridge Computer Laborartory, 1985.

    Google Scholar 

  7. Michael. C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. J. Milne and P. A. Subrahmanyan, editors, Formal Aspects of VLSI Design, pages 153–178. Springer-Verlag, 1986.

    Google Scholar 

  8. Brian T. Graham. The SECD Microprocessor — a Verification Case Study. Kluwer Academic Publishers, 1992.

    Google Scholar 

  9. J. Joyce, G. Birtwistle, and M. J. C. Gordon. Proving a computer correct in higher order logic. Technical Report 100, University of Cambridge Computer Laborartory, December 1986.

    Google Scholar 

  10. J. J. Joyce. Formal specification and verification of microprocessor systems. In S. Winter and H. Schumny, editors, EUROMICRO 88:Proceedings of the 14th Symposium on Microprocessing and Microprogramming. Horth-Holland, 1988.

    Google Scholar 

  11. T. F. Melham. Automating recursive type definition in higher-order logic. In Graham Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341–386. Springer-Verlag, 1989.

    Google Scholar 

  12. T. F. Melham. Formalizing abstraction mechanisms for hardware verification in higher order logic. Technical Report 201, University of Cambridge Computer Laboratory, 1990.

    Google Scholar 

  13. T. F. Melham. The HOL logic extended with quantification over type variables. In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications. Horth-Holland, 1993.

    Google Scholar 

  14. W. Wong. Formal verification of VIPER's ALU. Technical Report 300, University of Cambridge Computer Laboratory, University of Cambridge Computer laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, ENGLAND, May 1993.

    Google Scholar 

  15. W. Wong. The HOL res-quan Library. Computer Laboratory, University of Cambridge, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Laboratory New Museums Site, University of Cambridge, Pembroke Street, CB2 3QG, Cambridge

    Wai Wong

Authors
  1. Wai Wong
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jeffrey J. Joyce Carl-Johan H. Seger

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wong, W. (1994). Modelling bit vectors in HOL: The word library. In: Joyce, J.J., Seger, CJ.H. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1993. Lecture Notes in Computer Science, vol 780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57826-9_149

Download citation

  • DOI: https://doi.org/10.1007/3-540-57826-9_149

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57826-0

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation