Verificação de equivalência combinacional utilizando hiper-resolução binária

Abstract

The capacity of cramming more components into integrated circuits has doubled roughly every 18 months since mid-1960, with projections to continue this pace until 2050. This growing complexity of computing devices leads the integrated circuit industry to invest more than 50% of development time in the stage of verification of new projects in order to minimize losses due to the replacement of defective components. This paper proposes an improvement for the combinational equivalence checking problem using pre-processing techniques based on hyper binary resolution, applied to graphs extracted from circuit implications. The text describes a tool that implements these techniques, and in the end the results shows the efficacy of hyper-binary resolution as a technique for simplification, but at the same time eliminate any structural information concerning the circuit under verification.