基于增量可满足性的等价性检验方法

摘要

组合验证是数字集成电路形式化设计验证的重要方面.该文提出了一种基于增量布尔可满足性的组合等价性检验方法,通过合理选择候选等价结点和增量可满足性算法来提高算法性能,并通过对内部等价结点的置换及将等价关系转化为相应的合取范式公式,避免了误判的发生,又能缩小验证程序的搜索空间.针对ISCAS'85电路的实验结果表明,该文提出的方法比以往同类方法更快、更强健.