Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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.
C. Berg, C. Jacobi, and D. Kroening. Formal verification of a basic circuits library. In IASTED International Conference on Applied Informatics. ACTA Press, 2001.
Y.-A. Chen and R. E. Bryant. Verification of floating point adders. In CAV’98, volume 1427 of LNCS, 1998.
M. Cornea-Hasegan. Proving the IEEE correctness of iterative floating-point square root, divide, and remainder algorithms. Intel Technology Journal, Q2, 1998.
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.
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.
D. Goldberg. Computer Arithmetic. In [9], 1996.
J. Harrison. A machine checked theory of floating point arithmetic. In TPHOL’ 99, volume 1690 of LNCS. Springer, 1999.
J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, San Mateo, CA, second edition, 1996.
Institute of Electrical and Electronics Engineers. ANSI/IEEE standard 754-1985, IEEE Standard for Binary Floating-Point Arithmetic, 1985.
C. Jacobi. A formally verified theory of IEEE rounding. Unpublished, available at http://www-wjp.cs.uni-sb.de/cj/ieee-lib.ps, 2001.
C. Jacobi and D. Kroening. Proving the correctness of a complete microprocessor. In GI Jahrestagung 2000. Springer, 2000.
D. Kroening. Formal Verification of Pipelined Microprocessors. PhD thesis, Saarland University, Computer Science Department, 2001.
P. S. Miner. Defining the IEEE-854 floating-point standard in PVS. Technical Report TM-110167, NASA Langley Research Center, 1995.
P. S. Miner and J. F. Leathrum. Verification of IEEE compliant subtractive division algorithms. In FMCAD-96, volume 1166 of LNCS, pages 64-, 1996.
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.
S. M. Mueller and W. J. Paul. Computer Architecture. Complexity and Correctness. Springer, 2000.
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.
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.
H. Ruess, N. Shankar, and M. K. Srivas. Modular verification of SRT division. In CAV’96, volume 1102 of LNCS, 1996.
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.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berg, C., Jacobi, C. (2001). Formal Verification of the VAMP Floating Point Unit. In: Margaria, T., Melham, T. (eds) Correct Hardware Design and Verification Methods. CHARME 2001. Lecture Notes in Computer Science, vol 2144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44798-9_26
Download citation
DOI: https://doi.org/10.1007/3-540-44798-9_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42541-0
Online ISBN: 978-3-540-44798-6
eBook Packages: Springer Book Archive