Issue No. 09 - September (1998 vol. 47)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/12.713311
<p><b>Abstract</b>—In this article, we report the successful application of a mechanical theorem prover to the problem of verifying the division microcode program used on the AMD5<sub><it>K</it></sub>86 microprocessor. The division algorithm is an iterative shift and subtract type. It was implemented using floating-point microcode instructions. As a consequence, the floating quotient digits have data dependent precision. This breaks the constraints of conventional SRT division theory. Hence, an important question was whether the algorithm still provided perfectly rounded results at 24, 53, or 64 bits. The mechanically checked proof of this assertion is the central topic of this paper. The proof was constructed in three steps. First, the divide microcode was translated into a formal intermediate language. Then, a manually created proof was transliterated into a series of formal assertions in the ACL2 dialect. After many expansions and modifications to the original proof, the theorem prover certified the assertion that the quotient will always be correctly rounded to the target precision.</p>
Division, verification, computer arithmetic, formal verification, theorem proving.
Thomas W. Lynch, Matt Kaufmann, J Strother Moore, "A Mechanically Checked Proof of the AMD5K86TM Floating-Point Division Program", IEEE Transactions on Computers, vol. 47, no. , pp. 913-926, September 1998, doi:10.1109/12.713311