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.
KeywordsInput Valuation Combinational Circuit Hardware Description Language Circuit Description Informal Proof
Unable to display preview. Download preview PDF.