| 基于深度优先搜索与增量式求解的极小一阶不可满足子式提取算法 |
| |
| 引用本文： | 张建民,黎铁军,张峻,徐炜遐,李思昆.基于深度优先搜索与增量式求解的极小一阶不可满足子式提取算法[J].国防科技大学学报,2012,34(5):121-126. |
| |
| 作者姓名： | 张建民 黎铁军 张峻 徐炜遐 李思昆 |
| |
| 作者单位： | 国防科技大学 计算机学院,湖南 长沙,410073 |
| |
| 基金项目： | 国家自然科学基金资助项目 |
| |
| 摘 要： | 随着寄存器传输级甚至行为级的硬件描述语言应用越来越广泛,基于一阶逻辑的可满足性模理论(Satisfiability Modulo Theories,SMT)逐渐替代布尔可满足性(Boolean Satisfiability,SAT),在VLSI形式化验证领域具有更加重要的应用价值。而极小不可满足子式能够帮助EDA工具迅速定位硬件中的逻辑错误。针对极小SMT不可满足子式的求解问题,采用深度优先搜索与增量式求解策略,提出了深度优先搜索的极小SMT不可满足子式求解算法。与目前最优的宽度优先搜索算法对比实验表明:该算法能够有效地求解极小不可满足子式,随着公式的规模逐渐增大时,深度优先搜索算法优于宽度优先搜索算法。
|
| 关 键 词： | 形式化验证 硬件错误定位 可满足性模理论 极小不可满足子式 |
| 收稿时间： | 1/6/2012 12:00:00 AM |
An algorithm for extracting minimal first-order unsatisfiable subformulae
on depth-first-search and incremental solving |
| |
| ZHANG Jianmin,LI Tiejun,ZHANG Jun,XU Weixia and LI Sikun.An algorithm for extracting minimal first-order unsatisfiable subformulae
on depth-first-search and incremental solving[J].Journal of National University of Defense Technology,2012,34(5):121-126. |
| |
| Authors: | ZHANG Jianmin LI Tiejun ZHANG Jun XU Weixia and LI Sikun |
| |
| Institution: | (College of Computer,National University of Defense Technology,Changsha 410073,China) |
| |
| Abstract: | |
| |
| Keywords: | formal verification error localization of hardware: Satisfiability Modulo Theories (SMT) minimal unsatisfiable subformula |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《国防科技大学学报》浏览原始摘要信息 |
| 点击此处可从《国防科技大学学报》下载免费的PDF全文 |
|
