Application Specified Soft-Error Failure Rate Analysis Using Sequential Equivalence Checking Techniques

作     者：Tun Li Qinhan Yu Hai Wan Sikun Li Tun Li;Qinhan Yu;Hai Wan;Sikun Li

作者机构：School of Computer ScienceNational University of Defense TechnologyChangsha 410073China the Laboratory of Software Engineering for Complex SystemsNational University of Defense TechnologyChangsha 410073China. School of SoftwareTsinghua UniversityBeijing 100084China 

出 版 物：《Tsinghua Science and Technology》 (清华大学学报（自然科学版（英文版）)

年 卷 期：2020年第25卷第1期

页      面：103-116页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：supported by the National Key Basic R&D Program (973) of China (No. 2017YFB1001802) 

主　　题：soft error failure rate analysis Sequential Equivalence Checking(SEC) application specified 

摘      要：Soft errors have become a critical challenge as a result of technology scaling. Existing circuit-hardening techniques are commonly associated with prohibitive overhead of performance, area, and power. However,evaluating the influence of soft errors in Flip-Flops(FFs) on the failure of circuit is a difficult verification ***, we proposed a novel flip-flop soft-error failure rate analysis methodology using a formal method with respect to application behaviors. Approach and optimization techniques to implement the proposed methodology based on the given formula using Sequential Equivalence Checking(SEC) are introduced. The proposed method combines the advantage of formal technique-based approaches in completeness and the advantage of application behaviors in accuracy to differentiate vulnerability of components. As a result, the FFs in a circuit are sorted by their failure rates, and designers can use this information to perform optimal hardening of selected sequential components against soft errors. Experimental results of an implementation of a SpaceWire end node and the largest ISCAS’89 benchmark sequential circuits indicate the feasibility and potential scalability of our approach. A case study on an instruction decoder of a practical 32-bit microprocessor demonstrates the applicability of our method.