A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD AthlonTM Processor
2000
One obstacle to mathematical verification of industrial hard-ware designs is that the commercial hardware description languages in which they are usually encoded are too complicated and poorly specified to be readily susceptible to formal analysis. As an alternative to these commercial languages, AMD has developed an RTL language for microprocessor designs that is simple enough to admit a clear semantic definition, providing a basis for formal verification. We describe a mechanical proof system for designs represented in this language, consisting of a translator to the ACL2 logical programming language and a methodology for verifiying properties of the resulting programs using the ACL2 prover. As an illustration, we present a proof of IEEE compliance of the floating-point adder of the AMD Athlon processor.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
9
References
43
Citations
NaN
KQI