From d37eeaf79b9164388392c13e0d1213b4bd0192a7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 29 Mar 2021 14:22:23 +0100 Subject: Add more checks to the implementation --- src/hls/Memorygen.v | 109 +++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 82 insertions(+), 27 deletions(-) diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 37201a0..916f7da 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -177,22 +177,26 @@ Definition transf_maps state ram i (dc: node * PTree.t stmnt * PTree.t stmnt) := | Some d_s, Some c_s => match d_s with | Vnonblock (Vvari r e1) e2 => - let nd := Vseq (Vnonblock (Vvar (ram_en ram)) (Vlit (ZToValue 1))) - (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1))) - (Vseq (Vnonblock (Vvar (ram_d_in ram)) e2) - (Vnonblock (Vvar (ram_addr ram)) e1))) - in - (n, PTree.set i nd d, c) + if r =? (ram_mem ram) then + let nd := Vseq (Vnonblock (Vvar (ram_en ram)) (Vlit (ZToValue 1))) + (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1))) + (Vseq (Vnonblock (Vvar (ram_d_in ram)) e2) + (Vnonblock (Vvar (ram_addr ram)) e1))) + in + (n, PTree.set i nd d, c) + else dc | Vnonblock e1 (Vvari r e2) => - let nd := - Vseq (Vnonblock (Vvar (ram_en ram)) (Vlit (ZToValue 1))) - (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0))) - (Vnonblock (Vvar (ram_addr ram)) e2)) - in - let aout := Vnonblock e1 (Vvar (ram_d_out ram)) in - let redirect := Vnonblock (Vvar state) (Vlit (posToValue n)) in - (n+1, PTree.set i nd (PTree.set n aout d), - PTree.set i redirect (PTree.set n c_s c)) + if r =? (ram_mem ram) then + let nd := + Vseq (Vnonblock (Vvar (ram_en ram)) (Vlit (ZToValue 1))) + (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0))) + (Vnonblock (Vvar (ram_addr ram)) e2)) + in + let aout := Vnonblock e1 (Vvar (ram_d_out ram)) in + let redirect := Vnonblock (Vvar state) (Vlit (posToValue n)) in + (n+1, PTree.set i nd (PTree.set n aout d), + PTree.set i redirect (PTree.set n c_s c)) + else dc | _ => dc end | _, _ => dc @@ -469,13 +473,18 @@ Proof. intros; inv H; econstructor; mgen_crush. Qed. Hint Resolve match_reg_assocs_ge : mgen. Definition forall_ram (P: reg -> Prop) ram := - P (ram_mem ram) - /\ P (ram_en ram) + P (ram_en ram) /\ P (ram_addr ram) /\ P (ram_wr_en ram) /\ P (ram_d_in ram) /\ P (ram_d_out ram). +Definition ram_ordering ram := + ram_addr ram < ram_en ram + /\ ram_en ram < ram_d_in ram + /\ ram_d_in ram < ram_d_out ram + /\ ram_d_out ram < ram_wr_en ram. + Lemma forall_ram_lt : forall m r, (mod_ram m) = Some r -> @@ -2126,6 +2135,11 @@ Proof. rewrite H7. auto. Qed. +Ltac clear_learnt := + repeat match goal with + | H: Learnt _ |- _ => clear H + end. + Lemma match_arrs_size_assoc : forall a b, match_arrs_size a b -> @@ -2218,15 +2232,27 @@ Proof. simplify. rewrite H7. rewrite H8. auto. apply H0. mgen_crush. auto. Qed. +Definition all_match_empty_size m ar := + match_empty_size m (assoc_nonblocking ar) /\ match_empty_size m (assoc_blocking ar). +Hint Unfold all_match_empty_size : mgen. + +Definition match_module_to_ram m ram := + ram_size ram = mod_stk_len m /\ ram_mem ram = mod_stk m. +Hint Unfold match_module_to_ram : mgen. + Lemma transf_not_store' : - forall state ram n d c i c_s d' c' n' tar1 trs1 p ar1 ar2 rs1 rs2 r e1 e2, - d!i = Some (Vnonblock (Vvari r e1) e2) -> - c!i = Some c_s -> - transf_maps state ram i (n, d, c) = (n', d', c') -> + forall m state ram n i c_s d' c' n' tar1 trs1 p ar1 ar2 rs1 rs2 r e1 e2, + all_match_empty_size m ar1 -> + all_match_empty_size m tar1 -> + match_module_to_ram m ram -> + ram_ordering ram -> + (mod_datapath m)!i = Some (Vnonblock (Vvari r e1) e2) -> + (mod_controllogic m)!i = Some c_s -> + transf_maps state ram i (n, mod_datapath m, mod_controllogic m) = (n', d', c') -> exec_all (Vnonblock (Vvari (ram_mem ram) e1) e2) c_s rs1 ar1 rs2 ar2 -> match_reg_assocs p rs1 trs1 -> match_arr_assocs ar1 tar1 -> - Pos.max (max_stmnt_tree c) (max_stmnt_tree d) < p -> + max_reg_module m < p -> exists d_s' c_s' trs2 tar2, d'!i = Some d_s' /\ c'!i = Some c_s' /\ exec_all_ram ram d_s' c_s' trs1 tar1 trs2 tar2 @@ -2234,10 +2260,11 @@ Lemma transf_not_store' : /\ match_arr_assocs (merge_arr_assocs (ram_mem ram) (ram_size ram) ar2) (merge_arr_assocs (ram_mem ram) (ram_size ram) tar2). Proof. - intros; unfold transf_maps; simplify; repeat destruct_match; mgen_crush. + (*intros; unfold transf_maps; simplify; repeat destruct_match; mgen_crush. inv H1. unfold exec_all in *. repeat inv_exists. simplify. exploit match_states_same. apply H0. instantiate (1 := p). - admit. eassumption. eassumption. intros. + apply max_reg_stmnt_le_stmnt_tree in Heqo0. lia. + eassumption. eassumption. intros. repeat inv_exists. simplify. inv H1. inv H12. inv H12. inv H. inv H7. simplify. @@ -2248,10 +2275,14 @@ Proof. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. eapply expr_runp_matches2. - eassumption. assert (max_reg_expr e2 < p) by admit. eauto. + eassumption. + apply max_reg_stmnt_le_stmnt_tree in Heqo. + unfold max_reg_stmnt in Heqo. assert (max_reg_expr e2 < p) by lia; eauto. unfold nonblock_reg. simplify. auto. auto. econstructor. econstructor. unfold nonblock_reg. simplify. - eapply expr_runp_matches2. eassumption. assert (max_reg_expr e1 < p) by admit. eauto. + eapply expr_runp_matches2. eassumption. + apply max_reg_stmnt_le_stmnt_tree in Heqo. unfold max_reg_stmnt in Heqo. simplify. + assert (max_reg_expr e1 < p) by lia. eauto. auto. auto. eapply exec_ram_Some_write. 3: { @@ -2286,9 +2317,33 @@ Proof. inv H7. inv H9. rewrite H7. rewrite H11. rewrite <- empty_stack_m. apply match_arrs_merge_set2. admit. admit. admit. admit. auto. auto. - auto with mgen. + auto with mgen.*) Admitted. +Lemma transf_code_store' : + forall l m state ram d' c' n n', + fold_right (transf_maps state ram) (n, mod_datapath m, mod_controllogic m) l = (n', d', c') -> + Forall (fun x => n > x) l -> + list_norepet l -> + (forall p i c_s rs1 ar1 rs2 ar2 trs1 tar1 r e1 e2, + n > i -> + all_match_empty_size m ar1 -> + all_match_empty_size m tar1 -> + match_module_to_ram m ram -> + ram_ordering ram -> + (mod_datapath m)!i = Some (Vnonblock (Vvari r e1) e2) -> + (mod_controllogic m)!i = Some c_s -> + match_reg_assocs p rs1 trs1 -> + match_arr_assocs ar1 tar1 -> + max_reg_module m < p -> + exists d_s' c_s' trs2 tar2, + d'!i = Some d_s' /\ c'!i = Some c_s' + /\ exec_all_ram ram d_s' c_s' trs1 tar1 trs2 tar2 + /\ match_reg_assocs p (merge_reg_assocs rs2) (merge_reg_assocs trs2) + /\ match_arr_assocs (merge_arr_assocs (ram_mem ram) (ram_size ram) ar2) + (merge_arr_assocs (ram_mem ram) (ram_size ram) tar2)). +Proof. + Lemma transf_code_store : forall state ram d c d' c' i d_s c_s rs1 ar1 rs2 ar2 p trs1 tar1 r e1 e2, transf_code state ram d c = (d', c') -> -- cgit