期刊文献+

电路宽度制导的布尔推理 被引量:3

Circuit-Width Directed Boolean Reasoning
下载PDF
导出
摘要 在基于逻辑电路的布尔推理过程中 ,经常用到二叉判决图 (BDD)与布尔可满足性 (SAT)相结合的算法 由于电路宽度能很好地反映电路的复杂性 ,提出了一种基于电路宽度的启发式策略 ,根据电路宽度来实现SAT算法与BDD算法的交替 充分发挥两者的优势 ,不仅可以防止因构造BDD可能导致的内存爆炸 ,而且还能避免SAT算法可能遇到的超时现象 与以往同类策略相比 ,该启发式策略更节省计算资源 ,提高算法性能 针对组合电路的测试产生实验 。 Binary decision diagram (BDD) and Boolean satisfiability (SAT) are common techniques of logic circuit-based Boolean reasoning scheme Since circuit-width is a good measure of circuit complexity, in this paper, we present a circuit-width based heuristic, which can be used to integrate the BDD technique and SAT technique for Boolean reasoning The scheme switches one engine to another in terms of the circuit-width, thus it takes both advantages of these two engines The circuit-width directed Boolean reasoning algorithm avoids the potential memory explosion caused by constructing the BDDs, and also prevents from the time-outs phenomenon of SAT techniques In comparison with the previous heuristic schemes in literature, the new schemes can save more computational resources, and improve the performance of Boolean reasoning algorithms On the automatic test pattern generation of combinational circuits, the experimental results demonstrate that the proposed heuristic scheme can be applied in Boolean reasoning effectively
出处 《计算机辅助设计与图形学学报》 EI CSCD 北大核心 2004年第11期1568-1574,共7页 Journal of Computer-Aided Design & Computer Graphics
基金 国家自然科学基金重点项目 ( 90 2 0 70 0 2 ) 北京市重点科技项目 (H0 2 0 12 0 12 0 13 0 ) 浙江省自然科学基金项目 (M60 3 0 97)资助
关键词 电路宽度 布尔推理 二叉判决图 布尔可满足性 测试产生 circuit width Boolean reasoning binary decision diagram Boolean satisfiability test generation
  • 相关文献

参考文献16

  • 1Hassoun Soha, Sasao Tsutomu, Brayton R K. Logic Synthesis and Verification [M]. Boston/Dordrecht/London: Kluwer Academic Publishers, 2002
  • 2Larrabee Tracy. Test pattern generation using Boolean satisfiability [J]. IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems, 1995, 14(1): 4~15
  • 3Stephan P, Brayton R K, Sangiovanni-Vincenteli A. Combinational test generation using satisfiability [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1996, 15(9): 1167~1176
  • 4Prasad Mukul R, Chong Philip, Keutzer Kurt. Why is ATPG easy [A]. In: Proceedings of the Design Automatic Conference, New Orleans, 1999. 22~28
  • 5Stanion Robert T, Bhattacharya Debashis, Sechen Carl. An efficient method for generating exhaustive test sets [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1995, 14(12): 1516~1525
  • 6Paruthi V, Kuehlmann A. Equivalence checking combining a structural SAT-solver, BDDs, and simulation [A]. In: Proceedings of the International Conference on Computer Design: VLSI in Computers & Processors, Austin, 2000. 459~464
  • 7Brand D. Verification of large synthesized designs [A]. In: Proceedings of the International Conference of Computer-Aided Design, San Jose, 1993. 534~537
  • 8Burch J R, Singhal V. Tight integration of combinational verification methods [A]. In: Proceedings of IEEE/ACM International Conference on Computer-Aided Design, San Jose, 1998. 570~576
  • 9Goldberg E I, Prasad M R, Brayton R K. Using SAT for combinational equivalence checking [A]. In: Proceedings of the IEEE Design Automation, Test in Europe, Munich, 2001. 114~121
  • 10Reda Sherief, Salem Ashraf. Combinational equivalence checking using Boolean satisfiability and binary decision diagrams [A]. In: IEEE Proceedings of the Design Automation, Test in Europe, Munich, 2001. 122~126

二级参考文献15

  • 1Tracy Larrabee.Test pattern generation using Boolean satisfiability.IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems,1995,14( 1 ):4~ 15
  • 2Robert T Stanion,Debashis Bhattacharya,Carl Sechen.An efficient method for generating exhaustive test sets.IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems,1995,14(12):1516~1525
  • 3P Stephan,R K Brayton,A Sangiovanni-Vincenteli.Combinational test generation using satisfiability.IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems,1996,15(9):1167~1176
  • 4Emil Gizdaraki,Hidio Fujiwara.SPIRIT:A highly robust combinational test generation algorithm.IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems,2002,21(12):1446~1458
  • 5Randal E Bryant.Graph-based algorithms for Boolean function manipulation.IEEE Trans on Computers,1986,35(8):677~691
  • 6J Kim et al.On applying incremental satisfiability to delay fault testing.In:Proc of IEEE/ACM Design,Automation and Test in Europe Conference.Paris:ACM Press,2000.380~384
  • 7D Brand.Verification of large synthesized designs.In:Proc of Int'l Conf on Computer-Aided Design.San Joes:IEEE Press,1993.534~537
  • 8C Leonard Berman.Circuit width,register allocation,and ordered binary decision diagrams.IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems,1991,10(8):1059~1066
  • 9Mukul R Prasad,Philip Chong,Kurt Keutzer.Why is ATPG easy ? In:Proc of the Design Automatic Conference.New Orleans:ACM Press,1999.22~28
  • 10F Somenzi.CUDD:CU Decision Diagram Package.Release 2.3.1 [ CP],Boulder:University of Colorado,2001

共引文献4

同被引文献81

引证文献3

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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