Get ApplyExternctrl compiling with RAM inference

1 files changed, 16 insertions, 8 deletions

diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v
index edd413c..ef056cf 100644
--- a/src/hls/ApplyExternctrl.v
+++ b/src/hls/ApplyExternctrl.v
@@ -142,11 +142,19 @@ 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) :
+  Definition option_ram_wf (clk : reg) (mr : option HTL.ram) :
     option (forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive).
-  destruct mr.
-  - intros.
+    refine (
+    match mr with
+    | Some r =>
+      match (plt clk (ram_addr r)) with
+      | left LE => Some _
+      | _ => None
+      end
+    | None => None
+    end).
+    crush.
+  Defined.
 
   Definition module_apply_externctrl : res HTL.module :=
     do mod_start' <- reg_apply_externctrl (HTL.mod_start m);
@@ -168,8 +176,8 @@ Section APPLY_EXTERNCTRL.
           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 =>
+          option_ram_wf mod_clk' (HTL.mod_ram m) with
+    | left LEDATA, left LECTRL, left MORD, left WFPARAMS, Some WFRAM =>
       OK (HTL.mkmodule
           mod_params'
           mod_datapath'
@@ -189,9 +197,9 @@ Section APPLY_EXTERNCTRL.
           (HTL.mod_ram m)
           (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))
           MORD
-          (HTL.mod_ram_wf m)
+          WFRAM
           WFPARAMS)
-    | _, _, _, _ => Error (Errors.msg "ApplyExternctrl")
+    | _, _, _, _, _ => Error (Errors.msg "ApplyExternctrl")
     end.
 End APPLY_EXTERNCTRL.