From 873162771e87c6c358dc07e58bc0bd3a08f9a00e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 4 Apr 2021 23:07:16 +0100 Subject: Finish Veriloggenproof completely --- src/hls/Memorygen.v | 78 +++++++++++++----- src/hls/Verilog.v | 99 +++++++++++++++++++---- src/hls/Veriloggen.v | 21 +++-- src/hls/Veriloggenproof.v | 198 +++++++++++++++++++++++++++++++++++++++++++--- 4 files changed, 339 insertions(+), 57 deletions(-) diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 99df6d4..87317ef 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -3045,6 +3045,7 @@ Proof. 2: { inv H23. } inv H23. inv H27. simplify. inv H4. 2: { inv H24. } + inv H24. do 2 econstructor. eapply Smallstep.plus_two. econstructor. mgen_crush. mgen_crush. mgen_crush. eassumption. eassumption. econstructor. simplify. econstructor. econstructor. simplify. @@ -3118,6 +3119,27 @@ Proof. { eassumption. } { econstructor. econstructor. simplify. unfold merge_regs. unfold_merge. eapply expr_runp_matches. eassumption. + assert (max_reg_expr x0 + 1 <= max_reg_module m + 1). + { pose proof H2 as X. apply max_reg_stmnt_le_stmnt_tree in X. + apply expr_lt_max_module_controllogic in X. simplify. remember (max_reg_module m). lia. } + assert (max_reg_expr x0 + 1 <= mod_st m). + { unfold module_ordering in *. simplify. + repeat match goal with + | H: context[_ apply Pos.ltb_lt in H + end. + pose proof H2 as X. apply max_reg_stmnt_le_stmnt_tree in X. + simplify. lia. + } + remember (max_reg_module m). + apply match_assocmaps_gt; [lia|]. + apply match_assocmaps_gt; [lia|]. + apply match_assocmaps_gt; [lia|]. + apply match_assocmaps_gt; [lia|]. + apply match_assocmaps_gt; [lia|]. + apply match_assocmaps_gt; [lia|]. + simplify. + eapply match_assocmaps_ge. eauto. lia. + mgen_crush. } { simplify. unfold merge_regs. unfold_merge. unfold transf_module; repeat destruct_match; try discriminate; simplify. @@ -3148,9 +3170,18 @@ Proof. { crush. } { crush. } { unfold merge_regs. unfold_merge. simplify. - assert (mod_st (transf_module m) <> r) by admit. - repeat rewrite AssocMap.gso by lia. + assert (r < mod_st m). + { unfold module_ordering in *. simplify. + repeat match goal with + | H: context[_ apply Pos.ltb_lt in H + end. + pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. + simplify. lia. + } + unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8. + simplify. rewrite AssocMap.gso in H8 by lia. rewrite AssocMap.gss in H8. unfold transf_module; repeat destruct_match; try discriminate; simplify. + repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. } { eassumption. } } @@ -3175,7 +3206,14 @@ Proof. apply match_assocmaps_gt; [lia|]. apply match_assocmaps_duplicate. apply match_assocmaps_gss. auto. - assert (mod_st m <> r) by admit; auto. + assert (r < mod_st m). + { unfold module_ordering in *. simplify. + repeat match goal with + | H: context[_ apply Pos.ltb_lt in H + end. + pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. + simplify. lia. + } lia. } { apply merge_arr_empty. mgen_crush. @@ -3302,7 +3340,9 @@ Section CORRECTNESS. end. induction 1; destruct (mod_ram m) eqn:RAM; simplify; repeat transf_step_correct_assum; repeat transf_step_correct_tac. - - assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1). + - assert (RAM0: transf_module m = m). + { eapply transf_module_code_ram. left. eassumption. } + assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1). { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. } simplify. assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2). @@ -3313,17 +3353,17 @@ Section CORRECTNESS. assert (MATCH_ARR3: match_arrs_size nasa3 basa3) by mgen_crush. exploit match_states_same. apply H4. eauto with mgen. econstructor; eauto. econstructor; eauto. econstructor; eauto. econstructor; eauto. - intros. repeat inv_exists. simplify. inv H18. inv H21. + intros. repeat inv_exists. simplify. inv H17. inv H20. exploit match_states_same. apply H6. eauto with mgen. - econstructor; eauto. econstructor; eauto. intros. repeat inv_exists. simplify. inv H18. inv H23. + econstructor; eauto. econstructor; eauto. intros. repeat inv_exists. simplify. inv H17. inv H22. exploit exec_ram_same; eauto. eauto with mgen. econstructor. eapply match_assocmaps_merge; eauto. eauto with mgen. econstructor. apply match_arrs_merge; eauto with mgen. eauto with mgen. - intros. repeat inv_exists. simplify. inv H18. inv H28. + intros. repeat inv_exists. simplify. inv H17. inv H27. econstructor; simplify. apply Smallstep.plus_one. econstructor. mgen_crush. mgen_crush. mgen_crush. rewrite RAM0; eassumption. rewrite RAM0; eassumption. - rewrite RAM0. eassumption. mgen_crush. eassumption. rewrite RAM0 in H21. rewrite RAM0. + rewrite RAM0. eassumption. mgen_crush. eassumption. rewrite RAM0 in H20. rewrite RAM0. rewrite RAM. eassumption. eauto. eauto. eauto with mgen. eauto. econstructor. mgen_crush. apply match_arrs_merge; mgen_crush. eauto. apply match_empty_size_merge; mgen_crush; mgen_crush. @@ -3339,14 +3379,16 @@ Section CORRECTNESS. apply match_empty_size_merge; mgen_crush; mgen_crush. unfold disable_ram. unfold transf_module; repeat destruct_match; crush. - apply exec_ram_resets_en in H21. unfold merge_reg_assocs in H21. + apply exec_ram_resets_en in H20. unfold merge_reg_assocs in H20. simplify. auto. auto. - - eapply translation_correct; eauto. + - eapply translation_correct; eauto. admit. - do 2 econstructor. apply Smallstep.plus_one. apply step_finish; mgen_crush. constructor; eauto. - do 2 econstructor. apply Smallstep.plus_one. apply step_finish; mgen_crush. econstructor; eauto. - - econstructor. econstructor. apply Smallstep.plus_one. econstructor. + - assert (RAM0: transf_module m = m). + { eapply transf_module_code_ram. left. eassumption. } + econstructor. econstructor. apply Smallstep.plus_one. econstructor. replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m) by (rewrite RAM0; auto). replace (mod_reset (transf_module m)) with (mod_reset m) by (rewrite RAM0; auto). replace (mod_finish (transf_module m)) with (mod_finish m) by (rewrite RAM0; auto). @@ -3355,9 +3397,7 @@ Section CORRECTNESS. replace (mod_st (transf_module m)) with (mod_st m) by (rewrite RAM0; auto). repeat econstructor; mgen_crush. unfold disable_ram. unfold transf_module; repeat destruct_match; crush. - unfold find_assocmap, AssocMapExt.get_default. destruct_match. - rewrite AssocMap.gso in Heqo1 by admit. rewrite AssocMap.gso in Heqo1 by admit. - rewrite AssocMap.gso in Heqo1 by admit. admit. admit. + admit. - econstructor. econstructor. apply Smallstep.plus_one. econstructor. replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m). replace (mod_reset (transf_module m)) with (mod_reset m). @@ -3371,10 +3411,12 @@ Section CORRECTNESS. unfold find_assocmap, AssocMapExt.get_default. destruct_match. rewrite AssocMap.gso in Heqo by admit. rewrite AssocMap.gso in Heqo by admit. rewrite AssocMap.gso in Heqo by admit. admit. admit. - - inv STACKS. destruct b1; subst. + - assert (RAM0: transf_module m = m). + { eapply transf_module_code_ram. left. eassumption. } + inv STACKS. destruct b1; subst. econstructor. econstructor. apply Smallstep.plus_one. econstructor. eauto. - clear Learn. inv H0. inv H3. inv STACKS. inv H3. constructor. + clear Learn. inv H0. inv H2. inv STACKS. inv H2. constructor. constructor. intros. rewrite RAM0. destruct (Pos.eq_dec r res); subst. @@ -3386,9 +3428,9 @@ Section CORRECTNESS. rewrite AssocMap.gss. rewrite AssocMap.gss. auto. rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC0. apply H1. auto. + symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC0. apply H0. auto. auto. auto. auto. auto. - rewrite RAM0. rewrite H. rewrite RAM0 in DISABLE_RAM. rewrite H in DISABLE_RAM. + rewrite RAM0. rewrite RAM. rewrite RAM0 in DISABLE_RAM. rewrite RAM in DISABLE_RAM. apply disable_ram_set_gso. apply disable_ram_set_gso. auto. admit. admit. admit. admit. - inv STACKS. destruct b1; subst. diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index a9ec5a1..46a9674 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -519,18 +519,27 @@ Inductive mi_stepp : fext -> reg_associations -> arr_associations -> | mi_stepp_Valways : forall f sr0 sa0 st sr1 sa1 c, stmnt_runp f sr0 sa0 st sr1 sa1 -> - mi_stepp f sr0 sa0 (Valways c st) sr1 sa1 -| mi_stepp_Valways_ff : - forall f sr0 sa0 st sr1 sa1 c, - stmnt_runp f sr0 sa0 st sr1 sa1 -> - mi_stepp f sr0 sa0 (Valways_ff c st) sr1 sa1 -| mi_stepp_Valways_comb : + mi_stepp f sr0 sa0 (Valways (Vposedge c) st) sr1 sa1 +| mi_stepp_Valways_ne : + forall f sr0 sa0 c st, + mi_stepp f sr0 sa0 (Valways (Vnegedge c) st) sr0 sa0 +| mi_stepp_Vdecl : + forall f sr0 sa0 d, + mi_stepp f sr0 sa0 (Vdeclaration d) sr0 sa0. +Hint Constructors mi_stepp : verilog. + +Inductive mi_stepp_negedge : fext -> reg_associations -> arr_associations -> + module_item -> reg_associations -> arr_associations -> Prop := +| mi_stepp_negedge_Valways : forall f sr0 sa0 st sr1 sa1 c, stmnt_runp f sr0 sa0 st sr1 sa1 -> - mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1 -| mi_stepp_Vdecl : - forall f sr sa d, - mi_stepp f sr sa (Vdeclaration d) sr sa. + mi_stepp_negedge f sr0 sa0 (Valways (Vnegedge c) st) sr1 sa1 +| mi_stepp_negedge_Valways_ne : + forall f sr0 sa0 c st, + mi_stepp_negedge f sr0 sa0 (Valways (Vposedge c) st) sr0 sa0 +| mi_stepp_negedge_Vdecl : + forall f sr0 sa0 d, + mi_stepp_negedge f sr0 sa0 (Vdeclaration d) sr0 sa0. Hint Constructors mi_stepp : verilog. Inductive mis_stepp : fext -> reg_associations -> arr_associations -> @@ -545,6 +554,18 @@ Inductive mis_stepp : fext -> reg_associations -> arr_associations -> mis_stepp f sr sa nil sr sa. Hint Constructors mis_stepp : verilog. +Inductive mis_stepp_negedge : fext -> reg_associations -> arr_associations -> + list module_item -> reg_associations -> arr_associations -> Prop := +| mis_stepp_negedge_Cons : + forall f mi mis sr0 sa0 sr1 sa1 sr2 sa2, + mi_stepp_negedge f sr0 sa0 mi sr1 sa1 -> + mis_stepp_negedge f sr1 sa1 mis sr2 sa2 -> + mis_stepp_negedge f sr0 sa0 (mi :: mis) sr2 sa2 +| mis_stepp_negedge_Nil : + forall f sr sa, + mis_stepp_negedge f sr sa nil sr sa. +Hint Constructors mis_stepp : verilog. + Local Close Scope error_monad_scope. Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := @@ -559,18 +580,24 @@ Definition empty_stack (m : module) : assocmap_arr := Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist, + forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 basr2 nasr2 + basa2 nasa2 f stval pstval m sf st g ist, asr!(m.(mod_reset)) = Some (ZToValue 0) -> asr!(m.(mod_finish)) = Some (ZToValue 0) -> asr!(m.(mod_st)) = Some ist -> valueToPos ist = st -> mis_stepp f (mkassociations asr empty_assocmap) (mkassociations asa (empty_stack m)) - m.(mod_body) + (mod_body m) (mkassociations basr1 nasr1) - (mkassociations basa1 nasa1)-> - asr' = merge_regs nasr1 basr1 -> - asa' = merge_arrs nasa1 basa1 -> + (mkassociations basa1 nasa1) -> + mis_stepp_negedge f (mkassociations (merge_regs nasr1 basr1) empty_assocmap) + (mkassociations (merge_arrs nasa1 basa1) (empty_stack m)) + (mod_body m) + (mkassociations basr2 nasr2) + (mkassociations basa2 nasa2) -> + asr' = merge_regs nasr2 basr2 -> + asa' = merge_arrs nasa2 basa2 -> asr'!(m.(mod_st)) = Some stval -> valueToPos stval = pstval -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') @@ -718,6 +745,22 @@ Proof. end; crush). Qed. +Lemma mi_stepp_negedge_determinate : + forall f asr0 asa0 m asr1 asa1, + mi_stepp_negedge f asr0 asa0 m asr1 asa1 -> + forall asr1' asa1', + mi_stepp_negedge f asr0 asa0 m asr1' asa1' -> + asr1' = asr1 /\ asa1' = asa1. +Proof. + intros. destruct m; invert H; invert H0; + + repeat (try match goal with + | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _, + H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] => + learn (stmnt_runp_determinate H1 H2) + end; crush). +Qed. + Lemma mis_stepp_determinate : forall f asr0 asa0 m asr1 asa1, mis_stepp f asr0 asa0 m asr1 asa1 -> @@ -741,13 +784,37 @@ Proof. end; crush). Qed. +Lemma mis_stepp_negedge_determinate : + forall f asr0 asa0 m asr1 asa1, + mis_stepp_negedge f asr0 asa0 m asr1 asa1 -> + forall asr1' asa1', + mis_stepp_negedge f asr0 asa0 m asr1' asa1' -> + asr1' = asr1 /\ asa1' = asa1. +Proof. + induction 1; intros; + + repeat (try match goal with + | [ H : mis_stepp_negedge _ _ _ [] _ _ |- _ ] => invert H + | [ H : mis_stepp_negedge _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H + + | [ H1 : mi_stepp_negedge _ ?asr0 ?asa0 ?s _ _, + H2 : mi_stepp_negedge _ ?asr0 ?asa0 ?s _ _ |- _ ] => + learn (mi_stepp_negedge_determinate H1 H2) + + | [ H1 : forall asr1 asa1, mis_stepp_negedge _ ?asr0 ?asa0 ?m asr1 asa1 -> _, + H2 : mis_stepp_negedge _ ?asr0 ?asa0 ?m _ _ |- _ ] => + learn (H1 _ _ H2) + end; crush). +Qed. + Lemma semantics_determinate : forall (p: program), Smallstep.determinate (semantics p). Proof. intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. - invert H; invert H0; constructor. (* Traces are always empty *) - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst. - pose proof (mis_stepp_determinate H5 H15). + pose proof (mis_stepp_determinate H5 H15). simplify. inv H0. inv H4. + pose proof (mis_stepp_negedge_determinate H6 H17). crush. - constructor. invert H; crush. - invert H; invert H0; unfold ge0, ge1 in *; crush. diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index e43ab66..aba2293 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -42,17 +42,16 @@ Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) := Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. -Definition inst_ram clk stk_len ram := +Definition inst_ram clk ram := Valways (Vnegedge clk) - (Vseq (Vcond (Vbinop Vand (Vbinop Vne (Vvar (ram_u_en ram)) (Vvar (ram_en ram))) - (Vbinop Vlt (Vvar (ram_addr ram)) (Vlit (natToValue stk_len)))) - (Vcond (Vvar (ram_wr_en ram)) - (Vnonblock (Vvari (ram_mem ram) (Vvar (ram_addr ram))) - (Vvar (ram_d_in ram))) - (Vnonblock (Vvar (ram_d_out ram)) - (Vvari (ram_mem ram) (Vvar (ram_addr ram))))) - Vskip) - (Vnonblock (Vvar (ram_en ram)) (Vvar (ram_u_en ram)))). + (Vcond (Vbinop Vne (Vvar (ram_u_en ram)) (Vvar (ram_en ram))) + (Vseq (Vcond (Vvar (ram_wr_en ram)) + (Vnonblock (Vvari (ram_mem ram) (Vvar (ram_addr ram))) + (Vvar (ram_d_in ram))) + (Vnonblock (Vvar (ram_d_out ram)) + (Vvari (ram_mem ram) (Vvar (ram_addr ram))))) + (Vnonblock (Vvar (ram_en ram)) (Vvar (ram_u_en ram)))) + Vskip). Definition transl_module (m : HTL.module) : Verilog.module := let case_el_ctrl := list_to_stmnt (transl_list (PTree.elements m.(mod_controllogic))) in @@ -64,7 +63,7 @@ Definition transl_module (m : HTL.module) : Verilog.module := (Vnonblock (Vvar m.(HTL.mod_st)) (Vlit (posToValue m.(HTL.mod_entrypoint)))) (Vcase (Vvar m.(HTL.mod_st)) case_el_ctrl (Some Vskip))) :: Valways (Vposedge m.(HTL.mod_clk)) (Vcase (Vvar m.(HTL.mod_st)) case_el_data (Some Vskip)) - :: inst_ram m.(HTL.mod_clk) (HTL.mod_stk_len m) ram + :: inst_ram m.(HTL.mod_clk) ram :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in Verilog.mkmodule m.(HTL.mod_start) diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 5c484d3..ccc0688 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -225,6 +225,116 @@ Proof. Qed. Hint Resolve mis_stepp_decl : verilogproof. +Lemma mis_stepp_negedge_decl : + forall l asr asa f, + mis_stepp_negedge f asr asa (map Vdeclaration l) asr asa. +Proof. + induction l. + - intros. constructor. + - intros. simplify. econstructor. constructor. auto. +Qed. +Hint Resolve mis_stepp_negedge_decl : verilogproof. + +Lemma mod_entrypoint_equiv m : mod_entrypoint (transl_module m) = HTL.mod_entrypoint m. +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. +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. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_finish_equiv m : mod_finish (transl_module m) = HTL.mod_finish m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_reset_equiv m : mod_reset (transl_module m) = HTL.mod_reset m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_clk_equiv m : mod_clk (transl_module m) = HTL.mod_clk m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_return_equiv m : mod_return (transl_module m) = HTL.mod_return m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_params_equiv m : mod_args (transl_module m) = HTL.mod_params m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma empty_stack_equiv m : empty_stack (transl_module m) = HTL.empty_stack m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Ltac rewrite_eq := rewrite mod_return_equiv + || rewrite mod_clk_equiv + || rewrite mod_reset_equiv + || rewrite mod_finish_equiv + || rewrite mod_stk_len_equiv + || rewrite mod_stk_equiv + || rewrite mod_st_equiv + || rewrite mod_entrypoint_equiv + || rewrite mod_params_equiv + || rewrite empty_stack_equiv. + +Lemma find_assocmap_get r i v : r ! i = Some v -> r # i = v. +Proof. + intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. auto. +Qed. + +Lemma ram_exec_match : + forall f asr asa asr' asa' r clk, + HTL.exec_ram asr asa (Some r) asr' asa' -> + mi_stepp_negedge f asr asa (inst_ram clk r) asr' asa'. +Proof. + inversion 1; subst; simplify. + { unfold inst_ram. econstructor. + eapply stmnt_runp_Vcond_false. + econstructor. econstructor. econstructor. auto. + econstructor. auto. + simplify. + unfold boolToValue, natToValue, valueToBool. + rewrite Int.eq_sym. rewrite H3. simplify. + auto. constructor. } + { unfold inst_ram. econstructor. econstructor. econstructor. + econstructor. econstructor. auto. + econstructor. auto. + simplify. + unfold boolToValue, natToValue, valueToBool. + pose proof H4 as X. apply find_assocmap_get in X. + rewrite X. rewrite Int.eq_sym. rewrite H1. auto. + econstructor. econstructor. econstructor. econstructor. + pose proof H5 as X. apply find_assocmap_get in X. + rewrite X. + unfold valueToBool. unfold ZToValue in *. + unfold Int.eq in H2. + unfold uvalueToZ. + assert (Int.unsigned wr_en =? 0 = false). + apply Z.eqb_neq. rewrite Int.unsigned_repr in H2 by (simplify; lia). + destruct (zeq (Int.unsigned wr_en) 0); crush. + rewrite H0. auto. + apply stmnt_runp_Vnonblock_arr. econstructor. econstructor. auto. + econstructor. econstructor. + apply find_assocmap_get in H9. rewrite H9. + apply find_assocmap_get in H6. rewrite H6. + repeat econstructor. apply find_assocmap_get; auto. + } + { econstructor. econstructor. econstructor. econstructor. auto. + econstructor. auto. + econstructor. + unfold boolToValue, natToValue, valueToBool. + apply find_assocmap_get in H3. rewrite H3. + rewrite Int.eq_sym. rewrite H1. auto. + econstructor. + eapply stmnt_runp_Vcond_false. econstructor. auto. + simplify. apply find_assocmap_get in H4. rewrite H4. + auto. + repeat (econstructor; auto). apply find_assocmap_get in H5. + rewrite H5. eassumption. + repeat econstructor. simplify. apply find_assocmap_get; auto. + } +Qed. + + Section CORRECTNESS. Variable prog: HTL.program. @@ -269,6 +379,12 @@ Section CORRECTNESS. Qed. Hint Resolve senv_preserved : verilogproof. + Ltac unfold_replace := + match goal with + | H: HTL.mod_ram _ = _ |- context[transl_module] => + unfold transl_module; rewrite H + end. + Theorem transl_step_correct : forall (S1 : HTL.state) t S2, HTL.step ge S1 t S2 -> @@ -276,13 +392,14 @@ Section CORRECTNESS. match_states S1 R1 -> exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. Proof. - induction 1; intros R1 MSTATE; inv MSTATE. - Admitted. -(* - econstructor; split. apply Smallstep.plus_one. econstructor. - assumption. assumption. eassumption. apply valueToPos_posToValue. + induction 1; intros R1 MSTATE; inv MSTATE; destruct (HTL.mod_ram m) eqn:?. + - econstructor; split. apply Smallstep.plus_one. econstructor. + unfold_replace. assumption. unfold_replace. assumption. + unfold_replace. eassumption. apply valueToPos_posToValue. split. lia. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. split. lia. apply HP. eassumption. eassumption. + unfold_replace. econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. simpl. unfold find_assocmap. unfold AssocMapExt.get_default. rewrite H. trivial. @@ -314,19 +431,76 @@ Section CORRECTNESS. split. lia. apply HP. eassumption. eassumption. trivial. } apply Maps.PTree.elements_correct. eassumption. eassumption. + econstructor. econstructor. + apply mis_stepp_decl. simplify. unfold_replace. simplify. + econstructor. econstructor. econstructor. econstructor. + econstructor. + apply ram_exec_match. eauto. + apply mis_stepp_negedge_decl. simplify. auto. auto. + rewrite_eq. eauto. auto. + rewrite valueToPos_posToValue. econstructor. auto. + simplify; lia. + - inv H7. econstructor; split. apply Smallstep.plus_one. econstructor. + unfold_replace. assumption. unfold_replace. assumption. + unfold_replace. eassumption. apply valueToPos_posToValue. + split. lia. + eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. + unfold_replace. + econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. + simpl. unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite H. trivial. - apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto. - rewrite valueToPos_posToValue. constructor; assumption. lia. + econstructor. simpl. auto. auto. + + eapply transl_list_correct. + intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto. + apply Maps.PTree.elements_keys_norepet. eassumption. + 2: { apply valueToPos_inj. apply unsigned_posToValue_le. + eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. + apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. + destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. trivial. + } + apply Maps.PTree.elements_correct. eassumption. eassumption. + + econstructor. econstructor. + + eapply transl_list_correct. + intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. + apply Maps.PTree.elements_keys_norepet. eassumption. + 2: { apply valueToPos_inj. apply unsigned_posToValue_le. + eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. + apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. + destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. trivial. + } + apply Maps.PTree.elements_correct. eassumption. eassumption. - - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption. + apply mis_stepp_decl. simplify. + unfold_replace. + repeat econstructor. apply mis_stepp_negedge_decl. trivial. trivial. + simpl. unfold_replace. eassumption. auto. simplify. + rewrite valueToPos_posToValue. constructor; eassumption. simplify; lia. + - econstructor; split. apply Smallstep.plus_one. apply step_finish. + rewrite_eq. assumption. + rewrite_eq. eassumption. + econstructor; auto. + - econstructor; split. apply Smallstep.plus_one. apply step_finish. + unfold transl_module. rewrite Heqo. simplify. + assumption. unfold_replace. eassumption. constructor; assumption. - econstructor; split. apply Smallstep.plus_one. constructor. - - constructor. constructor. + repeat rewrite_eq. constructor. constructor. + - econstructor; split. apply Smallstep.plus_one. constructor. + repeat rewrite_eq. constructor. constructor. - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. - - apply match_state. assumption. - Qed.*) + repeat rewrite_eq. apply match_state. assumption. + - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. + repeat rewrite_eq. apply match_state. assumption. + Qed. Hint Resolve transl_step_correct : verilogproof. Lemma transl_initial_states : -- cgit