  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.
