A static analysis for the minimization of voters in fault-tolerant circuits

Dmitry Burlyaev 1 Pascal Fradet 1 Alain Girault 1
1 SPADES - Sound Programming of Adaptive Dependable Embedded Systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : We present a formal approach to minimize the number of voters in triple-modular redundant (TMR) sequential circuits. Our technique actually works on a single copy of the TMR circuit and considers a large class of fault models of the form ``at most 1 SEU or SET every k clock cycles''. Verification-based voter minimization guarantees that the resulting TMR circuit (i) is fault tolerant to the soft-errors defined by the fault model and (ii) is functionally equivalent to the initial TMR circuit. Our approach operates at the logic level and takes into account the input and output interface specifications of the circuit. Its implementation makes use of graph traversal algorithms, fixed-point iterations, and binary decision diagrams (BDD). Experimental results on the ITC'99 benchmark suite indicate that our method significantly decreases the number of inserted voters, yielding a hardware reduction of up to 55% and a clock frequency increase of up to35% compared to full TMR.
Complete list of metadatas

Cited literature [42 references]  Display  Hide  Download

https://hal.inria.fr/hal-01417164
Contributor : Pascal Fradet <>
Submitted on : Thursday, December 15, 2016 - 12:47:41 PM
Last modification on : Thursday, October 11, 2018 - 8:48:04 AM
Long-term archiving on : Thursday, March 16, 2017 - 6:44:34 PM

File

RR-9004.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01417164, version 1

Citation

Dmitry Burlyaev, Pascal Fradet, Alain Girault. A static analysis for the minimization of voters in fault-tolerant circuits. [Research Report] RR-9004, Inria - Research Centre Grenoble – Rhône-Alpes. 2016, pp.1-27. ⟨hal-01417164⟩

Share

Metrics

Record views

244

Files downloads

223