Exportar este item: EndNote BibTex

Use este identificador para citar ou linkar para este item: http://tede.ufam.edu.br/handle/tede/4495
Tipo do documento: Dissertação
Título: Avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidade
Autor: Abreu, Renato Barbosa 
Primeiro orientador: Cordeiro, Lucas Carvalho
Resumo: 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.
Abstract: 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.
Palavras-chave: Implementação de filtros digitais
Processamento de sinais - Estouro aritmético
Processamento de sinais - Ruídos indesejados
ESBMC
Teoria do módulo da satisfatibilidade
Model checking
Área(s) do CNPq: ENGENHARIAS: ENGENHARIA ELÉTRICA
Idioma: por
País: Brasil
Instituição: Universidade Federal do Amazonas
Sigla da instituição: UFAM
Departamento: Faculdade de Tecnologia
Programa: Programa de Pós-Graduação em Engenharia Elétrica
Citação: ABREU, Renato Barbosa. Avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidade. 2014. 63 f. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Manaus, 2014.
Tipo de acesso: Acesso Aberto
URI: http://tede.ufam.edu.br/handle/tede/4495
Data de defesa: 17-Jun-2014
Aparece nas coleções:Mestrado em Engenharia Elétrica

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
Dissertação - Renato Barbosa Abreu.pdfDissertação - Renato Barbosa Abreu728,38 kBAdobe PDFThumbnail

Baixar/Abrir Pré-Visualizar


Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.