Abstract
The formal hardware verification effort at Advanced Micro Devices, Inc. has emphasized theorem proving using ACL2, and has focused on the elementary floating-point operations. Floating-point modules, along with the rest of our microprocessor designs, are specified at the register-transfer level in a small synthesizable subset of Verilog. This language is simple enough to admit a clear semantic definition, providing a basis for formal analysis and verification. Thus, we have developed a scheme for automatically translating RTL code into the ACL2 logic, thereby reducing the potential for error in the development of formal hardware models.
Chapter PDF
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Russinoff, D.M. (2007). A Mathematical Approach to RTL Verification. In: Damm, W., Hermanns, H. (eds) Computer Aided Verification. CAV 2007. Lecture Notes in Computer Science, vol 4590. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73368-3_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-73368-3_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73367-6
Online ISBN: 978-3-540-73368-3
eBook Packages: Computer ScienceComputer Science (R0)