Abstract: With the rapid development of information industry, the design complexity of chips is increasing. In a complex circuit, there are some modules of unknown function, which are called a partial implementation circuit. In order to ensure the correctness of product design, we use equivalence checking methods to verify partial implementation circuits. The paper presents an optimization algorithm based satisfiability. The first, divide a partial implementation circuit into some “logic cones”; the second, create circuits of Miter in according with matched logic cones and perform variable constraints to unknown function modules using symbolic simulation technology in Miter circuits; the last, verify CNFs of Miter circuits in turn using SAT engine. A series of experimental results are generated based on ISCAS'85 benchmark circuits containing a single unknown module and similar size combinational circuits containing some unknown modules. Those experimental data demonstrate that the algorithm can improve the detection rate of circuits.

Key words: partial implementation circuits, logic cone, SAT, equivalence checking, unknown module