Department of Computer Sciences

1999 ACL2 Workshop

March 29 - March 31, 1999

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

We describe a methodology for formal verification of register-transfer logic (RTL) models of floating-point designs, based on a mechanical translator from the AMD RTL language to ACL2 and a library of ACL2 results pertaining to logical operations on bit vectors and floating-point rounding. As an illustration, we present a mechanical proof of IEEE-compliance of a simple floating-point multiplier.


David Russinoff

Last updated March 1999
Computer Sciences Department
University of Texas at Austin