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

摘要：

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

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

分类号：TP331(计算技术、计算机技术)

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

在线出版日期：2014-02-22（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：301-304