Akbarpour, Behzad, Tahar, Sofiène and Dekdouk, Abdelkader (2005) Formalization of Fixed-Point Arithmetic in HOL. Formal Methods in System Design, 27 (1-2). pp. 173-200. ISSN 0925-9856
Preview |
Text (application/pdf)
338kBFMSD-2005.pdf - Accepted Version |
Official URL: http://dx.doi.org/10.1007/s10703-005-2256-8
Abstract
This paper addresses the formalization in higher-order logic of fixed-point arithmetic. We encoded the fixed-point number system and specified the different quantization modes in fixed-point 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 floating-point to fixed-point 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/s10703-005-2256-8 |
| Keywords: | fixed-point arithmetic floating-point arithmetic theorem-proving 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 double-precision IEEE floating-point 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. SE-15, 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, Springer-Verlag, 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, Springer-Verlag, 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 IEEE-854 floating-point standard and definition in the HOL system,” NASA TM-110189, September 1995.
M. Cornea-Hasegan, “Proving the IEEE correctness of iterative floating-point 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, Springer-Verlag, 1998, pp. 488–499.
M. Daumas, L. Rideau, and L. Thèry, “A generic library for floating-point numbers and its application to exact computing,” in Theorem Proving in Higher Order Logics, LNCS 2152, Springer-Verlag, 2001, pp. 169-184.
M.J.C. Gordon and T.F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher-Order 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 machine-checked theory of floating-point arithmetic,” in Theorem Proving in Higher Order Logics, LNCS 1690, Springer-Verlag, 1999, pp. 113–130.
J.R. Harrison, “Floating-point 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 Computer-Aided Design, LNCS 1954, Springer-Verlag, 2000, pp. 217–233.
J.R. Harrison, “Formal verification of IA-64 division algorithms,” in Theorem Proving in Higher Order Logics, LNCS 1869, Springer-Verlag, 2000, pp. 234–251.
The Institute of Electrical and Electronic Engineers, Inc., “IEEE, Standard for Binary Floating-Point Arithmetic,” ANSI/IEEE Standard 754, USA, 1985.
The Institute of Electrical and Electronic Engineers, Inc., “IEEE, Standard for Radix-Independent Floating-Point 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, Springer-Verlag, 2000, pp. 338–355.
R. Kaivola and N. Narasimhan, “Formal verification of the Pentium® 4 floating-point multiplier,” in Proceedings Design Automation and Test in Europe Conference, Paris, France, March 2002, pp. 20-27.
R. Kaivola and K.R. Kohatsu, “Proof engineering in the large: Formal verification of Pentium® 4 Floating-point 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 fixed-point design and simulation environment,” in Proceedings Design Automation and Test in Europe Conference, Paris, France, February 1998, pp. 429-435.
M. Leeser and J. O’Leary, “Verification of a subtractive Radix-2 square root algorithm and implementation,” in Proceedings International Conference on Computer Design, Austin, Texas, USA, October 1995, pp. 526-531.
Mathworks, Inc., Simulink Reference Manual, USA, 1996.
Mathworks, Inc., Fixed-Point 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 IEEE-854 Floating-Point Standard in PVS,” NASA TM-110167, June 1995.
P.S. Miner and J.F. Leathrum, “Verification of IEEE Compliant Subtractive Division Algorithms,” in Formal Methods in Computer-Aided Design, LNCS 1166, Springer-Verlag, 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 floating-point 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, Springer-Verlag, 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 floating-point hardware,” Intel Technology Journal, Vol. Q1, pp. 1–14, 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 Formal Methods in Computer-Aided Design, LNCS 1954, Springer-Verlag, 2000, pp. 3–36.
J. Sawada and R. Gamboa, “Mechanical verification of a square root algorithm using Taylor’s theorem,” in Formal Methods in Computer-Aided Design, LNCS 2517, Springer-Verlag, 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, Springer-Verlag, 1994, pp. 371–384.
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.
Repository Staff Only: item control page
Download Statistics
Download Statistics