Formal Verification of Automatic Circuit Transformations for Fault-Tolerance

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.
Type de document :
Communication dans un congrès
Formal Methods in Computer-Aided Design (FMCAD 2015), Sep 2015, Austin, Texas, United States
Liste complète des métadonnées

https://hal.inria.fr/hal-01253127
Contributeur : Pascal Fradet <>
Soumis le : vendredi 8 janvier 2016 - 16:39:14
Dernière modification le : samedi 9 janvier 2016 - 01:07:17

Identifiants

  • HAL Id : hal-01253127, version 1

Collections

Citation

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>

Partager

Métriques

Consultations de la notice

130