部分实现组合电路的等价验证优化算法  

An equivalence checking optimization algorithm for partial implementation combinational circuits

作　　者：岳园[1] 田双亮[1] 陈秀萍[1] 

机构地区：[1]西北民族大学数学与计算机科学学院,甘肃兰州730030

出　　处：《山东大学学报（理学版）》2016年第3期116-121,共6页Journal of Shandong University(Natural Science)

基　　金：国家自然科学基金资助项目(11205074);2013年西北民族大学中央高校基本科研业务费专项资金资助项目(31920130008);2014年西北民族大学中央高校基本科研业务费专项资金资助项目(31920140090);西北民族大学科研创新团队计划资助项目

摘　　要：信息产业飞速发展,芯片设计的复杂性与日俱增。在复杂的电路设计中,经常包含某些功能未知的模块,这样的电路称为部分实现电路。为了保证产品设计的正确性,对部分实现电路进行等价性验证,提出了一种基于可满足性的优化算法。首先对部分实现组合电路进行"逻辑锥"分割;其次根据匹配的逻辑锥创建Miter电路,并且使用符号模拟技术对电路中的功能未知模块进行变量约束;最后对多个Miter电路的合取范式依次进行可满足性验证。通过在包含单个未知模块的ISCAS'85基准电路以及包含若干大小相近未知模块的组合电路上得到的实验数据,表明了此算法能够较好地提高电路检错率。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 M iter in according with matched logic cones and perform variable constraints to unknown function modules using symbolic simulation technology in M iter circuits; the last,verify CNFs of M iter 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.

关 键 词：部分实现电路 等价性验证 逻辑锥 未知模块 可满足性 

分 类 号：TN402[电子电信—微电子学与固体电子学]