Use of Formal Verification at Centaur Technology

  • Warren A. HuntJr.
  • Sol Swords
  • Jared Davis
  • Anna Slobodova
Chapter

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.

Keywords

Europe Hunt Veri 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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–407Google Scholar
  2. 2.
    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
  3. 3.
    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–89CrossRefGoogle Scholar
  4. 4.
    Boyer RS, Hunt WA Jr (2009) Symbolic simulation in ACL2. In: Proceedings of the eighth international workshop on the ACL2 theorem prover and its applicationsGoogle Scholar
  5. 5.
    Brock B, Hunt WA Jr (1991) Report on the formal specification and partial verification of the VIPER microprocessor. In: NASA contractor report, 187540Google Scholar
  6. 6.
    Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput C-35(8):677–691CrossRefGoogle Scholar
  7. 7.
    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, HeidelbergGoogle Scholar
  8. 8.
    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–242Google Scholar
  9. 9.
    Hunt WA Jr (1994) FM8501: a verified microprocessor. Springer, LondonMATHGoogle Scholar
  10. 10.
    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–34Google Scholar
  11. 11.
    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–367Google Scholar
  12. 12.
    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, UKGoogle Scholar
  13. 13.
    IEEE (2005) IEEE standard (1364-2005) for verilog hardware description languageGoogle Scholar
  14. 14.
    IEEE Computer Society (2008) IEEE standard for floating-point arithmetic, IEEE std 754TM-2008 ednGoogle Scholar
  15. 15.
    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–1303CrossRefGoogle Scholar
  16. 16.
    Jones RB (2002) Symbolic simulation methods for industrial formal verification. Kluwer, DordrechtGoogle Scholar
  17. 17.
    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–429Google Scholar
  18. 18.
    Price D (1995) Pentium FDIV flaw – lessons learned. IEEE Micro 15(2):88–87CrossRefGoogle Scholar
  19. 19.
    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–55CrossRefGoogle Scholar
  20. 20.
    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):1381CrossRefGoogle Scholar
  21. 21.
    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–22Google Scholar
  22. 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.Google Scholar
  23. 23.
    Visser E (2005) A survey of strategies in rule-based program transformation systems. J Symbolic Comput 40:831–873MATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2010

Authors and Affiliations

  • Warren A. HuntJr.
    • 1
    • 2
  • Sol Swords
  • Jared Davis
  • Anna Slobodova
  1. 1.Centaur TechnologyAustinUSA
  2. 2.University of Texas at AustinAustinUSA

Personalised recommendations