| 一种基于SAT的运算电路查错方法 |
| |
| 引用本文： | 陈云霁,张健,沈海华,胡伟武.一种基于SAT的运算电路查错方法[J].计算机学报,2007,30(12):2082-2089. |
| |
| 作者姓名： | 陈云霁 张健 沈海华 胡伟武 |
| |
| 作者单位： | 1. 中国科学院计算技术研究所计算机系统结构重点实验室,北京,100080
2. 中国科学院软件研究所计算机科学国家重点实验室,北京,100080 |
| |
| 基金项目： | 国家重点基础研究发展计划(973计划)
,
国家高技术研究发展计划(863计划)
,
中国科学院基金
,
国家自然科学基金 |
| |
| 摘 要： | 基于SAT的运算电路查错方法将被验证系统中系统规范成立与否的问题转换为布尔公式和数学公式的混合形式E-CNF,通过采用了标志子句技术的E-SAT求解器进行求解.实验表明该方法自动化程度高,能处理大规模的运算电路,有较强的查找错误能力.
|
| 关 键 词： | 形式验证 模型检验 SAT E-CNF 标志子句 运算电路 查错方法 Method Circuit 能力 查找错误 大规模 处理 程度 自动化 实验 求解器 子句 标志 混合 数学公式 布尔 问题转换 范成 验证系统 |
| 修稿时间： | 2006年1月17日 |
A SAT-Based Arithmetic Circuit Bug-Hunting Method |
| |
| CHEN Yun-Ji,ZHANG Jian,SHEN Hai-Hua,HU Wei-Wu.A SAT-Based Arithmetic Circuit Bug-Hunting Method[J].Chinese Journal of Computers,2007,30(12):2082-2089. |
| |
| Authors: | CHEN Yun-Ji ZHANG Jian SHEN Hai-Hua HU Wei-Wu |
| |
| Abstract: | E-CNF is hybrid of Boolean formula and mathematic formula. SAT-based arithmetic circuit bug-hunting method translates the verification problem into E-CNF, and solves E-CNF through E-SAT solver. E-SAT solver is an extension of complete SAT solver, with tag clause technique. Experiments show that SAT-based arithmetic bug-hunting method is powerful in finding bugs in arithmetic circuits. |
| |
| Keywords: | Formal verification SAT E-CNF Tag clause |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
