中文摘要：

信息产业飞速发展,芯片设计的复杂性与日俱增。在复杂的电路设计中,经常包含某些功能未知的模块,这样的电路称为部分实现电路。为了保证产品设计的正确性,对部分实现电路进行等价性验证,提出了一种基于可满足性的优化算法。首先对部分实现组合电路进行"逻辑锥"分割;其次根据匹配的逻辑锥创建Miter电路,并且使用符号模拟技术对电路中的功能未知模块进行变量约束;最后对多个Miter电路的合取范式依次进行可满足性验证。通过在包含单个未知模块的ISCAS’85基准电路以及包含若干大小相近未知模块的组合电路上得到的实验数据,表明了此算法能够较好地提高电路检错率。

英文摘要：

With the rapid development of information industry,the design complexity of chips is increasing.In a com-plex 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.