| 引用本文: | 张建民,黎铁军,张峻,等.基于深度优先搜索与增量式求解的极小一阶不可满足子式提取算法.[J].国防科技大学学报,2012,34(5):121-126.[点击复制] |
| ZHANG Jianmin,LI Tiejun,ZHANG Jun,et al.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[点击复制] |
|
| |
|
|
| 本文已被：浏览 10150次 下载 7525次 |
| 基于深度优先搜索与增量式求解的极小一阶不可满足子式提取算法 |
| 张建民, 黎铁军, 张峻, 徐炜遐, 李思昆 |
|
(国防科技大学 计算机学院，湖南 长沙 410073)
|
| 摘要: |
| 随着寄存器传输级甚至行为级的硬件描述语言应用越来越广泛，基于一阶逻辑的可满足性模理论(Satisfiability Modulo Theories，SMT)逐渐替代布尔可满足性(Boolean Satisfiability，SAT)，在VLSI形式化验证领域具有更加重要的应用价值。而极小不可满足子式能够帮助EDA工具迅速定位硬件中的逻辑错误。针对极小SMT不可满足子式的求解问题，采用深度优先搜索与增量式求解策略，提出了深度优先搜索的极小SMT不可满足子式求解算法。与目前最优的宽度优先搜索算法对比实验表明：该算法能够有效地求解极小不可满足子式，随着公式的规模逐渐增大时，深度优先搜索算法优于宽度优先搜索算法。 |
| 关键词: 形式化验证 硬件错误定位 可满足性模理论 极小不可满足子式 |
| DOI： |
| 投稿日期：2012-01-06 |
| 基金项目:国家自然科学基金资助项目(61103083, 61133007) |
|
| An algorithm for extracting minimal first-order unsatisfiable subformulae on depth-first-search and incremental solving |
| ZHANG Jianmin, LI Tiejun, ZHANG Jun, XU Weixia, LI Sikun |
|
(College of Computer, National University of Defense Technology, Changsha 410073, China)
|
| Abstract: |
| While registering transfer level or even behavioral level, the hardware description language is widely used, and Satisfiability Modulo Theories(SMT) gradually replaces Boolean Satisfiability(SAT), and plays an important role in VLSI formal verification. A minimal unsatisfiable subformula can help automatic tools to rapidly locate the errors. A depth-first-search algorithm is proposed to extract minimal unsatisfiable subformulae in SMT to adopt depth-first searching and incremental solving strategy. The experimental results show that the depth-first-search algorithm effectively derived minimal unsatisfiable subformulae, and is more efficient than the breadth-first-search algorithm, which is the best method for computing the minimal unsatisfiable subformulae in SMT, with the number of variables and clauses in the original formulae increasing. |
| Keywords: formal verification error localization of hardware: Satisfiability Modulo Theories (SMT) minimal unsatisfiable subformula |
|
|
|
|
|
