Dependability modeling and optimization of triple modular redundancy partitioning for SRAM-based FPGAs. (February 2019)

• Record Type: Journal Article
• Authors: Hoque, Khaza Anuarul; Ait Mohamed, Otmane; Savaria, Yvon
• Is Part Of: Reliability engineering & system safety. Volume 182(2019)
• Page Start: 107
• Page End: 119
• Publication Date: 2019-02
• Subjects: Single event upset -- Multiple-cell upset -- Triple modular redundancy -- Formal verification -- FPGAs -- TMR partitioning.; Reliability (Engineering) -- Periodicals; System safety -- Periodicals; Industrial safety -- Periodicals; Fiabilité -- Périodiques; Sécurité des systèmes -- Périodiques; Sécurité du travail -- Périodiques; 620.00452
• DOI: 10.1016/j.ress.2018.10.011
• Languages: English
• ISSNs: 0951-8320

Abstract

Highlights: We propose a methodology for early trade-off assessment of TMR partitioning with periodic blind scrubbing. The proposed formal models (using the CTMC formalism) of partitioned-TMR systems captures both single-cell upsets and multi-cell upsets irrespective of the partition size (equal/non-equal sized partitions). Our analysis shows that increasing the number of TMR partitions increases the reliability and availability if the voter is failure-free. However, when a voter is prone to failure, increasing only the number of partitions does not help anymore. By applying the proposed methodology, it is possible to identify the required number of partitions in such cases. Abstract: SRAM-based FPGAs are popular in the aerospace industry for their field programmability and low cost. However, they suffer from cosmic radiation-induced Single Event Upsets (SEUs). Triple Modular Redundancy (TMR) is a well-known technique to mitigate SEUs in FPGAs that is often used with another SEU mitigation technique known as configuration scrubbing. Traditional TMR provides protection against a single fault at a time, while partitioned TMR provides improved reliability and availability. In this paper, we present a methodology to analyze TMR partitioning at early design stage using probabilistic model checking. The proposed formal model can capture both single and multiple-cell upset scenarios, regardless of any assumption of equal partition sizes. Starting with a high-level description of a design, a Markov model is constructed from the Data Flow Graph (DFG) using a specified number of partitions, a component characterization library and a user defined scrub rate. Such a model and exhaustive analysis captures all the considered failures and repairs possible in the system within the radiation environment. Various reliability and availability properties are then verified automatically using the PRISM model checker exploring the relationship between the scrub frequency and the number of TMR partitions required to meet the design requirements. Also, the reported results show that based on a known voter failure rate, it is possible to find an optimal number of partitions at early design stages using our proposed method.