diff options
Diffstat (limited to 'src/hls/Veriloggenproof.v')
| -rw-r--r-- | src/hls/Veriloggenproof.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 90cf4cb..d1494ec 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -241,7 +241,7 @@ Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. Lemma mod_st_equiv m : mod_st (transl_module m) = HTL.mod_st m. Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. -(*Lemma mod_stk_equiv m : mod_stk (transl_module m) = HTL.mod_stk m. +Lemma mod_stk_equiv m : mod_stk (transl_module m) = HTL.mod_stk m. Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. Lemma mod_stk_len_equiv m : mod_stk_len (transl_module m) = HTL.mod_stk_len m. @@ -335,7 +335,7 @@ Proof. Qed. -*)Section CORRECTNESS. +Section CORRECTNESS. Variable prog: HTL.program. Variable tprog: program. @@ -345,7 +345,7 @@ Qed. Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. Let tge : genv := Globalenvs.Genv.globalenv tprog. -(* Lemma symbols_preserved: + Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed. #[local] Hint Resolve symbols_preserved : verilogproof. @@ -532,13 +532,13 @@ Qed. Proof. intros. inv H0. inv H. inv H3. constructor. reflexivity. Qed. - #[local] Hint Resolve transl_final_states : verilogproof.*) + #[local] Hint Resolve transl_final_states : verilogproof. Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). Proof. eapply Smallstep.forward_simulation_plus; eauto with verilogproof. - (*apply senv_preserved. - Qed.*) Admitted. + apply senv_preserved. + Qed. End CORRECTNESS. |