Use este identificador para citar o ir al link de este elemento:
http://hdl.handle.net/1843/RVMR-6TJRJ6
Tipo: | Dissertação de Mestrado |
Título: | Um núcleo inteligente para processamento distribuído de resolvedores SAT em verificação por equivalências |
Autor(es): | Marcia Carolina Marra de Oliveira |
primer Tutor: | Claudionor Jose Nunes Coelho Junior |
primer miembro del tribunal : | Ricardo dos Santos Ferreira |
Segundo miembro del tribunal: | Antonio Otavio Fernandes |
Tercer miembro del tribunal: | Sergio Vale Aguiar Campos |
Resumen: | Verificação por Equivalência é um dos componentes chave da metodologia de verificação formal atual para sistemas digitais. Ela é técnica de Verificação Formal mais utilizada atualmente pela indústria para verificação de igualdade entre duas descrições de um circuito. Diversas abordagens baseadas BDDs e SAT obtiveram um considerável sucesso nesta área. No entanto a crescente distânciaentre a capacidade dos resolvedores atuais e a complexidade das instâncias a serem verificadas motivam a exploração de novas alternativas, em busca de soluções melhores. Esta dissertação apresenta um núcleo inteligente para processamento distribuído de resolvedores SAT em Verificação por Equivalência. Especificamente, o núcleo proposto explora o processamento paralelo de resolvedores SAT e propõe uma nova técnica para a identificação de similaridades estruturais entre os circuitos a serem verificados. Ao final, são apresentados resultados que comprovam a eficiência da metodologia proposta. |
Abstract: | Equivalence Checking is one the of the key components in formal verification for digital systems. It is also one of the most widely used approaches in industry for functional equivalence verification of different designs. A number of recently proposed BDD and SAT based approaches have met with considerable success in this area. However, the growing gap between the current solvers capabilities and the increasing complexity in digital designs lead to exploring alternative, better solutions. This work proposes an intelligent kernel for distributed processing of SAT solvers in Equivalence Checking. Specifically, the proposed kernel exploits a new technique for identifying structural similarities between the circuits. Finally, results of verification using the proposed methodology are presented. |
Asunto: | Circuitos eletronicos Projetos Processamento de dados Computação Circuitos integrados Verificação Processamento eletrônico de dados Processamento distribuído |
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-6TJRJ6 |
Fecha del documento: | 27-jun-2006 |
Aparece en las colecciones: | Dissertações de Mestrado |
archivos asociados a este elemento:
archivo | Descripción | Tamaño | Formato | |
---|---|---|---|---|
marciacarolinamarraoliveira.pdf | 554.23 kB | 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.