应用吴方法进行高层次定界模型检验

• 作者: 冯刚 杨志 邵晶波 马光胜
• 来源期刊: 计算机辅助设计与图形学学报
• 学科: 工学
• 关键词: 高层次设计 定界模型检验 吴方法 形式验证
• 年，卷（期）: 2008,（2）
• 所属期刊栏目: VLSI设计与测试及电子设计自动化
• 页码范围: 137-143
• 页数: 7页
• 分类号: TP391.7
• 字数: 7265字
• 语种: 中文

摘要

以吴方法为理论基础,提出一种针对高层次设计验证的定界模型检验方法.通过使用多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并用吴方法有效地解决该定理证明问题.实验结果表明,与基于布尔SAT、基于LP的RTL SAT以及基于非线性求解器的性质检验方法相比,该方法在时间消耗上具有相当大的优势.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	马光胜	哈尔滨工程大学计算机科学与技术学院	74	240	8.0	12.0
2	冯刚	哈尔滨工程大学计算机科学与技术学院	20	75	5.0	7.0
3	杨志	哈尔滨工程大学计算机科学与技术学院	7	20	4.0	4.0
4	邵晶波	哈尔滨工程大学计算机科学与技术学院	4	9	2.0	3.0