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

AUTOR(ES)
DATA DE PUBLICAÇÃO

2008

RESUMO

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 to assure 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 of the 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) for benchmarks. 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 by this 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.

ASSUNTO(S)

eletrônica digital testes teses. computação teses. circuitos integrados verificação teses. circuitos eletronicos projetos processamento de dados teses.

ACESSO AO ARTIGO

Documentos Relacionados