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)