This development gathers the following Coq folders:
- Common/ defining the syntax and semantics of LDDL, a core hardware description language with dependent types;
- TMR/ defining and proving the correctness of the triple modular redundancy transformation on LDDL. We use full TMR i.e., with a triplicated voter after each cell;
- TTR/ defining and proving the correctness of the triple time redundancy transformation on LDDL. It is a simplified version (only mode 3) of the DyTR3 transformation described in our AHS’15 paper;
- DTR/ defining and proving the correctness of the double time redundancy transformation on LDDL. This transformation is described in our FPGA’15 paper.
- SEMT/ defining and proving the correctness of an adaptation of full TMR to tolerate SEMTs. (available starting from the Coq v8.13 version).
Each transformation needs and imports Common. The proof of DTR also imports TMR which is used in DTR to protect a small control circuit.
The whole development can be dowloaded for Coq v8.4 (LDDL8.4), Coq v8.5 (LDDL8.5), Coq v8.9 (LDDL8.9) or Coq v8.13 (LDDL8.13).
