Login | Register

Error analysis of digital filters using HOL theorem proving

Title:

Error analysis of digital filters using HOL theorem proving

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

[img]
Preview
Text (application/pdf)
JAL-2007.pdf - Accepted Version
203kB

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)
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

Downloads per month over past year

Back to top Back to top