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

Abstract

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.