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

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