From 0e5f9cba25297c604242cbf326fd307f8956cca1 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Thu, 2 Sep 2021 16:31:38 +0100 Subject: Address ram in renaming pass --- src/hls/HTL.v | 19 ++++++++++++++----- src/hls/Memorygen.v | 12 +++++------- src/hls/Renaming.v | 22 ++++++++++++++++++++-- 3 files changed, 39 insertions(+), 14 deletions(-) diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 303dc70..1a23ef5 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -58,6 +58,8 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := In p0 (map fst (Maps.PTree.elements m)) -> (Z.pos p0 <= Integers.Int.max_unsigned)%Z. +Definition ram_ordering a b c d e f := a < b < c /\ c < d < e /\ e < f. + Record ram := mk_ram { ram_size: nat; ram_mem: reg; @@ -67,11 +69,7 @@ Record ram := mk_ram { ram_wr_en: reg; ram_d_in: reg; ram_d_out: reg; - ram_ordering: (ram_addr < ram_en - /\ ram_en < ram_d_in - /\ ram_d_in < ram_d_out - /\ ram_d_out < ram_wr_en - /\ ram_wr_en < ram_u_en) + ram_ordering_wf: ram_ordering ram_addr ram_en ram_d_in ram_d_out ram_wr_en ram_u_en }. Definition module_ordering a b c d e f g := a < b < c /\ c < d < e /\ e < f < g. @@ -448,6 +446,17 @@ Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True} end; unfold module_ordering; auto. Defined. +Definition decide_ram_ordering a b c d e f : {ram_ordering a b c d e f} + {True}. + refine (match bool_dec ((a left _ + | _ => _ + end); auto. + simplify; repeat match goal with + | H: context[(_ apply Pos.ltb_lt in H + end; unfold ram_ordering; auto. +Defined. + Definition decide_ram_wf (clk : reg) (mr : option HTL.ram) : {forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive} + {True}. refine ( diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index a044836..864419d 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -199,10 +199,8 @@ Lemma transf_code_wf : map_well_formed c' /\ map_well_formed d'. Proof. eauto using transf_code_wf'. Qed. -Lemma ram_wf : - forall x, - x + 1 < x + 2 /\ x + 2 < x + 3 /\ x + 3 < x + 4 /\ x + 4 < x + 5 /\ x + 5 < x + 6. -Proof. lia. Qed. +Lemma ram_wf : forall x, ram_ordering (x + 1) (x + 2) (x + 3) (x + 4) (x + 5) (x + 6). +Proof. unfold ram_ordering. lia. Qed. Lemma module_ram_wf' : forall m addr, @@ -1091,7 +1089,7 @@ Lemma transf_module_code : ram_d_in := max_reg_module m + 3; ram_d_out := max_reg_module m + 4; ram_u_en := max_reg_module m + 6; - ram_ordering := ram_wf (max_reg_module m) |} + ram_ordering_wf := ram_wf (max_reg_module m) |} (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. @@ -2930,11 +2928,11 @@ Proof. - unfold merge_regs. rewrite H12. unfold_merge. unfold find_assocmap, AssocMapExt.get_default in *. rewrite AssocMap.gss; auto. rewrite AssocMap.gso; auto. setoid_rewrite H4. apply Int.eq_true. - pose proof (ram_ordering r); lia. + pose proof (ram_ordering_wf r); unfold ram_ordering in *; lia. - unfold merge_regs. rewrite H11. unfold_merge. unfold find_assocmap, AssocMapExt.get_default in *. rewrite AssocMap.gss; auto. - repeat rewrite AssocMap.gso by (pose proof (ram_ordering r); lia). + repeat rewrite AssocMap.gso by (pose proof (ram_ordering_wf r); unfold ram_ordering in *; lia). setoid_rewrite H3. apply Int.eq_true. Qed. diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v index 91a6673..e4453d1 100644 --- a/src/hls/Renaming.v +++ b/src/hls/Renaming.v @@ -129,6 +129,22 @@ Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) := ret (Vnonblock e1' e2') end. +Program Definition renumber_ram (mr : option HTL.ram) : mon (option HTL.ram) := + match mr with + | None => ret None + | Some r => + do ram_addr' <- renumber_reg (ram_addr r); + do ram_en' <- renumber_reg (ram_en r); + do ram_d_in' <- renumber_reg (ram_d_in r); + do ram_d_out' <- renumber_reg (ram_d_out r); + do ram_wr_en' <- renumber_reg (ram_wr_en r); + do ram_u_en' <- renumber_reg (ram_u_en r); + match decide_ram_ordering ram_addr' ram_en' ram_d_in' ram_d_out' ram_wr_en' ram_u_en' with + | left wf => ret (Some (mk_ram (ram_size r) (ram_mem r) ram_en' ram_u_en' ram_addr' ram_wr_en' ram_d_in' ram_d_out' wf)) + | right _ => error (Errors.msg "Renaming: Incorrect ordering of RAM registers") + end + end. + Fixpoint xrenumber_reg_assocmap {A} (regmap : list (reg * A)) : mon (list (reg * A)) := match regmap with | nil => ret nil @@ -153,6 +169,8 @@ Definition renumber_module (m : HTL.module) : mon HTL.module := do mod_reset' <- renumber_reg (HTL.mod_reset m); do mod_clk' <- renumber_reg (HTL.mod_clk m); + do mod_ram' <- renumber_ram (HTL.mod_ram m); + do mod_controllogic' <- traverse_ptree1 renumber_stmnt (HTL.mod_controllogic m); do mod_datapath' <- traverse_ptree1 renumber_stmnt (HTL.mod_datapath m); @@ -166,7 +184,7 @@ Definition renumber_module (m : HTL.module) : mon HTL.module := zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned, decide_order mod_st' mod_finish' mod_return' mod_stk' mod_start' mod_reset' mod_clk', max_list_dec mod_params' mod_st', - decide_ram_wf mod_clk' (HTL.mod_ram m) with + decide_ram_wf mod_clk' mod_ram' with | left LEDATA, left LECTRL, left MORD, left WFPARAMS, left WFRAM => ret (HTL.mkmodule mod_params' @@ -184,7 +202,7 @@ Definition renumber_module (m : HTL.module) : mon HTL.module := mod_scldecls' mod_arrdecls' mod_externctrl' - (HTL.mod_ram m) + mod_ram' (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA)) MORD WFRAM -- cgit