 ACL2, successor to Nqtm (BoyerMoore Theorem Prover), used at AMD to
formally verify floating point units
 First used by Moore et al. to check the proof of correctness
of the Kernel of the AMD 5k86 floating point division algorithm
 mechanically checked proof of correctness of the kernel

Recently used to verify the RTL of the K7 Floating
Point Unit
 RTL primitives are logical operations on bit vectors
 Developed theory of bit vectors to prove RTL correct with respect
to the more abstract IEEE standard
