Um núcleo inteligente para processamento distribuído de resolvedores SAT em verificação por equivalências

Abstract

Equivalence Checking is one the of the key components in formal verification for digital systems. It is also one of the most widely used approaches in industry for functional equivalence verification of different designs. A number of recently proposed BDD and SAT based approaches have met with considerable success in this area. However, the growing gap between the current solvers capabilities and the increasing complexity in digital designs lead to exploring alternative, better solutions. This work proposes an intelligent kernel for distributed processing of SAT solvers in Equivalence Checking. Specifically, the proposed kernel exploits a new technique for identifying structural similarities between the circuits. Finally, results of verification using the proposed methodology are presented.