使用输出分组和电路可满足性的等价性验证算法

Efficient Equivalence Checking Using Output Grouping and Circuit SAT Solver

摘要: 介绍了一种使用电路可满足性解算器的组合电路等价性验证算法.对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题.同时,注意各个子问题间的有用隐含信息的共享,减小了SAT推理的搜索空间.实验结果表明,该算法是实用有效的.

Abstract: A new combinational equivalence checking technique using Circuit SAT is proposed in the paper.By the algorithm,a heuristic is used to do output grouping for complex problem first,then the equivalence checking problem is converted into some Circuit SAT problems.To reduce the search space,useful learned information of some sub-problem is shared.Experimental results show the efficiency of the proposed algorithm.