Use este identificador para citar o ir al link de este elemento:
http://hdl.handle.net/1843/RVMR-8PHG73
Tipo: | Tese de Doutorado |
Título: | Um modelo estatístico multivariado para prever o comportamento de heurísticas em verificação formal |
Autor(es): | Georgia Penido Safe |
primer Tutor: | Claudionor Jose Nunes Coelho Junior |
primer miembro del tribunal : | Antonio Otavio Fernandes |
Segundo miembro del tribunal: | Sergio Vale Aguiar Campos |
Tercer miembro del tribunal: | Ivan Saraiva Silva |
Cuarto miembro del tribunal: | Ricardo Augusto da Luz Reis |
Resumen: | 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. |
Asunto: | Computação Programação paralela (Computação) |
Idioma: | Português |
Editor: | Universidade Federal de Minas Gerais |
Sigla da Institución: | UFMG |
Tipo de acceso: | Acesso Aberto |
URI: | http://hdl.handle.net/1843/RVMR-8PHG73 |
Fecha del documento: | 2-dic-2011 |
Aparece en las colecciones: | Teses de Doutorado |
archivos asociados a este elemento:
archivo | Descripción | Tamaño | Formato | |
---|---|---|---|---|
georgiapenidosafe.pdf | 2.79 MB | Adobe PDF | Visualizar/Abrir |
Los elementos en el repositorio están protegidos por copyright, con todos los derechos reservados, salvo cuando es indicado lo contrario.