Research On Sequential Equivalence Checking Based System-level Soft Error Reliability Analysis Of Circuits

As technology scales, soft errors induced by various environment problems, such as cosmic radiation and random noise, threaten the system reliability severely. To reach the design goals of reliability, performance, power consumption and area simultaneously, the design can only be protected selectively. For selective protection, reliability evaluation is critical. Circuit's system-level soft error reliability analysis is carried out early in design process, which is more efficient and can provide earlier guidance for soft error tolerance design to avoid reworking. System-level soft error reliability analysis has been the common research focus of the industrial circle and the academy circle.Most of the existing approaches for system-level reliability evaluation of circuits can be classified into two categories: simulation based approaches and formal techniques based approaches. Though simulation based approaches are used most widely, they are incomplete since they cannot cover the input space and fault space completely. Formal techniques based approaches are complete, but most of the conventional approaches based on formal techniques are based on property checking and theorem proving, which both require experience and support from experts. Moreover, theorem proving needs manual intervention.With the advantages in simplicity, ease-of-understanding and ease-of-use out of other formal verification techniques, sequential equivalence checking (SEC) is introduced into the area of circuit's system-level reliability evaluation in this thesis, which focuses on the theory and approaches of SEC-based system-level reliability evaluation. The major innovative achievements are listed as follows:1. A fault propagation characteristics and SEC guided soft error reliability evaluation approach is proposed. For scalability, fault propagation sequential dependence graph (SDG) is advanced to extract the soft error propagation characteristics. In this approach, equivalence checking is localized in the circuit parts affected by soft error propagation. Experimental results indicate that the propose approach not only can locate all the soft error vulnerable spots, but also can check the effectiveness of the protection logics in circuits.2. It is theoretically proved that the circuit's intrinsic immunity to soft errors mainly stems from the circuit components with partial immunity, and that the soft error reliability of a circuit at runtime varies with the input distribution as well as time. These conclusions provide theoretical basis for the research on reliability evaluation approaches which can make full use of circuits'intrinsic immunity to guide selective soft error hardening.3. A run-time soft error reliability sorting approach and an approximated soft error reliability sorting approach are proposed. According to the input distribution and the initial state distribution, the run-time approach can exactly predict the runtime reliability sorting of sequential units by offline analysis, while the approximate approach can help engineers make preliminary vulnerability estimation to make necessary tradeoff between reliability and other design targets even when a good workload estimation of the design is unavailable. Experimental results show that both of the two approaches can guide the deployment of soft error protection mechanisms efficiently, and the runtime approach can achieve higher reliability than the approximate one at the same cost while the approximate approach can analyze lager-scale circuits.4. A two dimensional (2D) decomposition SEC approach is advanced. Here,"2D"means the space dimension and the time dimension. The approach builds verification model for the slice of a single output variable every time first. And during the equivalence checking of the corresponding slices, logic cutpoints are dynamically inserted to split the verification problem in the time dimension. Promising experimental results demonstrate that this approach can reduce the storage explosion of SEC.5. A SEC based Hybrid Soft Error Reliability Analyzer (SEC-SERA) is designed and developed, which integrates all the proposed soft error reliability evaluation approaches including the soft error vulnerable spots selection approach, the runtime soft error reliability sorting approach, the approximate reliability sorting approach, as well as the 2D decomposition SEC approach. The prototype system of SEC-HSERA is applied to analyze the reliability of the decoder in a 32bit embedded microprocessor. Guided by the result from SEC-HSERA, 90.4% error coverage was achieved with extra 22.5% power consumption and 0.59% area.