Formal Verification of Automatic Circuit Transformations for Fault-Tolerance

Autor: Dmitry Burlyaev, Pascal Fradet
Přispěvatelé: Sound Programming of Adaptive Dependable Embedded Systems (SPADES), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)
Jazyk: angličtina
Rok vydání: 2015
Předmět:
[INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR]
Correctness
Digital circuit transformations
ACM: B.: Hardware/B.7: INTEGRATED CIRCUITS/B.7.3: Reliability and Testing/B.7.3.2: Redundant design
Semantics (computer science)
Computer science
ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.2: Language Classifications/D.3.2.0: Applicative (functional) languages
Hardware_PERFORMANCEANDRELIABILITY
02 engineering and technology
computer.software_genre
Formal proof
ACM: B.: Hardware/B.7: INTEGRATED CIRCUITS/B.7.2: Design Aids/B.7.2.4: Verification
0202 electrical engineering
electronic engineering
information engineering
Redundancy (engineering)
Coq
ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.2: Correctness proofs
Formal verification
computer.programming_language
060201 languages & linguistics
ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.1: Formal Definitions and Theory/D.3.1.0: Semantics
Fault-Tolerance
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Programming language
Hardware description language
Proof assistant
Fault tolerance
06 humanities and the arts
Formal proofs
0602 languages and literature
020201 artificial intelligence & image processing
computer
Zdroj: Formal Methods in Computer-Aided Design (FMCAD 2015)
Formal Methods in Computer-Aided Design (FMCAD 2015), Sep 2015, Austin, Texas, United States
FMCAD
Popis: International audience; 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 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.
Databáze: OpenAIRE
Externí odkaz: