diff options
-rw-r--r-- | src/hls/HTLPargen.v | 4 | ||||
-rw-r--r-- | src/hls/Memorygen.v | 348 | ||||
-rw-r--r-- | src/hls/Schedule.ml | 31 |
3 files changed, 204 insertions, 179 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 10c4357..f22cc39 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -409,11 +409,11 @@ Definition transf_instr (fin rtrn stack state preg: reg) Errors.OK (curr_p, Vseq d stmnt) | RBload p mem addr args dst => do src <- translate_arr_access mem addr args stack; - let stmnt := translate_predicate Vblock preg (npred p) (Vvar dst) src in + let stmnt := translate_predicate Vnonblock preg (npred p) (Vvar dst) src in Errors.OK (curr_p, Vseq d stmnt) | RBstore p mem addr args src => do dst <- translate_arr_access mem addr args stack; - let stmnt := translate_predicate Vblock preg (npred p) dst (Vvar src) in + let stmnt := translate_predicate Vnonblock preg (npred p) dst (Vvar src) in Errors.OK (curr_p, Vseq d stmnt) | RBsetpred p' cond args p => do cond' <- translate_condition cond args; diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 515e944..34e264d 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -2737,180 +2737,180 @@ Proof. unfold merge_regs. admit. } { unfold disable_ram, transf_module in DISABLE_RAM; - repeat destruct_match; try discriminate. simplify. apply int_eq_not. auto. } - { unfold merge_regs; unfold_merge. repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. } - { unfold merge_regs; unfold_merge. apply AssocMap.gss. } - { eapply match_arrs_read. eassumption. mgen_crush_local. } - { crush. } - { crush. } - { unfold merge_regs. unfold_merge. - unfold transf_module; repeat destruct_match; try discriminate; simplify. - assert (mod_st m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - remember (max_reg_module m). repeat rewrite AssocMap.gso by lia. - apply AssocMap.gss. - } - { auto. } - - { econstructor. - { unfold merge_regs. unfold_merge. - assert (mod_reset m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - unfold transf_module; repeat destruct_match; try discriminate; simplify. - assert (mod_st m < mod_reset m). - { pose proof (mod_ordering_wf m); unfold module_ordering in *. simplify. - repeat match goal with - | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H - end; lia. - } - repeat rewrite AssocMap.gso by lia. - inv ASSOC. rewrite <- H19. auto. lia. - } - { unfold merge_regs. unfold_merge. - assert (mod_finish m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - unfold transf_module; repeat destruct_match; try discriminate; simplify. - assert (mod_st m < mod_finish m). - { pose proof (mod_ordering_wf m). unfold module_ordering in *. simplify. - repeat match goal with - | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H - end; lia. - } - repeat rewrite AssocMap.gso by lia. - inv ASSOC. rewrite <- H19. auto. lia. - } - { unfold merge_regs. unfold_merge. - assert (mod_st m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - unfold transf_module; repeat destruct_match; try discriminate; simplify. - repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. - } - { eassumption. } - { 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_local. - } - { simplify. unfold merge_regs. unfold_merge. - unfold transf_module; repeat destruct_match; try discriminate; simplify. - assert (mod_st m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - remember (max_reg_module m). - repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. - } - { - simplify. econstructor. econstructor. econstructor. simplify. - unfold merge_regs; unfold_merge. - repeat rewrite find_assocmap_gso by lia. apply find_assocmap_gss. - } - { simplify. rewrite empty_stack_transf. - unfold transf_module; repeat destruct_match; try discriminate; simplify. - econstructor. simplify. - unfold merge_regs; unfold_merge. simplify. - assert (r < max_reg_module m + 1). - { pose proof H3 as X. eapply max_reg_module_datapath_gt with (p := max_reg_module m + 1) in X. - unfold max_reg_stmnt in X. simplify. - lia. lia. } - assert (mod_st m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss. - repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss. - apply Int.eq_true. - } - { crush. } - { crush. } - { unfold merge_regs. unfold_merge. simplify. - 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. } - } - { eauto. } - { econstructor. - { unfold merge_regs. unfold_merge. simplify. - apply match_assocmaps_gss. - unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8. - rewrite AssocMap.gso in H8. rewrite AssocMap.gss in H8. inv H8. - remember (max_reg_module m). - assert (mod_st m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - apply match_assocmaps_switch_neq; [|lia]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_switch_neq; [|lia]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_switch_neq; [|lia]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_switch_neq; [|lia]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_switch_neq; [|lia]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_duplicate. - apply match_assocmaps_gss. 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_local. - apply merge_arr_empty2. mgen_crush_local. - apply merge_arr_empty2. mgen_crush_local. - apply merge_arr_empty2. mgen_crush_local. - mgen_crush_local. - } - { auto. } - { mgen_crush_local. } - { mgen_crush_local. } - { unfold disable_ram. - unfold transf_module; repeat destruct_match; try discriminate; simplify. - unfold merge_regs. unfold_merge. simplify. - assert (mod_st m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - assert (r < max_reg_module m + 1). - { pose proof H3 as X. eapply max_reg_module_datapath_gt with (p := max_reg_module m + 1) in X. - unfold max_reg_stmnt in X. simplify. - lia. lia. } - repeat rewrite find_assocmap_gso by lia. - rewrite find_assocmap_gss. - repeat rewrite find_assocmap_gso by lia. - rewrite find_assocmap_gss. apply Int.eq_true. - } - } -Qed. + repeat destruct_match; try discriminate. simplify. apply int_eq_not. auto. admit. } (* } *) +(* { unfold merge_regs; unfold_merge. repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. } *) +(* { unfold merge_regs; unfold_merge. apply AssocMap.gss. } *) +(* { eapply match_arrs_read. eassumption. mgen_crush_local. } *) +(* { crush. } *) +(* { crush. } *) +(* { unfold merge_regs. unfold_merge. *) +(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) +(* assert (mod_st m < max_reg_module m + 1). *) +(* { unfold max_reg_module; lia. } *) +(* remember (max_reg_module m). repeat rewrite AssocMap.gso by lia. *) +(* apply AssocMap.gss. *) +(* } *) +(* { auto. } *) + +(* { econstructor. *) +(* { unfold merge_regs. unfold_merge. *) +(* assert (mod_reset m < max_reg_module m + 1). *) +(* { unfold max_reg_module; lia. } *) +(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) +(* assert (mod_st m < mod_reset m). *) +(* { pose proof (mod_ordering_wf m); unfold module_ordering in *. simplify. *) +(* repeat match goal with *) +(* | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H *) +(* end; lia. *) +(* } *) +(* repeat rewrite AssocMap.gso by lia. *) +(* inv ASSOC. rewrite <- H19. auto. lia. *) +(* } *) +(* { unfold merge_regs. unfold_merge. *) +(* assert (mod_finish m < max_reg_module m + 1). *) +(* { unfold max_reg_module; lia. } *) +(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) +(* assert (mod_st m < mod_finish m). *) +(* { pose proof (mod_ordering_wf m). unfold module_ordering in *. simplify. *) +(* repeat match goal with *) +(* | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H *) +(* end; lia. *) +(* } *) +(* repeat rewrite AssocMap.gso by lia. *) +(* inv ASSOC. rewrite <- H19. auto. lia. *) +(* } *) +(* { unfold merge_regs. unfold_merge. *) +(* assert (mod_st m < max_reg_module m + 1). *) +(* { unfold max_reg_module; lia. } *) +(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) +(* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) +(* } *) +(* { eassumption. } *) +(* { 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_local. *) +(* } *) +(* { simplify. unfold merge_regs. unfold_merge. *) +(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) +(* assert (mod_st m < max_reg_module m + 1). *) +(* { unfold max_reg_module; lia. } *) +(* remember (max_reg_module m). *) +(* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) +(* } *) +(* { *) +(* simplify. econstructor. econstructor. econstructor. simplify. *) +(* unfold merge_regs; unfold_merge. *) +(* repeat rewrite find_assocmap_gso by lia. apply find_assocmap_gss. *) +(* } *) +(* { simplify. rewrite empty_stack_transf. *) +(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) +(* econstructor. simplify. *) +(* unfold merge_regs; unfold_merge. simplify. *) +(* assert (r < max_reg_module m + 1). *) +(* { pose proof H3 as X. eapply max_reg_module_datapath_gt with (p := max_reg_module m + 1) in X. *) +(* unfold max_reg_stmnt in X. simplify. *) +(* lia. lia. } *) +(* assert (mod_st m < max_reg_module m + 1). *) +(* { unfold max_reg_module; lia. } *) +(* repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss. *) +(* repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss. *) +(* apply Int.eq_true. *) +(* } *) +(* { crush. } *) +(* { crush. } *) +(* { unfold merge_regs. unfold_merge. simplify. *) +(* 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. } *) +(* } *) +(* { eauto. } *) +(* { econstructor. *) +(* { unfold merge_regs. unfold_merge. simplify. *) +(* apply match_assocmaps_gss. *) +(* unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8. *) +(* rewrite AssocMap.gso in H8. rewrite AssocMap.gss in H8. inv H8. *) +(* remember (max_reg_module m). *) +(* assert (mod_st m < max_reg_module m + 1). *) +(* { unfold max_reg_module; lia. } *) +(* apply match_assocmaps_switch_neq; [|lia]. *) +(* apply match_assocmaps_gt; [lia|]. *) +(* apply match_assocmaps_switch_neq; [|lia]. *) +(* apply match_assocmaps_gt; [lia|]. *) +(* apply match_assocmaps_switch_neq; [|lia]. *) +(* apply match_assocmaps_gt; [lia|]. *) +(* apply match_assocmaps_switch_neq; [|lia]. *) +(* apply match_assocmaps_gt; [lia|]. *) +(* apply match_assocmaps_switch_neq; [|lia]. *) +(* apply match_assocmaps_gt; [lia|]. *) +(* apply match_assocmaps_duplicate. *) +(* apply match_assocmaps_gss. 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_local. *) +(* apply merge_arr_empty2. mgen_crush_local. *) +(* apply merge_arr_empty2. mgen_crush_local. *) +(* apply merge_arr_empty2. mgen_crush_local. *) +(* mgen_crush_local. *) +(* } *) +(* { auto. } *) +(* { mgen_crush_local. } *) +(* { mgen_crush_local. } *) +(* { unfold disable_ram. *) +(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) +(* unfold merge_regs. unfold_merge. simplify. *) +(* assert (mod_st m < max_reg_module m + 1). *) +(* { unfold max_reg_module; lia. } *) +(* assert (r < max_reg_module m + 1). *) +(* { pose proof H3 as X. eapply max_reg_module_datapath_gt with (p := max_reg_module m + 1) in X. *) +(* unfold max_reg_stmnt in X. simplify. *) +(* lia. lia. } *) +(* repeat rewrite find_assocmap_gso by lia. *) +(* rewrite find_assocmap_gss. *) +(* repeat rewrite find_assocmap_gso by lia. *) +(* rewrite find_assocmap_gss. apply Int.eq_true. *) +(* } *) +(* } *) +(* Qed. *) Admitted. Lemma exec_ram_resets_en : forall rs ar rs' ar' r, diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index f952f60..683dd29 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -297,7 +297,8 @@ let comb_delay = function | _ -> 1 let pipeline_stages = function - | RBload _ -> 2 + | RBload _ -> 1 (* TODO: Set back to 2 when memory inferrence is fixed. *) + | RBstore _ -> 1 | RBop (_, op, _, _) -> (match op with | Odiv -> 32 @@ -881,6 +882,31 @@ let range s e = List.init (e - s) (fun i -> i) |> List.map (fun x -> x + s) +let remove_nop = function + | RBnop -> [] + | a -> [a] + +let separate_mem_operations l = + let added = ref false in + List.concat_map (fun par_list -> + List.fold_left (fun new_l seq_list -> + match List.concat_map remove_nop seq_list with + | [RBload _] | [RBstore _] -> (added := true; new_l @ [[seq_list]]) + | [] -> new_l + | seq_list' -> + ((if !added then (added := false; new_l @ [[seq_list']]) + else + (match List.rev new_l with + | [] -> [[seq_list']] + | new_lx :: new_ly -> List.rev ((new_lx @ [seq_list']) :: new_ly)))) + ) [] par_list + ) l + +(* let print_nested = print_list (print_list (print_list (fun a b -> fprintf a "%d" b))) *) + +(* let _ = *) +(* printf "%a\n" print_nested (separate_mem_operations [[[1]; [3]; [3]; [2]; [3]; [2]]]) *) + (** Should generate the [RTLPar] code based on the input [RTLBlock] description. *) let transf_rtlpar c c' schedule = let f i bb : ParBB.t = @@ -917,8 +943,7 @@ let transf_rtlpar c c' schedule = (*|> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x []) |> List.rev) body2*) in - final_body2 - | _ -> List.map (fun i -> [[i]]) bb + (separate_mem_operations final_body2) in PTree.map f c |