提出了一种改进现有基于SAT的组合电路验证方法的新技术。主要创新在于提出了对CUVs的模拟蕴含学习方法.能快速地将许多间接的蕴含关系转化成子句。将这些子旬加入原有的CNF表达数据中。可以减少SAT解决器的搜索空间并且加速BCP过程。对于ISCAS测试电路的实验可以看出该方法比常规算法有着近一个数量级的速度提升。
We present a novel technique of improving the SAT-based Combinational Equivalence Checking. Many indirect implications can be quickly changed into clauses by inducing simulated implication learning into the oringinal circuits under verification. These clauses are appended to the existing CNF database and they will prime the search space of SAT-solver engine and enhances the Boolean Constraint Propagation (BCP). Experiments on the ISCAS benchmark circuits show about lOx speedup can be achieved over the conventional approach.