利用改善的静态隐含策略加速等价性验证

Enhancing sat-based equivalence checking with improved static implications

随着近年来高效SAT(Satisfiability)求解算法提出,SAT已成为集成电路形式验证方法中重要引擎之一。但在运用SAT验证时需将电路结构转化为成OR-AND两级逻辑描述,丢失了电路的拓扑信息。本文利用改善的静态隐含策略来提取有用子句作为预处理,来加快验证过程。本文算法在原有静态隐含技术的基础上,引入了关联节点隐含及隐含过程加速策略。给出的ISCAS85电路的实验结果表明算法的有效性。

In recent years, with much progress made in the field of Boolean satisfiability (SAT), SAT has become an essential engine in formal verification, such as combinational equivalence checking (CEC). But when the circuit is converted into CNF, the structure information is lost. We propose a novel technique to improve SAT-based combinational equivalence checking by statically adding meaningful clauses to the CNF formula of the miter circuit. Based on the old static implications technique, the algorithm is improved using correlative signal implications and implications’ speedup strategy. Experimental results on ISCAS’85 instances show the efficiency of proposed approach.