Details

Autor(en) / Beteiligte

• Cox, Arlen
• Sankaranarayanan, Sriram
• Chang, Bor-Yuh Evan

Titel

A Bit Too Precise? Bounded Verification of Quantized Digital Filters

Ist Teil von

• Tools and Algorithms for the Construction and Analysis of Systems, p.33-47

Ort / Verlag

Berlin, Heidelberg: Springer Berlin Heidelberg

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• Digital filters are simple yet ubiquitous components of a wide variety of digital processing and control systems. Errors in the filters can be catastrophic. 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 empirically evaluate several variants of these two fundamental approaches for verifying fixed-point implementations of digital filters. We design our comparison to reveal 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 using modern satisfiability-modulo-theories (SMT) solvers.