Skip to Main content Skip to Navigation
Conference papers

Formal Verification of Automatic Circuit Transformations for Fault-Tolerance

Dmitry Burlyaev 1 Pascal Fradet 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 language-based approach to certify fault-tolerance techniques for digital circuits. Circuits are expressed in a gate-level Hardware Description Language (HDL), fault-tolerance techniques are described as automatic circuit transformations in that language, and fault-models are specified as particular semantics of the HDL. These elements are formalized in the Coq proof assistant and the properties, ensuring that for all circuits their transformed version masks all faults of the considered fault-model, can be expressed and proved. In this article, we consider Single-Event Transients (SETs) and faultmodels of the form “at most 1 SET within k clock cycles”. The primary motivation of this work was to certify the Double-Time Redundant Transformation (DTR), a new technique proposed recently. The DTR transformation combines double-time redundancy, micro-checkpointing, rollback, several execution modes and input/output buffers. That intricacy requested a formal proof to make sure that no single-point of failure existed. The correctness of DTR as well as two other transformations for fault-tolerance (TMR & TTR) have been proved in Coq.
Complete list of metadata
Contributor : Pascal Fradet <>
Submitted on : Friday, January 8, 2016 - 4:39:14 PM
Last modification on : Monday, February 15, 2021 - 3:52:02 PM


  • HAL Id : hal-01253127, version 1



Dmitry Burlyaev, Pascal Fradet. Formal Verification of Automatic Circuit Transformations for Fault-Tolerance. Formal Methods in Computer-Aided Design (FMCAD 2015), Sep 2015, Austin, Texas, United States. ⟨hal-01253127⟩



Record views