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

Abstract

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.

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.