From 2837868fcc427b2161b083f33d3de495f0c21bf7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 31 Mar 2021 20:45:15 +0100 Subject: Add memory disable --- src/hls/HTL.v | 5 +- src/hls/Memorygen.v | 449 +++++++++++++++++++++++++++++++----------------- src/hls/PrintVerilog.ml | 9 +- src/hls/Veriloggen.v | 6 +- 4 files changed, 306 insertions(+), 163 deletions(-) (limited to 'src') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 32b91ab..4899671 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -139,7 +139,7 @@ Inductive exec_ram: (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some wr_en -> (Verilog.assoc_blocking ra)!(ram_d_in r) = Some d_in -> (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> - exec_ram ra ar (Some r) ra + exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) ra (ZToValue 0)) (Verilog.nonblock_arr (ram_mem r) (valueToNat addr) ar d_in) | exec_ram_Some_read: forall ra ar r addr v_d_out en, @@ -149,7 +149,8 @@ Inductive exec_ram: (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar) (ram_mem r) (valueToNat addr) = Some v_d_out -> - exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) ar + exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) + (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) (ZToValue 0)) ar | exec_ram_None: forall r a, exec_ram r a None r a. diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 65e4bbc..f88bdbf 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -170,9 +170,9 @@ Proof. Qed. Hint Resolve max_stmnt_lt_module : mgen. -Definition transf_maps state ram i (dc: node * PTree.t stmnt * PTree.t stmnt) := - match dc with - | (n, d, c) => +Definition transf_maps state ram in_ (dc: PTree.t stmnt * PTree.t stmnt) := + match dc, in_ with + | (d, c), (i, n) => match PTree.get i d, PTree.get i c with | Some d_s, Some c_s => match d_s with @@ -183,8 +183,8 @@ Definition transf_maps state ram i (dc: node * PTree.t stmnt * PTree.t stmnt) := (Vseq (Vnonblock (Vvar (ram_d_in ram)) e2) (Vnonblock (Vvar (ram_addr ram)) e1))) in - (n, PTree.set i nd d, c) - else dc + (PTree.set i nd d, c) + else (d, c) | Vnonblock e1 (Vvari r e2) => if r =? (ram_mem ram) then let nd := @@ -194,22 +194,22 @@ Definition transf_maps state ram i (dc: node * PTree.t stmnt * PTree.t stmnt) := 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 nd (PTree.set n aout d), PTree.set i redirect (PTree.set n c_s c)) - else dc - | _ => dc + else (d, c) + | _ => (d, c) end - | _, _ => dc + | _, _ => (d, c) end end. Lemma transf_maps_wf : - forall state ram n d c n' d' c' i, + forall state ram d c d' c' i, map_well_formed c /\ map_well_formed d -> - transf_maps state ram i (n, d, c) = (n', d', c') -> + transf_maps state ram i (d, c) = (d', c') -> map_well_formed c' /\ map_well_formed d'. -Proof. - unfold map_well_formed; simplify; +Proof. Abort. +(*) unfold map_well_formed; simplify; repeat destruct_match; match goal with | H: (_, _, _) = (_, _, _) |- _ => inv H end; eauto; simplify. @@ -220,7 +220,7 @@ Proof. apply in_map. apply PTree.elements_correct. apply PTree.elements_complete in H4. -Abort. +Abort.*) Definition set_mod_datapath d c wf m := mkmodule (mod_params m) @@ -248,13 +248,56 @@ Admitted. Definition max_pc {A: Type} (m: PTree.t A) := fold_right Pos.max 1%positive (map fst (PTree.elements m)). -Definition transf_code state ram d c := - match fold_right (transf_maps state ram) - (max_pc d + 1, d, c) - (map fst (PTree.elements d)) with - | (_, d', c') => (d', c') +Fixpoint zip_range {A: Type} n (l: list A) {struct l} := + match l with + | nil => nil + | a :: b => (a, n) :: zip_range (n+1) b end. +Lemma zip_range_fst_idem : forall A (l: list A) a, map fst (zip_range a l) = l. +Proof. induction l; crush. Qed. + +Lemma zip_range_not_in_snd : + forall A (l: list A) a n, a < n -> ~ In a (map snd (zip_range n l)). +Proof. + unfold not; induction l; crush. + inv H0; try lia. eapply IHl. + assert (X: a0 < n + 1) by lia. apply X; auto. auto. +Qed. + +Lemma zip_range_snd_no_repet : + forall A (l: list A) a, list_norepet (map snd (zip_range a l)). +Proof. + induction l; crush; constructor; auto; []. + apply zip_range_not_in_snd; lia. +Qed. + +Lemma zip_range_in : + forall A (l: list A) a n i, In (a, i) (zip_range n l) -> In a l. +Proof. + induction l; crush. inv H. inv H0. auto. right. eapply IHl; eauto. +Qed. + +Lemma zip_range_not_in : + forall A (l: list A) a i n, ~ In a l -> ~ In (a, i) (zip_range n l). +Proof. + unfold not; induction l; crush. inv H0. inv H1. apply H. left. auto. + apply H. right. eapply zip_range_in; eauto. +Qed. + +Lemma zip_range_no_repet : + forall A (l: list A) a, list_norepet l -> list_norepet (zip_range a l). +Proof. + induction l; simplify; constructor; + match goal with H: list_norepet _ |- _ => inv H end; + [apply zip_range_not_in|]; auto. +Qed. + +Definition transf_code state ram d c := + fold_right (transf_maps state ram) (d, c) + (zip_range (Pos.max (max_pc c) (max_pc d) + 1) + (map fst (PTree.elements d))). + Definition transf_module (m: module): module := let max_reg := max_reg_module m in let addr := max_reg+1 in @@ -339,6 +382,12 @@ Inductive match_stackframes : stackframe -> stackframe -> Prop := match_stackframes (Stackframe r m pc asr asa) (Stackframe r (transf_module m) pc asr' asa'). +Definition disable_ram (ram: option ram) (asr : assocmap_reg) : Prop := + match ram with + | Some r => asr # ((ram_en r), 32) = ZToValue 0%Z + | None => True + end. + Inductive match_states : state -> state -> Prop := | match_state : forall res res' m st asr asr' asa asa' @@ -346,7 +395,8 @@ Inductive match_states : state -> state -> Prop := (ARRS: match_arrs asa asa') (STACKS: list_forall2 match_stackframes res res') (ARRS_SIZE: match_empty_size m asa) - (ARRS_SIZE2: match_empty_size m asa'), + (ARRS_SIZE2: match_empty_size m asa') + (DISABLE_RAM: disable_ram (mod_ram (transf_module m)) asr'), match_states (State res m st asr asa) (State res' (transf_module m) st asr' asa') | match_returnstate : @@ -958,7 +1008,7 @@ Qed. /\ match_reg_assocs p (merge_reg_assocs rs2) (merge_reg_assocs trs2) /\ match_arr_assocs (merge_arr_assocs (ram_mem r) (ram_size r) ar2) (merge_arr_assocs (ram_mem r) (ram_size r) tar2). -*) + *) Lemma match_reg_assocs_merge : forall p rs rs', @@ -1064,31 +1114,23 @@ Lemma transf_not_changed : (forall e1 e2 r, d_s <> Vnonblock e1 (Vvari r e2)) -> d!i = Some d_s -> c!i = Some c_s -> - transf_maps state ram i (n, d, c) = (n, d, c). + transf_maps state ram (i, n) (d, c) = (d, c). Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Qed. Lemma transf_not_changed_neq : - forall state ram n d c n' d' c' i a d_s c_s, - transf_maps state ram a (n, d, c) = (n', d', c') -> + forall state ram n d c d' c' i a d_s c_s, + transf_maps state ram (a, n) (d, c) = (d', c') -> d!i = Some d_s -> c!i = Some c_s -> a <> i -> n <> i -> d'!i = Some d_s /\ c'!i = Some c_s. Proof. unfold transf_maps; intros; repeat destruct_match; mgen_crush; - match goal with [ H: (_, _, _) = (_, _, _) |- _ ] => inv H end; + match goal with [ H: (_, _) = (_, _) |- _ ] => inv H end; repeat (rewrite AssocMap.gso; auto). Qed. -Lemma transf_gteq : - forall state ram n d c n' d' c' i, - transf_maps state ram i (n, d, c) = (n', d', c') -> n <= n'. -Proof. - unfold transf_maps; intros; repeat destruct_match; mgen_crush; - match goal with [ H: (_, _, _) = (_, _, _) |- _ ] => inv H end; lia. -Qed. - -Lemma transf_fold_gteq : +(*Lemma transf_fold_gteq : forall l state ram n d c n' d' c', fold_right (transf_maps state ram) (n, d, c) l = (n', d', c') -> n <= n'. Proof. @@ -1134,10 +1176,10 @@ Proof. | Hneq: a <> ?i, H: fold_right _ _ _ = _ |- _ <> _ => apply transf_fold_gteq in H; lia end. -Qed. +Qed.*) Lemma forall_gt : - forall l, Forall (fun x : positive => fold_right Pos.max 1 l + 1 > x) l. + forall l, Forall (Pos.ge (fold_right Pos.max 1 l)) l. Proof. induction l; auto. constructor. inv IHl; simplify; lia. @@ -1145,10 +1187,8 @@ Proof. rewrite e. apply Pos.max_l_iff in e. apply Pos.le_ge in e. apply Forall_forall. rewrite Forall_forall in IHl. intros. - assert (forall a b c, a >= c -> c > b -> a > b) by lia. - assert (forall a b, a >= b -> a + 1 >= b + 1) by lia. - apply H1 in e. - apply H0 with (b := x) in e; auto. + assert (X: forall a b c, a >= c -> c >= b -> a >= b) by lia. + apply X with (b := x) in e; auto. rewrite e; auto. Qed. @@ -1156,26 +1196,29 @@ Lemma max_index_list : forall A (l : list (positive * A)) i d_s, In (i, d_s) l -> list_norepet (map fst l) -> - fold_right Pos.max 1 (map fst l) + 1 > i. + i <= fold_right Pos.max 1 (map fst l). Proof. induction l; crush. inv H. inv H0. simplify. lia. inv H0. let H := fresh "H" in - assert (H: forall a b c, b + 1 > c -> Pos.max a b + 1 > c) by lia; + assert (H: forall a b c, c <= b -> c <= Pos.max a b) by lia; apply H; eapply IHl; eauto. Qed. Lemma max_index : - forall A d i d_s, - d ! i = Some d_s -> @max_pc A d + 1 > i. + forall A d i (d_s: A), d ! i = Some d_s -> i <= max_pc d. Proof. unfold max_pc; eauto using max_index_list, PTree.elements_correct, PTree.elements_keys_norepet. Qed. -Lemma transf_code_not_changed : +Lemma max_index_2 : + forall A (d: AssocMap.t A) i, i > max_pc d -> d ! i = None. +Proof. Admitted. + +(*Lemma transf_code_not_changed : forall state ram d c d' c' i d_s c_s, transf_code state ram d c = (d', c') -> (forall e1 e2 r, d_s <> Vnonblock (Vvari r e1) e2) -> @@ -1188,7 +1231,7 @@ Proof. intros; repeat destruct_match; inv H; eapply transf_fold_not_changed; eauto using forall_gt, PTree.elements_keys_norepet, max_index. -Qed. +Qed.*) (*Lemma transf_all : forall state d c d' c' ram, @@ -2241,14 +2284,14 @@ Definition match_module_to_ram m ram := Hint Unfold match_module_to_ram : mgen. Lemma transf_not_store' : - forall m state ram n i c_s d' c' n' tar1 trs1 p ar1 ar2 rs1 rs2 r e1 e2, + forall m state ram n i c_s d' c' 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') -> + transf_maps state ram (i, n) (mod_datapath m, mod_controllogic m) = (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 -> @@ -2320,13 +2363,24 @@ Proof. auto with mgen.*) Admitted. +Lemma zip_range_forall_le : + forall A (l: list A) n, Forall (Pos.le n) (map snd (zip_range n l)). +Proof. + induction l; crush; constructor; [lia|]. + assert (forall n x, n+1 <= x -> n <= x) by lia. + apply Forall_forall. intros. apply H. generalize dependent x. + apply Forall_forall. apply IHl. +Qed. + Lemma transf_code_fold_correct: - 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 l m state ram d' c' n, + fold_right (transf_maps state ram) (mod_datapath m, mod_controllogic m) l = (d', c') -> + Forall (fun x => x < n) (map fst l) -> + Forall (Pos.le n) (map snd l) -> + list_norepet (map fst l) -> + list_norepet (map snd l) -> (forall p i c_s rs1 ar1 rs2 ar2 trs1 tar1 d_s, - n > i -> + i < n -> all_match_empty_size m ar1 -> all_match_empty_size m tar1 -> match_module_to_ram m ram -> @@ -2346,7 +2400,7 @@ Lemma transf_code_fold_correct: Proof. induction l as [| a l IHl]; simplify. - match goal with - | H: (_, _, _) = (_, _, _) |- _ => inv H + | H: (_, _) = (_, _) |- _ => inv H end; unfold exec_all in *; repeat inv_exists; simplify. exploit match_states_same; @@ -2403,40 +2457,19 @@ Lemma empty_stack_transf : Proof. unfold empty_stack, transf_module; intros; repeat destruct_match; crush. Qed. Definition alt_unchanged (d : AssocMap.t stmnt) (c: AssocMap.t stmnt) d' c' i := - (d ! i = d' ! i /\ c ! i = c' ! i). + d ! i = d' ! i /\ c ! i = c' ! i. Definition alt_store ram d (c : AssocMap.t stmnt) d' c' i := - (exists e1 e2, + exists e1 e2, d' ! i = Some (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)))) /\ c' ! i = c ! i - /\ d ! i = Some (Vnonblock (Vvari (ram_mem ram) e1) e2)). + /\ d ! i = Some (Vnonblock (Vvari (ram_mem ram) e1) e2). Definition alt_load state ram d (c : AssocMap.t stmnt) d' c' i n := - (exists c_s e1 e2, - d' ! i = Some (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))) - /\ d' ! n = Some (Vnonblock e1 (Vvar (ram_d_out ram))) - /\ c' ! i = Some (Vnonblock (Vvar state) (Vlit (posToValue n))) - /\ c' ! n = Some c_s - /\ c ! n = None - /\ c ! i = Some c_s - /\ d ! i = Some (Vnonblock e1 (Vvari (ram_mem ram) e2)) - /\ d ! n = None). - -(*Definition alternatives_1 state ram d c d' c' i := - (d ! i = d' ! i /\ c ! i = c' ! i) - \/ (exists e1 e2, - d' ! i = Some (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)))) - /\ c' ! i = c ! i - /\ d ! i = Some (Vnonblock (Vvari (ram_mem ram) e1) e2)). - \/ (exists c_s e1 e2, + exists c_s e1 e2, d' ! i = Some (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))) @@ -2446,54 +2479,75 @@ Definition alt_load state ram d (c : AssocMap.t stmnt) d' c' i n := /\ c ! n = None /\ c ! i = Some c_s /\ d ! i = Some (Vnonblock e1 (Vvari (ram_mem ram) e2)) - /\ d ! n = None).*) + /\ d ! n = None. Definition alternatives state ram d c d' c' i n := - alt_unchanged d c d' c' i \/ alt_store ram d c d' c' i \/ alt_load state ram d c d' c' i n. + alt_unchanged d c d' c' i + \/ alt_store ram d c d' c' i + \/ alt_load state ram d c d' c' i n. Lemma transf_alternatives : - forall ram n d c state i n' d' c', - transf_maps state ram i (n, d, c) = (n', d', c') -> + forall ram n d c state i d' c', + i <= Pos.max (max_pc c) (max_pc d) < n -> + transf_maps state ram (i, n) (d, c) = (d', c') -> alternatives state ram d c d' c' i n. Proof. intros. unfold transf_maps in *. repeat destruct_match; match goal with - | H: (_, _, _) = (_, _, _) |- _ => inv H - end; try solve [left; econstructor; crush]. - Admitted. + | H: (_, _) = (_, _) |- _ => inv H + end; try solve [left; econstructor; crush]; + match goal with + | H: (_ =? _) = true |- _ => apply Peqb_true_eq in H; subst + end; unfold alternatives; right; + match goal with + | H: context[Vnonblock (Vvari _ _) _] |- _ => left + | _ => right + end; repeat econstructor; simplify; + repeat match goal with + | |- ( _ # ?s <- _ ) ! ?s = Some _ => apply AssocMap.gss + | |- ( _ # ?s <- _ ) ! ?r = Some _ => rewrite AssocMap.gso by lia + | |- _ = None => apply max_index_2; lia + end; auto. +Qed. Lemma transf_alternatives_neq : - forall state ram a n t0 t n' d' c' i d c nn, - transf_maps state ram a (n, t0, t) = (n', d', c') -> - a <> i -> i < nn -> a < nn -> nn < n -> - alternatives state ram d c t0 t i nn -> - alternatives state ram d c d' c' i nn. + forall state ram a n' n d'' c'' d' c' i d c, + transf_maps state ram (a, n) (d, c) = (d', c') -> + a <> i -> n' < n -> i < n' -> a < n' -> + alternatives state ram d'' c'' d c i n' -> + alternatives state ram d'' c'' d' c' i n'. Proof. unfold alternatives, alt_unchanged, alt_store, alt_load, transf_maps; intros; repeat match goal with H: _ \/ _ |- _ => inv H | H: _ /\ _ |- _ => destruct H end; [left | right; left | right; right]; repeat inv_exists; simplify; - repeat destruct_match; - repeat match goal with - | H: (_, _, _) = (_, _, _) |- _ => inv H - | |- exists _, _ => econstructor - end; repeat split; repeat (rewrite AssocMap.gso by lia); eauto; lia. + repeat destruct_match; + repeat match goal with + | H: (_, _) = (_, _) |- _ => inv H + | |- exists _, _ => econstructor + end; repeat split; repeat rewrite AssocMap.gso by lia; eauto; lia. Qed. -Lemma transf_fold_alternatives : - forall l state ram n d c n' d' c', +(*Lemma transf_assigned_gt : + forall state ram a n1 t2 t1 n0 t0 t, + transf_maps state ram a (t2, t1) = (t0, t) -> + max_pc t1 < n1 -> + max_pc t < n0. +Proof. + intros. unfold transf_maps in *. + repeat destruct_match; match goal with + | H: (_, _, _) = (_, _, _) |- _ => inv H + end; try lia. + apply max_index in Heqo0. + Admitted. + +Lemma transf_fold_assigned : + forall l n d c n0 t0 t state ram, + fold_right (transf_maps state ram) (n, d, c) l = (n0, t0, t) -> max_pc c < n -> - fold_right (transf_maps state ram) (n, d, c) l = (n', d', c') -> - Forall (fun x => n > x) l -> - list_norepet l -> - (forall i nn d_s c_s, - In i l -> - n <= nn < n' -> - d ! i = Some d_s -> - c ! i = Some c_s -> - alternatives state ram d c d' c' i nn). + max_pc t < n0. Proof. - induction l; crush; []. + induction l; crush; repeat match goal with | H: context[_ :: _] |- _ => inv H | H: transf_maps _ _ _ (fold_right (transf_maps ?s ?r) (?n, ?d, ?c) ?l) = (_, _, _) |- _ => @@ -2501,25 +2555,72 @@ Proof. remember (fold_right (transf_maps s r) (n, d, c) l) as X | X: _ * _ |- _ => destruct X | H: (_, _, _) = _ |- _ => symmetry in H + end. assert (max_pc t1 < n1). eapply IHl. eauto. eauto. + eapply transf_assigned_gt; eauto. +Qed.*) + +Lemma transf_fold_alternatives : + forall l state ram d c d' c' i n d_s c_s, + fold_right (transf_maps state ram) (d, c) l = (d', c') -> + Pos.max (max_pc c) (max_pc d) < n -> + Forall (Pos.lt (Pos.max (max_pc c) (max_pc d))) (map snd l) -> + Forall (Pos.ge (Pos.max (max_pc c) (max_pc d))) (map fst l) -> + list_norepet (map fst l) -> + list_norepet (map snd l) -> + In (i, n) l -> + d ! i = Some d_s -> + c ! i = Some c_s -> + alternatives state ram d c d' c' i n. +Proof. + Opaque transf_maps. + induction l; crush; []. + repeat match goal with + | H: context[_ :: _] |- _ => inv H + | H: transf_maps _ _ _ (fold_right (transf_maps ?s ?r) (?d, ?c) ?l) = (_, _) |- _ => + let X := fresh "X" in + remember (fold_right (transf_maps s r) (d, c) l) as X + | X: _ * _ |- _ => destruct X + | H: (_, _) = _ |- _ => symmetry in H end. - inv H3. admit. - eapply transf_alternatives_neq; eauto. destruct (Pos.eq_dec a i); subst; congruence. - apply max_index in H6. lia. lia. admit. eapply IHl; eauto. split. auto. admit. + inv H5. inv H1. apply transf_alternatives. simpl in H8. simpl in H4. lia. admit. + simplify. + assert (X: In i (map fst l)). { replace i with (fst (i, n)) by auto. apply in_map; auto. } + assert (X2: In n (map snd l)). { replace n with (snd (i, n)) by auto. apply in_map; auto. } + assert (X3: n <> p0). { destruct (Pos.eq_dec n p0); subst; crush. } + assert (X4: i <> p). { destruct (Pos.eq_dec i p); subst; crush. } + eapply transf_alternatives_neq; eauto. + Transparent transf_maps. Admitted. +Lemma zip_range_inv : + forall A (l: list A) i n, + In i l -> + exists n', In (i, n') (zip_range n l) /\ n' >= n. +Proof. + induction l; crush. + inv H. econstructor. + split. left. eauto. lia. + eapply IHl in H0. inv H0. inv H. + econstructor. split. right. apply H0. lia. +Qed. + Lemma transf_code_alternatives : forall state ram d c d' c' i d_s c_s, transf_code state ram d c = (d', c') -> d ! i = Some d_s -> c ! i = Some c_s -> - alternatives state ram d c d' c' i. + exists n, alternatives state ram d c d' c' i n. Proof. unfold transf_code; - intros; repeat destruct_match; inv H; + intros. + apply PTree.elements_correct in H0. assert (In i (map fst (PTree.elements d))). + { replace i with (fst (i, d_s)) by auto. apply in_map. auto. } + exploit zip_range_inv. apply H2. intros. inv H3. simplify. + instantiate (1 := (Pos.max (max_pc c) (max_pc d) + 1)) in H3. + exists x. eapply transf_fold_alternatives; - eauto using forall_gt, PTree.elements_keys_norepet, max_index. - apply AssocMapExt.elements_iff; eauto. -Qed. + eauto using forall_gt, PTree.elements_keys_norepet, max_index. lia. +Admitted. Lemma translation_correct : forall m asr nasa1 basa1 nasr1 basr1 basr2 nasr2 nasa2 basa2 nasr3 basr3 @@ -2550,6 +2651,11 @@ Lemma translation_correct : Smallstep.plus step tge (State res' (transf_module m) st asr'0 asa'0) Events.E0 R2 /\ match_states (State sf m pstval (merge_regs nasr3 basr3) (merge_arrs nasa3 basa3)) R2. Proof. + Ltac tac0 := + repeat match goal with + | H: match_reg_assocs _ _ _ |- _ => inv H + | H: match_arr_assocs _ _ |- _ => inv H + end. intros. repeat match goal with | H: match_states _ _ |- _ => inv H @@ -2557,46 +2663,62 @@ Proof. | H: mod_ram _ = None |- _ => let H2 := fresh "TRANSF" in learn H as H2; apply transf_module_code in H2 end. - eapply transf_code_alternatives in TRANSF; eauto; simplify. - inv TRANSF. - inv H16. admit. admit. - econstructor. simplify. - eapply Smallstep.plus_two. - econstructor; - repeat match goal with - | |- context[empty_stack (transf_module _)] => rewrite empty_stack_transf - | |- context[mod_ram (transf_module _)] => unfold transf_module; repeat destruct_match - end; mgen_crush. - Admitted. + eapply transf_code_alternatives in TRANSF; eauto; simplify; unfold alternatives in *. + repeat match goal with H: _ \/ _ |- _ => inv H end. + - unfold alt_unchanged in *; simplify. + 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. } + assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2). + { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify. + assert (MATCH_ARR3: match_arrs_size nasa2 basa2) by mgen_crush. + exploit match_states_same; try solve [apply H4 | eapply max_stmnt_lt_module; eauto + | econstructor; eauto with mgen]; + intros; repeat inv_exists; simplify; tac0. + exploit match_states_same; try solve [eapply H6 | eapply max_stmnt_lt_module; eauto + | econstructor; eauto with mgen]; + intros; repeat inv_exists; simplify; tac0. + assert (MATCH_SIZE1': match_empty_size m ran'0 /\ match_empty_size m rab'0). + { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. + rewrite empty_stack_transf; eauto with mgen. } + assert (MATCH_SIZE2': match_empty_size m ran'2 /\ match_empty_size m rab'2). + { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify. + assert (MATCH_ARR3': match_arrs_size ran'2 rab'2) by mgen_crush. + do 2 econstructor. apply Smallstep.plus_one. econstructor. + mgen_crush. mgen_crush. mgen_crush. + rewrite <- H12. eassumption. rewrite <- H7. eassumption. + eauto. mgen_crush. eauto. + rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; crush. + econstructor. admit. auto. auto. mgen_crush. auto. + econstructor; mgen_crush. apply merge_arr_empty; mgen_crush. + apply match_empty_size_merge; auto. + assert (match_arrs (merge_arrs nasa2 basa2) (merge_arrs (empty_stack m) + (merge_arrs ran'2 rab'2))) by admit; auto. + apply merge_arr_empty_match; apply match_empty_size_merge; auto. + apply merge_arr_empty_match; apply match_empty_size_merge; auto. + admit. + - admit. + - admit. -(* exploit transf_code_all. - eassumption. - assert (X: all_match_empty_size m {| assoc_blocking := asa; - assoc_nonblocking := empty_stack m |}) by mgen_crush; eassumption. - assert (X: all_match_empty_size m {| assoc_blocking := asa'0; - assoc_nonblocking := empty_stack m |}) by mgen_crush; eassumption. - unfold match_module_to_ram; simplify; solve [auto]. - unfold ram_ordering; simplify; lia. - eassumption. eassumption. constructor. eassumption. - assert (EMPTY: match_assocmaps (max_reg_module m + 1) empty_assocmap empty_assocmap) - by eauto with mgen. apply EMPTY. - constructor; solve [eauto with mgen]. - lia. unfold exec_all. - repeat match goal with - | |- exists _, _ => econstructor - end; simplify; eassumption. - intros. simplify. - unfold exec_all_ram in *; simplify; - repeat match goal with - | r: arr_associations |- _ => - let r1 := fresh "bar" in - let r2 := fresh "nar" in - destruct r as [r1 r2] - | r: reg_associations |- _ => - let r1 := fresh "brs" in - let r2 := fresh "nrs" in - destruct r as [r1 r2] - end.*) +Admitted. + +Lemma exec_ram_resets_en : + forall rs ar rs' ar' r, + exec_ram rs ar (Some r) rs' ar' -> + assoc_nonblocking rs = empty_assocmap -> + (assoc_blocking (merge_reg_assocs rs')) # (ram_en r, 32) = ZToValue 0. +Proof. + inversion 1; intros; subst; unfold merge_reg_assocs; simplify. + - rewrite H6. unfold find_assocmap, AssocMapExt.get_default in *. + destruct ((assoc_blocking rs') ! (ram_en r)) eqn:?. + simplify. rewrite Heqo. auto. + simplify. rewrite Heqo. auto. + - unfold merge_regs. rewrite H11. unfold_merge. + unfold find_assocmap, AssocMapExt.get_default in *. + rewrite AssocMap.gss; auto. + - unfold merge_regs. rewrite H10. unfold_merge. + unfold find_assocmap, AssocMapExt.get_default in *. + rewrite AssocMap.gss; auto. +Qed. Section CORRECTNESS. @@ -2697,6 +2819,9 @@ Section CORRECTNESS. repeat destruct_match; crush. mgen_crush. unfold match_empty_size. mgen_crush. unfold match_empty_size. mgen_crush. apply match_empty_size_merge; mgen_crush. } 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. simplify. auto. auto. - eapply translation_correct; eauto. - do 2 econstructor. apply Smallstep.plus_one. apply step_finish; mgen_crush. constructor; eauto. @@ -2710,6 +2835,10 @@ Section CORRECTNESS. replace (mod_params (transf_module m)) with (mod_params m) by (rewrite RAM0; auto). 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. auto. - 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). @@ -2719,6 +2848,10 @@ Section CORRECTNESS. replace (mod_st (transf_module m)) with (mod_st m). all: try solve [unfold transf_module; repeat destruct_match; mgen_crush]. 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 Heqo by admit. rewrite AssocMap.gso in Heqo by admit. + rewrite AssocMap.gso in Heqo by admit. admit. auto. - inv STACKS. destruct b1; subst. econstructor. econstructor. apply Smallstep.plus_one. econstructor. eauto. @@ -2736,6 +2869,8 @@ Section CORRECTNESS. rewrite AssocMap.gso; auto. symmetry. rewrite AssocMap.gso; auto. inv H8. apply H1. auto. auto. auto. auto. auto. + unfold disable_ram. unfold transf_module; repeat destruct_match; crush. + admit. - inv STACKS. destruct b1; subst. econstructor. econstructor. apply Smallstep.plus_one. econstructor. eauto. @@ -2753,7 +2888,9 @@ Section CORRECTNESS. rewrite AssocMap.gso; auto. symmetry. rewrite AssocMap.gso; auto. inv H6. apply H. auto. auto. auto. auto. auto. - Qed. + unfold disable_ram. unfold transf_module; repeat destruct_match; crush. + admit. + Admitted. Hint Resolve transf_step_correct : mgen. Lemma transf_initial_states : diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index d076386..61f5b5e 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -164,11 +164,14 @@ let decl i = function let pprint_module_item i = function | Vdeclaration d -> decl i d | Valways (e, s) -> - concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] + concat [indent i; "always "; pprint_edge_top i e; "begin\n"; + pprint_stmnt (i+1) s; indent i; "end\n"] | Valways_ff (e, s) -> - concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] + concat [indent i; "always "; pprint_edge_top i e; "begin\n"; + pprint_stmnt (i+1) s; indent i; "end\n"] | Valways_comb (e, s) -> - concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] + concat [indent i; "always "; pprint_edge_top i e; "begin\n"; + pprint_stmnt (i+1) s; indent i; "end\n"] let rec intersperse c = function | [] -> [] diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index 776f17f..108e816 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -44,13 +44,15 @@ Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. Definition inst_ram clk stk_len ram := Valways (Vnegedge clk) - (Vcond (Vbinop Vand (Vvar (ram_en ram)) (Vbinop Vlt (Vvar (ram_addr ram)) (Vlit (natToValue stk_len)))) + (Vseq (Vcond (Vbinop Vand (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). + Vskip) + (Vnonblock (Vvar (ram_en ram)) (Vlit (ZToValue 0)))). Definition transl_module (m : HTL.module) : Verilog.module := let case_el_ctrl := list_to_stmnt (transl_list (PTree.elements m.(mod_controllogic))) in -- cgit