Abstract
We present a case study of hardware specification and verification in the Nuprl Proof Development System. Within Nuprl we have built a specialized environment consisting of tactics, definitions, and theorems for specifying and reasoning about hardware. Such reasoning typically consists of term-rewriting, case-analysis, induction, and arithmetic reasoning. We have built tools that provide high-level assistance for these tasks.
The hardware component that we have proven is the front end of a floating-point adder/subtractor. This component, the MAEC (Mantissa Adjuster and Exponent Calculator), has 5459 transistors and has been proven down to the transistor level. As the circuit has 116 inputs and 107 outputs, verification by traditional methods such as case analysis would have been a practical impossibility.
Supported in part by an IBM Fellowship.
Supported in part by NSF grant CCR8616552 and ONR grant N00014-88-K-0409.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
G. Barrett. Formal methods applied to a floating point number system. IEEE Transactions on Software Engineering, 15(5):611–621, May 1989.
David A. Basin. Implementing Problem Solving Environments In Constructive Type Theory. PhD thesis, Cornell University, 1990. To appear.
David A. Basin. Building theories in Nuprl. In Logic At Botik, '89, 1989. To Appear.
Robert S. Boyer and J. Strother Moore. A Computational Logic. Academic Press, 1979.
A. J. Camillieri, M. J. C. Gordon, and T. F. Melham. Hardware verification using higher-order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. North Holland, September 1986.
A. Cohn. A proof of correctness of the VIPER microprocessor: The first level. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis, pages 27–72. Kluwer, 1988.
R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.
Michael J. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.
Douglas J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988.
Warren J. Hunt. The mechanical verification of a microprocessor design. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 89–129. Elsevier Science Publishers B. V. (North-Holland), 1987.
INMOS. T800 architecture. INMOS Technical note 6.
Per Martin-Löf. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153–175, Amsterdam, 1982. North Holland.
Lawrence C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119–149, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basin, D.A., Del Vecchio, P. (1990). Verification of combinational logic in Nuprl. 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_36
Download citation
DOI: https://doi.org/10.1007/0-387-97226-9_36
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