期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

基于SAT的电路错误定位方法研究进展

Research advances in SAT-based error localization methods on circuits
在线阅读 下载PDF
导出
摘要 随着VLSI芯片复杂度不断增加,功能验证与调试已占到整个芯片设计周期的60%以上。而错误的定位往往消耗大量的时间与精力,因此迫切需要一种高效的方法诊断与定位电路中的错误。针对近年来出现的许多电路错误定位方法,介绍了电路错误诊断方法的分类与工作流程,深入分析了基于SAT的错误定位方法的基本原理;对各种算法进行了概述评论,并简要介绍了在不可满足子式求解方面所做的一些研究工作,而不可满足子式能够显著提高错误定位效率与精度;讨论了电路错误定位技术所面临的主要挑战,并对今后的研究方向进行了展望。 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 SATbased 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.
作者 张建民 黎铁军 张峻 李思昆
机构地区 国防科技大学计算机学院
出处 《国防科技大学学报》 EI CAS CSCD 北大核心 2014年第2期81-86,共6页 Journal of National University of Defense Technology
基金 国家自然科学基金资助项目(61103083 61133007) 国家"863"高技术研究发展计划资助项目(2012AA01A301)
关键词 形式化验证 错误定位 布尔可满足性 可满足性模 formal verification error localization boolean satisfiability satisfiability modulo theories
分类号 TP391 [自动化与计算机技术—计算机应用技术]
  • 相关文献

参考文献28

  • 1Bose P, Albonesi D H, Mareulescu D. vip editors' introduction: power and complexity aware design [ J ]. IEEE Micro, 2003, 23 (5) : 8 - 11.
  • 2Kumar N, Kumar V, Viswanathan M. On the complexity of error explanation [ C ]//Proceedings of VMCAI' 05, 2005 : 448 -464.
  • 3Smith A, Veneris A, Ali M F, et al. Fault diagnosis and logic debugging using Boolean satisfiability[ J ]. IEEE Transaction on CAD, 2005, 24(10) : 1606 -1621.
  • 4Larrabee T. Test pattern generation using Boolean satisability[J]. IEEE Transaction on CAD, 1992, 11 (1) : 4 -15.
  • 5Veneris A, Abadir M S, Amiri M. Design rewiring using ATPG[J]. IEEE Transaction on CAD, 2002, 21 (12) : 1469 - 1479.
  • 6Ali M F, Venefs A, Safarpour S, et al. Debugging sequential circuits using Boolean satisfiability [ C ]//Proceedings of ICCAD' 04, 2004 : 204 - 209.
  • 7Smith A, Veneris A, Viglas A. Design diagnosis using Boolean satisfiability[ C]//Proceedings of ASP - DAC ' 04, 2004 : 218 - 223.
  • 8Ali M F, Safarpour S, Veneris A, et al. Post-verification debugging of hierarchical designs [ C ]//Proceedings of ICCAD' 05, 2005 : 871 - 876.
  • 9Fey G, Safarpour S, Veneris A, et al. On the relation between simulation-based and SAT-based diagnosis [ C ]//Proceedings of DATE'06, 2006:1139 - 1144.
  • 10Safarpour S, Liffiton M H, Mangassarian H, et al. Improved design debugging using maximum satisfiability [ C ]// Proceedings of FMCAD'07, 2007 : 13 - 19.

二级参考文献28

  • 1Huang Shi-Yu, Cheng Kwang-Ting. Formal equivalence checking and design debugging [M]. Boston/Dordrecht/London: Kluwer Academic Publishers, 1998
  • 2Chung Pi-Yu, Wang Yi-Min, Hajj lbrahim N. Logic design error diagnosis and correction [J]. IEEE Transactions on VLSI Systems, 1994, 2(3) : 320-332
  • 3Huang Shi-Yu, Cheng Kwang-Ting. ErrorTracer: design error diagnosis based on fault simulation techniques [J]. IEEE Transactions on Computer-Aided Design, 1999,18(9) : 13411352
  • 4Brand D, Drumm A, Kundu S, et al. Incremental synthesis[C] //Proceedings of International Conference on Computer-Aided Design, San Jose, 1994:14-18
  • 5Veneris A, Hajj 1 N. Design error diagnosis and correction via test vector simulation [J]. IEEE Transactions on Computer-Aided Design, 1999, 18(12): 1803 1816
  • 6Abadir M S, Ferguson J, Kirkland T E. Logic verification via test generation [J]. IEEE Transactions on Computer-Aided Design, 1988, 7(1) : 138-148
  • 7Aitken R C. Modeling the unmodelable: algorithmic fault diagnosis[J]. IEEE Design & Test of Computers. 1997, 14(3) : 98-103
  • 8Liu J B, Veneris A. Incremental fault diagnosis [J]. IEEE Transactions on Computer-Aided Design, 2005, 24 (2) : 240 -251
  • 9Cook S A. The complexity of theorem-proving procedure [C]//Proceedings of the 3rd ACM Symposium on Theory of Computing, New York, 1971:151-158
  • 10Smith A, Veneris A, All M F, et al. Fault Diagnosis and Logic Debugging Using Boolean Satisfiability [J]. IEEE Transactions on Computer-Aided Design, 2005, 24(10): 1606-1621

共引文献1

国防科技大学学报
2014年 第2期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部