Abstract
Clio is a system for verifying properties of expressions written in Caliban, a higher-order polymorphic strongly-typed lazy functional language akin to Turner's Miranda. Clio was designed for verifying each step in the implementation of a program: the specification, the high-level language, the assembly language, the microcode, and the hardware. This paper describes the use of Clio for verifying the correctness of an instruction pipelined microprocessor design. The abstract and the realization levels of behavior of the processor are modeled as infinite streams. The abstract specification describes the behavior in terms of a suitably chosen programmer's model of the processor. A realization specification gives a description of the design of the processor by describing the activities that happen in the circuit over a single microcycle. We develop a general criterion of correctness to relate the two levels which is verified using a form of fixed-point induction.
This work was funded by the Air Force Systems Command at Rome Air Development Center under Contract No. F30602-86-C-0115.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Harry G. Barrow. “Verify: A Program for Proving Correctness of Digital Hardware Designs”, Artificial Intelligence, 24:437–491, 1984.
M. Bickford, C. Mills, and E.A. Schneider. “Clio: An Applicative Language-Based Verification System”. Technical Report TR 15-7, Odyssey Research Associates Inc., 301A Harris B. Dates Drive, Ithaca, NY 14850, March 1989.
Mark Bickford and Mandayam Srivas. “The Verification of MiniCayuga Using Clio”. Technical Report TR 15-11, Odyssey Research Associates, Inc., 301A Harris B. Dates Drive, Ithaca, NY 14850, September 1989.
D. Borrione, P. Camurati, J.L. Paillet, and P. Prinetto. “A Functional Approach to Formal Hardware Verification”. In ICCD-88, pages 592–595, Rye Brook, NY, Oct 1988.
Robert S. Boyer and J Strother Moore. ACM Monograph Series: A Computational Logic. Academic Press, Inc., 1979.
Albert Camilleri, Mike Gordon, and Tom Melham. “Hardware Verification using Higher-Order Logic”. In IFIP WG 10.2 Workshop, From HDL to Guaranteed Correct Circuit Designs, pages 85–114. North-Holland Publishing Co., 1986.
Avra Cohn. “Correctness Properties of the Viper Block Model: The Second Level”. Technical Report 134, Computer Laboratory, University of Cambridge, Cambridge, U.K., May 1988.
Ganesh Gopalakrishnan. “Specification and Verification of Pipelined Hardware in HOP”. In Computer Hardware Description Languages and their Applications, pages 117–132, Washington, DC, June 19–21, 1989.
Michael J.C. Gordon. “LCF-LSM”. Technical report, Computer Laboratory, University of Cambridge, Cambridge, UK, 1983.
Mike Gordon. “A Machine Oriented Formulation of Higher Order Logic”. Technical Report 68, Computer Laboratory, University of Cambridge, Cambridge, U.K., July 1985.
M.J. Gordon. “Proving a Computer Correct”. Technical Report 42, Computer Laboratory, University of Cambridge, Cambridge, UK, 1983.
The Cayuga Group. “Gayuga Chip Specification: Release 2.2”. Technical report, Departments of Computer Science and Electrical Engineering, Cornell University, Ithaca, NY 14853, December 1988.
Warren A. Hunt. “FM8501: A Verified Microprocessor”. In IFIP WG 10.2 Workshop, From HDL to Guaranteed Correct Circuit Designs, pages 85–114. North-Holland Publishing Co., 1986.
J. Joyce. “Formal Specification and Verification of Microprocessor Systems”. In Proceedings of the 14th Symposium on Microprocessing and Microprogramming (EUROMICRO 88), Zurich, Switzerland, August 29 — September 1, 1988. North-Holland Publishing Co.
J. Joyce, G. Birtwistle, and M.J. Gordon. “Proving a Computer Correct in Higher Order Logic”. Technical Report Research Report No. 85/208/21, Department of Computer Science, University of Calgary, 2500 University Drive, Calgary, Canada T2N 1N4, August 1985.
R.C. Sekar and M.K. Srivas. “Formal Verification of a Microprocessor Using Equational Techniques”. In Banff Hardware Verification Workshop, Banff, Canada, June 12–18 1988.
Joseph E. Stoy. Denotational Semantics: A Scott-Strachey Approach. MIT Press, Cambridge, MA 02139, 1977.
D.A. Turner. “An overview of Miranda”. ACM SIGPLAN Notices, 21(12):158–166, December 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bickford, M., Srivas, M. (1990). Verification of a pipelined microprocessor using clio. 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_35
Download citation
DOI: https://doi.org/10.1007/0-387-97226-9_35
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