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

Equivalence Verification of Circuits Based on Mining-SEC Approach

作　　者：王冠军[1] 童敏明[2] 周勇[1] 赵莹[1] 

机构地区：[1]中国矿业大学计算机科学与技术学院,江苏徐州221116 [2]中国矿业大学信息与电气工程学院,江苏徐州221116

出　　处：《计算机工程》2014年第1期301-304,共4页Computer Engineering

基　　金：国家自然科学基金资助项目(51104157);中央高校基本科研业务费专项基金资助项目(2010NQA28);国家大学生创业实践基金资助项目(201310290080)

摘　　要：针对时序电路的等价性验证难题，提出基于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.

关 键 词：时间序列 数据挖掘 多项式符号代数 时序电路等价性检验 可满足性模理论 虚假验证 

分 类 号：TP331[自动化与计算机技术—计算机系统结构]