proving division from comp.arch.arithmetic

[David G. Hough at validgh]

Article: 1800 of comp.arch.arithmetic
From: cohenaalamo.cli.com (Rich Cohen)
Newsgroups: comp.arch.arithmetic,comp.arch,comp.specification.misc,comp.sys.intel
Subject: Proof of a Floating Point Division Algorithm
Date: 22 Apr 96 20:14:35 GMT
Organization: Computational Logic, Inc.

[I'm forwarding this on behalf of J Moore.  Contact J (Mooreacli.com)
 or one of the other authors below for follow-ups.  -- RMC]

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 AMD 5K86, 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.

The paper may be obtained via the URL:

 http://devil.ece.utexas.edu:80/~lynch/divide/divide.html

The title and abstract are shown below.


Thanks,
J Strother Moore

-------

         A Mechanically Checked Proof of the Correctness of the Kernel
             of the AMD 5K86 (tm) Floating-point Division Algorithm

		       J Strother Moore (Mooreacli.com)
			 Tom Lynch (Tom.Lynchaamd.com)
		  Matt Kaufmann (Matt_Kaufmannaemail.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.

<PRE>