Abstract
We describe the formal methodology we are using to verify components of a commercial 64-bit, x86-compatible microprocessor design at Centaur Technology. This methodology is based on the ACL2 theorem prover. In this methodology, we mechanically translate the RTL design into a formal HDL for which we have an interpreter in ACL2. We use AIG- and BDD-based symbolic simulation and theorem proving techniques to show that the hardware models satisfy their specifications, which are ACL2 functions. Completed verifications yield theorems admitted by ACL2, ensuring that the verification is based on sound reasoning. We have used this methodology to verify instructions such as SIMD floating-point addition and subtraction, integer and floating-point multiplication, comparisons, bit-wise logical operations, and integer/float conversions. We discuss our floating-point addition verification as a case study.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aagaard MD, Jones RB, Seger CJH (1999) Formal verification using parametric representations of boolean constraints. In: Proceedings of the 36th design automation conference, pp 402–407
Baumgartner J (2006) Integrating FV into main-stream verification: the IBM experience. Tutorial given at FMCAD. Available at http://domino.research.ibm.com/comm/research_projects.nsf/pages/sixthsense.presentations.html
Boyer RS, Hunt WA Jr (2006) Function memoization and unique object representation for ACL2 functions. In: ACL2 ’06: Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications. ACM, New York, NY, pp 81–89
Boyer RS, Hunt WA Jr (2009) Symbolic simulation in ACL2. In: Proceedings of the eighth international workshop on the ACL2 theorem prover and its applications
Brock B, Hunt WA Jr (1991) Report on the formal specification and partial verification of the VIPER microprocessor. In: NASA contractor report, 187540
Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput C-35(8):677–691
Chen Y-A, Bryant RE (1998) Verification of floating-point adders. In: Hu AJ, Vardi MY (eds) Computer aided verification, Lecture notes in computer science, vol 1427. Springer, Heidelberg
Harrison J (2006) Floating-point verification using theorem proving. In: Bernardo M, Cimatti A (eds) Formal methods for hardware verification, Sixth international school on formal methods for the design of computer, communication, and software systems, SFM 2006, Lecture notes in computer science, Bertinoro, Italy, vol 3965. Springer, New York, pp 211–242
Hunt WA Jr (1994) FM8501: a verified microprocessor. Springer, London
Hunt WA Jr, Reeber E (2005) Formalization of the DE2 language. In: Proceedings of the 13th conference on correct hardware design and verification methods (CHARME 2005), pp 20–34
Hunt WA Jr, Swords S (2009a) Centaur technology media unit verification: case study: floating-point addition. In: Computer aided verification, Lecture notes in computer science 5643. Springer, Berlin, pp 353–367
Hunt WA Jr, Swords S (2009b) Use of the E language. In: Martin A, O’Leary J (eds) Hardware design and functional languages ETAPS 2009 Workshop, York, UK
IEEE (2005) IEEE standard (1364-2005) for verilog hardware description language
IEEE Computer Society (2008) IEEE standard for floating-point arithmetic, IEEE std 754TM-2008 edn
Jacobi C, Weber K, Paruthi V, Baumgartner J (2005) Automatic formal verification of fused-multiply-add FPUs. In: Proceedings of design, automation and test in Europe, vol 2, pp 1298–1303
Jones RB (2002) Symbolic simulation methods for industrial formal verification. Kluwer, Dordrecht
Kaivola R, Ghughal R, Narasimhan N, Telfer A, Whittemore J, Pandav S, Slobodová A, Taylor C, Frolov V, Reeber E, Naik A (2009) Replacing testing with formal verification in IntelⓇ CoreTMi7 processor execution engine validation. In: Computer aided verification, Lecture notes in computer science. Springer, Berlin, pp 414–429
Price D (1995) Pentium FDIV flaw – lessons learned. IEEE Micro 15(2):88–87
Russinoff D (2000) A case study in formal verification of register-transfer logic with ACL2: the floating point adder of the AMD Athlon (TM) processor. In: Hunt WA Jr, Johnson SD (eds) Formal methods in computer-aided design, LNCS 1954. Springer, Berlin, pp 22–55
Seger CJH, Jones RB, O’Leary JW, Melham T, Aagaard MD, Barrett C, Syme D (2005) An industrially effective environment for formal hardware verification. IEEE Trans Comput Aided Des Integr Circuits Syst 24(9):1381
Slobodová A (2006) Challenges for formal verification in industrial setting. In: Brim L, Haverkort B, Leucker M, van de Pol J (eds) Formal methods: applications and technology, LNCS 4346. Springer, Berlin, pp 1–22
University of California at Berkeley, Department of Electrical Engineering and Computer Science, Industrial Liaison Program. A compact test suite for P754 arithmetic – version 2.0.
Visser E (2005) A survey of strategies in rule-based program transformation systems. J Symbolic Comput 40:831–873
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer Science+Business Media, LLC
About this chapter
Cite this chapter
Hunt, W.A., Swords, S., Davis, J., Slobodova, A. (2010). Use of Formal Verification at Centaur Technology. In: Hardin, D. (eds) Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer, Boston, MA. https://doi.org/10.1007/978-1-4419-1539-9_3
Download citation
DOI: https://doi.org/10.1007/978-1-4419-1539-9_3
Published:
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-1538-2
Online ISBN: 978-1-4419-1539-9
eBook Packages: EngineeringEngineering (R0)