FenixEdu™

Dissertação

SoC-FPGA Accelerated BDD-Based Model Checking EVALUATED

Detalhes: Verificação de Modelos é considerada uma das ferramentas mais importantes em verificação formal, geralmente usada para verificar requerimentos de hardware e software. Uma das mais importantes descobertas em verificação de modelos foi o uso de Diagramas de Decisão Binária (Binary Decision Diagrams) para melhorar significativamente o tempo de execução e permitir abordar problemas maiores. Devido ao problema fundamental associado a sistemas que exploram espaços de estados, Verificadores de Modelos são considerados demasiado dispendiosos em relação ao tempo gasto para serem amplamente utilizados. Neste trabalho, propomos uma arquitetura HW/SW que usa um dispositivo SoC-FPGA para melhorar o tempo de execução de Verificador de Modelos baseados em BDD. Desenvolvemos uma arquitetura base e duas modificações para um total de quatro arquiteturas diferentes. O resultado final chega perto, mas não melhora as implementações de software em termos de performance relativa.
Keywords: Verificação de Modelos, Diagramas de Decisão Binária, SoC-FPGA, Sistema Hardware/Software

Discussão: janeiro 26, 2021, 16:30