Equivalence Checking For Logic Circuits

Since integrated circuit designs are becoming more and more complex, functional validation has been the main bottleneck of the design flow. The design team spends more than 50% effort of the development on verification. The traditional way of functional verification is simulation, which is very time-consuming, and difficult to obtain complete functional coverage. Formal verification uses rigorous mathematical reasoning to show that a design meets all or parts of its specification,and has attracted dramatically the interests of both academic and industrial fields. Equivalence checking is a common-used formal method, which proves that two different descriptions of design have the same functionality. This thesis covers some key aspects on logic circuits equivalence checking: how to improve the efficiency of the incremental equivalence checking algorithms, how to verify the designs with black boxes, how to integrate effectively the different engines of Boolean reasoning, and how to improve the resolution of design error diagnosis.The original contributions of this thesis are as follows.1. An equivalence checking method based on incremental satisfiability has been proposed. This method applies the internal structural similarities between two designs, and breaks the whole verification into some sub-tasks to finish incrementally. Compared with the previous algorithms in literatures, the proposed method has three features:(1) The method prunes the candidate equivalent pairs with new techniques to avoid the frequent calling of SAT procedure.(2) By substituting the internal equivalent pairs and converting the equivalence relations into conjunctive normal form (CNF) formulas, the method can avoid the false negatives, but also can reduce the search space of SAT procedure.(3) This method improves the performance using incremental satisfiability. The experimental results show that, the presented method is on average three factors to one magnitude faster than those methods of the same kind in literature.2. A formal method of verifying designs with black boxes has been presented. This method integrates logic simulation and Boolean satisfiability, and uses parallel logic simulation to detect the error out of the black boxes, then uses Boolean comparison...