RTL verification: a floating-point multiplier
2000
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:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
0
References
22
Citations
NaN
KQI