Akbarpour, Behzad and Tahar, Sofiène (2007) Error analysis of digital filters using HOL theorem proving. Journal of Applied Logic, 5 (4). pp. 651-666. ISSN 15708683
Preview |
Text (application/pdf)
203kBJAL-2007.pdf - Accepted Version |
Official URL: http://dx.doi.org/10.1016/j.jal.2006.11.001
Abstract
When a digital filter is realized with floating-point or fixed-point arithmetics, errors and constraints due to finite word length are unavoidable. In this paper, we show how these errors can be mechanically analysed using the HOL theorem prover. We first model the ideal real filter specification and the corresponding floating-point and fixed-point implementations as predicates in higher-order logic. We use valuation functions to find the real values of the floating-point and fixed-point filter outputs and define the error as the difference between these values and the corresponding output of the ideal real specification. Fundamental analysis lemmas have been established to derive expressions for the accumulation of roundoff error in parametric Lth-order digital filters, for each of the three canonical forms of realization: direct, parallel, and cascade. The HOL formalization and proofs are found to be in a good agreement with existing theoretical paper-and-pencil counterparts.
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 |
Journal or Publication: | Journal of Applied Logic |
Date: | 2007 |
Digital Object Identifier (DOI): | 10.1016/j.jal.2006.11.001 |
Keywords: | Error analysis; Digital filters; Theorem proving; Fixed-point; Floating-point; HOL |
ID Code: | 977373 |
Deposited By: | Danielle Dennie |
Deposited On: | 14 Jun 2013 15:01 |
Last Modified: | 18 Jan 2018 17:44 |
References:
B. Akbarpour, Modeling and verification of DSP designs in HOL, Ph.D. Thesis, Concordia University, Department of Electrical and Computer Engineering, Montreal, QC, Canada, March 2005[2]
B. Akbarpour, S. Tahar, A. Dekdouk Formalization of fixed-point arithmetic in HOL Formal Methods in System Design, 27 (1/2) (2005), pp. 173–200
[3]
Cadence Design Systems, Inc., Signal Processing WorkSystem (SPW) User's Guide, USA, July 1999
[4]
G. Forsythe, C.B. Moler Computer Solution of Linear Algebraic Systems Prentice-Hall (1967)
[5]
M.J.C. Gordon, T.F. Melham Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic Cambridge University Press (1993)
[6]
B. Gold, C. M. Radar, Effects of quantization noise in digital filters, in: Proceedings AFIPS Spring Joint Computer Conference, vol. 28, 1966, pp. 213–219
[7]
J.R. Harrison Constructing the real numbers in HOL Formal Methods in System Design, 5 (1/2) (1994), pp. 35–59
[8]
J.R. Harrison A machine-checked theory of floating-point arithmetic Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 1690, Springer-Verlag (1999), pp. 113–130
[9]
J.R. Harrison Floating-point verification in HOL Light: The exponential function Formal Methods in System Design, 16 (3) (2000), pp. 271–305
[10]
J.R. Harrison, L. Théry A skeptic's approach to combining HOL and Maple Journal of Automated Reasoning, 21 (1998), pp. 279–294
[11]
M. Huhn, K. Schneider, T. Kropf, G. Logothetis, Verifying imprecisely working arithmetic circuits, in: Proceedings Design Automation and Test in Europe Conference, March 1999, pp. 65–69
[12]
L.B. Jackson Roundoff-noise analysis for fixed-point digital filters realized in cascade or parallel form IEEE Transactions on Audio and Electroacoustics, AU-18 (June 1970), pp. 107–122
[13]
J.F. Kaiser Digital filters F.F. Kuo, J.F. Kaiser (Eds.), System Analysis by Digital ComputerWiley (1966), pp. 218–285
[14]
J.B. Knowles, R. Edwards Effects of a finite-word-length computer in a sampled-data feedback system IEE Proceedings, 112 (June 1965), pp. 1197–1207
[15]
B. Liu, T. Kaneko Error analysis of digital filters realized with floating-point arithmetic Proceedings of the IEEE, 57 (October 1969), pp. 1735–1747
[16]
Mathworks, Inc., Simulink Reference Manual, USA, 1996
[17]
A.V. Oppenheim, C.J. Weinstein Effects of finite register length in digital filtering and the fast Fourier transform Proceedings of the IEEE, 60 (8) (August 1972), pp. 957–976
[18]
A.V. Oppenheim, R.W. Schafer Discrete-Time Signal Processing
Prentice-Hall (1989)
[19]
I.W. Sandberg Floating-point-roundoff accumulation in Digital filter realization The Bell System Technical Journal, 46 (October 1967), pp. 1775–1791
[20]
Synopsys, Inc., CoCentricTM System Studio User's Guide, USA, August 2001
[21]
C. Weinstein, A.V. Oppenheim A comparison of roundoff noise in floating point and fixed point digital filter realizations Proceedings of the IEEE (Proceedings Letters), 57 (June 1969), pp. 1181–1183
[22]
H. Keding, M. Willems, M. Coors, H. Meyr, FRIDGE: A fixed-point design and simulation environment, in: Proceedings Design Automation and Test in Europe Conference, February 1998, pp. 429–435
[23]
J.H. Wilkinson Rounding Errors in Algebraic Processes
Prentice-Hall (1963)
Repository Staff Only: item control page