diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-18 12:06:57 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-18 12:06:57 +0100 |
| commit | 92188c18a3761fa14dfdb97010cebe919548a010 (patch) | |
| tree | cd65e3ecf1dd3678200aeeb8edd8dae9b40228ed /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 2636b70dc48752ce21221c1fcf18c7a83086171d (diff) | |
| download | compcert-kvx-92188c18a3761fa14dfdb97010cebe919548a010.tar.gz compcert-kvx-92188c18a3761fa14dfdb97010cebe919548a010.zip | |
Idée de preuve VLIW
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 23 |
1 files changed, 21 insertions, 2 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 2e463f18..7d6d9a7a 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -658,8 +658,8 @@ Proof. eapply external_call_symbols_preserved; eauto. apply senv_preserved. Qed. -Theorem transf_program_correct: - forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog). (* FIXME a remplacer par Asmvliw.semantics tprog *) +Theorem transf_program_correct_Asmblock: + forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog). Proof. eapply forward_simulation_plus. - apply senv_preserved. @@ -668,4 +668,23 @@ Proof. - apply transf_step_correct. Qed. +(* TODO: +Require Import Asmvliw. + +Theorem transf_program_correct: + forward_simulation (Asmblock.semantics tprog) (Asmvliw.semantics tprog). +Proof. + eapply forward_simulation_one_one. (* FIXME *) +Admitted. + +Theorem transf_program_correct: + forward_simulation (Asmblock.semantics prog) (Asmvliw.semantics tprog). +Proof. + eapply forward_simulation_compose. (* FIXME *) +Admitted. + +*) + + + End PRESERVATION. |