| 无界模型检验中融合电路信息的SAT算法研究 |
| |
| 引用本文： | 赵阳,吕涛,李华伟,李晓维.无界模型检验中融合电路信息的SAT算法研究[J].计算机学报,2009,32(6). |
| |
| 作者姓名： | 赵阳 吕涛 李华伟 李晓维 |
| |
| 作者单位： | 1. 中国科学院计算机系统结构重点实验室,北京,100190;中国科学院计算技术研究所,北京,100190;中国科学院研究生院,北京,100039
2. 中国科学院计算机系统结构重点实验室,北京,10019;0中国科学院计算技术研究所,北京,100190 |
| |
| 基金项目： | 国家自然科学基金，国家重点基础研究发展规划(973计划)，国家高技术研究发展计划(863计划) |
| |
| 摘 要： | 针对从电路转化而来的SAT问题.通用SAT求解器存在一个缺陷-电路互连信息的缺失,这是造成很多无关推导的根源.文中提出了一个统一的基于CNF数据结构的电路SAT无界模型检验框架.首先作者提出了定值子句的概念,利用这一概念可以在CNF结构中保存电路的互连信息,在搜索过程中更早地识别可满足解,减少不必要的搜索.其次,文中提出了在CNF结构上的状态变量赋值精简方法,摆脱了以往基于SAT的无界模型检验中这一步骤对门级电路结构的依赖.实验数据表明,利用文中方法进行前像计算能够取得明显的加速.同时,文章比较了两种搜索顺序在多时帧搜索中的效果.实验结果表明利用文中方法可以验证传统模型检验方法难以验证的复杂电路属性.
|
| 关 键 词： | 设计验证 无界模型检验 Boolean可满足性问题(SAT) 寄存器传输级(RTL) |
A Novel Circuit SAT Solver in Unbounded Model Checking |
| |
| ZHAO Yang,LV Tao,LI Hua-Wei,LI Xiao-Wei.A Novel Circuit SAT Solver in Unbounded Model Checking[J].Chinese Journal of Computers,2009,32(6). |
| |
| Authors: | ZHAO Yang LV Tao LI Hua-Wei LI Xiao-Wei |
| |
| Affiliation: | Key Laboratory of Computer System and Architecture;Chinese Academy of Sciences;Beijing 100190;Institute of Computing Technology;Beijing 100190;Graduate University of Chinese Academy of Sciences;Beijing 100039 |
| |
| Abstract: | For the circuit-oriented SAT problems,general purpose SAT solver will make some unnecessary decision and implication. The reason lies in that the circuit structure information is lost in the conversion to CNF. To overcome this drawback in SAT-based unbounded model checking,an improved SAT solver is proposed. First,the concept of define-value clauses is given to store the circuit structure in CNF. The improved solver avoids many redundant decisions which would be made by previous solvers. And then,A CNF-base... |
| |
| Keywords: | |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
