This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Mechanically Checked Proof of the AMD5K86TM Floating-Point Division Program
September 1998 (vol. 47 no. 9)
pp. 913-926
ASCII Text
x 
 
J Strother Moore, Thomas W. Lynch, Matt Kaufmann, "A Mechanically Checked Proof of the AMD5K86TM Floating-Point Division Program," IEEE Transactions on Computers, vol. 47, no. 9, pp. 913-926, September, 1998.
 
 
BibTex
x
 
@article{ 10.1109/12.713311,
author = {J Strother Moore and Thomas W. Lynch and Matt Kaufmann},
title = {A Mechanically Checked Proof of the AMD5K86TM Floating-Point Division Program},
journal ={IEEE Transactions on Computers},
volume = {47},
number = {9},
issn = {0018-9340},
year = {1998},
pages = {913-926},
doi = {http://doi.ieeecomputersociety.org/10.1109/12.713311},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Computers
TI - A Mechanically Checked Proof of the AMD5K86TM Floating-Point Division Program
IS - 9
SN - 0018-9340
SP913
EP926
EPD - 913-926
A1 - J Strother Moore,
A1 - Thomas W. Lynch,
A1 - Matt Kaufmann,
PY - 1998
KW - Division
KW - verification
KW - computer arithmetic
KW - formal verification
KW - theorem proving.
VL - 47
JA - IEEE Transactions on Computers
ER -
 

Abstract—In this article, we report the successful application of a mechanical theorem prover to the problem of verifying the division microcode program used on the AMD5K86 microprocessor. The division algorithm is an iterative shift and subtract type. It was implemented using floating-point microcode instructions. As a consequence, the floating quotient digits have data dependent precision. This breaks the constraints of conventional SRT division theory. Hence, an important question was whether the algorithm still provided perfectly rounded results at 24, 53, or 64 bits. The mechanically checked proof of this assertion is the central topic of this paper. The proof was constructed in three steps. First, the divide microcode was translated into a formal intermediate language. Then, a manually created proof was transliterated into a series of formal assertions in the ACL2 dialect. After many expansions and modifications to the original proof, the theorem prover certified the assertion that the quotient will always be correctly rounded to the target precision.

[1] D. Shephard, "Using Mathematical Logic and Formal Methods to Write Correct Microcode," SIGMICRO Newsletter, vol. 19, nos. 1-2, pp. 60-64, June 1988.
[2] M.K. Srivas and S.P. Miller, "Applying Formal Verification to a Commercial Microprocessor," Proc. ASP-DAC95/CHDL95/VLSI95 Asia and South Pacific Design Automation Conf., pp. 493-502, Aug. 1995.
[3] A. Camilleri, M. Gordon, and T. Melham, "Hardware Verification Using Higher Order Logic," HDL Descriptions to Guaranteed Correct Circuit Designs. Elsevier, 1987.
[4] ——,“Microprocessor design verification,”J. Automated Reasoning, vol. 5, pp. 429–460, 1989.
[5] T. Lynch et al., “The K5 Transcendental Functions,” Proc. 12th Symp. Computer Arithmetic, pp. 163-171, 1995.
[6] S. Coupet-Grimal and L. Jakubiec, "Coq and Hardware Verification: A Case Study," Theorem Proving and Higher Order Logics, pp. 125-139. Springer-Verlag, 1996.
[7] D.E. Atkins, "Higher-Radix Division Using Estimates of the Divisor and Partial Remainders," IEEE Trans. Computers, vol. 17, p. 930, Oct., 1968.
[8] C.S. Wallace, "Suggested Design for a Fast Multiplier," IEEE Trans. Electronic Computers, vol. 13, pp. 14-17, 1964.
[9] D. Ferrari, "A Division Method Using a Parallel Multiplier," IEEE Trans. Electronic Computers, vol. 16, pp. 224-226, Apr. 1967.
[10] M.J. Schulte, "Optimal Approximations for the Newton-Raphson Division Algorithm," Proc. SCAN-93 Conf. Scientific Computing, Computer Arithmetic, and Numeric Validation,Vienna, Sept. 1993.
[11] W.B. Brigs and D.W. Matula, "Method and Apparatus for Performing Division Using a Rectangular Aspect Ratio Multiplier," U.S. Patent No. 5046038, 1991.
[12] D. Das Sarma and D.W. Matula, “Measuring the Accuracy of ROM Reciprocal Tables,” IEEE Trans. Computers, vol. 43, no. 8, Aug. 1994.
[13] W.F. Wong and E. Goto, “Fast Hardware-Based Algorithms for Elementary Function Computations,” IEEE Trans. Computers, vol. 43, no. 3, pp. 278-294, Mar. 1994.
[14] D. Wong and M. Flynn,“Fast division using accurate quotient approximations to reduce the number of iterations,” IEEE Trans. Computers, vol. 41, pp. 981-995, Aug. 1992.
[15] D.M. Priest, "Algorithms for Arbitrary Precision Floating Point Arithmetic," Proc. 10th Symp. Computer Arithmetic, pp. 132-153,Grenoble, France, 1991.
[16] J.H. Wilkinson, Rounding Errors in Algebraic Process.London: Her Majesty's Stationary Office, 1963.
[17] P.H. Sterbenz, Floating-Point Computation.Englewood Cliffs, N.J.: Prentice Hall, 1974.
[18] J.B. Wilson, "An Algorithm for Rapid Binary Division," IEEE Trans. Electronic Computers, vol. 10, pp. 662-670, Dec. 1961.
[19] E. Ukkonen, "On the Calculation of the Effects of Roundoff Errors," ACM Trans. Mathematical Software, vol. 7, no. 3, pp. 259-271, Sept. 1981.
[20] R.S. Boyer, M. Kaufmann, and J S. Moore, "The Boyer-Moore Theorem Prover and Its Interactive Enhancement," Computers and Mathematics with Applications, vol. 29, no. 2, pp. 27-62, 1995.
[21] R. Boyer and J. Moore, A Computational Logic Handbook. New York: Academic Press, 1988.
[22] R.S. Boyer and Y. Yu, "Automated Proofs of Object Code for a Widely Used Microprocessor," J. ACM, vol. 43, no. 1, pp. 166-192, Jan. 1996.
[23] B. Brock, M. Kaufmann, and J S. Moore, "ACL2 Theorems about Commercial Microprocessors," Formal Methods in Computer-Aided Design (FMCAD '96), M. Srivas and A. Camilleri, eds. , pp. 275-293. Springer-Verlag, Nov. 1996.
[24] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams," ACM Computing Surveys, vol., 24 no. 3, pp. 293-318, 1992.
[25] R.E. Bryant, "Bit-Level Analysis of an SRT Divider Circuit," Technical Report CMU-CS-95-140, School of Computer Science, Carnegie Mellon Univ., Pittsburgh, Penn.
[26] D. Christie, "Developing the AMD-K5 Architecture," IEEE Micro, pp. 16-26, April, 1996.
[27] J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas, "A Tutorial Introduction to PVS," presented at Workshop Industrial-Strength Formal Specification Techniques,Boca Raton, Fla., Apr. 1995 (seehttp://www.csl.sri.compvs.html).
[28] M.D. Ercegovac and T. Lang, Division and Square Root—Digit-Recurrence Algorithms and Implementations. Kluwer Academic, 1994.
[29] S.F. Oberman and M.J. Flynn, “Design Issues in Division and Other Floating Point Operations,” IEEE Trans. Computers, vol. 46, no. 2, pp. 154-161, Feb. 1997.
[30] D. Goldberg, “What Every Computer Scientist Should Know About Floating-Point Arithmetic,” Computing Surveys, vol. 23, no. 1, pp. 5-48, 1991.
[31] W.A. Hunt Jr. and B. Brock, "A Formal HDL and Its Use in the FM9001 Verification," Proc. Royal Soc., 1992.
[32] M. Kaufmann and J S. Moore, ACL2 Version 2.1, http://www.cs.utexas.edu/ users/mooreacl2 , 1998.
[33] M. Kaufmann and J S. Moore, "ACL2: An Industrial Strength Theorem Prover for a Logic Based on Common LISP," IEEE Trans. Software Eng., vol. 23, no. 4, pp. 203-213, Apr. 1997.
[34] T. Lynch, A. Ahmed, and M. Schulte, "Rounding Error Analysis for Division," technical report, Advanced Micro Devices, Inc., 5204 East Ben White Blvd., Austin, TX 78741,26 May 1995.
[35] S.P. Miller and M. Srivas, "Formal Verification of the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods," WIFT '95 Workshop on Industrial-Strength Formal Specification Techniques, Apr. 1995.
[36] P.M. Miner, "Defining the IEEE-854 Floating-Point Standard in PVS," NASA Technical Memorandum 110167, NASA Langley Research Center, Hampton, Va., 1995.
[37] P.M. Miner, "Verification of IEEE Compliant Subtractive Division Algorithms," Formal Methods in Computer-Aided Design (FMCAD'96), M. Srivas and A. Camilleri, eds., pp. 64-78. Springer-Verlag, Nov. 1996.
[38] J.L. Hennessy and D.A. Patterson, Computer Architecture: A Quantitative Approach, Morgan Kaufmann, San Mateo, Calif., 1990.
[39] ANSI/IEEE Std. 754-1985, Binary Floating-Point Arithmetic, IEEE Press, Piscataway, N.J., 1985 (also called ISO/IEC 559).
[40] Standards Committee of the IEEE Computer Society. IEEE Standard for Radix-Independent Floating-Point Arithmetic, IEEE Std. 854-1987, 1987.
[41] H. Rueß, M.K. Srivas, and N. Shankar, "Modular Verification of SRT Division," Computer Science Laboratory, SRI Int'l, Menlo Park, Calif., 1996.
[42] D. Russinoff, "A Mechanically Checked Proof of Correctness of the AMD5K86 Floating-Point Square Root Microcode," http://www.onr.com/user/russ/davidfsqrt.html , Feb. 1997.
[43] D. Rusinoff, "A Mechanically Checked Proof of IEEE Compliance of a Register-Transfer-Level Specification of the AMD K7 Floating-Point Division and Square Root Instructions," http://www.onr.com/user/russ/davidk7-div-sqrt , Feb. 1998.
[44] G.L. Steele Jr., Common LISP: The Language.Bedford, Mass.: Digital Press, 1984.
[45] G.L. Steele, Common Lisp: The Language, second ed. Digital Press, 1990.

Index Terms:
Division, verification, computer arithmetic, formal verification, theorem proving.
Citation:
J Strother Moore, Thomas W. Lynch, Matt Kaufmann, "A Mechanically Checked Proof of the AMD5K86TM Floating-Point Division Program," IEEE Transactions on Computers, vol. 47, no. 9, pp. 913-926, Sept. 1998, doi:10.1109/12.713311
Usage of this product signifies your acceptance of the Terms of Use.