A Mathematical Approach to RTL Verification

David M. Russinoff

Invited talk
19th International Conference on Computer Aided Verification
(CAV 2007)


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