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

摘要

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