Formal Verification of the VAMP Floating Point Unit

  • Christoph Berg
  • Christian Jacobi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


We report on the formal verification of the floating point unit used in the VAMP processor. The FPU is fully IEEE compliant, and supports denormals and exceptions in hardware. The supported operations are addition, subtraction, multiplication, division, comparison, and conversions. The hardware is verified on the gate level against a formal description of the IEEE standard by means of the theorem pro ver PVS.


Double Precision IEEE Standard Computation Unit Division Algorithm Point Unit 
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 and C.-J. H. Seger. The formal verification of a pipelined double-precision IEEE floating-point multiplier. In ICCAD, pages 7–10. IEEE, Nov. 1995.Google Scholar
  2. 2.
    C. Berg, C. Jacobi, and D. Kroening. Formal verification of a basic circuits library. In IASTED International Conference on Applied Informatics. ACTA Press, 2001.Google Scholar
  3. 3.
    Y.-A. Chen and R. E. Bryant. Verification of floating point adders. In CAV’98, volume 1427 of LNCS, 1998.Google Scholar
  4. 4.
    M. Cornea-Hasegan. Proving the IEEE correctness of iterative floating-point square root, divide, and remainder algorithms. Intel Technology Journal, Q2, 1998.Google Scholar
  5. 5.
    E. M. Clarke, S. M. German, and X. Zhao. Verifying the SRT division algorithm using theorem proving techniques. In CAV’96, volume 1102 of LNCS, 1996.Google Scholar
  6. 6.
    G. Even and W. Paul. On the design of IEEE compliant floating point units. In Proceedings of the 13th Symposium on Computer Arithmetic. IEEE Computer Society Press, 1997.Google Scholar
  7. 7.
    D. Goldberg. Computer Arithmetic. In [9], 1996.Google Scholar
  8. 8.
    J. Harrison. A machine checked theory of floating point arithmetic. In TPHOL’ 99, volume 1690 of LNCS. Springer, 1999.Google Scholar
  9. 9.
    J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, San Mateo, CA, second edition, 1996.zbMATHGoogle Scholar
  10. 10.
    Institute of Electrical and Electronics Engineers. ANSI/IEEE standard 754-1985, IEEE Standard for Binary Floating-Point Arithmetic, 1985.Google Scholar
  11. 11.
    C. Jacobi. A formally verified theory of IEEE rounding. Unpublished, available at, 2001.
  12. 12.
    C. Jacobi and D. Kroening. Proving the correctness of a complete microprocessor. In GI Jahrestagung 2000. Springer, 2000.Google Scholar
  13. 13.
    D. Kroening. Formal Verification of Pipelined Microprocessors. PhD thesis, Saarland University, Computer Science Department, 2001.Google Scholar
  14. 14.
    P. S. Miner. Defining the IEEE-854 floating-point standard in PVS. Technical Report TM-110167, NASA Langley Research Center, 1995.Google Scholar
  15. 15.
    P. S. Miner and J. F. Leathrum. Verification of IEEE compliant subtractive division algorithms. In FMCAD-96, volume 1166 of LNCS, pages 64-, 1996.Google Scholar
  16. 16.
    J Moore, T. Lynch, and M. Kaufmann. A mechanically checked proof of the AMD5K86 floating point division program. IEEE Transactions on Computers, 47(9):913–926, 1998.CrossRefMathSciNetGoogle Scholar
  17. 17.
    S. M. Mueller and W. J. Paul. Computer Architecture. Complexity and Correctness. Springer, 2000.Google Scholar
  18. 18.
    J. O’Leary, X. Zhao, R. Gerth, and C.-J. H. Seger. IA-64 floating point operations and the IEEE standard for binary floating-point arithmetic. Intel Technology Journal, Q4, 1999.Google Scholar
  19. 19.
    S. Owre, N. Shankar, and J. M. Rushby. PVS: A prototype verification system. In CADE 11, volume 607 of LNAI, pages 748–752. Springer, 1992.Google Scholar
  20. 20.
    H. Ruess, N. Shankar, and M. K. Srivas. Modular verification of SRT division. In CAV’96, volume 1102 of LNCS, 1996.Google Scholar
  21. 21.
    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. LMS Journal of Computation and Mathematics, 1:148–200, 1998.zbMATHMathSciNetGoogle Scholar
  22. 22.
    D. M. Russinoff. A mechanically checked proof of correctness of the AMD K5 floating point square root microcode. Formal Methods in System Design, 14(1):75–125, Jan. 1999.Google Scholar
  23. 23.
    D. M. Russinoff. A case study in formal verification of register-transfer logic with ACL2: The floating point adder of the AMD Athlon processor. In FMCAD-00, volume 1954 of LNCS. Springer, 2000.Google Scholar
  24. 24.
    D. Verkest, L. Claesen, and H. De Man. A proof on the nonrestoring division algorithm and its implementation on an ALU. Formal Methods in System Design, 4, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Christoph Berg
    • 1
  • Christian Jacobi
    • 1
  1. 1.Computer Science DepartmentSaarland UniversitySaarbrückenGermany

Personalised recommendations