Digital filters are simple yet ubiquitous components of a wide vari ety of digital processing and control systems. Errors in the filters can be catas trophic. Traditionally digital filters have been verified using methods from control theory and extensive testing. We study two alternative verification techniques: bit precise analysis and real-valued error approximations. In this paper, we empiri cally evaluate several variants of these two fundamental approaches for verifying fixed-point implementations of digital filters. We design our comparison to re veal the best possible approach towards verifying real-world designs of infinite impulse response (IIR) digital filters. Our study reveals broader insights into cases where bit-reasoning is absolutely necessary and suggests efficient approaches us ing modern satisfiability-modulo-theories (SMT) solvers.
展开▼
