Repositório Digital

A- A A+

Verificador temporal de propriedades em tempo de execução implementado em VHDL

.

Verificador temporal de propriedades em tempo de execução implementado em VHDL

Mostrar registro completo

Estatísticas

Título Verificador temporal de propriedades em tempo de execução implementado em VHDL
Outro título Temporal checker of properties in execution time implemented in VHDL
Autor Wilges, Peterson
Orientador Ribas, Renato Perez
Co-orientador Braun, Axel
Data 2014
Nível Graduação
Instituição Universidade Federal do Rio Grande do Sul. Instituto de Informática. Curso de Ciência da Computação: Ênfase em Engenharia da Computação: Bacharelado.
Assunto Microeletronica
Vhdl
[en] Fault detection
[en] Formal verification
[en] Reliability
[en] Safety
Resumo A verificação de projetos digitais é essencial para garantir o correto funcionamento e aumentar a confiabilidade de um sistema. Este trabalho visa fazer a verificação de sistemas reativos através de propriedades formais usando lógica temporal linear finita (FLTL) a fim de aumentar a confiabilidade de circuitos. Muitas técnicas têm sido desenvolvidas para a verificação em tempo de execução. A proposta deste trabalho é o desenvolvimento de um circuito verificador para checar a validade propriedades temporais de sistemas através da análise de sinais Booleanos. Neste sentido, um compilador será desenvolvido em linguagem C++ para criar instruções que possam ser interpretadas em um circuito verificador que será desenvolvido em VHDL. Tais instruções devem ser gravadas na memória RAM do FPGA que será o alvo para o desenvolvimento do circuito verificador HDL. O verificador será rápido o suficiente para checar as propriedades temporais de um dispositivo no exato ciclo de relógio especificado pela fórmula FLTL.
Abstract Verification of digital designs is essential to ensure the correctness and to improve the reliability of systems. The checker developed makes the verification of reactive systems through formal properties using finite linear temporal logic (FLTL) in order to increase the circuits' reliability. Many techniques have been proposed in order to make verification in execution time. This approach is to make verification in VHDL to check the validity of temporal properties of systems by analyzing Booleans signals. In this way, a compiler will be developed using C++ to create instructions to be interpreted in a HDL checker circuit. This instructions should be stored in the RAM memory of the FPGA used as target architecture for our HDL developed. The checker will be fast enough to check the temporal properties of the device in the exact clock cycle specified by the FLTL formula.
Tipo Trabalho de conclusão de graduação
URI http://hdl.handle.net/10183/110748
Arquivos Descrição Formato
000952911.pdf (1.203Mb) Texto completo Adobe PDF Visualizar/abrir

Este item está licenciado na Creative Commons License

Este item aparece na(s) seguinte(s) coleção(ões)


Mostrar registro completo

Percorrer



  • O autor é titular dos direitos autorais dos documentos disponíveis neste repositório e é vedada, nos termos da lei, a comercialização de qualquer espécie sem sua autorização prévia.
    Projeto gráfico elaborado pelo Caixola - Clube de Criação Fabico/UFRGS Powered by DSpace software, Version 1.8.1.