RTL verification: a floating-point multiplier

We describe a mechanical proof system for designs represented in the AMD1 RTL language, consisting of a translator to the ACL2 logical programming language and a methology for verifiying properties of the resulting programs using the ACL2 prover. As an illustration, we present a proof of correctness of a simple floating-point multiplier.