One of the notable results of ACL2 was a proof that the floating-point unit (FPU) of AMD Athlon processor executes elementary FP operations (additions, subtraction, multiplication, division and the square root) strictly according to the IEEE specification. To be precise, they proved that the unit that operates 'extended precision' FP numbers is correct. The regular FP numbers are converted to the extended format by a separate hardware unit, which also deals with unnormalized numbers, NaNs and infinities. This was at a time of a Pentium FDIV scandal. AMD management was terrified to think that the upcoming Athlon may have some rare but immensely embarrassing bug.

The FP unit was specified in Register Transfer Language (RTL) -- a common hardware description language that describes registers of various logical/arithmetical components and data transfers. To prove the correctness of FPU, Moore and his group had to develop a translator from RTL to ACL2, the input language of the prover. Moore had to convince the AMD management that the translation is sound. Alas, RTL is not specified precisely; its semantics is defined by an RTL emulator.

The fact that ACL2 specification is itself ACL2 code, which is applicative Common Lisp code, turned out very handy. ACL2 specifications can be executed! The ACL2 _specification_ for the FPU can therefore be considered an emulator for the FPU: it takes bit patterns representing input FP numbers and prints the output bit patterns. To convince the management that the ACL2 FPU specification is a sound representation of the original RTL specification, one needs to show that the two FPU emulators are equivalent. The management gave Moore 80 million test vectors, designed to verify the RTL specs. The compiled ACL2 specs code produced the same results for these vectors as the RTL emulator. That convinced the AMD management that the ACL2 specs accurately reflect RTL code for their FPU. After that, Moore and his students proceeded to prove that the ACL2 FPU specs are consistent with the IEEE arithmetic rules. They found four real bugs -- which were confirmed as bugs by the RTL emulator. These four bugs survived all perviously tried 80 million test vectors!