Computer Science ›› 2019, Vol. 46 ›› Issue (4): 309-314.doi: 10.11896/j.issn.1002-137X.2019.04.048

• Interdiscipline & Frontier • Previous Articles     Next Articles

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

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

CLC Number: 

  • 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] LI Shao-Rong, XU Yu-Ting (College of Opto-electronic Information, UESTC of China, Chengdu 610054). [J]. Computer Science, 2007, 34(3): 293-294.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!