Move renumbering to be HTL->HTL

4 files changed, 234 insertions, 237 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index a87dacf..b5b33e7 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -80,7 +80,7 @@ We then need to declare the external OCaml functions used to print out intermedi
 |*)
 
 Parameter print_RTL: Z -> RTL.program -> unit.
-Parameter print_HTL: HTL.program -> unit.
+Parameter print_HTL: Z -> HTL.program -> unit.
 Parameter print_RTLBlock: Z -> RTLBlock.program -> unit.
 
 Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
@@ -190,7 +190,9 @@ Definition transf_backend (r : RTL.program) : res Verilog.program :=
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 7)
   @@@ HTLgen.transl_program
-   @@ print print_HTL
+   @@ print (print_HTL 1)
+  @@@ HTLgen.renumber_program
+   @@ print (print_HTL 2)
   @@@ Veriloggen.transl_program.
 
 Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
@@ -236,7 +238,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_RTLBlock 2)
   @@@ RTLPargen.transl_program
   @@@ HTLPargen.transl_program
-   @@ print print_HTL
+   @@ print (print_HTL 1)
   @@@ Veriloggen.transl_program.
 
 (*|
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index a12b7f9..9347f39 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -28,6 +28,7 @@ Require Import compcert.backend.RTL.
 
 Require Import vericert.common.Statemonad.
 Require Import vericert.common.Vericertlib.
+Require Import vericert.common.Maps.
 Require Import vericert.hls.AssocMap.
 Require Import vericert.hls.HTL.
 Require Import vericert.hls.ValueInt.
@@ -652,6 +653,218 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program :=
                              (fun i v => Errors.OK v) p.
 *)
 
