计算机工程

• 开发研究与工程应用 • 上一篇    下一篇

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

王冠军a,童敏明b,周 勇a,赵 莹a   

  1. (中国矿业大学 a. 计算机科学与技术学院;b. 信息与电气工程学院,江苏 徐州 221116)
  • 收稿日期:2012-12-07 出版日期:2014-01-15 发布日期:2014-01-13
  • 作者简介:王冠军(1981-),男,讲师、博士,主研方向:CAD/EDA技术,机器人技术;童敏明,教授、博士生导师;周 勇,副教授;赵 莹,讲师、博士
  • 基金项目:
    国家自然科学基金资助项目(51104157);中央高校基本科研业务费专项基金资助项目(2010NQA28);国家大学生创业实践基金资助项目(201310290080 )

Equivalence Verification of Circuits Based on Mining-SEC Approach

WANG Guan-jun a, TONG Min-ming b, ZHOU Yong a, ZHAO Ying a   

  1. (a. School of Computer Science and Technology; b. School of Information and Electrical Engineering, China University of Mining and Technology, Xuzhou 221116, China)
  • Received:2012-12-07 Online:2014-01-15 Published:2014-01-13

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

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

Abstract: 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.

Key words: time series, data mining, Polynomial Symbolic Algebra(PSA), Sequential Equivalence Checking(SEC), Satisfiablity Module Theory(SMT), false verification

中图分类号: