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]