SAT-Based Equivalence Checking Based on Circuit Partitioning and Special Approaches for Conflict Clause Reuse
SAT-Based Equivalence Checking Based on Circuit Partitioning and Special Approaches for Conflict Clause Reuse
复制标题
基于电路划分和冲突条款重用特殊方法的 SAT 等价检查
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
C. Coelho
中科院分区：
文献类型：
--
作者：
F. V. Andrade;Márcia C. M. Oliveira;A. O. Fernandes;C. Coelho
本文提出了一种新的基于SAT的CEC方法验证电路的结构依赖。该方法基于电路划分和冲突条款重用的特殊方法，大大降低了CEC问题的复杂性。使用这种方法，它是可能的，以提高整体验证时间的相似和不相似的电路。例如，对于类似的乘法器电路，可以在近40分钟内检查高达37乘以37位的等效性，而无需任何电路拓扑信息。对于不同的电路，所提出的方法是能够检查等价性高达24倍24位在一个小时内克服基于BDD的方法，使用切割点不能检查超过12倍12位乘法器与合理的时间限制。
This paper presents a new SAT-based CEC methodology for the verification of circuits with structural dependence. This methodology is based on circuit partitioning and special approaches for conflict clauses reuse, reducing highly the CEC problem complexity. Using this methodology it is possible to improve the overall verification time of similar and dissimilar circuits. For instance, for similar multiplier circuits it was possible to check equivalence up to 37 times 37 bit without any circuit topological information in nearly 40 minutes. For dissimilar circuits, the proposed methodology is able to check equivalence up to 24 times 24 bit in one hour overcoming the BDD-based approaches that using cutpoints cannot check beyond a 12 times 12 bit multiplier with reasonable time limit.