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. / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:bibliotecadigital.ufmg.br:MTD2BR-RVMR-8PHG73 |
| Date | 02 December 2011 |
| Creators | Georgia Penido Safe |
| Contributors | Claudionor Jose Nunes Coelho Junior, Antonio Otavio Fernandes, Sergio Vale Aguiar Campos, Ivan Saraiva Silva, Ricardo Augusto da Luz Reis |
| Publisher | Universidade Federal de Minas Gerais, 32001010004P6 - CIÊNCIA DA COMPUTAÇÃO, UFMG, BR |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Format | text/html |
| Source | reponame:Biblioteca Digital de Teses e Dissertações da UFMG, instname:Universidade Federal de Minas Gerais, instacron:UFMG |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0237 seconds