Verificação de Propriedades de Filtros Digitais Implementados com Aritmética de Ponto Fixo

Mauro L. de Freitas, Mikhail Y. R. Gadelha, Lucas Cordeiro, Waldir S. S. Júnior, Eddie B. L. Filho

DOI: 10.14209/sbrt.2013.161

Evento: XXXI Simpósio Brasileiro de Telecomunicações (SBrT2013)

Keywords: ESBMC Model checking Digital Filters Frequency Response overflow

Abstract

In the digital signal processing area, one of the most important tasks is the digital filter design. Currently, this procedure is performed with the aid of computational tools, which generally assume filter coefficients represented with floating-point arithmetic. However, during the implementation phase, which is often done in digital signal processors or field programmable gate arrays, the representation of the obtained coefficients can be carried out through integer or fixed-point arithmetic, which often results in unexpected behavior or even unstable filters. The present work addresses this issue and proposes an evaluation methodology based on the efficient SMT-based context-bounded model checker approach [2], [3], in order to analyze if the number of bits used in the coefficients representation will result in a filter with the same features specified in the design phase. Simulations show that errors regarding frequency response and overflow are likely to be identified with the proposed methodology, which provides greater reliability to the project.

Download