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

• 作者: 周勇 王冠军 童敏明 赵莹
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 时间序列 数据挖掘 多项式符号代数 时序电路等价性检验 可满足性模理论 虚假验证
• 年，卷（期）: 2014,（1）
• 所属期刊栏目: 开发研究与工程应用
• 页码范围: 301-304
• 页数: 4页
• 分类号: TP331
• 字数: 3631字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2014.01.065

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周勇	中国矿业大学计算机科学与技术学院	85	984	16.0	29.0
2	童敏明	中国矿业大学信息与电气工程学院	143	1024	16.0	25.0
3	赵莹	中国矿业大学计算机科学与技术学院	20	78	5.0	8.0
4	王冠军	中国矿业大学计算机科学与技术学院	19	80	5.0	8.0