A Case Study in Formal Verification
of Register-Transfer Logic with ACL2:
The Floating Point Adder of the AMD Athlon Processor

David M. Russinoff


As an alternative to commercial hardware description languages, AMD has developed an RTL language for microprocessor designs that is simple enough to admit a clear semantic definition, providing a basis for formal verification. We describe a mechanical proof system for designs represented in this language, consisting of a translator to the ACL2 logical programming language and a methodology for verifying properties of the resulting programs using the ACL2 prover. As an illustration, we present a proof of IEEE compliance of the floating-point adder of the AMD Athlon processor.

Full paper: ps, pdf (Invited paper, FMCAD 2000)

Slides: ps, pdf