Please use this identifier to cite or link to this item:
http://hdl.handle.net/1843/RVMR-7AAPAR
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.advisor1 | Claudionor Jose Nunes Coelho Junior | pt_BR |
dc.contributor.referee1 | Luis Humberto Rezende Barbosa | pt_BR |
dc.contributor.referee2 | Diogenes Cecilio da Silva Junior | pt_BR |
dc.contributor.referee3 | Antonio Otavio Fernandes | pt_BR |
dc.creator | Thiago Radicchi Roque | pt_BR |
dc.date.accessioned | 2019-08-14T20:58:02Z | - |
dc.date.available | 2019-08-14T20:58:02Z | - |
dc.date.issued | 2007-04-27 | pt_BR |
dc.identifier.uri | http://hdl.handle.net/1843/RVMR-7AAPAR | - |
dc.description.abstract | Equivalence checking (EQ) is a very common formal verification method used in the semiconductor industry. It makes possible to verify if two different implementation of the same design have the same functional behavior which is very useful to make sure that the design still behaves correctly after optimizations (likeretiming) or synthesis. Several known methods are used efficiently, involving techniques like BDDs and SAT. However, the increasing complexity of digital designs turns EQ into a harder problem, motivating the research for new alternatives in this field. This work proposes a equivalence checking tool, based on the following points: design partitioning by width, a parallel SAT solver, and SAT conflict clause learning by applying induction when unrolling sequential circuits. We aim to solve bigger problems faster than the existing solutions in some cases. | pt_BR |
dc.description.resumo | Verificação de equivalência de sistemas digitais é uma técnica amplamente usada atualmente na indústria de fabricação e projeto de circuitos integrados. Ela permite verificar se duas implementações diferentes de uma mesma funcionalidade possuem comportamento idêntico, como por exemplo, uma versão original esua contraparte otimizada por alguma metodologia conhecida (retiming), ou então a implementação antes e depois de sua síntese. Diversos métodos são utilizados atualmente nessa área com bastante eficiência, envolvendo algoritmos que utilizam BDDs e SAT. No entanto, a crescente complexidade dos sistemas digitais atuais e a dificuldade de se verificar a equivalência decorrente dessa complexidade motivam a busca de novas soluções. Este trabalho propõe uma ferramenta de verificação, baseada nos seguintes pontos: particionamento dos circuitos em largura, um resolvedor SAT paralelo e reaproveitamento de cláusulas de conflito encontradas pelo resolvedor SAT por indução em circuitos sequenciais. Esperamos com estas técnicas resolver problemas maiores e mais rapidamente do que as soluções existentes. | pt_BR |
dc.language | Português | pt_BR |
dc.publisher | Universidade Federal de Minas Gerais | pt_BR |
dc.publisher.initials | UFMG | pt_BR |
dc.rights | Acesso Aberto | pt_BR |
dc.subject | circuitos eletronicos | pt_BR |
dc.subject.other | Eletrônica digital Testes | pt_BR |
dc.subject.other | Computação | pt_BR |
dc.subject.other | Circuitos integrados Verificação | pt_BR |
dc.subject.other | Circuitos eletrônicos Verificação | pt_BR |
dc.title | Verificação de equivalência de circuitos com aceleração por largura e aprendizado de cláusulas de conflito | pt_BR |
dc.type | Dissertação de Mestrado | pt_BR |
Appears in Collections: | Dissertações de Mestrado |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
thiagoradicchiroque.pdf | 480.71 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.