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.

Slides

• One slide per page
• Four slides per page

David Russinoff