Please use this identifier to cite or link to this item:
http://hdl.handle.net/1843/RVMR-6TJRJ6
Type: | Dissertação de Mestrado |
Title: | Um núcleo inteligente para processamento distribuído de resolvedores SAT em verificação por equivalências |
Authors: | Marcia Carolina Marra de Oliveira |
First Advisor: | Claudionor Jose Nunes Coelho Junior |
First Referee: | Ricardo dos Santos Ferreira |
Second Referee: | Antonio Otavio Fernandes |
Third Referee: | Sergio Vale Aguiar Campos |
Abstract: | 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. |
Subject: | Circuitos eletronicos Projetos Processamento de dados Computação Circuitos integrados Verificação Processamento eletrônico de dados Processamento distribuído |
language: | Português |
Publisher: | Universidade Federal de Minas Gerais |
Publisher Initials: | UFMG |
Rights: | Acesso Aberto |
URI: | http://hdl.handle.net/1843/RVMR-6TJRJ6 |
Issue Date: | 27-Jun-2006 |
Appears in Collections: | Dissertações de Mestrado |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
marciacarolinamarraoliveira.pdf | 554.23 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.