Akbarpour, Behzad, Tahar, Sofiène and Dekdouk, Abdelkader (2005) Formalization of FixedPoint Arithmetic in HOL. Formal Methods in System Design, 27 (12). pp. 173200. ISSN 09259856

Text (application/pdf)
338kBFMSD2005.pdf  Accepted Version 
Official URL: http://dx.doi.org/10.1007/s1070300522568
Abstract
This paper addresses the formalization in higherorder logic of fixedpoint arithmetic. We encoded the fixedpoint number system and specified the different quantization modes in fixedpoint arithmetic such as the directed and even quantization 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 quantized result after carrying out basic arithmetic operations, such as 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 floatingpoint to fixedpoint algorithmic level in the signal processing design flow.
Divisions:  Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering 

Item Type:  Article 
Refereed:  Yes 
Authors:  Akbarpour, Behzad and Tahar, Sofiène and Dekdouk, Abdelkader 
Journal or Publication:  Formal Methods in System Design 
Date:  2005 
Digital Object Identifier (DOI):  10.1007/s1070300522568 
Keywords:  fixedpoint arithmetic floatingpoint arithmetic theoremproving HOL 
ID Code:  977379 
Deposited By:  DANIELLE DENNIE 
Deposited On:  14 Jun 2013 15:36 
Last Modified:  18 Jan 2018 17:44 
References:
M.D. Aagaard and C.J.H. Seger, “The formal verification of a pipelined doubleprecision IEEE floatingpoint multiplier,” in Proceedings International Conference on Computer Aided Design, San Jose, California, USA, November 1995, pp. 7–10.G. Barrett, “Formal methods applied to a floating point number system,” IEEE Transactions on Software Engineering, Vol. SE15, No. 5, pp. 611–621, 1989.
C. Berg and C. Jacobi, “Formal Verification of the VAMP Floating Point Unit,” in Correct Hardware Design and Verification Methods, LNCS 2144, SpringerVerlag, 2001, pp. 325–339.
S. Beyer, C. Jacobi, D. Kröning, D. Leinenbach, and W. J. Paul, “Instantiating uninterpreted functional units and memory system: Functional verification of the VAMP,” in Correct Hardware Design and Verification Methods, LNCS 2860, SpringerVerlag, 2003, pp. 51–65.
S. Boldo, M. Daumas, and L. Thèry, “Formal proofs and computations in finite precision arithmetic,” in Proceedings of the 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Rome, Italy, September 2003, pp. 101–111.
S. Boldo and M. Daumas, “Properties of two’s complement floating point notations,” Software Tools for Technology Transfer, Vol. 5, Nos. 2/3, pp. 237–246, 2004.
Cadence Design Systems, Inc., Signal Processing WorkSystem (SPW) User’s Guide, USA, July 1999.
V.A. Carreno, “Interpretation of IEEE854 floatingpoint standard and definition in the HOL system,” NASA TM110189, September 1995.
M. CorneaHasegan, “Proving the IEEE correctness of iterative floatingpoint square root, divide, and remainder algorithms,” Intel Technology Journal, Vol. Q2, pp. 1–11, 1998.
Y.A. Chen and R.E. Bryant, “Verification of floating point adders,” in Computer Aided Verification, LNCS 1427, SpringerVerlag, 1998, pp. 488–499.
M. Daumas, L. Rideau, and L. Thèry, “A generic library for floatingpoint numbers and its application to exact computing,” in Theorem Proving in Higher Order Logics, LNCS 2152, SpringerVerlag, 2001, pp. 169184.
M.J.C. Gordon and T.F. Melham, Introduction to HOL: A Theorem Proving Environment for HigherOrder Logic, Cambridge University Press, 1993.
J.R. Harrison, “Constructing the real numbers in HOL,” Formal Methods in System Design, Vol. 5, Nos. 1/2, pp. 35–59, 1994.
J.R. Harrison, “A machinechecked theory of floatingpoint arithmetic,” in Theorem Proving in Higher Order Logics, LNCS 1690, SpringerVerlag, 1999, pp. 113–130.
J.R. Harrison, “Floatingpoint verification in HOL light: The exponential function,” Formal Methods in System Design, Vol. 16, No. 3, pp. 271–305, 2000.
J.R. Harrison, “Formal verification of floating point trigonometric functions,” in Formal Methods in ComputerAided Design, LNCS 1954, SpringerVerlag, 2000, pp. 217–233.
J.R. Harrison, “Formal verification of IA64 division algorithms,” in Theorem Proving in Higher Order Logics, LNCS 1869, SpringerVerlag, 2000, pp. 234–251.
The Institute of Electrical and Electronic Engineers, Inc., “IEEE, Standard for Binary FloatingPoint Arithmetic,” ANSI/IEEE Standard 754, USA, 1985.
The Institute of Electrical and Electronic Engineers, Inc., “IEEE, Standard for RadixIndependent FloatingPoint Arithmetic,” ANSI/IEEE Std 854, USA, 1987.
R. Kaivola and M.D. Aagaard, “Divider circuit verification with model checking and theorem proving,” in Theorem Proving in Higher Order Logics, LNCS 1869, SpringerVerlag, 2000, pp. 338–355.
R. Kaivola and N. Narasimhan, “Formal verification of the Pentium® 4 floatingpoint multiplier,” in Proceedings Design Automation and Test in Europe Conference, Paris, France, March 2002, pp. 2027.
R. Kaivola and K.R. Kohatsu, “Proof engineering in the large: Formal verification of Pentium® 4 Floatingpoint divider,” Software Tools for Technology Transfer, Vol. 4, No. 3, pp. 323–334, 2003.
H. Keding, M. Willems, M. Coors, and H. Meyr, “FRIDGE: A fixedpoint design and simulation environment,” in Proceedings Design Automation and Test in Europe Conference, Paris, France, February 1998, pp. 429435.
M. Leeser and J. O’Leary, “Verification of a subtractive Radix2 square root algorithm and implementation,” in Proceedings International Conference on Computer Design, Austin, Texas, USA, October 1995, pp. 526531.
Mathworks, Inc., Simulink Reference Manual, USA, 1996.
Mathworks, Inc., FixedPoint Blockset, For Use with Simulink, User’s Guide, USA, 2004.
Mentor Graphics, Inc., DSP Station User’s Manual, USA, 1993.
T.F. Melharn, The HOL pred_sets Library, University of Cambridge, Computer Laboratory, February 1992.
P.S. Miner, “Defining the IEEE854 FloatingPoint Standard in PVS,” NASA TM110167, June 1995.
P.S. Miner and J.F. Leathrum, “Verification of IEEE Compliant Subtractive Division Algorithms,” in Formal Methods in ComputerAided Design, LNCS 1166, SpringerVerlag, 1996, pp. 64–78.
J.S. Moore, T. Lynch, and M. Kaufmann, “A mechanically checked proof of the correctness of the kernel of the AMD5K86 floatingpoint division algorithm,” IEEE Transactions on Computers, Vol. 47, No. 9, pp. 913–926, 1998.
S.M. Mueller and W.J. Paul, Computer Architecture. Complexity and Correctness, SpringerVerlag, 2000.
Open SystemC Initiative, SystemC Language Reference Manual, USA, 2004.
J. O’Leary, X. Zhao, R. Gerth, and C.J.H. Seger, “Formally verifying IEEE compliance of floatingpoint hardware,” Intel Technology Journal, Vol. Q1, pp. 1–14, 1999.
D.M. Russinoff, “A case study in formal verification of registertransfer logic with ACL2: The floatingpoint adder of the AMD athlon processor,” in Formal Methods in ComputerAided Design, LNCS 1954, SpringerVerlag, 2000, pp. 3–36.
J. Sawada and R. Gamboa, “Mechanical verification of a square root algorithm using Taylor’s theorem,” in Formal Methods in ComputerAided Design, LNCS 2517, SpringerVerlag, 2002, pp. 274–291.
Synopsys, Inc., CoCentric TM System Studio User’s Guide, USA, August 2001.
University of Cambridge, “The HOL System Reference,” Computer Laboratory, Cambridge, UK, March 2004.
W. Wong, “Modeling bit vectors in HOL: The word library,” in Higher Order Logic and its Applications, LNCS 780, SpringerVerlag, 1994, pp. 371–384.
Repository Staff Only: item control page