Address ram in renaming pass

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 <? b) && (b <? c) && (c <? d)
+                          && (d <? e) && (e <? f))%positive true with
+          | left t => left _
+          | _ => _
+          end); auto.
+  simplify; repeat match goal with
+                   | H: context[(_ <? _)%positive] |- _ => 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