Mechanical Verification of Register-Transfer Logic:
A Floating-Point Multiplier

David M. Russinoff
Arthur Flatau

Abstract

We describe a mechanical proof system for designs represented in the AMD RTL 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 correctness of a simple floating-point multiplier.

Full paper: ps, pdf (appeared in M. Kaufmann, P. Manolios, and J Moore, Editors, Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Press, 2000)