This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Modeling and Verification of Microprocessors
January 1995 (vol. 44 no. 1)
pp. 54-72

Abstract—Formal verification has long been promised as a means of reducing the amount of testing required to ensure correct VLSI devices. Verification requires at least two mathematical models: one that describes the structure of a computer system and another that models its intended behavior. These models are called specifications. Verification is a mathematical analysis showing that the behavior follows from the structure. Formal verification of microprocessor designs has been quite successful. Indeed, several verified microprocessors have been presented in the literature, and one microprocessor where formal modeling has been applied is commercially available. These efforts were virtuoso performances—largely academic exercises carried out by experts in logic and specification.

This paper presents a methodology for microprocessor verification that significantly reduces the learning curve for performing verification. The methodology is formalized in the HOL theorem-proving system. The paper includes a description of a large case study performed to evaluate the methodology.

The novel aspects of this research include the use of abstract theories to formalize hardware models. Because our model is described using abstract theories, it provides a framework for both the specification and the verification. This framework reduces the number of ad hoc modeling decisions that must be made to complete the verification. Another unique aspect of our research is the use of hierarchical abstractions to reduce the number of difficult lemmas in completing the verification. Our formalism frees the user from directly reasoning about the difficult aspects of modeling the hierarchy, namely the temporal and data abstractions.

We believe that our formalism, coupled with case studies and tools, allows microprocessor verification to be done by engineers with relatively little experience in microprocessor specification or logic. We are currently testing that hypothesis by using the methodology to teach graduate students formal microprocessor modeling.

[1] Advanced Micro Devices,Bipolar Microprocessor Logic and Interface Data Book, AMD Inc., 1983.
[2] F. Anceau,The Architecture of Microprocessors. Reading, MA: Addison-Wesley, 1986.
[3] A. Camilleri, M. Gordon, and T. Melham,“Hardware verification using higher order logic,”inFrom HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione, Ed. New York: Elsevier, 1987.
[4] A. Church,“A formulation of the simple theory of types,”J. Symbolic Logic, vol. 5, pp. 56–115, 1940.
[5] A. Cohn,“Correctness properties of the VIPER block model: The second level,”Tech. Rep. 134, Univ. of Cambridge Comput. Lab., May 1988.
[6] ——,“The notion of proof in hardware verification,”J. Automated Reasoning, vol. 5, pp. 127–139, 1989.
[7] J. W. Gambles and P. J. Windley,“Integrating formal verification with CAD tool environments,”inProc. Fourth Annu. IEEE/NASA Symp. VLSI Design, Oct. 1992, pp. 6.3.1–6.3.12.
[8] M. J. Gordon,“HOL: A proof generating system for higher order logic,”inVLSI Specification, Verification, and Synthesis, G. Birtwhistle and P. Subrahmanyam, Eds. New York: Kluwer Academic Press, 1988.
[9] J. Herbert,“Temporal abstraction of digital designs,”inThe Fusion of Hardware Design and Verification, Proceedings of the IFIP WG 10.2 International Working Conference, Glasgow, Scotland, G. Milne, Ed. Amsterdam, The Netherlands: North-Holland, 1988.
[10] W. A. Hunt,“The mechanical verification of a microprocessor design,”inFrom HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione, Ed. New York: Elsevier, 1987.
[11] ——,“Microprocessor design verification,”J. Automated Reasoning, vol. 5, pp. 429–460, 1989.
[12] J. J. Joyce,“Multi-level verification of microprocessor-based systems,”Ph.D. thesis, Cambridge Univ., Dec. 1989.
[13] J. J. Joyce and C. Seger, private communication, Univ. of British Columbia, Oct. 1992.
[14] M.G.H. Katevenis, Reduced Instruction Set Computer Architectures for VLSI.Cambridge, Mass.: MIT Press, 1985.
[15] T. Melham,“Abstraction mechanisms for hardware verification,”inVLSI Specification, Verification and Synthesis, G. Birtwhistle and P. A. Subrahmanyam, Eds. New York: Kluwer Academic Publishers, 1988.
[16] SRI Int. Comput. Sci. Lab.,EHDM Specification and Verification System: User's Guide,Version 4.1, 1988.
[17] P. J. Windley,“The Formal verification of generic interpreters,”Ph.D. thesis, Univ. of California, Davis, Div. of Comput. Sci., June 1990.
[18] ——,“A hierarchical methodology for the verification of microprogrammed microprocessors,”inProc. IEEE Symp. Security and Privacy, May 1990, pp. 345–359.
[19] ——,“The verification of AVM-1, Tech. Rep. CSE-90-21, Univ. of California, Davis, Div. of Comput. Sci., 1990.
[20] ——,“Using correctness results to verify behavioral properties of microprocessors,”inProc. IEEE Comput. Assurance Conf., June 1991, pp. 99–106.
[21] ——,“Abstract theories in HOL,”inProceedings of the 1992 International Workshop on the HOL Theorem Prover and its Applications, L. Claesen and M. J. C. Gordon, Eds. New York: North-Holland, Nov. 1992.
[22] ——,“Instruction set commutivity,”inProc. Fourth Annu. IEEE/NASA Symp. VLSI Design, Oct. 1992, pp. 6.5.1–6.5.11.
[23] P. J. Windley and M. Coe,“The formal verification of instruction pipelines,”inProceedings of the 1994 Conference on Theorem Provers in Circuit Design, Lecture Notes in Computer Science, R. Kumar and T. Kropf, Eds. New York: Springer-Verlag, Sept. 1994.

Citation:
Phillip J. Windley, "Formal Modeling and Verification of Microprocessors," IEEE Transactions on Computers, vol. 44, no. 1, pp. 54-72, Jan. 1995, doi:10.1109/12.368009
Usage of this product signifies your acceptance of the Terms of Use.