
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
J Strother Moore, Thomas W. Lynch, Matt Kaufmann, "A Mechanically Checked Proof of the AMD5K86TM FloatingPoint Division Program," IEEE Transactions on Computers, vol. 47, no. 9, pp. 913926, 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 FloatingPoint Division Program}, journal ={IEEE Transactions on Computers}, volume = {47}, number = {9}, issn = {00189340}, year = {1998}, pages = {913926}, 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 FloatingPoint Division Program IS  9 SN  00189340 SP913 EP926 EPD  913926 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 AMD5_{K}86 microprocessor. The division algorithm is an iterative shift and subtract type. It was implemented using floatingpoint 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. 12, pp. 6064, June 1988.
[2] M.K. Srivas and S.P. Miller, "Applying Formal Verification to a Commercial Microprocessor," Proc. ASPDAC95/CHDL95/VLSI95 Asia and South Pacific Design Automation Conf., pp. 493502, 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. 163171, 1995.
[6] S. CoupetGrimal and L. Jakubiec, "Coq and Hardware Verification: A Case Study," Theorem Proving and Higher Order Logics, pp. 125139. SpringerVerlag, 1996.
[7] D.E. Atkins, "HigherRadix 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. 1417, 1964.
[9] D. Ferrari, "A Division Method Using a Parallel Multiplier," IEEE Trans. Electronic Computers, vol. 16, pp. 224226, Apr. 1967.
[10] M.J. Schulte, "Optimal Approximations for the NewtonRaphson Division Algorithm," Proc. SCAN93 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 HardwareBased Algorithms for Elementary Function Computations,” IEEE Trans. Computers, vol. 43, no. 3, pp. 278294, 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. 981995, Aug. 1992.
[15] D.M. Priest, "Algorithms for Arbitrary Precision Floating Point Arithmetic," Proc. 10th Symp. Computer Arithmetic, pp. 132153,Grenoble, France, 1991.
[16] J.H. Wilkinson, Rounding Errors in Algebraic Process.London: Her Majesty's Stationary Office, 1963.
[17] P.H. Sterbenz, FloatingPoint 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. 662670, Dec. 1961.
[19] E. Ukkonen, "On the Calculation of the Effects of Roundoff Errors," ACM Trans. Mathematical Software, vol. 7, no. 3, pp. 259271, Sept. 1981.
[20] R.S. Boyer, M. Kaufmann, and J S. Moore, "The BoyerMoore Theorem Prover and Its Interactive Enhancement," Computers and Mathematics with Applications, vol. 29, no. 2, pp. 2762, 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. 166192, Jan. 1996.
[23] B. Brock, M. Kaufmann, and J S. Moore, "ACL2 Theorems about Commercial Microprocessors," Formal Methods in ComputerAided Design (FMCAD '96), M. Srivas and A. Camilleri, eds. , pp. 275293. SpringerVerlag, Nov. 1996.
[24] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered BinaryDecision Diagrams," ACM Computing Surveys, vol., 24 no. 3, pp. 293318, 1992.
[25] R.E. Bryant, "BitLevel Analysis of an SRT Divider Circuit," Technical Report CMUCS95140, School of Computer Science, Carnegie Mellon Univ., Pittsburgh, Penn.
[26] D. Christie, "Developing the AMDK5 Architecture," IEEE Micro, pp. 1626, April, 1996.
[27] J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas, "A Tutorial Introduction to PVS," presented at Workshop IndustrialStrength 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—DigitRecurrence 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. 154161, Feb. 1997.
[30] D. Goldberg, “What Every Computer Scientist Should Know About FloatingPoint Arithmetic,” Computing Surveys, vol. 23, no. 1, pp. 548, 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. 203213, 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 IndustrialStrength Formal Specification Techniques, Apr. 1995.
[36] P.M. Miner, "Defining the IEEE854 FloatingPoint 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 ComputerAided Design (FMCAD'96), M. Srivas and A. Camilleri, eds., pp. 6478. SpringerVerlag, 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. 7541985, Binary FloatingPoint Arithmetic, IEEE Press, Piscataway, N.J., 1985 (also called ISO/IEC 559).
[40] Standards Committee of the IEEE Computer Society. IEEE Standard for RadixIndependent FloatingPoint Arithmetic, IEEE Std. 8541987, 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 FloatingPoint 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 RegisterTransferLevel Specification of the AMD K7 FloatingPoint Division and Square Root Instructions," http://www.onr.com/user/russ/davidk7divsqrt , 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.