@MASTERSTHESIS{ 2014:817897136,
 	title = {Avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidade},
 	year = {2014},
 	url = "http://tede.ufam.edu.br/handle/tede/4495",
 	abstract = "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.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de Pós-graduação em Engenharia Elétrica},
 	note = {Faculdade de Tecnologia}
}