Contribuições para o problema de verificação de equivalência combinacional

• Main Author: Fabricio Vivas Andrade
• Other Authors: Antonio Otavio Fernandes
• Format: Others
• Language: Portuguese
• Published: Universidade Federal de Minas Gerais 2008
• Online Access: http://hdl.handle.net/1843/RVMR-7K6R63

=== A decrease the SAT solver solving time used to prove equivalence between the circuits. Through this technique, which was implemented in a tool called Vimplic, we have been able to dramatically reduce the overall verification time of several circuits outperforming the state-of-the-art techniques for CEC. This technique has been formalized in order toassure correctness of the derived implications and also to guarantee that it does not produce results with false-positives or false-negatives according to the equivalence between the circuits under CEC. Besides presenting Vimplic's implementation details, this work also describes a complete bibliographic review of the CEC techniques, specially ofthe SAT-based preprocessing techniques. Finally, by means of Vimplic tool, relations among the present work and other works on Satisfiability has been established with respect to the study of redundancy in Conjunctive Normal Form (CNF) formulas. The second major contribution presents a digital circuit generation tool (BenCGen) forbenchmarks. This tool can be used to generate 24 very popular types of circuits with parameterized size. More than 1,000,000 different designs may be produced using thistool, ranging from the smallest to the largest size of each circuit. Since there is a growing need for new benchmark circuits, BenCGen can supply a wide range of circuit to supply this demand. Correctness is a significant feature of the circuits generated bythis tool. In addition, a complete bibliographic review of the most popular benchmarks for Formal Verification is presented. Finally, a comparison among the most efficient SAT solvers is performed and presented using a large benchmark of CEC instance. The selected benchmark was produced by BenCGen and the results of this comparison point out the mostappropriate SAT solver for CEC instances. === O objetivo desse trabalho é apresentar duas contribuições importantes para o problema de Verificação de Equivalência Combinacional (CEC, do Inglês, Combinational Equivalence Checking). A primeira contribuição importante é uma técnica de pré-processamento que deriva informações redundantes dos dois circuitos sob CEC de modo a reduzir o tempo utilizado pelo Resolvedor de Satisfabilidade (SAT) para aprova de equivalência entre ambos circuitos. Através dessa técnica, implementada em uma ferramenta denominada Vimplic, é possível superar em desempenho as principais ferramentas do estado da arte de CEC baseado em SAT. É importante ressaltar que a técnica depré-processamento proposta é formalizada de modo a garantir a exatidão das implicações derivadas e assegurar que a mesma não produz falsos negativos e nem falsos positivos em relação à equivalência dos circuitos sob CEC. Além de detalhes de implementação da Vimplic, o presente trabalho também apresenta uma revisão bibliográfica completa das técnicas de CEC e, principalmente, das técnicas de pré-processamento para SAT. Finalmente, através da aplicação da ferramenta Vimplic, é possível estabelecer relaçõesimportantes entre o presente trabalho e os trabalhos na área de Satisfabilidade através do estudo de redundância em fórmulas em CNF.A segunda contribuição importante proposta é uma ferramenta para geração de circuitos, a BenCGen, que tem como principal objetivo a produção de circuitos para benchmarks. Essa ferramenta é capaz de gerar 24 tipos de circuitos diferentes com tamanhos parametrizados.Variando-se do menor para o maior tamanho de cada circuito, mais de 1.000.000 circuitos podem ser gerados. Tal ferramenta vem suprir uma grande demanda de novos benchmarks para CEC e para outras áreas de Verificação Formal. É importante ressaltar que a maior parte dos circuitos gerados pela ferramenta foram provados corretos. Além disso, uma revisão bibliográfica dos principais benchmarks para a área de Verificação Formal é mostrada no presente trabalho, na qual são destacados os seus principais benefícios e limitações.Finalmente, um comparativo entre os resolvedores de Satisfabilidade mais eficientes na resolução de instância de problemas de CEC é apresentado. O comparativo foi feito por meio de um benchmark produzido pela ferramenta BenCGen e através do mesmo foi possívelindicar o resolvedor de SAT mais adequado para os problemas de CEC estudados.