A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon

David M. Russinoff

Browse the full FMCAD paper archive.