论文部分内容阅读
在等价性验证领域中，随着电路规模和电路设计的复杂度日益增大，传统的只基于二叉决策图(Binary Decision Diagram, BDD)或者只基于SAT的单等价性验证引擎面对这些问题无法有效的解决。然而，每种方法有自己的优点和缺点，适用于不同类型的等价性验证电路问题。在过去研究中，Kuehlmann将基于SAT的验证引擎和基于BDD的验证引擎结合起来,适用于解决单个引擎很难解决的等价性验证问题。本文将研究一种多引擎的等价性验证系统,将基于SMT-Sweeping和割集的验证方法结合起来进行组合电路的等价性验证。SMT-Sweeping是将Sweeping算法和可满足性模理论（SMT）结合的一种对电路进行简化的方法，和SAT-Sweeping一样是一种完备的Sweeping算法，并且效率高于基于SAT的Sweeping算法。基于SAT的Sweeping算法针对与门反向图（And-Inverter Graph,AIG）进行电路的冗余节点消除，这就首先需要将源电路设计转为为AIG布尔逻辑图，然后进行不断调用SAT求解器进行SAT-Sweeping。基于SMT的Sweeping直接对电路的多种逻辑函数进行Sweeping，SMT求解器能处理比SAT求解器更复杂的命题逻辑公式，不需要将电路转化为AIG图的布尔逻辑函数再进行处理。在SMT-Sweeping算法的基础上，我们实现了基于SMT-Sweeping的等价性验证系统，并且对ISCAS85电路, RTL算术逻辑电路进行实验测试，实验结果表明本系统能够正确地对这些电路进行等价性验证并且效果良好。基于割集的方法根据电路结构的相似性，在电路内部引入候选等价节点，将整个电路验证的问题分为一系列子电路，通过验证子电路的等价性来达到验证整个电路的目的。然而，割集的引入会导致误判现象的发生，我们对割集的误判方法进行研究，提出一种通过提取部分极小不可满足核来快速消除误判的方案。在对割集研究的基础上，本文将基于SMT-Sweeping验证方法与其结合，在进行SMT-Sweeping验证前，对SMT-Sweeping验证引擎设置阈值来保证简单的电路的验证问题能由SMT-Sweeping验证引擎解决，复杂的电路验证问题进行一定程度的化简后交给割集引擎处理。我们实现了基于SMT-Sweeping和割集的多引擎验证系统并且进行了实验，将其和只基于SMT-Sweeping和只基于割集的单引擎验证系统进行了对比，实验表明通过多种引擎的结合使用，多引擎验证系统有着较强的适用性，更适合解决复杂组合电路的验证问题。