Abstract
This paper addresses the formalization in higher-order logic of fixed-point arithmetic based on the SPW (Signal Processing WorkSystem) tool. We encoded the fixed-point number system and specified the different rounding modes in fixed-point arithmetic such as the directed and even rounding modes. We also considered the formalization of exceptions detection and their handling like overflow and invalid operation. An error analysis is then performed to check the correctness of the rounding and to verify the basic arithmetic operations, addition, subtraction, multiplication and division against their mathematical counterparts. Finally, we showed by an example how this formalization can be used to enable the verification of the transition from the floating-point to fixed-point algorithmic levels in the design flow of signal processors.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
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.
G. Barrett, “Formal Methods Applied to a Floating Point Number System”, IEEE Transactions on Software Engineering, SE-15(5): 611–621, May 1989.
C. Berg and C. Jacobi, “Formal Verification of the VAMP Floating Point Unit”, Proc. 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2001:325–339.
V. A. Carreno, “Interpretation of IEEE-854 Floating-Point Standard and Definition in the HOL System”, NASA Technical Memorandum 110189, September 1995.
M. Cornea-Hasegan, “Proving the IEEE Correctness of Iterative Floating-Point Square Root, Divide, and Remainder Algorithms”, Intel Technology Journal, Q2, 1998.
Y.-A. Chen and R. E. Bryant, “Verification of Floating Point Adders”, In CAV’98, Volume 1427 of LNCS, 1998.
M. Daumas, L. Rideau, L. Théry, “A Generic Library for Floating-Point Numbers and Its Application to Exact Computing”, Proc. TPHOLs’2001:169–184, November 2001.
M. J. Gordon and T. F. Melham, “Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic.” Cambridge University Press, 1993.
J. R. Harrison, “Theorem Proving with the Real Numbers”, Technical Report Number 408, University of Cambridge Computer Laboratory, December 1996.
J. R. Harrison, “Floating-Point Verification in HOL Light: The Exponential Function”, Technical Report Number 28, University of Cambridge Computer Laboratory. UK, June 1997.
J. R. Harrison, “A Machine-Checked Theory of Floating-Point Arithmetic”, Proc. TPHOLs’99, August 1999.
G. Huet, G. Kahn, and C. Paulin-Mohring, “The Coq Proof Assistant: A Tutorial: Version 6.1” Technical Report 204, INRIA, 1997.
IEEE, “IEEE Standard for Binary Floating-Point Arithmetic”, 1985. ANSI/IEEE Std 754-1985.
IEEE, “IEEE Standard for Radix-Independent Floating-Point Arithmetic”, 1987. ANSI/IEEE Std 854-1987.
M. Leeser, and J. O’Leary, “Verification of a Subtractive Radix-2 Square Root Algorithm and Implementation”, Proc. ICCD’95, October 1995.
J. O’Leary, X. Zhao, R. Gerth, and C. H. Seger, “Formally Verifying IEEE Compliance of Floating-Point Hardware”, Intel Technology Journal, 1999.
P. S. Miner, and J. F. Leathrum, “Verification of IEEE Compliant Subtractive Division Algorithms”, In FMCAD-96, Volume 1166 of LNCS, pages 64-, November 1996.
P.S. Miner, “Defining the IEEE-854 Floating-Point Standard in PVS”, Technical Memorandum 110167, NASA, Langley Research Center, Hampton, VA 236810001, USA, June 1995.
J. S. 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.
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 Proceedings of FMCAD-00, volume 1954 of LNCS. Springer, 2000.
“Signal Processing WorkSystem (SPW) User’s Guide”, Cadence Design Systems, Inc., July 1999.
W. Wong, “The HOL word Library”, University of Cambridge, Computer Laboratory, May 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Akbarpour, B., Dekdouk, A., Tahar, S. (2002). Formalization of Cadence SPW Fixed-Point Arithmetic in HOL. In: Butler, M., Petre, L., Sere, K. (eds) Integrated Formal Methods. IFM 2002. Lecture Notes in Computer Science, vol 2335. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47884-1_11
Download citation
DOI: https://doi.org/10.1007/3-540-47884-1_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43703-1
Online ISBN: 978-3-540-47884-3
eBook Packages: Springer Book Archive