Formal Verification of Automatic Circuit Transformations for Fault-Tolerance

International audienceWe 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 thatfor 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 aformal proof to make sure that no single-point of failure existed. The correctness of DTR as well as two other transformations forfault-tolerance (TMR & TTR) have been proved in Coq