Skip to main content
SpringerLink
Log in

The verification of a bit-slice ALU

  • Conference paper
  • First Online:
Hardware Specification, Verification and Synthesis: Mathematical Aspects

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

Abstract

The verification of a bit-slice ALU has been accomplished using a mechanical theorem prover. This ALU has an n-bit design specification, which has been verified to implement its top-level specification. The ALU and top-level specifications were written in the Boyer-Moore logic. The verification was carried out with the aid of Boyer-Moore theorem prover in a hierarchical fashion.

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. S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, Boston, 1988.

    Google Scholar 

  2. Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8):677–691, August, 1986.

    Google Scholar 

  3. Warren A. Hunt, Jr. FM8501: A Verified Microprocessor. Technical Report ICSCA-CMP-47, University of Texas at Austin, 1985.

    Google Scholar 

  4. Warren A. Hunt, Jr. The Mechanical Verification of a Microprocessor Design. In D. Borrione (editor), From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 89–132. North Holland, 1987.

    Google Scholar 

  5. Warren A. Hunt, Jr. Microprocessor Design Verification. Journal of Automated Reasoning (to appear), 1989.

    Google Scholar 

  6. J S. Moore. Piton: A Verified Assembly Level Language. Technical Report 22, Computational Logic, Inc., 1717 West Sixth Street, Suite 290 Austin, TX 78703, 1988.

    Google Scholar 

  7. Guy L. Steele Jr. Common LISP: The Language. Digital Press, 1984.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computational Logic, Inc., 1717 West Sixth Street, Suite 290, 78703-4776, Austin, Texas, U.S.A.

    Warren A. Hunt Jr. & Bishop C. Brock

Authors
  1. Warren A. Hunt Jr.
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bishop C. Brock
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Miriam Leeser Geoffrey Brown

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hunt, W.A., Brock, B.C. (1990). The verification of a bit-slice ALU. In: Leeser, M., Brown, G. (eds) Hardware Specification, Verification and Synthesis: Mathematical Aspects. Lecture Notes in Computer Science, vol 408. Springer, New York, NY. https://doi.org/10.1007/0-387-97226-9_34

Download citation

  • DOI: https://doi.org/10.1007/0-387-97226-9_34

  • Published:

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-0-387-97226-8

  • Online ISBN: 978-0-387-34801-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation