Um modelo estatístico multivariado para prever o comportamento de heurísticas em verificação formal
Carregando...
Arquivos
Data
Autor(es)
Título da Revista
ISSN da Revista
Título de Volume
Editor
Universidade Federal de Minas Gerais
Descrição
Tipo
Tese de doutorado
Título alternativo
Primeiro orientador
Membros da banca
Antonio Otavio Fernandes
Sergio Vale Aguiar Campos
Ivan Saraiva Silva
Ricardo Augusto da Luz Reis
Sergio Vale Aguiar Campos
Ivan Saraiva Silva
Ricardo Augusto da Luz Reis
Resumo
Verificação funcional é o principal gargalo na produtividade de empresas desenvolvedoras de chips. Como a verificação funcional é um problema NP-completo, ela depende de um grande número de heurísticas e seus parâmetros (resolvedores). Normalmente o número de resolvedores disponíveis excede em muito o poder de processamento disponível. Com o advento da programação paralela, a verificação funcional pode ser otimizada através da seleção dos n melhores resolvedores para rodar em paralelo, aumentando assim a chance de se alcançar o término da verificação. Este trabalho apresenta um modelo estatístico baseado em métricas estruturais para construir estimadores de tempo para os resolvedores, permitindo então a seleção dos melhores resolvedores. Esta metodologia considera tanto o tempo de execução estimado dos resolvedores quanto a correlação entre os mesmos. Resultados confirmaram que a metodologia pode ser um mecanismo muito rápido e eficaz para a seleção dos melhores resolvedores.
Abstract
Functional verification is the major design-phase bottleneck for silicon productivity. Since functional verification is an NP-complete problem, it relies on a large number of heuristics with associated parameters (engines). With the advent of parallel processing, formal verification can be optimized by selecting the best n engines to run in parallel, increasing the chance of reaching verification successful termination. In this work, we present an statistical model to build engine estimators based on structural metrics and to select n engines to run in parallel. The methodology considers both engines' estimated performance and engines' correlation. Results confirmed that the methodology can be a very quick selection mechanism for parallelization of engines in order to increase the chance of running the best engines to solve the problem.
Assunto
Computação, Programação paralela (Computação)
Palavras-chave
Ciência da Computação