Proof Engineering in the Large: Formal Verification of Pentium®4 Floating-Point Divider

  • Roope Kaivola
  • Katherine Kohatsu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


We examine the challenges presented by large-scale formal verification of industrial-size circuits, based on our experiences in verifying the class of all micro-operations executing on the floating-point division and square root unit of the Intel IA-32 Pentium®4 microprocessor. The verification methodology is based on combining human-guided mechanised theorem-proving with low-level steps verified by fully automated model-checking. A key observation in the work is the need to explicitly address the issues of proof design and proof engineering, i.e. the process of creating proofs and the craft of structuring and formulating them, as concerns on their own right.


Model Check Theorem Prove Single Instruction Multiple Data Division Algorithm Divider Circuit 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    M. D. Aagaard, R. B. Jones, T. F. Melhan, J. W. O’Leary, and C.-J. H. Seger. A methodology for large-scale hardware verification. In FMCAD, volume 1954 of LNCS, pages 263–282. Springer, 2000.Google Scholar
  2. 2.
    M. D. Aagaard, R. B. Jones, and C.-J. H. Seger. Lifted-fl: A pragmatic implementation of combined model checking and theorem proving. In TPHOLs. Springer, 1999.Google Scholar
  3. 3.
    M. D. Aagaard, T. F. Melham, and J. W. O’Leary. Xs are for trajectory evaluation, Booleans are for theorem proving. In CHARME. Springer, 1999.Google Scholar
  4. 4.
    C.-T. Chou. The mathematical foundation of symbolic trajectory evaluation. In CAV. Springer, 1999.Google Scholar
  5. 5.
    P. Curzon. The importance of proof maintenance and reengineering. In J. Alves-Foss, editor, HOL-95: B-track Proceedings, pages 17–31, Sept. 1995.Google Scholar
  6. 6.
    M. D. Ercegovac and T. Lang. Division and Square Root, Digit-Recurrence Algorithms and Implementations. Kluwer Academic, 1994.Google Scholar
  7. 7.
    D. Gries. The Science of Programming. Springer-Verlag, 1981.Google Scholar
  8. 8.
    I. Hayes. Applying formal verification to software development in industry. In I. Hayes, editor, Specification case studies, pages 285–310. Prentice-Hall, 1987.Google Scholar
  9. 9.
    S. Hazelhurst and C.-J. H. Seger. Symbolic trajectory evaluation. In T. Kropf, editor, Formal Hardware Verification, chapter 1, pages 3–78. Springer Verlag; New York, 1997.Google Scholar
  10. 10.
    Hinton, G., Sager, D., Upton, M., Boggs, D., Carmean, D, Kyker, A. and Roussel, P. The microarchitecture of the Pentium 4 processor. Intel Technology Journal, Q1, Feb. 2001.Google Scholar
  11. 11.
    IEEE. IEEE Standard for binary floating-point arithmetic. ANSI/IEEE Std 754-1985, 1985.Google Scholar
  12. 12.
    M. Jones and G. Gopalakrishnan. A PCI formalization and refinement. In TPHOLs 2000, Supplemental Proceedings, OGI Technical Report CSE 00-090, pages 115–124, 2000.Google Scholar
  13. 13.
    R. Kaivola and M. D. Aagaard. Divider circuit verification with model checking and theorem proving. In TPHOLs, volume 1869 of LNCS, pages 338–355. Springer, 2000.Google Scholar
  14. 14.
    R. Kaivola and N. Narasimhan. Multiplier verification with symbolic simulation and theorem proving. Submitted for publication, 2001.Google Scholar
  15. 15.
    A. Mokkedem and T. Leonard. Formal verification of the Alpha 21364 network protocol. In TPHOLs, volume 1869 of LNCS, pages 443–461. Springer, 2000.Google Scholar
  16. 16.
    L. Paulson. ML for the Working Programmer., Cambridge University Press, 1996.Google Scholar
  17. 17.
    D. M. Russinoff. A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. London Mathematical Society Journal of Computational Mathematics, 1:148–200, 1998.zbMATHMathSciNetGoogle Scholar
  18. 18.
    C.-J. H. Seger and R. E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6(2): 147–189, Mar. 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Roope Kaivola
    • 1
  • Katherine Kohatsu
    • 1
  1. 1.Intel CorporationHillsboroUSA

Personalised recommendations