Verificação de equivalência de circuitos combinacionais dissimilares através do reaproveitamento de cláusulas de conflito

Abstract

As time goes by, integrated circuits are becoming ever more present in our lives. From the mobile phones we use to the cars we drive, we have almost constant interaction with electronic devices. This proliferation leads to the necessity for more agile and compact circuits, which in turn, makes them more complex and expensive. To produce error-free circuits, a considerable amount of time and money is spent on hardware verification during the design process. Equivalence checking of two combinational circuits is one of the most widely used techniques, which checks whether two combinational circuits (at any design level) that are given the same input data will produce equivalent output data. During the last few years, researchers have attempted to develop techniques to increase the verification of larger circuits and decrease the time spent on this task, but there has been no notable success for dissimilar circuits. This thesis presents and analyzes methodologies that rely on conflict clause reuse between circuit partitions during the equivalence checking of two dissimilar combinational circuits using a SAT solver.