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

一种基于SAT的运算电路查错方法 被引量：4

A SAT-Based Arithmetic Circuit Bug-Hunting Method
下载PDF
导出
摘要 基于SAT的运算电路查错方法将被验证系统中系统规范成立与否的问题转换为布尔公式和数学公式的混合形式E-CNF,通过采用了标志子句技术的E-SAT求解器进行求解.实验表明该方法自动化程度高,能处理大规模的运算电路,有较强的查找错误能力. 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.
作者 陈云霁 张健 沈海华 胡伟武
机构地区 中国科学院计算技术研究所计算机系统结构重点实验室 中国科学院软件研究所计算机科学国家重点实验室
出处 《计算机学报》 EI CSCD 北大核心 2007年第12期2082-2089,共8页 Chinese Journal of Computers
基金 国家"九七三"重点基础研究发展规划项目基金(2005CB321600) 国家"八六三"高技术研究发展计划项目基金(2002AA110010 2005AA119020 2005AA110010) 中国科学院知识创新工程重大项目基金"高性能通用CPU芯片研制"(KGCX1-SW-09) 国家自然科学基金(60603049 60673044)资助~~
关键词 形式验证 模型检验 SAT E—CNF 标志子句 Formal verification SAT E-CNF Tag clause
分类号 TP301 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献15

  • 1McMillan K. Symbolic model checking: An approach to the state explosion problem[Ph. D. dissertation]. Pittsburgh, PA, USA: Carnegie Mellon University, 1992
  • 2Biere A, Cimatti A, Clarke E, Zhu Y. Symbolic model checking without BDDs//Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of System, LNCS 1579, 1999:193-207
  • 3Clarke E M, Khaira M, Zhao X. Word level model checking-Avoiding the pentium FDIV error//Proceedings of the 33rd ACM/IEEE Design Automation Conference. Las Vegas, Nevada, USA, 1996:645-648
  • 4Bryant R E, Chen Y A. Verification of arithmetic functions with binary moment diagrams//Proceedings of the 32nd ACM/IEEE Design Automation Conference. San Francisco, California, USA, 1995: 535-541
  • 5Clarke E M, Fujita M, Zhao X. Hybrid decision diagrams: Overcoming the limitations of MTBDDs and BMDs//Proceedings of the 1995 IEEE International Conference on Computer Aided Design. San Jose, California, USA, 1995: 159- 163
  • 6Chen Y A, Bryant R E. *PHDD: An efficient graph representation for floating point circuit verification//Proceedings of the 1997 International Conference on Computer Aided Design. San Jose, California, USA, 1997:2-7
  • 7Chen Y A, Bryant R E. ACV: An arithmetic circuit verifier//Proceedings of the 1996 International Conference on Computer Aided Design. San Jose, California, USA, 1996: 361-365
  • 8Audemard Gilles, Bertoli Piergiorgio, Cimatti Alessandro, Kornilowicz Artur, Sebastiani Roberto. Integrating Boolean and mathematical solving: Foundations, basic algorithms,and requirements//Proceedings of the Artificial Intelligence, Automated Reasoning, and Symbolic Computation. Marseille, France, 2002: 231-245
  • 9Zhang Jian, Wang Xiao-Xu. A constraint solver and its application to path feasibility analysis. International Journal of Software Engineering and Knowledge Engineering, 2001, 11 (2) : 139-156
  • 10季晓慧,黄拙,张健.约束求解与优化技术的结合[J].计算机学报,2005,28(11):1790-1797. 被引量：9

二级参考文献1

共引文献8

同被引文献145

  • 1黄杰,陈琳,邹鹏.一种求解极小诊断的遗传模拟退火算法[J].软件学报,2004,15(9):1345-1350. 被引量：22
  • 2栾尚敏,戴国忠.利用结构信息的故障诊断方法[J].计算机学报,2005,28(5):801-808. 被引量：24
  • 3朱丹,李暾,郭阳,李思昆.微处理器体系结构级测试程序自动生成技术[J].软件学报,2005,16(12):2172-2180. 被引量：7
  • 4易江芳,佟冬,程旭.使用贝叶斯网络的高效模拟矢量生成方法[J].计算机辅助设计与图形学学报,2007,19(5):616-621. 被引量：7
  • 5Josephson D. The good, the bad, and the ugly of silicon debug [C] //Proc of Design Automation Conference 2006. New York: ACM, 2006:3-6.
  • 6Paniccia M, Eiles T M, Rao V R M, et al. Novel optical probing technique for flip chip packaged microprocessors [C]//Proc of Int Test Conf 1998. Piscataway, NJ: IEEE, 1998: 740-747.
  • 7Rowlette J A, Eiles T M. Critical timing analysis in microprocessors using near-IR laser assisted device alteration (LADA)[C] //Proc of Int Test Conf 2003. Piscataway, NJ: IEEE, 2003: 264-273.
  • 8Knebel D, Sanda P, Manus M M C, et al. Diagnosis and characterization of timing-related defects by time-dependent light emission [C] //Proc of Int Test Conf 1998. Piscataway, NJ: IEEE, 1998: 733-739.
  • 9Livengood R H, Medeiros D. Design for (physical) debug for silicon microsurgery and probing of flip-chip packaged integrated circuits [C] //Proc of Int Test Conf 1999. Piscataway, NJ: IEEE, 1999:877-882.
  • 10Josephson D D. The manic depression of microprocessor debug[C]//Proc of Int Test Conf 2002. Piscataway, NJ: IEEE, 2002:657-663.

引证文献4

二级引证文献18

计算机学报
2007年 第12期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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