WIP

1 files changed, 36 insertions, 23 deletions

diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v
index b024b9e..edd413c 100644
--- a/src/hls/ApplyExternctrl.v
+++ b/src/hls/ApplyExternctrl.v
@@ -89,14 +89,14 @@ Section APPLY_EXTERNCTRL.
     end.
 
   Definition cases_apply_externctrl_ (stmnt_apply_externctrl_ : Verilog.stmnt -> res Verilog.stmnt) :=
-    fix cases_apply_externctrl (cs : list (Verilog.expr * Verilog.stmnt)) :=
+    fix cases_apply_externctrl (cs : stmnt_expr_list) :=
       match cs with
-      | nil => OK nil
-      | (c_e, c_s) :: tl =>
+      | Stmntnil  => OK Stmntnil
+      | Stmntcons c_e c_s tl =>
         do c_e' <- expr_apply_externctrl c_e;
         do c_s' <- stmnt_apply_externctrl_ c_s;
         do tl' <- cases_apply_externctrl tl;
-        OK ((c_e', c_s') :: tl')
+        OK (Stmntcons c_e' c_s' tl')
       end.
 
   Fixpoint stmnt_apply_externctrl (stmnt : Verilog.stmnt) {struct stmnt} : res Verilog.stmnt :=
@@ -142,6 +142,12 @@ Section APPLY_EXTERNCTRL.
     do l <- xassocmap_apply_externctrl (AssocMap.elements regmap);
     OK (AssocMap_Properties.of_list l).
 
+
+  Definition decide_ram_wf (clk : reg) (mr : option HTL.ram) :
+    option (forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive).
+  destruct mr.
+  - intros.
+
   Definition module_apply_externctrl : res HTL.module :=
     do mod_start' <- reg_apply_externctrl (HTL.mod_start m);
     do mod_reset' <- reg_apply_externctrl (HTL.mod_reset m);
@@ -159,26 +165,33 @@ Section APPLY_EXTERNCTRL.
     do mod_externctrl' <- assocmap_apply_externctrl (HTL.mod_externctrl m);
 
     match zle (Z.pos (max_pc_map mod_datapath')) Integers.Int.max_unsigned,
-          zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned with
-    | left LEDATA, left LECTRL =>
+          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
+    | left LEDATA, left LECTRL, left MORD, left WFPARAMS =>
       OK (HTL.mkmodule
-             mod_params'
-             mod_datapath'
-             mod_controllogic'
-             (HTL.mod_entrypoint m)
-             mod_st'
-             mod_stk'
-             (HTL.mod_stk_len m)
-             mod_finish'
-             mod_return'
-             mod_start'
-             mod_reset'
-             mod_clk'
-             mod_scldecls'
-             mod_arrdecls'
-             mod_externctrl'
-             (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA)))
-    | _, _ => Error (Errors.msg "More than 2^32 states.")
+          mod_params'
+          mod_datapath'
+          mod_controllogic'
+          (HTL.mod_entrypoint m)
+          mod_st'
+          mod_stk'
+          (HTL.mod_stk_len m)
+          mod_finish'
+          mod_return'
+          mod_start'
+          mod_reset'
+          mod_clk'
+          mod_scldecls'
+          mod_arrdecls'
+          mod_externctrl'
+          (HTL.mod_ram m)
+          (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))
+          MORD
+          (HTL.mod_ram_wf m)
+          WFPARAMS)
+    | _, _, _, _ => Error (Errors.msg "ApplyExternctrl")
     end.
 End APPLY_EXTERNCTRL.