Avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidade
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 p...
| Autor principal: | Abreu, Renato Barbosa |
|---|---|
| Outros Autores: | http://lattes.cnpq.br/3090810159736491 |
| Grau: | Dissertação |
| Idioma: | por |
| Publicado em: |
Universidade Federal do Amazonas
2015
|
| Assuntos: | |
| Acesso em linha: |
http://tede.ufam.edu.br/handle/tede/4495 |
| id |
oai:https:--tede.ufam.edu.br-handle-:tede-4495 |
|---|---|
| recordtype |
dspace |
| spelling |
oai:https:--tede.ufam.edu.br-handle-:tede-44952016-05-02T14:15:43Z Avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidade Abreu, Renato Barbosa Cordeiro, Lucas Carvalho http://lattes.cnpq.br/3090810159736491 http://lattes.cnpq.br/5005832876603012 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 ENGENHARIAS: ENGENHARIA ELÉTRICA 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. 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. Não Informada 2015-07-23T15:38:02Z 2014-06-17 Dissertaçã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. http://tede.ufam.edu.br/handle/tede/4495 por Acesso Aberto application/pdf Universidade Federal do Amazonas Faculdade de Tecnologia Brasil UFAM Programa de Pós-graduação em Engenharia Elétrica |
| institution |
TEDE - Universidade Federal do Amazonas |
| collection |
TEDE-UFAM |
| language |
por |
| topic |
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 ENGENHARIAS: ENGENHARIA ELÉTRICA |
| spellingShingle |
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 ENGENHARIAS: ENGENHARIA ELÉTRICA Abreu, Renato Barbosa Avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidade |
| topic_facet |
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 ENGENHARIAS: ENGENHARIA ELÉTRICA |
| description |
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. |
| author_additional |
Cordeiro, Lucas Carvalho |
| author_additionalStr |
Cordeiro, Lucas Carvalho |
| format |
Dissertação |
| author |
Abreu, Renato Barbosa |
| author2 |
http://lattes.cnpq.br/3090810159736491 |
| author2Str |
http://lattes.cnpq.br/3090810159736491 |
| title |
Avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidade |
| title_short |
Avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidade |
| title_full |
Avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidade |
| title_fullStr |
Avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidade |
| title_full_unstemmed |
Avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidade |
| title_sort |
avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidade |
| publisher |
Universidade Federal do Amazonas |
| publishDate |
2015 |
| url |
http://tede.ufam.edu.br/handle/tede/4495 |
| _version_ |
1831969292979011584 |
| score |
11.753735 |