| 结合ATPG和SAT的无界模型检验前像计算方法 |
| |
| 引用本文： | 刘领一,赵阳,吕涛,李华伟,李晓维.结合ATPG和SAT的无界模型检验前像计算方法[J].计算机辅助设计与图形学学报,2007,19(3):376-380. |
| |
| 作者姓名： | 刘领一 赵阳 吕涛 李华伟 李晓维 |
| |
| 作者单位： | 中国科学院计算机系统结构重点实验室,北京,100080;中国科学院计算技术研究所计算机先进测试技术实验室,北京,100080;中国科学院研究生院,北京,100049;中国科学院计算机系统结构重点实验室,北京,100080;中国科学院计算技术研究所计算机先进测试技术实验室,北京,100080 |
| |
| 基金项目： | 国家重点基础研究发展计划(973计划)
,
国家自然科学基金 |
| |
| 摘 要： | 提出一种无界模型检验的前像计算方法,该方法有效地结合ATPG和SAT引擎,充分利用引擎各自的优点.SAT用来判断是否已经穷尽所有解;每次SAT枚举出一个前像解后,采用一个专门的ATPG过程减少状态变量上的赋值,从而减少前像解的总个数,加快后面的不动点迭代处理.最后通过在ISCAS89和ITC99电路上的实验证明了文中方法的有效性.
|
| 关 键 词： | 形式验证 无界模型检验 前像计算 自动化测试激励生成 布尔可满足性问题 |
| 收稿时间： | 2006-07-07 |
| 修稿时间： | 2006-07-072006-10-13 |
Combining ATPG and SAT for Preimage Computation in Unbounded Model Checking |
| |
| Liu Lingyi,Zhao Yang,Lu Tao,Li Huawei,Li Xiaowei.Combining ATPG and SAT for Preimage Computation in Unbounded Model Checking[J].Journal of Computer-Aided Design & Computer Graphics,2007,19(3):376-380. |
| |
| Authors: | Liu Lingyi Zhao Yang Lu Tao Li Huawei Li Xiaowei |
| |
| Affiliation: | 1. Key Laboratory of Computer System and Architecture, Chinese Academy of Sciences, Beijing 100080;2. Advanced Test Technology Laboratory, Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100080; 3. Graduate University of Chinese Academy of Sciences, Beijing 100049 |
| |
| Abstract: | This paper presents a preimage computation approach used in unbounded model checking. The approach combines ATPG and SAT engines effectively and makes full use of their respective advantages. First, a SAT solver is used to determine whether the preimage solution has been exhausted. When a preimage solution is generated by the SAT solver, a specific ATPG process is adopted to minimize the sets of assignments to state variables. This in turn reduces the number of all the preimage solutions and accelerates the fixed point iteration process. Experimental results on ISCAS89 and ITC99 benchmark demonstrate the effectiveness of our proposed approach. |
| |
| Keywords: | formal verification unbounded model checking preimage computation automatic test pattern generation Boolean satisfiability |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
