无界模型检验中融合电路信息的SAT算法研究

• 作者: 吕涛 李华伟 李晓维 赵阳
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 设计验证 无界模型检验 Boolean可满足性问题(SAT) 寄存器传输级(RTL)
• 年，卷（期）: 2009,（6）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 1110-1118
• 页数: 9页
• 分类号: TP306
• 字数: 8422字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2009.01110

摘要

针对从电路转化而来的SAT问题.通用SAT求解器存在一个缺陷-电路互连信息的缺失,这是造成很多无关推导的根源.文中提出了一个统一的基于CNF数据结构的电路SAT无界模型检验框架.首先作者提出了定值子句的概念,利用这一概念可以在CNF结构中保存电路的互连信息,在搜索过程中更早地识别可满足解,减少不必要的搜索.其次,文中提出了在CNF结构上的状态变量赋值精简方法,摆脱了以往基于SAT的无界模型检验中这一步骤对门级电路结构的依赖.实验数据表明,利用文中方法进行前像计算能够取得明显的加速.同时,文章比较了两种搜索顺序在多时帧搜索中的效果.实验结果表明利用文中方法可以验证传统模型检验方法难以验证的复杂电路属性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李华伟	中国科学院计算机系统结构重点实验室	55	595	14.0	22.0
3	吕涛	中国科学院计算机系统结构重点实验室	41	423	10.0	20.0
12	赵阳	中国科学院计算机系统结构重点实验室	32	397	12.0	19.0