一种基于完备仿真的组合运算电路等价性验证方法及系统
CN116050311A 蔡少伟老师
背景介绍
目前在学术界和工业界，用于求解LEC（Logic Equivalence Checking）问题的方法主要有以下两种：
SAT方法：
直接将问题编码为CNF（Conjunctive Normal Form）并使用SAT求解器进行求解，或者对电路进行静态或动态的分析，添加额外约束子句后再利用SAT求解器解决。代数方法：
验证乘法器等规范运算电路的代数方法。此外，还存在基于BDD（Binary Decision Diagrams）、ATPG（Automatic Test Pattern Generation）、定理证明等技术的方法。
对于复杂的运算电路，目前还没有一个特别高效的办法。
SAT求解器的局限性
基于SAT求解器的算法在处理复杂的运算电路（例如具有复杂联系关系和异或门级联的电路）时表现不佳。尤其对于大于16bit的乘法器，SAT求解器很难在可接受的时间内求解。
代数方法的局限性
基于代数方式的等价性验证需要电路具有特别规范的功能，不能破坏原始数据通路。电路的功能必须能够用简洁的数学表达式表示，且电路中不能存在控制逻辑。因此，这种方法通常只能用于验证乘法器电路的原始设计，无法处理通用情况的等价性验证。
本发明的新方法
一种基于完备仿真的组合运算电路等价性验证方法，该方法深度结合了电路仿真和SAT求解的LEC验证技术，具体如下：
- 电路输入与输出未被修改。
- 电路输入为AIG（And-Inverter Graph）格式。
初步化简和逆向：
删除无扇出的门电路，通过异或门的数量来删除非门电路。多次随机仿真：
获得一个可能的等价类节点集合。- 启发式算法：
选择SAT求解器或完备仿真进行求解。
若节点对不等价，则将对应PI的赋值作为反例重新仿真，进一步在候选等价节点集合中剔除其他不等价节点；若点对等价，则记录该信息，在后续SAT求解中直接将此信息编码并提供给SAT求解器来加速求解。
具体步骤为：首先将两个等价节点涉及的扇入锥子电路提取出来，使用异或门连接等价节点，并将异或门视为该子电路的PO，子电路中的原电路PI作为新的PI。
临时电路的使用
在求解节点对是否等价时，不直接修改原始电路，而是提取需要的部分，创建一个新的临时电路进行求解。得到等价性验证结果后删除该临时电路。