Submitted by Geyciane Santos (geyciane_thamires@hotmail.com) on 2015-07-23T14:25:32Z No. of bitstreams: 1 Dissertação - Renato Barbosa Abreu.pdf: 745859 bytes, checksum: aedacf2a1901d7a7fb83eb1ddb429e77 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-23T15:35:05Z (GMT) No. of bitstreams: 1 Dissertação - Renato Barbosa Abreu.pdf: 745859 bytes, checksum: aedacf2a1901d7a7fb83eb1ddb429e77 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-23T15:38:02Z (GMT) No. of bitstreams: 1 Dissertação - Renato Barbosa Abreu.pdf: 745859 bytes, checksum: aedacf2a1901d7a7fb83eb1ddb429e77 (MD5) / Made available in DSpace on 2015-07-23T15:38:02Z (GMT). No. of bitstreams: 1 Dissertação - Renato Barbosa Abreu.pdf: 745859 bytes, checksum: aedacf2a1901d7a7fb83eb1ddb429e77 (MD5) Previous issue date: 2014-06-17 / Não Informada / Currently, digital filters are employed in a wide variety of signal processing applications, using floating- and fixed-point processors. Regarding the latter, some filter implementations may be prone to errors, due to problems related to finite word-length. In particular, signal processing modules present in such realizations can produce overflows and unwanted noise caused by the quantization and round-off effects, during accumulativeaddition and multiplication operations. The present work addresses this problem and proposes a new methodology to verify digital filters, based on a state-of-the-art bounded model checker called ESBMC, which supports full C/C++ and employs satisfiabilitymodulo- theories solvers. In addition to verifying overflow and limit-cycle occurrences, the present approach can also check design properties, like stability and frequency response, as well as output errors and time constraints, based on discrete-time models implemented in C. The experiments conducted during this work show that the proposed methodology is effective, when finding realistic design errors related to fixed-point implementations of digital filters. It is worth noting that the proposed method, in addition to helping the designer to determine the number of bits for fixedpoint representations, can also aid to define details of filter realization and structure. / Atualmente, os filtros digitais são empregados em uma ampla variedade de aplicações para processamento de sinais, utilizando tanto processadores de ponto flutuante quanto de ponto fixo. No que diz respeito a este último, algumas implementações de filtro podem estar mais propensas a erros, devido a problemas relacionados com a palavra de dados de comprimento finito. Em particular, o processamento de sinais utilizando tais realizações pode produzir o problema de estouro aritmético e ruídos indesejados causados pela quantização e efeitos de arredondamento, durante operações acumulativas de adição e multiplicação. O presente trabalho aborda este problema e propõe uma nova metodologia para a verificação de filtros digitais, com base em um verificador de modelos no estado da arte, chamado ESBMC, que suporta linguagens C/C++ e emprega solucionadores baseados em teoria do módulo da satisfatibilidade. Além de verificar a ocorrência de estouro aritmético e ciclo limite, a presente abordagem também pode verificar propriedades de projeto, como estabilidade e resposta em frequência, bem como restrições temporais e erro de saída, com base em modelos de tempo discreto implementados em C. Os experimentos realizados durante este trabalho mostram que a metodologia proposta é eficaz, pois encontra erros de projeto realistas, que estão relacionados a implementações de filtros digitais em ponto fixo. Vale ressaltar que os resultados apresentados evidenciam que o método proposto, além de auxiliar o projetista a determinar o número de bits da representação de ponto fixo, também pode ajudar a definir detalhes de realização e estrutura de filtro.