结合二叉判决图和布尔可满足性的等价性验证算法

Combining Binary Decision Diagrams and Boolean Satisfiability for Equivalence Checking

本文提出了一种结合二叉判决图BDD和布尔可满足性SAT的新颖组合电路等价性验证技术 .算法是在与 /非图AIG中进行推理 ,并交替使用BDD扩展和基于电路SAT解算器简化电路 .如尚未解决 ,将用基于合取范式SAT解算器进行推理 .与已有算法相比主要有如下改进 :在AIG中结合多种引擎进行简化 ,不存在误判可能 ;充分利用了基于电路解算器和基于合取范式解算器各自优点 ,减小了SAT推理的搜索空间 .实验结果表明了本算法的有效性 .

A new combinational equivalence checking approach integrating Binary Decision Diagrams and Boolean Satisfiability is proposed. The algorithm works on the representation called And/Inverter Graph of the circuit. The BDD propagation and Circuit-based SAT Solver are applied in an intertwined manner to reduce the space of the miter circuit. If failed, CNF-based SAT Solver is used to solve the problem. The efficiency of the proposed approach is shown through its application on the LGsynth91 benchmark circuits.