Abstract
The functional verification of microprocessor designs continues to represent one of the difficult challenges confronting the design of commercial microprocessors. In addition, test logic, transient errors, and power considerations complicate the problems by creating additional complexity and constraints on design solutions. Rigorious mechanized mathematics, often called formal methods, are being used to assist with functional verification and its use has spread to ensuring that test coverage and power limitations are met. While the successes have been notable, the wide-spread use of mathematical methods is still limited. Here we give a brief introduction to formal microprocessor verification, and then we present some scientific and engineering issues that need addressing to bring formal methods into the mainstream.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aagaard, M.D., Cook, B., Day, N.A., Jones, R.B.: A framework for microprocessor correctness statements. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 433–448. Springer, Heidelberg (2001)
Aagaard, M., Day, N., Lou, M.: Relating Multi-step and Single-Step Microprocessor Correctness Statements. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 123–141. Springer, Heidelberg (2002)
Bevier, W.R., Hunt, W.A.: An Approach to Systems Verification. Journal of Automated Reasoning  5 (1989)
Brock, B.C., Hunt Jr., W.: Formal Analysis of the Motorola CAP DSP. In: Hinchey, M., Bowen, J. (eds.) Industrial-Strength Formal Methods, Springer, Heidelberg (1999)
Burch, J.R., Dill, D.L.: Automatic Verification of Pipelined Microprocessor Control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Gordon, M., Hurd, J., Slind, K.: Executing the formal semantics of the accellera property specification language by mechanised theorem proving. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 200–215. Springer, Heidelberg (2003)
Hunt Jr., W.A.: FM8501: A Verified Microprocessor. LNCS(LNAI), vol. 795. Springer, Heidelberg (1994)
Hunt Jr., W., Brock, B.: A Formal HDL and Its Use in the FM9001 Verification. In: Hoare, C.A.R., Gordon, M.J.C. (eds.) Mechanized Reasoning and Hardware Design, pp. 35–48. Prentice-Hall International Series in Computer Science, Engle wood Cliffs (1992)
Hunt Jr., W., Sawada, J.: Verifying the FM9801 Microarchitecture. In: IEEE Micro., May-June 1999, pp. 47–55. IEEE Press, Los Alamitos (1999)
Kaufmann, M., Moore, J.S.: ACL2: An Industrial Strength Version of Nqthm. In: Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS 1996), June 1996, pp. 23–34. IEEE Computer Society Press, Los Alamitos (1996)
Manolios, P.: Correctness of pipelined machines. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 161–178. Springer, Heidelberg (2000)
McMillan, K.L.: A Methodology for Hardware Verification Using Compositional Model Checking. Science of Computer Programming 37(1-3), 279–309 (2000)
Ray, S., Hunt Jr., W.A.: Deductive verification of pipelined machines using first-order quantification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 31–43. Springer, Heidelberg (2004)
Sawada, J., Hunt Jr., W.: Trace Table Based Approach for Pipelined Microprocessor Verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 364–375. Springer, Heidelberg (1997)
Sawada, J., Hunt Jr, W.: Processor Verification with Precise Exceptions and Speculative Execution. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 135–146. Springer, Heidelberg (1998)
Sawada, J., Hunt Jr., W.: Verification of the FM9801 Microprocessor: An Outof- order Microprocessor Model with Speculative Execution, Exceptions, and Self- Modifying Code. In: Formal Methods in Systems Design, March 2002, vol. 20(2), pp. 187–222. Kluwer Academic Publishers, Dordrecht (2002)
Yang, J., Seger, C.: Generalized Symbolic Trajectory Evaluation — Abstraction in Action. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 70–87. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hunt, W.A. (2004). Mechanical Mathematical Methods for Microprocessor Verification. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_51
Download citation
DOI: https://doi.org/10.1007/978-3-540-27813-9_51
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22342-9
Online ISBN: 978-3-540-27813-9
eBook Packages: Springer Book Archive