Fix compilation with new HTL language

1 files changed, 41 insertions, 31 deletions

diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index f4552a5..551c66e 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -57,8 +57,6 @@ 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 module_ordering a b c d e f g := a < b < c /\ c < d < e /\ e < f < g.
-
 Record module: Type :=
   mkmodule {
     mod_params : list reg;
@@ -66,8 +64,6 @@ Record module: Type :=
     mod_controllogic : controllogic;
     mod_entrypoint : node;
     mod_st : reg;
-    mod_stk : reg;
-    mod_stk_len : nat;
     mod_finish : reg;
     mod_return : reg;
     mod_start : reg;
@@ -75,11 +71,7 @@ Record module: Type :=
     mod_clk : reg;
     mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl);
     mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl);
-    mod_ram : option ram;
-    mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath;
-    mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk;
-    mod_ram_wf : forall r', mod_ram = Some r' -> mod_clk < ram_addr r';
-    mod_params_wf : Forall (Pos.gt mod_st) mod_params;
+    mod_ram : ram;
   }.
 
 Definition fundef := AST.fundef module.
@@ -93,7 +85,7 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
   end.
 
 Definition empty_stack (m : module) : Verilog.assocmap_arr :=
-  (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)).
+  (AssocMap.set m.(mod_ram).(ram_mem) (Array.arr_repeat None m.(mod_ram).(ram_size)) (AssocMap.empty Verilog.arr)).
 
 (** * Operational Semantics *)
 
@@ -124,13 +116,13 @@ Inductive state : Type :=
            (args : list value), state.
 
 Inductive exec_ram:
-  Verilog.reg_associations -> Verilog.arr_associations -> option ram ->
+  Verilog.reg_associations -> Verilog.arr_associations -> ram ->
   Verilog.reg_associations -> Verilog.arr_associations -> Prop :=
 | exec_ram_Some_idle:
     forall ra ar r,
       Int.eq (Verilog.assoc_blocking ra)#(ram_en r, 32)
              (Verilog.assoc_blocking ra)#(ram_u_en r, 32) = true ->
-      exec_ram ra ar (Some r) ra ar
+      exec_ram ra ar r ra ar
 | exec_ram_Some_write:
     forall ra ar r d_in addr en wr_en u_en,
       Int.eq en u_en = false ->
@@ -140,7 +132,7 @@ Inductive exec_ram:
       (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some wr_en ->
       (Verilog.assoc_blocking ra)!(ram_d_in r) = Some d_in ->
       (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr ->
-      exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) ra u_en)
+      exec_ram ra ar r (Verilog.nonblock_reg (ram_en r) ra u_en)
                (Verilog.nonblock_arr (ram_mem r) (valueToNat addr) ar d_in)
 | exec_ram_Some_read:
     forall ra ar r addr v_d_out en u_en,
@@ -151,11 +143,8 @@ Inductive exec_ram:
       (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr ->
       Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar)
                                   (ram_mem r) (valueToNat addr) = Some v_d_out ->
-      exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r)
-                               (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) u_en) ar
-| exec_ram_None:
-    forall r a,
-      exec_ram r a None r a.
+      exec_ram ra ar r (Verilog.nonblock_reg (ram_en r)
+                               (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) u_en) ar.
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
@@ -233,6 +222,10 @@ Definition semantics (m : program) :=
   Smallstep.Semantics step (initial_state m) final_state
                       (Globalenvs.Genv.globalenv m).
 
+Definition all_module_regs m :=
+  all_ram_regs (mod_ram m) ++
+               (mod_st m::mod_finish m::mod_return m::mod_start m::mod_reset m::mod_clk m::nil).
+
 Definition max_pc_function (m: module) :=
   List.fold_left Pos.max (List.map fst (PTree.elements m.(mod_controllogic))) 1.
 
@@ -253,17 +246,20 @@ Definition max_reg_ram r :=
                      (Pos.max (ram_d_out ram) (ram_u_en ram)))))))
   end.
 
-Definition max_reg_module m :=
+Definition max_reg_body m :=
   Pos.max (max_list (mod_params m))
-   (Pos.max (max_stmnt_tree (mod_datapath m))
-    (Pos.max (max_stmnt_tree (mod_controllogic m))
-     (Pos.max (mod_st m)
-      (Pos.max (mod_stk m)
-       (Pos.max (mod_finish m)
-        (Pos.max (mod_return m)
-         (Pos.max (mod_start m)
-          (Pos.max (mod_reset m)
-           (Pos.max (mod_clk m) (max_reg_ram (mod_ram m))))))))))).
+          (Pos.max (max_stmnt_tree (mod_datapath m))
+                   (max_stmnt_tree (mod_controllogic m))).
+
+Definition max_reg_module m :=
+  Pos.max (max_reg_body m) (max_list (all_module_regs m)).
+
+Record wf_htl_module m :=
+  mk_wf_htl_module {
+      mod_wf : map_well_formed (mod_controllogic m) /\ map_well_formed (mod_datapath m);
+      mod_ordering_wf : list_norepet (all_module_regs m);
+      mod_gt : Forall (Pos.lt (max_reg_body m)) (all_module_regs m);
+    }.
 
 Lemma max_fold_lt :
   forall m l n, m <= n -> m <= (fold_left Pos.max l n).
@@ -320,12 +316,16 @@ Proof. intros. apply max_reg_stmnt_le_stmnt_tree in H; lia. Qed.
 
 Lemma max_stmnt_lt_module :
   forall m d i,
+    wf_htl_module m ->
     (mod_controllogic m) ! i = Some d \/ (mod_datapath m) ! i = Some d ->
     Verilog.max_reg_stmnt d < max_reg_module m + 1.
 Proof.
-  inversion 1 as [ Hv | Hv ]; unfold max_reg_module;
-  apply max_reg_stmnt_le_stmnt_tree in Hv; lia.
-Qed.
+  intros. apply mod_gt in H.
+  unfold Pos.lt, max_reg_body, max_reg_module, max_list, all_module_regs, all_ram_regs in *.
+  simplify.
+  repeat match goal with H: Forall _ _ |- _ => inv H end.
+  inversion H0 as [Hv | Hv]; apply max_reg_stmnt_le_stmnt_tree in Hv.
+  Admitted.
 
 Lemma max_list_correct l st : st > max_list l -> Forall (Pos.gt st) l.
 Proof. induction l; crush; constructor; [|apply IHl]; lia. Qed.
@@ -339,3 +339,13 @@ Definition max_list_dec (l: list reg) (st: reg) : {Forall (Pos.gt st) l} + {True
     ); auto.
   apply max_list_correct. apply Pos.ltb_lt in e. lia.
 Qed.
+
+Variant wf_htl_fundef: fundef -> Prop :=
+  | wf_htl_fundef_external: forall ef,
+      wf_htl_fundef (AST.External ef)
+  | wf_htl_function_internal: forall f,
+      wf_htl_module f ->
+      wf_htl_fundef (AST.Internal f).
+
+Definition wf_htl_program (p: program) : Prop :=
+  forall f id, In (id, AST.Gfun f) (AST.prog_defs p) -> wf_htl_fundef f.