From 92b6c68cdfd1e42ca1f9ebf70b7292e7c16570c2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 19 Oct 2023 18:21:00 +0100 Subject: Finished most of the giblesubpar proof --- src/hls/ClockMemory.v | 4 +-- src/hls/DHTLgen.v | 14 +++++------ src/hls/DMemorygen.v | 50 ++++++++++++++++++------------------- src/hls/DVeriloggen.v | 35 ++++++++++++++++++++------ src/hls/Verilog.v | 69 +++++++++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 131 insertions(+), 41 deletions(-) (limited to 'src/hls') diff --git a/src/hls/ClockMemory.v b/src/hls/ClockMemory.v index 3d068ad..549b310 100644 --- a/src/hls/ClockMemory.v +++ b/src/hls/ClockMemory.v @@ -44,9 +44,9 @@ Definition pred := positive. Definition transf_maps (d: stmnt) := match d with - | Vseq ((Vblock (Vvar _) _) as rest) (Vblock (Vvari r e1) e2) => + | Vseq (Vseq Vskip (Vblock (Vvari r e1) e2)) ((Vblock (Vvar _) _) as rest) => Vseq rest (Vnonblock (Vvari r e1) e2) - | Vseq (Vblock (Vvar st') e3) (Vblock (Vvar e1) (Vvari r e2)) => + | Vseq (Vseq Vskip (Vblock (Vvar e1) (Vvari r e2))) (Vblock (Vvar st') e3) => Vseq (Vblock (Vvar st') e3) (Vnonblock (Vvar e1) (Vvari r e2)) | _ => d end. diff --git a/src/hls/DHTLgen.v b/src/hls/DHTLgen.v index 4b931c7..49d2c87 100644 --- a/src/hls/DHTLgen.v +++ b/src/hls/DHTLgen.v @@ -103,7 +103,7 @@ Definition translate_predicate (a : assignment) | Some _ => a dst (Vternary (pred_expr pos') e dst) end end. - + Definition state_goto (p: option pred_op) (st : reg) (n : node) : stmnt := translate_predicate Vblock p (Vvar st) (Vlit (posToValue n)). @@ -302,12 +302,12 @@ Definition translate_cfi (ctrl: control_regs) p (cfi: cf_instr) | RBreturn r => match r with | Some r' => - Errors.OK (Vseq (block ctrl.(ctrl_fin) (Vlit (ZToValue 1%Z))) (block ctrl.(ctrl_return) (Vvar r'))) + Errors.OK (Vseq (Vblock (Vvar ctrl.(ctrl_fin)) (Vlit (ZToValue 1%Z))) (Vblock (Vvar ctrl.(ctrl_return)) (Vvar (reg_enc r')))) | None => - Errors.OK (Vseq (block ctrl.(ctrl_fin) (Vlit (ZToValue 1%Z))) (block ctrl.(ctrl_return) (Vlit (ZToValue 0%Z)))) + Errors.OK (Vseq (Vblock (Vvar ctrl.(ctrl_fin)) (Vlit (ZToValue 1%Z))) (Vblock (Vvar ctrl.(ctrl_return)) (Vlit (ZToValue 0%Z)))) end | RBjumptable r tbl => - Errors.OK (Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr ctrl.(ctrl_st) tbl)) (Some Vskip)) + Errors.OK (Vcase (Vvar (reg_enc r)) (list_to_stmnt (tbl_to_case_expr ctrl.(ctrl_st) tbl)) (Some Vskip)) | RBcall sig ri rl r n => Errors.Error (Errors.msg "HTLPargen: RBcall not supported.") | RBtailcall sig ri lr => @@ -324,15 +324,15 @@ Definition transf_instr (ctrl: control_regs) (dc: pred_op * stmnt) (i: instr) | RBnop => Errors.OK dc | RBop p op args dst => do instr <- translate_instr op args; - let stmnt := translate_predicate Vblock (npred p) (Vvar dst) instr in + let stmnt := translate_predicate Vblock (npred p) (Vvar (reg_enc dst)) instr in Errors.OK (curr_p, Vseq d stmnt) | RBload p mem addr args dst => do src <- translate_arr_access mem addr args ctrl.(ctrl_stack); - let stmnt := translate_predicate Vblock (npred p) (Vvar dst) src in + let stmnt := translate_predicate Vblock (npred p) (Vvar (reg_enc dst)) src in Errors.OK (curr_p, Vseq d stmnt) | RBstore p mem addr args src => do dst <- translate_arr_access mem addr args ctrl.(ctrl_stack); - let stmnt := translate_predicate Vblock (npred p) dst (Vvar src) in + let stmnt := translate_predicate Vblock (npred p) dst (Vvar (reg_enc 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/DMemorygen.v b/src/hls/DMemorygen.v index 846bfad..0c9fd80 100644 --- a/src/hls/DMemorygen.v +++ b/src/hls/DMemorygen.v @@ -164,28 +164,28 @@ Definition transf_maps state ram in_ (d: PTree.t stmnt) := | (i, n) => match PTree.get i d with (* Conditional store *) - | Some (Vseq ((Vblock (Vvar _) _) as rest) (Vnonblock (Vvari r e1) (Vternary cond e2 (Vvari r' e1')))) => - if (r =? (ram_mem ram)) && (r =? r') && (expr_eqb e1 e1') then - let nd := Vseq (Vblock (Vvar (ram_u_en ram)) (Vternary cond (Vunop Vnot (Vvar (ram_u_en ram))) (Vvar (ram_u_en ram)))) - (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1))) - (Vseq (Vblock (Vvar (ram_d_in ram)) e2) - (Vblock (Vvar (ram_addr ram)) e1))) - in - PTree.set i (Vseq rest nd) d - else d - | Some (Vseq (Vblock (Vvar st') e3) (Vnonblock (Vvar e1) (Vternary cond (Vvari r e2) edef))) => - if (r =? (ram_mem ram)) && (st' =? state) && (Z.pos n <=? Int.max_unsigned)%Z - && (e1 *) + (* if (r =? (ram_mem ram)) && (r =? r') && (expr_eqb e1 e1') then *) + (* let nd := Vseq (Vblock (Vvar (ram_u_en ram)) (Vternary cond (Vunop Vnot (Vvar (ram_u_en ram))) (Vvar (ram_u_en ram)))) *) + (* (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1))) *) + (* (Vseq (Vblock (Vvar (ram_d_in ram)) e2) *) + (* (Vblock (Vvar (ram_addr ram)) e1))) *) + (* in *) + (* PTree.set i (Vseq rest nd) d *) + (* else d *) + (* | Some (Vseq (Vblock (Vvar st') e3) (Vnonblock (Vvar e1) (Vternary cond (Vvari r e2) edef))) => *) + (* if (r =? (ram_mem ram)) && (st' =? state) && (Z.pos n <=? Int.max_unsigned)%Z *) + (* && (e1 if r =? (ram_mem ram) then let nd := Vseq (Vblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) @@ -240,7 +240,7 @@ Proof. eapply H. eapply AssocMapExt.elements_iff; eauto. + rewrite PTree.gso in H1 by auto. eapply H. eapply AssocMapExt.elements_iff; eauto. -Admitted. +Qed. Definition max_pc {A: Type} (m: PTree.t A) := fold_right Pos.max 1%positive (map fst (PTree.elements m)). @@ -1077,7 +1077,7 @@ Lemma transf_not_changed : (forall e1 e2 e3 e4 r, d_s <> (Vseq (Vblock (Vvar e1) e2) (Vnonblock e3 (Vvari r e4)))) -> d!i = Some d_s -> transf_maps state ram (i, n) d = d. -Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Admitted. +Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Qed. Lemma transf_not_changed_neq : forall state ram n d d' i a d_s, @@ -2270,7 +2270,7 @@ Proof. | |- _ = None => apply max_index_2; lia | H: context[_ apply Pos.ltb_lt in H end; auto. -Admitted. +Qed. Lemma transf_alternatives_neq : forall state ram a n' n d'' d' i d, diff --git a/src/hls/DVeriloggen.v b/src/hls/DVeriloggen.v index 6b47dd0..d751178 100644 --- a/src/hls/DVeriloggen.v +++ b/src/hls/DVeriloggen.v @@ -42,6 +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 declare_all (start reset clk finish ret st stk: reg) (stk_len: nat) (body: list module_item) := + Vdeclaration (Vdecl (Some Vinput) start 1) + :: Vdeclaration (Vdecl (Some Vinput) reset 1) + :: Vdeclaration (Vdecl (Some Vinput) clk 1) + :: Vdeclaration (Vdecl (Some Voutput) finish 1) + :: Vdeclaration (Vdecl (Some Voutput) ret 32) + :: Vdeclaration (Vdecl None st 32) + :: Vdeclaration (Vdeclarr None stk 32 stk_len) + :: (all_reg_declarations (start::reset::clk::finish::ret::st::stk::nil) body). + Definition inst_ram clk ram := Valways (Vnegedge clk) (Vcond (Vbinop Vne (Vvar (ram_u_en ram)) (Vvar (ram_en ram))) @@ -65,9 +75,7 @@ Definition transl_module (m : DHTL.module) : Verilog.module := (* :: Valways (Vposedge m.(DHTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(DHTL.mod_reset)) (Vlit (ZToValue 1))) *) (* (Vnonblock (Vvar (DHTL.mod_st m)) (Vlit (posToValue m.(DHTL.mod_entrypoint)))) (Vnonblock (Vvar (DHTL.mod_st m)) (Vvar m.(DHTL.mod_st)))) *) :: inst_ram m.(DHTL.mod_clk) ram - :: List.map Vdeclaration ((* Vdecl None nstate 32 :: *) - (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) - ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls)))) in + :: nil in Verilog.mkmodule m.(DHTL.mod_start) m.(DHTL.mod_reset) m.(DHTL.mod_clk) @@ -77,7 +85,14 @@ Definition transl_module (m : DHTL.module) : Verilog.module := m.(DHTL.mod_stk) m.(DHTL.mod_stk_len) m.(DHTL.mod_params) - body + (body ++ declare_all m.(DHTL.mod_start) + m.(DHTL.mod_reset) + m.(DHTL.mod_clk) + m.(DHTL.mod_finish) + m.(DHTL.mod_return) + m.(DHTL.mod_st) + m.(DHTL.mod_stk) + m.(DHTL.mod_stk_len) body) m.(DHTL.mod_entrypoint) | None => let body := @@ -87,8 +102,7 @@ Definition transl_module (m : DHTL.module) : Verilog.module := (* :: Valways (Vposedge m.(DHTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(DHTL.mod_reset)) (Vlit (ZToValue 1))) *) (* (Vnonblock (Vvar (DHTL.mod_st m)) (Vlit (posToValue m.(DHTL.mod_entrypoint)))) *) (* (Vnonblock (Vvar (DHTL.mod_st m)) (Vvar m.(DHTL.mod_st)))) *) - :: List.map Vdeclaration ((* Vdecl None (DHTL.mod_st m) 32 :: *)arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) - ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in + :: nil in Verilog.mkmodule m.(DHTL.mod_start) m.(DHTL.mod_reset) m.(DHTL.mod_clk) @@ -98,7 +112,14 @@ Definition transl_module (m : DHTL.module) : Verilog.module := m.(DHTL.mod_stk) m.(DHTL.mod_stk_len) m.(DHTL.mod_params) - body + (body ++ declare_all m.(DHTL.mod_start) + m.(DHTL.mod_reset) + m.(DHTL.mod_clk) + m.(DHTL.mod_finish) + m.(DHTL.mod_return) + m.(DHTL.mod_st) + m.(DHTL.mod_stk) + m.(DHTL.mod_stk_len) body) m.(DHTL.mod_entrypoint) end. diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 79ee723..69252ec 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -904,3 +904,72 @@ with max_reg_stmnt_expr_list (stl: stmnt_expr_list) := (Pos.max (max_reg_stmnt s) (max_reg_stmnt_expr_list stl')) end. + +Definition combine_reg (r1 r2 : option unit) := + match r1, r2 with + | Some _, _ => Some tt + | _, Some _ => Some tt + | _, _ => None + end. + +Import Maps. + +Fixpoint all_reg_expr (e: expr): PTree.t unit := + match e with + | Vlit _ => PTree.empty _ + | Vvar r => PTree.set r tt (PTree.empty _) + | Vvari r e => all_reg_expr e + | Vrange r e1 e2 => PTree.set r tt (PTree.empty _) + | Vinputvar r => PTree.empty _ + | Vbinop _ e1 e2 => PTree.combine combine_reg (all_reg_expr e1) (all_reg_expr e2) + | Vunop _ e => all_reg_expr e + | Vternary e1 e2 e3 => + PTree.combine combine_reg (all_reg_expr e1) (PTree.combine combine_reg (all_reg_expr e2) (all_reg_expr e3)) + end. + +Fixpoint all_reg_stmnt (st: stmnt): PTree.t unit := + match st with + | Vskip => PTree.empty _ + | Vseq s1 s2 => PTree.combine combine_reg (all_reg_stmnt s1) (all_reg_stmnt s2) + | Vcond e s1 s2 => + PTree.combine combine_reg (all_reg_expr e) (PTree.combine combine_reg (all_reg_stmnt s1) (all_reg_stmnt s2)) + | Vcase e stl None => PTree.combine combine_reg (all_reg_expr e) (all_reg_stmnt_expr_list stl) + | Vcase e stl (Some s) => + PTree.combine combine_reg (all_reg_stmnt s) + (PTree.combine combine_reg (all_reg_expr e) (all_reg_stmnt_expr_list stl)) + | Vblock e1 e2 => PTree.combine combine_reg (all_reg_expr e1) (all_reg_expr e2) + | Vnonblock e1 e2 => PTree.combine combine_reg (all_reg_expr e1) (all_reg_expr e2) + end +with all_reg_stmnt_expr_list (stl: stmnt_expr_list) := + match stl with + | Stmntnil => PTree.empty _ + | Stmntcons e s stl' => + PTree.combine combine_reg (all_reg_expr e) + (PTree.combine combine_reg (all_reg_stmnt s) + (all_reg_stmnt_expr_list stl')) + end. + +Fixpoint all_reg_edge (e: edge): PTree.t unit := + match e with + | Vposedge r => PTree.set r tt (PTree.empty _) + | Vnegedge r => PTree.set r tt (PTree.empty _) + | Valledge => PTree.empty _ + | Voredge e1 e2 => PTree.combine combine_reg (all_reg_edge e1) (all_reg_edge e2) + end. + +Definition all_reg_module_item (m: module_item): PTree.t unit := + match m with + | Vdeclaration d => PTree.empty _ + | Valways e s + | Valways_ff e s + | Valways_comb e s => PTree.combine combine_reg (all_reg_edge e) (all_reg_stmnt s) + end. + +Definition all_reg_module_item_l (ml: list module_item): PTree.t unit := + List.fold_left (fun a b => PTree.combine combine_reg a (all_reg_module_item b)) ml (PTree.empty _). + +Definition all_reg_to_declaration (tree: PTree.t unit): list module_item := + PTree.fold (fun ml p _ => Vdeclaration (Vdecl None p 32) :: ml) tree nil. + +Definition all_reg_declarations (rem: list positive) (ml: list module_item): list module_item := + all_reg_to_declaration (List.fold_left (fun a b => PTree.remove b a) rem (all_reg_module_item_l ml)). -- cgit