+Record renumber_state: Type :=
+  mk_renumber_state {
+    renumber_freshreg : reg;
+    renumber_regmap : PTree.t reg;
+    renumber_clk : reg;
+  }.
+
+Module RenumberState <: State.
+  Definition st := renumber_state.
+
+  Definition st_prop (st1 st2 : st) := renumber_clk st1 = renumber_clk st2.
+
+  Lemma st_refl : forall (s : st), st_prop s s.
+  Proof. constructor. Qed.
+
+  Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
+  Proof. congruence. Qed.
+End RenumberState.
+
+Module RenumberMonad := Statemonad(RenumberState).
+Module RenumberMonadExtra := Monad.MonadExtra(RenumberMonad).
+
+Section RENUMBER.
+  Import RenumberMonad.
+  Import RenumberState.
+  Import RenumberMonadExtra.
+  Import MonadNotation.
+
+  Program Definition map_reg (r: reg) : mon reg :=
+    fun st => OK
+         (renumber_freshreg st)
+         (mk_renumber_state (Pos.succ (renumber_freshreg st))
+                            (PTree.set r (renumber_freshreg st) (renumber_regmap st))
+                            (renumber_clk st))
+         _.
+  Next Obligation. unfold st_prop; auto. Qed.
+
+  Program Definition clear_mapping : mon unit :=
+    fun st => OK
+         tt
+         (mk_renumber_state (renumber_freshreg st)
+                            (PTree.empty reg)
+                            (renumber_clk st))
+         _.
+  Next Obligation. unfold st_prop; auto. Qed.
+
+  Definition renumber_reg (r : reg) : mon reg :=
+    do st <- get;
+    match PTree.get r (renumber_regmap st) with
+    | Some reg' => ret reg'
+    | None => map_reg r
+    end.
+
+  Definition get_clk : mon reg := do st <- get; ret (renumber_clk st).
+
+  Fixpoint renumber_expr (expr : Verilog.expr) :=
+    match expr with
+    | Vlit val => ret (Vlit val)
+    | Vvar reg =>
+      do reg' <- renumber_reg reg;
+      ret (Vvar reg')
+    | Vvari reg e =>
+      do reg' <- renumber_reg reg;
+      do e' <- renumber_expr e;
+      ret (Vvari reg' e')
+    | Vinputvar reg =>
+      do reg' <- renumber_reg reg;
+      ret (Vvar reg')
+    | Vbinop op e1 e2 =>
+      do e1' <- renumber_expr e1;
+      do e2' <- renumber_expr e2;
+      ret (Vbinop op e1' e2')
+    | Vunop op e =>
+      do e' <- renumber_expr e;
+      ret (Vunop op e')
+    | Vternary e1 e2 e3 =>
+      do e1' <- renumber_expr e1;
+      do e2' <- renumber_expr e2;
+      do e3' <- renumber_expr e3;
+      ret (Vternary e1' e2' e3')
+    | Vrange r e1 e2 =>
+      do e1' <- renumber_expr e1;
+      do e2' <- renumber_expr e2;
+      do r' <- renumber_reg r;
+      ret (Vrange r e1' e2')
+    end.
+
+  Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) :=
+    match stmnt with
+    | Vskip => ret Vskip
+    | Vseq s1 s2 =>
+      do s1' <- renumber_stmnt s1;
+      do s2' <- renumber_stmnt s2;
+      ret (Vseq s1' s2')
+    | Vcond e s1 s2 =>
+      do e' <- renumber_expr e;
+      do s1' <- renumber_stmnt s1;
+      do s2' <- renumber_stmnt s2;
+      ret (Vcond e' s1' s2')
+    | Vcase e cs def =>
+      do e' <- renumber_expr e;
+      do cs' <- sequence (map
+                       (fun (c : (Verilog.expr * Verilog.stmnt)) =>
+                      let (c_expr, c_stmnt) := c in
+                      do expr' <- renumber_expr c_expr;
+                      do stmnt' <- renumber_stmnt c_stmnt;
+                      ret (expr', stmnt')) cs);
+      do def' <- match def with
+                | None => ret None
+                | Some d => do def' <- renumber_stmnt d; ret (Some def')
+                end;
+      ret (Vcase e' cs' def')
+    | Vblock e1 e2 =>
+      do e1' <- renumber_expr e1;
+      do e2' <- renumber_expr e2;
+      ret (Vblock e1' e2')
+    | Vnonblock e1 e2 =>
+      do e1' <- renumber_expr e1;
+      do e2' <- renumber_expr e2;
+      ret (Vnonblock e1' e2')
+    end.
+
+  Definition renumber_module (m : HTL.module) : mon HTL.module :=
+      do mod_start' <- renumber_reg (HTL.mod_start m);
+      do mod_reset' <- renumber_reg (HTL.mod_reset m);
+      do mod_clk' <- get_clk;
+      do mod_finish' <- renumber_reg (HTL.mod_finish m);
+      do mod_return' <- renumber_reg (HTL.mod_return m);
+      do mod_st' <- renumber_reg (HTL.mod_st m);
+      do mod_stk' <- renumber_reg (HTL.mod_stk m);
+      do mod_params' <- traverselist renumber_reg (HTL.mod_params m);
+      do mod_controllogic' <- traverse_ptree1 renumber_stmnt (HTL.mod_controllogic m);
+      do mod_datapath' <- traverse_ptree1 renumber_stmnt (HTL.mod_datapath m);
+
+      do _ <- clear_mapping;
+
+      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 =>
+        ret (HTL.mkmodule
+           mod_params'
+           mod_datapath'
+           mod_controllogic'
+           (HTL.mod_entrypoint m)
+           mod_st'
+           (HTL.mod_stk m)
+           (HTL.mod_stk_len m)
+           mod_finish'
+           mod_return'
+           mod_start'
+           mod_reset'
+           mod_clk'
+           (HTL.mod_scldecls m)
+           (HTL.mod_arrdecls m)
+           (HTL.mod_externctrl m)
+           (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA)))
+      | _, _ => error (Errors.msg "More than 2^32 states.")
+      end.
+
+  Definition renumber_fundef (fundef : HTL.fundef) : mon HTL.fundef :=
+    match fundef with
+    | Internal m => do renumbered <- renumber_module m; ret (Internal renumbered)
+    | _ => ret fundef
+    end.
+
+  Section TRANSF_PROGRAM_STATEFUL.
+    Import RenumberMonad.
+    Import RenumberState.
+    Import RenumberMonadExtra.
+    Import MonadNotation.
+
+    Variables A B V : Type.
+    Variable transf_fun: ident -> A -> RenumberMonad.mon B.
+
+    Fixpoint transf_globdefs (l: list (ident * globdef A V)) : RenumberMonad.mon (list (ident * globdef B V)) :=
+      match l with
+      | nil => RenumberMonad.ret nil
+      | (id, Gfun f) :: l' =>
+        do tf <- transf_fun id f;
+        do tl' <- transf_globdefs l';
+        RenumberMonad.ret ((id, Gfun tf) :: tl')
+      | (id, Gvar v) :: l' =>
+        do tl' <- transf_globdefs l';
+        RenumberMonad.ret ((id, Gvar v) :: tl')
+      end.
+
+    Definition transform_stateful_program (init_state : RenumberState.st) (p: AST.program A V) : Errors.res (AST.program B V) :=
+      RenumberMonad.run_mon init_state (
+                          do gl' <- transf_globdefs p.(prog_defs);
+                          RenumberMonad.ret (mkprogram gl' p.(prog_public) p.(prog_main))).
+
+  End TRANSF_PROGRAM_STATEFUL.
+
+  Definition get_main_clk (p : HTL.program) : Errors.res reg :=
+    let ge := Globalenvs.Genv.globalenv p in
+    match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with
+    | Some b =>
+      match Globalenvs.Genv.find_funct_ptr ge b with
+      | Some (AST.Internal m) => Errors.OK (HTL.mod_clk m)
+      | _ => Errors.Error (Errors.msg "Cannot find internal main for renumbering")
+      end
+    | _ => Errors.Error (Errors.msg "Cannot find internal main for renumbering")
+    end.
+
+  Definition renumber_program (p : HTL.program) : Errors.res HTL.program :=
+    Errors.bind (get_main_clk p)
+                (fun main_clk => transform_stateful_program _ _ _
+                                                         (fun _ => renumber_fundef)
+                                                         (mk_renumber_state 1%positive (PTree.empty reg) main_clk)
+                                                         p).
+End RENUMBER.
+
 Definition main_is_internal (p : RTL.program) : bool :=
   let ge := Globalenvs.Genv.globalenv p in
   match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with
diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml
index 78e422a..65fe1f3 100644
--- a/src/hls/PrintHTL.ml
+++ b/src/hls/PrintHTL.ml
@@ -70,10 +70,10 @@ let print_program pp prog =
 
 let destination : string option ref = ref None
 
-let print_if prog =
+let print_if passno prog =
   match !destination with
   | None -> ()
   | Some f ->
-    let oc = open_out f in
-    print_program oc prog;
-    close_out oc
+      let oc = open_out (f ^ "." ^ Z.to_string passno) in
+      print_program oc prog;
+      close_out oc
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v
index 2ced686..0e359fd 100644
--- a/src/hls/Veriloggen.v
+++ b/src/hls/Veriloggen.v
@@ -31,235 +31,23 @@ Import ListNotations.
 
 Local Open Scope error_monad_scope.
 
-Record renumber_state: Type :=
-  mk_renumber_state {
-    st_freshreg : reg;
-    st_regmap : PTree.t reg;
-  }.
-
-Module RenumberState <: State.
-  Definition st := renumber_state.
-
-  Definition st_prop (st1 st2 : st) := True.
-
-  Lemma st_refl : forall (s : st), st_prop s s.
-  Proof. constructor. Qed.
-
-  Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
-  Proof. constructor. Qed.
-End RenumberState.
-
-Module VerilogMonad := Statemonad(RenumberState).
-
-Module VerilogMonadExtra := Monad.MonadExtra(VerilogMonad).
-
-Section RENUMBER.
-  Export RenumberState.
-  Export VerilogMonad.
-  Import VerilogMonadExtra.
-  Export MonadNotation.
-
-  Definition renumber_reg (r : reg) : mon reg :=
-    do st <- get;
-    match PTree.get r st.(st_regmap) with
-    | Some reg' => ret reg'
-    | None =>
-      do tt <- set (mk_renumber_state (Pos.succ st.(st_freshreg)) (PTree.set r st.(st_freshreg) st.(st_regmap))) (fun _ => I);
-      ret st.(st_freshreg)
-    end.
-
-  Fixpoint renumber_edge (edge : Verilog.edge) :=
-    match edge with
-    | Vposedge r =>
-      do r' <- renumber_reg r;
-      ret (Vposedge r')
-    | Vnegedge r =>
-      do r' <- renumber_reg r;
-      ret (Vposedge r')
-    | Valledge => ret Valledge
-    | Voredge e1 e2 =>
-      do e1' <- renumber_edge e1;
-      do e2' <- renumber_edge e2;
-      ret (Voredge e1' e2')
-    end.
-
-  Definition renumber_declaration (decl : Verilog.declaration) :=
-    match decl with
-    | Vdecl io reg sz =>
-      do reg' <- renumber_reg reg;
-      ret (Vdecl io reg' sz)
-    | Vdeclarr io reg sz len =>
-      do reg' <- renumber_reg reg;
-      ret (Vdeclarr io reg' sz len)
-    end.
-
-  Fixpoint renumber_expr (expr : Verilog.expr) :=
-    match expr with
-    | Vlit val => ret (Vlit val)
-    | Vvar reg =>
-      do reg' <- renumber_reg reg;
-      ret (Vvar reg')
-    | Vvari reg e =>
-      do reg' <- renumber_reg reg;
-      do e' <- renumber_expr e;
-      ret (Vvari reg' e')
-    | Vinputvar reg =>
-      do reg' <- renumber_reg reg;
-      ret (Vvar reg')
-    | Vbinop op e1 e2 =>
-      do e1' <- renumber_expr e1;
-      do e2' <- renumber_expr e2;
-      ret (Vbinop op e1' e2')
-    | Vunop op e =>
-      do e' <- renumber_expr e;
-      ret (Vunop op e')
-    | Vternary e1 e2 e3 =>
-      do e1' <- renumber_expr e1;
-      do e2' <- renumber_expr e2;
-      do e3' <- renumber_expr e3;
-      ret (Vternary e1' e2' e3')
-    | Vrange r e1 e2 =>
-      do e1' <- renumber_expr e1;
-      do e2' <- renumber_expr e2;
-      do r' <- renumber_reg r;
-      ret (Vrange r e1' e2')
-    end.
-
-  Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) :=
-    match stmnt with
-    | Vskip => ret Vskip
-    | Vseq s1 s2 =>
-      do s1' <- renumber_stmnt s1;
-      do s2' <- renumber_stmnt s2;
-      ret (Vseq s1' s2')
-    | Vcond e s1 s2 =>
-      do e' <- renumber_expr e;
-      do s1' <- renumber_stmnt s1;
-      do s2' <- renumber_stmnt s2;
-      ret (Vcond e' s1' s2')
-    | Vcase e cs def =>
-      do e' <- renumber_expr e;
-      do cs' <- sequence (map
-                       (fun (c : (Verilog.expr * Verilog.stmnt)) =>
-                      let (c_expr, c_stmnt) := c in
-                      do expr' <- renumber_expr c_expr;
-                      do stmnt' <- renumber_stmnt c_stmnt;
-                      ret (expr', stmnt')) cs);
-      do def' <- match def with
-                | None => ret None
-                | Some d => do def' <- renumber_stmnt d; ret (Some def')
-                end;
-      ret (Vcase e' cs' def')
-    | Vblock e1 e2 =>
-      do e1' <- renumber_expr e1;
-      do e2' <- renumber_expr e2;
-      ret (Vblock e1' e2')
-    | Vnonblock e1 e2 =>
-      do e1' <- renumber_expr e1;
-      do e2' <- renumber_expr e2;
-      ret (Vnonblock e1' e2')
-    end.
-
-  Definition renumber_module_item (item : Verilog.module_item) :=
-    match item with
-    | Vdeclaration decl =>
-      do decl' <- renumber_declaration decl;
-      ret (Vdeclaration decl')
-    | Valways edge stmnt =>
-      do edge' <- renumber_edge edge;
-      do stmnt' <- renumber_stmnt stmnt;
-      ret (Valways edge' stmnt')
-    | Valways_ff edge stmnt =>
-      do edge' <- renumber_edge edge;
-      do stmnt' <- renumber_stmnt stmnt;
-      ret (Valways edge' stmnt')
-    | Valways_comb edge stmnt =>
-      do edge' <- renumber_edge edge;
-      do stmnt' <- renumber_stmnt stmnt;
-      ret (Valways edge' stmnt')
-    end.
-
-  Definition renumber_module (m : Verilog.module) : mon Verilog.module :=
-    do mod_start' <- renumber_reg (Verilog.mod_start m);
-    do mod_reset' <- renumber_reg (Verilog.mod_reset m);
-    do mod_clk' <- renumber_reg (Verilog.mod_clk m);
-    do mod_finish' <- renumber_reg (Verilog.mod_finish m);
-    do mod_return' <- renumber_reg (Verilog.mod_return m);
-    do mod_st' <- renumber_reg (Verilog.mod_st m);
-    do mod_stk' <- renumber_reg (Verilog.mod_stk m);
-    do mod_args' <- traverselist renumber_reg (Verilog.mod_args m);
-    do mod_body' <- traverselist renumber_module_item (Verilog.mod_body m);
-
-    ret (Verilog.mkmodule
-       mod_start'
-       mod_reset'
-       mod_clk'
-       mod_finish'
-       mod_return'
-       mod_st'
-       mod_stk'
-       (Verilog.mod_stk_len m)
-       mod_args'
-       mod_body'
-       (Verilog.mod_entrypoint m)).
-
-  Definition renumber_all_modules
-             (modules : PTree.t Verilog.module)
-             (start_reg : reg)
-             (clk : reg) : Errors.res (PTree.t Verilog.module) :=
-
-    run_mon (mk_renumber_state start_reg (PTree.empty reg))
-            (VerilogMonadExtra.traverse_ptree1 (fun m =>
-                  do st <- VerilogMonad.get;
-                  do _ <- VerilogMonad.set
-                       (mk_renumber_state (st_freshreg st)
-                                          (PTree.set (mod_clk m) clk
-                                                     (PTree.empty reg)))
-                       (fun _ => I);
-                  renumber_module m)
-           modules).
-End RENUMBER.
-
 
 Section TRANSLATE.
   Local Open Scope error_monad_scope.
 
-  Definition transl_datapath_fun (modmap : PTree.t Verilog.module) (a : Verilog.node * HTL.datapath_stmnt) :=
+  Definition transl_datapath_fun (a : Verilog.node * HTL.datapath_stmnt) :=
     let (n, s) := a in
     let node := Verilog.Vlit (posToValue n) in
-    match s with
-    | HTL.HTLfork mod_name args =>
-      do m <- handle_opt (Errors.msg "module does not exist") (modmap ! mod_name);
-      let reset_mod := Vnonblock (Vvar (Verilog.mod_reset m)) (posToLit 1) in
-      let zipped_args := List.combine (Verilog.mod_args m) args in
-      let assign_args :=
-          List.fold_left (fun (acc : stmnt) (a : reg * reg) => let (to, from) := a in
-                                                            Vseq acc (Vnonblock (Vvar to) (Vvar from)))
-                         zipped_args Vskip in
-      OK (node, Vseq reset_mod assign_args)
-    | HTL.HTLjoin mod_name dst =>
-      do m <- handle_opt (Errors.msg "module does not exist") (modmap ! mod_name);
-      let set_result := Vnonblock (Vvar dst) (Vvar (Verilog.mod_return m)) in
-      let stop_reset := Vnonblock (Vvar (Verilog.mod_reset m)) (Vlit (ZToValue 0)) in
-      OK (node, Vseq stop_reset set_result)
-    | HTL.HTLDataVstmnt s => OK (node, s)
-    end.
+    OK (node, s).
 
-  Definition transl_datapath modmap st := Errors.mmap (transl_datapath_fun modmap) st.
+  Definition transl_datapath st := Errors.mmap transl_datapath_fun st.
 
-  Definition transl_ctrl_fun (modmap : PTree.t Verilog.module) (a : Verilog.node * HTL.control_stmnt) : Errors.res (Verilog.expr * Verilog.stmnt):=
+  Definition transl_ctrl_fun (a : Verilog.node * HTL.control_stmnt) : Errors.res (Verilog.expr * Verilog.stmnt):=
     let (n, s) := a in
     let node := Verilog.Vlit (posToValue n) in
-    match s with
-    | HTL.HTLwait mod_name status expr =>
-      do mod_body <- handle_opt (Errors.msg "module does not exist") (PTree.get mod_name modmap);
-      let is_done := Vbinop Veq (Vvar (Verilog.mod_finish mod_body)) (Vlit (posToValue 1)) in
-      let continue := Vnonblock (Vvar status) expr in
-      Errors.OK (node, Verilog.Vcond is_done continue Vskip)
-    | HTL.HTLCtrlVstmnt s => Errors.OK (node, s)
-    end.
+    Errors.OK (node, s).
 
-  Definition transl_ctrl modmap st := Errors.mmap (transl_ctrl_fun modmap) st.
+  Definition transl_ctrl st := Errors.mmap transl_ctrl_fun st.
 
   Definition scl_to_Vdecl_fun (a : reg * (option Verilog.io * Verilog.scl_decl)) :=
     match a with (r, (io, Verilog.VScalar sz)) => (Verilog.Vdecl io r sz) end.
@@ -271,13 +59,8 @@ Section TRANSLATE.
 
   Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl.
 
-  Definition called_functions (stmnts : list (Verilog.node * HTL.datapath_stmnt)) : list ident :=
-    List.nodup Pos.eq_dec (Option.map_option (fun (a : (positive * HTL.datapath_stmnt)) =>
-                                   let (n, stmt) := a in
-                                   match stmt with
-                                   | HTL.HTLfork fn _ => Some fn
-                                   | _ => None
-                                   end) stmnts).
+  Definition called_functions (m : HTL.module) : list ident :=
+    List.nodup Pos.eq_dec (List.map (Basics.compose fst snd) (PTree.elements (HTL.mod_externctrl m))).
 
   Definition find_module (program : HTL.program) (name : ident) : Errors.res HTL.module :=
     match option_map snd (find (fun named_module => Pos.eqb (fst named_module) name) program.(prog_defs)) with
@@ -323,17 +106,16 @@ Section TRANSLATE.
     | S fuel' =>
 
       let inline_start_reg := max_reg_module m in
-      let inline_names := called_functions (PTree.elements (HTL.mod_datapath m)) in
+      let inline_names := called_functions m in
       let htl_modules := PTree.filter
                        (fun m _ => List.existsb (Pos.eqb m) inline_names)
                        (prog_modmap program) in
       do translated_modules <- PTree.traverse (fun _ => transf_module fuel' program) htl_modules;
-      do renumbered_modules <- renumber_all_modules translated_modules (max_reg_module m) (HTL.mod_clk m);
       let cleaned_modules := PTree.map1 (map_body (Option.map_option (clean_up_decl (HTL.mod_clk m))))
-                                        renumbered_modules in
+                                        translated_modules in
 
-      do case_el_ctrl <- transl_ctrl renumbered_modules (PTree.elements (HTL.mod_controllogic m));
-      do case_el_data <- transl_datapath renumbered_modules (PTree.elements (HTL.mod_datapath m));
+      do case_el_ctrl <- transl_ctrl (PTree.elements (HTL.mod_controllogic m));
+      do case_el_data <- transl_datapath (PTree.elements (HTL.mod_datapath m));
 
       let body : list Verilog.module_item:=
           Valways (Vposedge (HTL.mod_clk m)) (Vcond (Vbinop Veq (Vvar (HTL.mod_reset m)) (Vlit (ZToValue 1)))