计算机科学 ›› 2019, Vol. 46 ›› Issue (4): 309-314.doi: 10.11896/j.issn.1002-137X.2019.04.048

• 交叉与前沿 • 上一篇    下一篇

一种基于SAT求解器的组合电路重汇聚现象分析方法

张璐婕, 刘畅, 张龙, 郭阳   

  1. 国防科技大学计算机学院 长沙410073
  • 收稿日期:2018-06-11 出版日期:2019-04-15 发布日期:2019-04-23
  • 通讯作者: 郭 阳(1971-),男,博士,研究员,博士生导师,CCF高级会员,主要研究方向为微处理器设计与验证技术,E-mail:guoyang@nudt.edu.cn(通信作者)
  • 作者简介:张璐婕(1996-),女,硕士生,主要研究方向为集成电路设计;刘 畅(1988-),男,博士生,主要研究方向为集成电路设计;张 龙(1987-),男,博士,主要研究方向为集成电路设计;
  • 基金资助:
    本文受国家自然科学基金项目(61872136,61772540)资助。

Reconvergence Phenomena Analysis Method in Combinational Circuits Based on SAT Solver

ZHANG Lu-jie, LIU Chang, ZHANG Long, GUO Yang   

  1. College of Computer,National University of Defense Technology,Changsha 410073,China
  • Received:2018-06-11 Online:2019-04-15 Published:2019-04-23

摘要: 为了研究组合电路重汇聚现象,提出了一种基于SAT求解器的分析方法。通过深度优先搜索算法,确定瞬态脉冲产生节点和输出节点之间的所有路径;建立待检查列表,对表中的元素施加敏化约束条件,并采用SAT求解器求解元素可满足性;最后判断是否存在满足条件的输入向量,使瞬态脉冲通过不同路径在输出节点发生重汇聚。所提方法可以有效地对较大规模组合电路进行分析,采用EPFL 和ISCAS’85作为测试集,实验结果表明,ISCAS’85测试集中约有一半节点处产生的瞬态脉冲能够发生重汇聚,这一比例明显高于EPFL测试集,因此不同类型功能电路重汇聚现象的发生率存在较大差异。

关键词: SAT求解器, 敏化路径, 输入向量, 瞬态脉冲, 重汇聚, 组合电路

Abstract: In order to study reconvergence phenomena of combinational circuits,this paper proposed an analysis method based on SAT solver.All paths between transient pulses generation nodes and output nodes are confirmed by depth-first search algorithm.Elements in the check-list are imposed with sensitization constraints,and elements satisfaction is judged by Minisat.Finally,whether there are input vectors satisfying the conditions so that the transient pulse reconverge at the output node through different paths or not are determined.The proposed method can analyze reconvergence phenomena of large-scale combinational circuits effectively.EPFL and ISCAS’85 were used as test sets.The experimental results show that transient pulses generated by certain nodes,which are about half of the total nodes of the ISCAS’85 test set,can reconverge finally.The ratio is significantly higher than that of the EPFL test set.Therefore,there is a significant difference of the occurrence rate of reconvergence for different types of functional circuits.

Key words: Combinational circuit, Input vector, Reconvergence, SAT solver, Sensitization path, Transient pulse

中图分类号: 

  • TP391.41
[1]LIU B,CHEN S,LIANG B,et al.The Effect of Re-Convergence on SER Estimation in Combinational Circuits.IEEE Tran-sactions on Nuclear Science,2009,56(6):3122-3129.
[2]RATIU I M,PEDERSON D O.VICTOR:A Fast VLSI Testability Analysis Program[C]∥International Test Conference 1982,Philadelphia,Pa,Usa,November.DBLP,1982:397-403.
[3]LIU B,CHEN S,XIAO H.Analysis of Glitch Reconvergence in Combinational Logic SER Estimation[C]∥Second Asia International Conference on Modelling & Simulation.IEEE Computer Society,2008:1015-1020.
[4]ZHANG B,WANG W S,ORSHANSKY M.FASER:fast analysis of soft error susceptibility for cell-based designs[C]∥International Symposium on Quality Electronic Design.IEEE,2006:755-760.
[5]YOSHIDA S ,MATSUKAWA G ,IZUMI S ,et al.An soft error propagation analysis considering logical masking effect on re-convergent path[C]∥IEEE International Symposium on On-line Testing & Robust System Design.IEEE,2016:13-16.
[6]MOHANRAM K,TOUBA N A.Cost-effective approach for reducing soft error failure rate in logic circuits[C]∥Test Confe-rence,2003(ITC 2003).International.IEEE,2003:893-901.
[7]ZHANG B,WANG W S,ORSHANSKY M.FASER:Fast analysis of soft error susceptibility for cell-based designs∥7th International Symposium on Quality Electronic Design,2006(ISQED’06).IEEE,2006:740-760.
[8]MING Z,SHANBHAG N R.Soft-Error-Rate-Analysis (SERA) Methodology.IEEE/ACM International Conference on Computer and Adided Design,2006,25(10):2140-2155.
[9]HUANG Z,ZHANG J.Generating SAT Instances from First- Order Formulas.Journal of Software,2005,16(3):327-335.
[10]GUO Y,ZHANG C S,ZHANG B,et al.Research Progress of Algorithms for Solving SAT Problem.Computer Science,2016,43(3):8-17.(in Chinese) 郭莹,张长胜,张斌.求解SAT问题的算法的研究进展.计算机科学,2016,43(3):8-17.
[11]MA K F,XIAO L Q,ZHANG J M,et al.Research and Development of SAT Solving Algorithm Based on Hardware Programmable Logic.Computer Engineering and Science,2016,38(4):634-639.(in Chinese) 马柯帆,肖立权,张建民,等.基于硬件可编程逻辑的SAT求解算法研究与进展.计算机工程与科学,2016,38(4):634-639.
[12]WANG R,LIU W,LI T,et al.Bounded model checking of ETL cooperating with finite and looping automata connectives.Journal of Applied Mathematics,2013,2013(2013):1-12.
[13]BRADLEY A R.SAT-based model checking without unrolling ∥International Workshop on Verification,Model Checking,and Abstract Interpretation.Springer,Berlin,Heidelberg,2011:70-87.
[14]WU G,CHEN Q,CAO F,et al.Parallel hybrid genetic algorithm for SAT problems based on OpenMP[C]∥International Conference on Intelligent Systems and Knowledge Engineering.2017:1-5.
[15]DAVIS M,LOGEMANN G,LOVELAND D.A Machine Pro- gram for Theorem-proving.Communications of the Acm,1962,5(5):394-397.
[16]DAVIS M.A Computing Procedure for Quantification Theory.Journal of the Acm,1960,7(3):201-215.
[17]SORENSSON N,EEN N.Minisat v1.13-a sat solver with conflict-clause minimization.SAT,2005,2005(53):1-2.
[18]BRYANT R E.Graph-based algorithms for boolean function manipulation.IEEE Transactions on Computers,1986,100(8):677-691.
[19]WU S X.Dual Logic Power Optimization Technology Based on AIG.Wireless Communication Technology,2017,26(3):43-47.(in Chinese) 吴世雄.基于AIG的双逻辑功耗优化技术.无线通信技术,2017,26(3):43-47.
[1] 李绍荣 徐玉婷.
基于BDD的组合电路等价性检验

计算机科学, 2007, 34(3): 293-294.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!