结合ATPG和SAT的无界模型检验前像计算方法
文献类型：期刊论文
| 作者 | 刘领一; 李晓维; 李华伟; 吕涛; 赵阳 |
| 刊名 | 计算机辅助设计与图形学学报
 |
| 出版日期 | 2007 |
| 卷号 | 19期号:3 |
| 关键词 | 形式验证 无界模型检验 前像计算 自动化测试激励生成 布尔可满足性问题 |
| 英文摘要 | 提出一种无界模型检验的前像计算方法,该方法有效地结合ATPG和SAT引擎,充分利用引擎各自的优点.SAT用来判断是否已经穷尽所有解;每次SAT枚举出一个前像解后,采用一个专门的ATPG过程减少状态变量上的赋值,从而减少前像解的总个数,加快后面的不动点迭代处理.最后通过在ISCAS89和ITC99电路上的实验证明了文中方法的有效性. |
| 语种 | 中文 |
| 公开日期 | 2010-11-22 |
| 源URL | [http://ictir.ict.ac.cn/handle/311040/888]  |
| 专题 | 中国科学院计算技术研究所期刊论文_2007年中文 |
| 推荐引用方式 GB/T 7714 | 刘领一,李晓维,李华伟,等. 结合ATPG和SAT的无界模型检验前像计算方法[J]. 计算机辅助设计与图形学学报,2007,19(3). |
| APA | 刘领一,李晓维,李华伟,吕涛,&赵阳.(2007).结合ATPG和SAT的无界模型检验前像计算方法.计算机辅助设计与图形学学报,19(3). |
| MLA | 刘领一,et al."结合ATPG和SAT的无界模型检验前像计算方法".计算机辅助设计与图形学学报 19.3(2007). |
入库方式： OAI收割
来源：计算技术研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。