Advertisement

RTL Verification: A Floating-Point Multiplier

  • David M. Russinoff
  • Arthur Flatau
Part of the Advances in Formal Methods book series (ADFM, volume 4)

Abstract

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.

Keywords

Input Valuation Combinational Circuit Hardware Description Language Circuit Description Informal Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 2000

Authors and Affiliations

  • David M. Russinoff
    • 1
  • Arthur Flatau
    • 1
  1. 1.Advanced Micro Devices, Inc.AustinUSA

Personalised recommendations