DROPS

Document

A Static Analysis for the Minimization of Voters in Fault-Tolerant Circuits

Authors: Dmitry Burlyaev, Pascal Fradet, and Alain Girault

Published in: LITES, Volume 5, Issue 1 (2018). Leibniz Transactions on Embedded Systems, Volume 5, Issue 1

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 mo dels of the form “at most 1 Single-Event Upset (SEU) or Single-Event Transient (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 to 35% compared to full TMR. As our experiments show, if the SEU fault-model is replaced with the stricter fault-model of SET, it has a minor impact on the number of removed voters. On the other hand, BDD-based modelling of SET effects represents a more complex task than the modelling of an SEU as a bit-flip. We propose solutions for this task and explain the nature of encountered problems. We address scalability issues arising from formal verification with approximations and assess their efficiency and precision.

Cite as

Dmitry Burlyaev, Pascal Fradet, and Alain Girault. A Static Analysis for the Minimization of Voters in Fault-Tolerant Circuits. In LITES, Volume 5, Issue 1 (2018). Leibniz Transactions on Embedded Systems, Volume 5, Issue 1, pp. 04:1-04:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{burlyaev_et_al:LITES-v005-i001-a004,
  author =	{Burlyaev, Dmitry and Fradet, Pascal and Girault, Alain},
  title =	{{A Static Analysis for the Minimization of Voters in Fault-Tolerant Circuits}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{04:1--04:26},
  ISSN =	{2199-2002},
  year =	{2018},
  volume =	{5},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v005-i001-a004},
  URN =		{urn:nbn:de:0030-drops-192753},
  doi =		{10.4230/LITES-v005-i001-a004},
  annote =	{Keywords: Digital Circuits, Fault-tolerance, Optimization, Static Analysis, Triple Modular Redundancy}
}

Document

DOI: 10.4230/DagRep.3.11.117

Synchronous Programming (Dagstuhl Seminar 13471)

Authors: Stephen A. Edwards, Alain Girault, and Klaus Schneider

Published in: Dagstuhl Reports, Volume 3, Issue 11 (2014)

Abstract

Synchronous programming languages are programming languages with an abstract (logical) notion of time: The execution of such programs is divided into discrete reaction steps, and in each of these reactions steps, the program reads new inputs and reacts by computing corresponding outputs of the considered reaction step. The programs are called synchronous because all outputs are computed together in zero time within a step and because parallel components synchronize their reaction steps by the semantics of the languages. For this reason, the synchronous composition is deterministic, which is a great advantage concerning predictability, verification of system design, and embedded code generation. Starting with the definition of the classic synchronous languages Esterel, Lustre and Signal in the late 1980's, the research during the past 20 years was very fruitful and lead to new languages, compilation techniques, software and hardware architectures, as well as extensions, transformations, and interfaces to other models of computations, in particular to asynchronous and hybrid systems. This report is a summary of the Dagstuhl Seminar 13471 "Synchronous Programming", which took place during November 18-22, 2013, and which was the 20th edition of the yearly workshop of the synchronous programming community. The report contains the abstracts of the presentations given during the seminar in addition to the documents provided by the participants on the web pages of the seminar.

Cite as

Stephen A. Edwards, Alain Girault, and Klaus Schneider. Synchronous Programming (Dagstuhl Seminar 13471). In Dagstuhl Reports, Volume 3, Issue 11, pp. 117-143, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{edwards_et_al:DagRep.3.11.117,
  author =	{Edwards, Stephen A. and Girault, Alain and Schneider, Klaus},
  title =	{{Synchronous Programming (Dagstuhl Seminar 13471)}},
  pages =	{117--143},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{3},
  number =	{11},
  editor =	{Edwards, Stephen A. and Girault, Alain and Schneider, Klaus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.11.117},
  URN =		{urn:nbn:de:0030-drops-44395},
  doi =		{10.4230/DagRep.3.11.117},
  annote =	{Keywords: Synchronous Languages, Hybrid Systems, Formal Verification, Models of Computation, WCET-Analysis, Embedded Systems}
}

Search Results

Documents authored by Girault, Alain

A Static Analysis for the Minimization of Voters in Fault-Tolerant Circuits

Abstract

Cite as

Synchronous Programming (Dagstuhl Seminar 13471)

Abstract

Cite as

Thanks for your feedback!

Could not send message