ACL2 was designed to let us tackle theorems of industrial interest. One such theorem is the correctness of the floating-point division microcode on the K5 microprocessor of Advanced Micro Devices, Inc. The microcode implements division using floating-point addition and multiplication, with directed rounding.
Using ACL2 we proved
Theorem: If p and d are extended precision floating-point numbers, where d is not 0, and mode is a rounding mode, then the microcode above produces the properly rounded mathematical quotient of p and d.
This work was done in collaboration with Tom Lynch and Matt Kaufmann.