Abstract
This paper develops a method for formally proving the correctness of a microprocessor using an equational method. The behavioral and structural specifications of the processor are expressed in a functional language. The asynchronous interaction between the memory and CPU is expressed in the specification by using a nondeterministic function random. This makes our specification more direct and natural than previous efforts based on a functional formalism. The previous efforts have had to encode in the specification the anticipated asynchronous interaction between the memory and the CPU.
The statement of correctness is expressed as a sentence in FOPC with equations relating expressions of the specification language as atomic formulae. The verification is carried out by formulating a set of invariants on the reachable states of the processor. The invariants are verified via symbolic evaluation employing appropriate induction and case analysis. The invariant approach makes the verification method modular in that it isolates the parts of the proof which are microcode-dependent from the rest. The method has been applied to verify an abstract version of the processor architecture used in Wirth’s Modula II machine LILITH.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barrow H.G.VERIFY: A Program for Proving Correctness of Digital Hardware Designs Artificial Intelligence 24 (1984), pp. 437-491, Elsevier Science Publishers B.V.(North-Holland).
Gordon M.J.Proving a Computer CorrectTechnical Report No. 42, Computer Laboratory, University of Cambridge, 1983.
Gopalakrishnan G. Smith, D.R., Srivas, M.K. “An Algebraic Approach to the Specification and Realization of VLSI Designs”,Proc. Seventh International Symposium on Computer Hardware Description Languages, Tokyo August 1985.
Gopalakrishnan G., Srivas, M.K., Smith, D.R.,From Algebraic Specifications to Correct VLSI CircuitsProc. of IFIP Working Conference on From H.D.L. Descriptions to Guaranteed Correct Circuit Designs Grenoble France September 9 - 11 1986.
Henderson, P.,Functional Programming: Application and Implementation, Prentice- Hall, 1980.
Hunt W.A.The Mechanical Verification of a Microprocessor Design Proc. of IFIP Working Conference on From H.D.L. Descriptions to Guaranteed Correct Circuit Designs Grenoble France September 9-11 1986.
Joyce J. Birtwistle G. Gordon M.,Proving a Computer Correct in Higher Order Logic, Research Report No. 85/208/21, University of Calgary, August 1985.
Kapur D. and SivakumarRewrite Rule Laboratory Proceedings of G.E. Workshop on Rewrite Rule Laboratory, Schnectady, September 1983.
Lee, N. C., “Integration of SBL into a VLSI Design System”, PhD thesis, Dept. EE., SUNY, Stony Brook, December 1987.
Lescanne P.Computer Experiments with the REVE Term Rewriting System Generator Proceedings of theTenth Annual Symposium on Principles of Programming Languages Austin, Texas, January 1983.
Manna Z.Mathematical Theory of Computation McGraw-Hill Publishing Co., New York, 1974.
Mills C.Introduction to ORACLE/Caliban Internal Memo, Odyssey Research Associates Inc. Ithaca, NY 14850.
Proceedings of International Working Conference onFrom H.D.L. Descriptions to Guaranteed Correct Circuit Designs IFIP Grenoble France September 1986.
Srivas, M.K., Smith, D.R., Lee, N.C. “The SBL Users Manual”, Tech. Rpt, Dept CS., SUNY, Stony Brook, Dec 1987.
Wirth, N., “The Personal Computer Lilith”, Tech. Report, Eidgenossische Technische Hochschule, Institut fur Informatik, Zurich, April 1981.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1989 Springer-Verlag New York Inc.
About this chapter
Cite this chapter
Sekar, R.C., Srivas, M.K. (1989). Formal Verification of a Microprocessor Using Equational Techniques. In: Birtwistle, G., Subrahmanyam, P.A. (eds) Current Trends in Hardware Verification and Automated Theorem Proving. Springer, New York, NY. https://doi.org/10.1007/978-1-4612-3658-0_4
Download citation
DOI: https://doi.org/10.1007/978-1-4612-3658-0_4
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4612-8195-5
Online ISBN: 978-1-4612-3658-0
eBook Packages: Springer Book Archive