- When a digital filter is realized with floating- and fixed-point arithmetics,
errors and constraints due to finite word length are unavoidable. These error
problems have already been extensively studied using theoretical paper and
pencil proofs and simulation techniques since the late sixties. In this
report, we show how this error analysis can be mechanically performed using
the HOL theorem prover. We first model the ideal real filter specification and
the corresponding floating- and fixed-point implementations as predicates in
higher-order logic. For this, we make use of existing theories in HOL on real,
IEEE standard based floating-point, and fixed-point arithmetics. We use
valuation functions to find the real values of the floating- and fixed-point
filter outputs and define the error as the difference between these values and
the corresponding output of the ideal real specification. Then, we established
fundamental analysis lemmas as our model to derive expressions for the
accumulation of roundoff error in a parametric Lth-order digital
filter, for each of the three canonical forms of realization: direct,
parallel, and cascade. The HOL formalization and proofs are found to be in
good agreement with the theoretical counterparts.
 Download
PDF file (PDF
File) |
| Download
postscript file (PS
File) |
| Send comments
and suggestions to: behzad@ece.concordia.ca |