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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media New York
About this chapter
Cite this chapter
Russinoff, D.M., Flatau, A. (2000). RTL Verification: A Floating-Point Multiplier. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds) Computer-Aided Reasoning. Advances in Formal Methods, vol 4. Springer, Boston, MA. https://doi.org/10.1007/978-1-4757-3188-0_13
Download citation
DOI: https://doi.org/10.1007/978-1-4757-3188-0_13
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-4981-3
Online ISBN: 978-1-4757-3188-0
eBook Packages: Springer Book Archive