Abstract
We present a rigorous mathematical proof of the correctness of the floating point square root instruction of the AMD K5 microprocessor. The instruction is represented as a program in a formal language that was designed for this purpose, based on the K5 microcode and the architecture of its FPU. We prove a statement of its correctness that corresponds directly with the IEEE Standard. We also derive an equivalent formulation, expressed in terms of rational arithmetic, which has been encoded as a formula in the ACL2 logic and mechanically verified with the ACL2 prover. Finally, we describe a microcode modification that was implemented as a result of this analysis in order to ensure the correctness of the instruction.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
R.S. Boyer and J. Moore, A Computational Logic Handbook, Academic Press, Boston, MA, 1988.
R.E. Bryant, Verification of arithmetic functions with binary moment diagrams, Technical Report CMU-CS–94–160, School of Computer Science, Carnegie-Mellon University, 1994.
E.M. Clarke and X. Zhao, Word level symbolic model checking: A new approach for verifying arithmetic circuits, Technical Report CMU-CS–95–161, School of Computer Science, Carnegie-Mellon University, 1995.
J. Harrison, Floating point verification in HOL, in Proc. 8th Intl. Workshop on Higher Order Logic Theorem Proving and its Applications, Springer-Verlag, 1995.
Institute of Electrical and Electronic Engineers, IEEE standard for binary floating point arithmetic, Std. 754–1985, New York, NY, 1985.
Intel Corporation, Pentium Family User's Manual, Vol. 3: Architecture and Programming Manual, 1994.
M. Kaufmann and J. Moore, A precise description of the ACL2 logic, http://www.cs.utexas.edu/users/moore/acl2/reports/km97a.ps
M. Leeser and J. O'Leary, Verification of a subtractive Radix-2 square root algorithm and implementation, in Proc. Intl. Conf. on Computer Design, 1995.
P. Miner and J. Leathrum, Verification of IEEE compliant subtractive division algorithms, in M. Srivas and A. Camilleri (Eds.), Proceedings of Formal Methods in Computer-Aided Design (FMCAD) '96, Springer-Verlag LNCS 1166, pp. 275–293, 1996.
J. Moore, T. Lynch, and M. Kaufmann, A mechanically checked proof of the correctness of the kernel of the AMD5K 86 floating-point division algorithm, http://devil.ece.utexas.edu/lynch/divide/divide.html
H. Rueß, M.K. Srivas, and N. Shankar, Modular verification of SRT division, in R. Alur and T. Henzinger (Eds.), Computer-Aided Verification (CAV '96), Springer Verlag LNCS 1102, pp. 123–134, July 1996.
D.M. Russinoff, A mechanically checked proof of IEEE compliance of the AMD K7 floating point multiplication, division, and square root instructions, http://www.onr.com/user/russ/david/k7-div-sqrt.ps.
G.L. Steele, Jr., Common Lisp The Language, 2nd edition, Digital Press, 1990.
Rights and permissions
About this article
Cite this article
Russinoff, D.M. A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode. Formal Methods in System Design 14, 75–125 (1999). https://doi.org/10.1023/A:1008669628911
Issue Date:
DOI: https://doi.org/10.1023/A:1008669628911