| 引用本文: | 张建民,黎铁军,张峻,等.基于SAT的电路错误定位方法研究进展.[J].国防科技大学学报,2014,36(2):81-86.[点击复制] |
| ZHANG Jianmin,LI Tiejun,ZHANG Jun,et al.Research advances in SAT-based error localization methods on circuits[J].Journal of National University of Defense Technology,2014,36(2):81-86[点击复制] |
|
| |
|
|
| 本文已被：浏览 8339次 下载 6801次 |
| 基于SAT的电路错误定位方法研究进展 |
| 张建民, 黎铁军, 张峻, 李思昆 |
|
(国防科技大学 计算机学院， 湖南 长沙 410073)
|
| 摘要: |
| 随着VLSI芯片复杂度不断增加，功能验证与调试已占到整个芯片设计周期的60%以上。而错误的定位往往消耗大量的时间与精力，因此迫切需要一种高效的方法诊断与定位电路中的错误。针对近年来出现的许多电路错误定位方法，介绍了电路错误诊断方法的分类与工作流程，深入分析了基于SAT的错误定位方法的基本原理；对各种算法进行了概述评论，并简要介绍了在不可满足子式求解方面所做的一些研究工作，而不可满足子式能够显著提高错误定位效率与精度；讨论了电路错误定位技术所面临的主要挑战，并对今后的研究方向进行了展望。 |
| 关键词: 形式化验证 错误定位 布尔可满足性 可满足性模 |
| DOI：10.11887/j.cn.201402014 |
| 投稿日期：2013-06-18 |
| 基金项目:国家自然科学基金资助项目（61103083,61133007）；国家“863”高技术研究发展计划资助项目(2012AA01A301) |
|
| Research advances in SAT-based error localization methods on circuits |
| ZHANG Jianmin, LI Tiejun, ZHANG Jun, LI Sikun |
|
(College of Computer, National University of Defense Technology, Changsha 410073, China)
|
| Abstract: |
| With the growing complexity of VLSI designs, functional verification and debugging has become a resource-intensive bottleneck in modern CAD flows, consuming as much as 60% of the total design cycle. Error localization in circuits is difficult and time-consuming. Therefore an efficient error debugging and localization method is necessary for hardware design. Recently there are many different contributions to research on error localization in circuits. Firstly, the categories and workflow of error debugging method were introduced. The fundamental principles of SAT-based error localization method were described. Then the existing algorithms were introduced and analyzed. Furthermore, the research results about extract unsatisfiable subformulae, which can strongly improve the efficiency and accuracy of error localization, were presented. Finally, the current challenges were discussed, and the future research directions of error localization in circuits were outlined. |
| Keywords: formal verification error localization boolean satisfiability satisfiability modulo theories |
|
|
|
|
|
