AMD5k86 Floating-Point Division

The K5 microprocessor of Advanced Micro Devices, Inc., AMD's first Pentium-class microprocessor, uses a microcoded floating-point division algorithm. An unusual aspect of the algorithm is that all intermediate values are represented with normalized floating-point numbers; the algorithm is coded in terms of floating-point addition and multiplication with directed rounding. It uses two Newton-Raphson iterations to approximate the inverse of the divisor and then uses the approximate inverse to compute four floating-point ``quotient digits'' which are then summed with ``sticky rounding.''

Using ACL2, Tom Lynch (the algorithm's designer), Matt Kaufmann and I proved the following theorem:

Correctness of the AMD5k86 Floating-Point Division: If p and d are double extended precision floating-point numbers (d /= 0) and mode is a rounding mode specifying a rounding style and target format of precision n not exceeding 64, then the result delivered by the K5 microcode is p/d rounded according to mode.

We also proved that every intermediate result is a floating-point number that fits in the resources allocated to it.

To carry out these proofs with ACL2 it was first necessary to formalize and prove much ``floating-point folklore.''

For details see

A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5k86 Floating-Point Division Algorithm, with T. Lynch and M. Kaufmann, IEEE Transactions on Computers, 47(9), pp. 913-926, Sep., 1998. [The URL provided is an early draft of the paper eventually published.]

[Best Ideas] [Publications] [Research] [Home]