An Equivalence Checking Method For Circuits With Black Boxes Based On Logic Cone And SAT

With the development of information industry, very large scale integrated (VLSI) circuits and digital systems have conquered a place in almost all areas of our life. Moreover, due to the chip complexity constantly increasing, the difficulty of functional verification of new product designs has been increased. For these reasons, it's necessary to find design errors early in the design process. Therefore, it's important to develop formal verification skills to handle these processes which may lead into functionally incorrect designs.Equivalence checking is one of formal verification methods, which is used to solve the problem of checking whether two circuits specify the same functionality. Nowadays, digital designs often contain regions where the implementation of certain modules is not known. These modules are called Black Boxes. We use equivalence checking between an implementation with Black Boxes and a specification in order to find design errors in early design stages.In this thesis, We investigate the theory of equivalence checking in digital circuits and their applications in equivalence checking with Black Boxes. Moreover, we present an equivalence checking algorithm in circuits with Black Boxes based on Logic Cone partition and SAT. The main content of this thesis are as follows:1. Equivalence Checking. It proves that two given designs have the same functionality, e.g., an optimized design is functionally equivalent to its earlier version. In verification process, the verification approaches are divided into two general categories: (1) symbolic approaches, and (2) incremental approaches. Symbolic approaches are referred to as those approaches that rely on symbolic techniques using the Ordered Binary Decision Diagram (OBDD). Incremental approaches are those approaches that explore the structural similarity of the two circuits under verification.2. Equivalence Checking with Black Boxes. Some approaches of equivalence checking with Black Boxes are presented under the assumption that a specification and an implementation with Black Boxes are of combinational nature. These methods include Local Check, Output Exact Check and Input Exact Check. The exactness and the complexity of the algorithm are successively increased using these methods.3. An Efficient Equivalence Checking method with Black Boxes. We present an equivalence checking algorithm based on Logic Cone partition and SAT. According to the "divide and conquer" approach, a whole circuit is divided into several sub-circuits and outputs of Black Boxes are represented by unknown constraints using a symbolic simulation technique. In additional, conjunctive normal form formulas (CNF) of sub-circuits are verified by SAT Solver. The algorithm enhances the capability of detecting errors. We give a series of experimental results on the ISCAS'85 benchmark circuits and 10 simple combinational circuits demonstrating the effectiveness and feasibility of the algorithm.