Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking
This addresses verification challenges for engineers implementing digital filters in fixed-point arithmetic, though it is incremental as it applies an existing model checker to this specific domain.
The paper tackles the problem of verifying fixed-point digital filters to detect overflows, limit cycles, and time constraints caused by finite word-length effects, using an SMT-based bounded model checker (ESBMC) on C implementations, and shows it can effectively find realistic design errors.
The implementation of digital filters in processors based on fixed-point arithmetic can lead to problems related to the finite word-length. In particular, the processing of signals in such filters can produce overflows and unwanted noise caused by quantization and round off effect during the accumulative addition and multiplication operations. In this paper, we describe a new approach to verify digital filters using an off-the-shelf bounded model checker called ESBMC, which supports full C/C++ and is based on satisfiability modulo theories solvers. In particular, we are able to verify the occurrence of overflows, limit cycles, and time constraints based on a discrete-time model implemented in C. The experiments show that the proposed approach can be used to verify potential problems in fixed-point implementation of digital filters and it can thus be effective in finding realistic design errors.