diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-03-20 17:04:28 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-03-20 17:04:28 +0000 |
commit | 46d2b685c5ccb2124c7460a41f68ab5cc9353358 (patch) | |
tree | a263a0b20c78b3f1031ac5257af0e3b1c06f0203 /src/hls | |
parent | 70979bfc74f423b284dbe85c62560728bc4558cc (diff) | |
download | vericert-46d2b685c5ccb2124c7460a41f68ab5cc9353358.tar.gz vericert-46d2b685c5ccb2124c7460a41f68ab5cc9353358.zip |
Add check for ram in module
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/Memorygen.v | 177 |
1 files changed, 161 insertions, 16 deletions
diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 06c40ec..32a6d16 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -183,8 +183,8 @@ Definition transf_module (m: module): module := let wr_en := max_reg+5 in let new_size := (2 ^ Nat.log2_up m.(mod_stk_len))%nat in let ram := mk_ram new_size (mod_stk m) en addr d_in d_out wr_en in - match transf_code (mod_st m) ram (mod_datapath m) (mod_controllogic m) with - | (nd, nc) => + match transf_code (mod_st m) ram (mod_datapath m) (mod_controllogic m), (mod_ram m) with + | (nd, nc), None => mkmodule m.(mod_params) nd nc @@ -205,6 +205,7 @@ Definition transf_module (m: module): module := (AssocMap.set m.(mod_stk) (None, VArray 32 new_size)%nat m.(mod_arrdecls)) (Some ram) (is_wf _ nc nd) + | _, _ => m end. Definition transf_fundef := transf_fundef transf_module. @@ -963,6 +964,128 @@ Proof. Abort. apply H. eapply IHl. apply Heqp. Qed.*) +Lemma empty_arrs_match : + forall m, + match_arrs (empty_stack m) (empty_stack (transf_module m)). +Proof. + unfold empty_stack. unfold transf_module. + intros. destruct_match. econstructor. simplify. eexists. + simplify. destruct_match; eauto. eauto. eauto. +Qed. +Hint Resolve empty_arrs_match : mgen. + +Lemma max_module_stmnts : + forall m, + Pos.max (max_stmnt_tree (mod_controllogic m)) + (max_stmnt_tree (mod_datapath m)) < max_reg_module m + 1. +Proof. intros. unfold max_reg_module. lia. Qed. +Hint Resolve max_module_stmnts : mgen. + +Lemma transf_module_code : + forall m, + mod_ram m = None -> + transf_code (mod_st m) + {| ram_size := 2 ^ Nat.log2_up (mod_stk_len m); + ram_mem := mod_stk m; + ram_en := max_reg_module m + 2; + ram_addr := max_reg_module m + 1; + ram_wr_en := max_reg_module m + 3; + ram_d_in := max_reg_module m + 4; + ram_d_out := max_reg_module m + 5 |} + (mod_datapath m) (mod_controllogic m) + = ((mod_datapath (transf_module m)), mod_controllogic (transf_module m)). +Proof. unfold transf_module; intros; repeat destruct_match; crush. Qed. +Hint Resolve transf_module_code : mgen. + +Lemma transf_module_code_ram : + forall m r, mod_ram m = Some r -> transf_module m = m. +Proof. unfold transf_module; intros; repeat destruct_match; crush. Qed. +Hint Resolve transf_module_code_ram : mgen. + +Lemma mod_reset_lt : forall m, mod_reset m < max_reg_module m + 1. +Proof. intros; unfold max_reg_module; lia. Qed. +Hint Resolve mod_reset_lt : mgen. + +Lemma mod_finish_lt : forall m, mod_finish m < max_reg_module m + 1. +Proof. intros; unfold max_reg_module; lia. Qed. +Hint Resolve mod_finish_lt : mgen. + +Lemma mod_return_lt : forall m, mod_return m < max_reg_module m + 1. +Proof. intros; unfold max_reg_module; lia. Qed. +Hint Resolve mod_return_lt : mgen. + +Lemma mod_start_lt : forall m, mod_start m < max_reg_module m + 1. +Proof. intros; unfold max_reg_module; lia. Qed. +Hint Resolve mod_start_lt : mgen. + +Lemma mod_stk_lt : forall m, mod_stk m < max_reg_module m + 1. +Proof. intros; unfold max_reg_module; lia. Qed. +Hint Resolve mod_stk_lt : mgen. + +Lemma mod_st_lt : forall m, mod_st m < max_reg_module m + 1. +Proof. intros; unfold max_reg_module; lia. Qed. +Hint Resolve mod_st_lt : mgen. + +Lemma mod_reset_modify : + forall m ar ar' v, + match_assocmaps (max_reg_module m + 1) ar ar' -> + ar ! (mod_reset m) = Some v -> + ar' ! (mod_reset (transf_module m)) = Some v. +Proof. + inversion 1. intros. + unfold transf_module; repeat destruct_match; simplify; + rewrite <- H0; eauto with mgen. +Qed. +Hint Resolve mod_reset_modify : mgen. + +Lemma mod_finish_modify : + forall m ar ar' v, + match_assocmaps (max_reg_module m + 1) ar ar' -> + ar ! (mod_finish m) = Some v -> + ar' ! (mod_finish (transf_module m)) = Some v. +Proof. + inversion 1. intros. + unfold transf_module; repeat destruct_match; simplify; + rewrite <- H0; eauto with mgen. +Qed. +Hint Resolve mod_finish_modify : mgen. + +Lemma mod_return_modify : + forall m ar ar' v, + match_assocmaps (max_reg_module m + 1) ar ar' -> + ar ! (mod_return m) = Some v -> + ar' ! (mod_return (transf_module m)) = Some v. +Proof. + inversion 1. intros. + unfold transf_module; repeat destruct_match; simplify; + rewrite <- H0; eauto with mgen. +Qed. +Hint Resolve mod_return_modify : mgen. + +Lemma mod_start_modify : + forall m ar ar' v, + match_assocmaps (max_reg_module m + 1) ar ar' -> + ar ! (mod_start m) = Some v -> + ar' ! (mod_start (transf_module m)) = Some v. +Proof. + inversion 1. intros. + unfold transf_module; repeat destruct_match; simplify; + rewrite <- H0; eauto with mgen. +Qed. +Hint Resolve mod_start_modify : mgen. + +Lemma mod_st_modify : + forall m ar ar' v, + match_assocmaps (max_reg_module m + 1) ar ar' -> + ar ! (mod_st m) = Some v -> + ar' ! (mod_st (transf_module m)) = Some v. +Proof. + inversion 1. intros. + unfold transf_module; repeat destruct_match; simplify; + rewrite <- H0; eauto with mgen. +Qed. +Hint Resolve mod_st_modify : mgen. + Section CORRECTNESS. Context (prog tprog: program). @@ -1003,6 +1126,11 @@ Section CORRECTNESS. Proof (Genv.senv_transf TRANSL). Hint Resolve senv_preserved : mgen. + Ltac inv_exists := + match goal with + | H: exists _, _ |- _ => inv H + end. + Theorem transf_step_correct: forall (S1 : state) t S2, step ge S1 t S2 -> @@ -1010,25 +1138,43 @@ Section CORRECTNESS. match_states S1 R1 -> exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. Proof. - induction 1. - - intros. inv H12. learn ASSOC as ASSOC1. inv ASSOC1. learn ARRS as ARRS1. inv ARRS1. simplify. - unfold transf_module. destruct_match. - exploit transf_code_all. apply Heqp. apply H3. - eassumption. - unfold exec_all. + Ltac transf_step_correct_assum := + match goal with + | H: match_states _ _ |- _ => let H2 := fresh "MATCH" in learn H as H2; inv H2 + | H: mod_ram ?m = Some ?r |- _ => + let H2 := fresh "RAM" in learn H; + pose proof (transf_module_code_ram m r H) as H2 + | H: mod_ram ?m = None |- _ => + let H2 := fresh "RAM" in learn H; + pose proof (transf_module_code m H) as H2 + end. + Ltac transf_step_correct_tac := + match goal with + | |- Smallstep.plus _ _ _ _ _ => apply Smallstep.plus_one + end. + induction 1; destruct (mod_ram m) eqn:RAM; simplify; repeat transf_step_correct_assum; + repeat transf_step_correct_tac. + - econstructor. econstructor. apply Smallstep.plus_one. econstructor; eauto with mgen. + rewrite RAM0; eassumption. rewrite RAM0; eassumption. rewrite RAM0. admit. admit. admit. admit. + - exploit transf_code_all; eauto. unfold exec_all. do 3 eexists. simplify. apply H4. apply H6. econstructor. apply ASSOC. instantiate (1 := empty_assocmap). econstructor. eauto. econstructor. eassumption. - instantiate (1 := empty_stack (transf_module m)). admit. - admit. intros. simplify. - unfold exec_all_ram in *. inv H14. inv H16. inv H14. inv H16. inv H14. simplify. + eauto with mgen. + eauto with mgen. + intros. simplify. + unfold exec_all_ram in *. repeat inv_exists. destruct x4. destruct x5. destruct x6. destruct x7. destruct x1. destruct x2. econstructor. econstructor. apply Smallstep.plus_one. econstructor. simplify. - admit. admit. admit. simplify. apply H12. simplify. apply H13. - unfold empty_stack in *. simplify. unfold transf_module in *. simplify. destruct_match. simplify. apply H14. simplify. admit. eassumption. simplify. unfold empty_stack in *. simplify. + eauto with mgen. eauto with mgen. eauto with mgen. eauto with mgen. eauto with mgen. + unfold empty_stack in *. simplify. unfold transf_module in *. + simplify. destruct_match. simplify. eassumption. simplify. + admit. + simplify. eassumption. simplify. unfold empty_stack in *. simplify. unfold merge_reg_assocs in *. unfold merge_arr_assocs in *. simplify. unfold empty_stack' in *. assert (2 ^ Nat.log2_up (mod_stk_len m) = (mod_stk_len m))%nat by admit. - rewrite H18 in H19. rewrite H18. eassumption. auto. auto. simplify. admit. - admit. + rewrite H18 in H19. unfold transf_module; repeat destruct_match; crush. rewrite H18. eassumption. auto. auto. simplify. + instantiate (1 := pstval). + admit. eassumption. admit. - intros. inv H1. inv ASSOC. inv ARRS. econstructor. econstructor. apply Smallstep.plus_one. @@ -1063,7 +1209,6 @@ Section CORRECTNESS. rewrite AssocMap.gss. auto. rewrite AssocMap.gso; auto. symmetry. rewrite AssocMap.gso; auto. - Unshelve. exact 1%positive. Admitted. Hint Resolve transf_step_correct : mgen. |