AMD5K86 Floating-Point Division Algorithm
J Strother Moore <moore@cli.com>
Fri, 19 Apr 96 14:28:31 CDT
I would like to bring your attention to some recent joint work by Advanced
Micro Devices, Inc., and Computational Logic, Inc., in which 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. Roughly speaking, we proved that
the algorithm implements division on the double extended precision normal
and denormal numbers of the IEEE standard, in the sense that (under
appropriate hypotheses) it returns the floating-point number obtained by
rounding the ``infinitely precise'' quotient by the method and to the
precision specified by a given rounding mode. The permitted rounding modes
include round to 0, round away from 0, round to nearest, round to positive
(or negative) infinity, and ``sticky'' rounding. The proof is quite
interesting, involving as it does the formalization of a lot of
floating-point ``folklore'' and classical numerical analysis.
J Strother Moore
The paper may be obtained via the URL:
http://devil.ece.utexas.edu:80/~lync...de/divide.html
The title and abstract are shown below.
A Mechanically Checked Proof of the Correctness of the Kernel
of the AMD5K86 (tm) Floating-point Division Algorithm
J Strother Moore (Moore@cli.com)
Tom Lynch (Tom.Lynch@amd.com)
Matt Kaufmann (Matt_Kaufmann@email.mot.com)
ABSTRACT:
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.
Partager