This talk is an account of my experience over the past decade in the development and application of a register-transfer logic verification methodology based on the ACL2 theorem prover, focusing on elementary floating-point operations. I describe lessons learned through the process, especially regarding the relevance of the established principles and methodologies of both software verification and traditional mathematics to the hardware problem. Finally, I briefly discuss prospects for extending these methods to functional areas beyond the floating-point unit and the ultimate objective of a fully verified microprocessor design.
Full paper: ps, pdf
Powerpoint slides
Photos