基于Mining-SEC方法的电路等价性验证

Equivalence Verification of Circuits Based on Mining-SEC Approach

针对时序电路的等价性验证难题，提出基于Mining-SEC的定界等价性验证方法。将待验证时序电路按时间帧展开为多项式符号代数表示的电路集合，利用时间序列数据挖掘方法挖掘其中的不变量和相应的全局约束，不变量可以是任意多项式。此外还可挖掘电路中的不合法约束和复杂的多项式关系，通过以上方法可以明显降低求解空间。使用基于SMT的验证引擎检验电路等价性。实验结果表明，该方法可以快速地实现验证收敛，得到平均1-2．个量级的验证加速，并且可以有效消除虚假验证。

This paper researches the sequential circuit equivalence verification problem. Bounding equivalence verification method based on Mining-Sequential Equivalence Checking（SEC） is put forwarded. To be verified sequential circuit is expansion to a set of Polynomial Symbolic Algebra（PSA） representation in accordance with time frame. The invariants and global constraints are mined over the expression database according to time series. The invariants can be arbitrary polynomial. Moreover, the approach can also mine the illegal constraints and complex polynomial relationship, with this the solving space is pruned dramatically. The equivalence verification approach based on Satisfiablity Module Theory（SMT） engine is proposed. Experimental result shows that the approach can realize rapid convergence, 1-2 order of magnitude verification speedups is achieved and false verification is eliminated effectively.