This work was performed jointly by Advanced Micro Devices, Inc. and Computational Logic, Inc.
The ACL2 theorem prover was used to prove the correctness of an algorithm of commercial interest. In particular we proved the correctness of the kernel of the floating point division algorithm on the AMD5K86, the first Pentium-class processor produced by AMD. As the abstract (below) makes clear, we proved that the algorithm produces the ``infinitely precise'' mathematical quotient, rounded according to a specified rounding mode. The proof is quite interesting, involving as it does the formalization of a lot of floating point ``folklore'' and classical numerical analysis.
A PostScript version of the paper abstracted below may be obtained here.
We describe a mechanically checked proof of the correctness of the kernel of the floating point division algorithm used on the AMD5K86 microprocessor. The kernel is a non-restoring division algorithm that computes the floating point quotient of two double extended precision floating point numbers, p and d (d \= 0), with respect to a rounding mode, mode. The algorithm is defined in terms of floating point addition and multiplication. First, two Newton-Raphson iterations are used to compute a floating point approximation of the reciprocal of d. The result is used to compute four floating point quotient digits in the 24,,17 format (24 bits of precision and 17 bit exponents) which are then summed using appropriate rounding modes. We prove that if p and d are 64,,15 (possibly denormal) floating point numbers, d \= 0 and mode specifies one of six rounding procedures and a desired precision 0 < n <= 64, then the output of the algorithm is p/d rounded according to mode. We prove that every intermediate result is a floating point number in the format required by the resources allocated to it. Our claims have been mechanically checked using the ACL2 theorem prover. http://dirleton.csres.utexas.edu/news/amd.html