Add wait instruction to HTL control path

7 files changed, 152 insertions, 76 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 6a4feb5..43c3d04 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -44,7 +44,7 @@ Definition init_state (st : reg) : state :=
           (AssocMap.empty (option io * scl_decl))
           (AssocMap.empty (option io * arr_decl))
           (AssocMap.empty datapath_stmnt)
-          (AssocMap.empty stmnt).
+          (AssocMap.empty control_stmnt).
 
 Module HTLState <: State.
 
@@ -87,13 +87,15 @@ Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
 Import HTLMonadExtra.
 Export MonadNotation.
 
-Definition state_goto (st : reg) (n : node) : stmnt :=
-  Vnonblock (Vvar st) (Vlit (posToValue n)).
+Definition data_vstmnt : Verilog.stmnt -> HTL.datapath_stmnt := HTLDataVstmnt.
+Definition ctrl_vstmnt : Verilog.stmnt -> HTL.control_stmnt := HTLCtrlVstmnt.
 
-Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
-  Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).
+Definition state_goto (st : reg) (n : node) : control_stmnt :=
+  ctrl_vstmnt (Vnonblock (Vvar st) (Vlit (posToValue n))).
+
+Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : control_stmnt :=
+  ctrl_vstmnt (Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2))).
 
-Definition vstmnt : Verilog.stmnt -> HTL.datapath_stmnt := HTLVstmnt.
 Definition nonblock (dst : reg) (e : expr) := (Vnonblock (Vvar dst) e).
 Definition block (dst : reg) (e : expr) := (Vblock (Vvar dst) e).
 
@@ -109,25 +111,6 @@ Proof.
   intros. case (s.(st_controllogic)!n); tauto.
 Defined.
 
-Lemma add_instr_state_incr :
-  forall s n n' st,
-    (st_datapath s)!n = None ->
-    (st_controllogic s)!n = None ->
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       (st_freshstate s)
-       s.(st_scldecls)
-       s.(st_arrdecls)
-       (AssocMap.set n st s.(st_datapath))
-       (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).
-Proof.
-  constructor; intros;
-    try (simpl; destruct (peq n n0); subst);
-    auto with htlh.
-Qed.
-
 Lemma declare_reg_state_incr :
   forall i s r sz,
     st_incr s
@@ -176,6 +159,25 @@ Definition create_state : mon node :=
                    (st_controllogic s))
               (create_state_state_incr s).
 
+Lemma add_instr_state_incr :
+  forall s n n' st,
+    (st_datapath s)!n = None ->
+    (st_controllogic s)!n = None ->
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       s.(st_scldecls)
+       s.(st_arrdecls)
+       (AssocMap.set n st s.(st_datapath))
+       (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
 Definition add_instr (n : node) (n' : node) (st : datapath_stmnt) : mon unit :=
   fun s =>
     match check_empty_node_datapath s n, check_empty_node_controllogic s n with
@@ -204,13 +206,48 @@ Lemma add_instr_skip_state_incr :
        s.(st_scldecls)
        s.(st_arrdecls)
        (AssocMap.set n st s.(st_datapath))
-       (AssocMap.set n Vskip s.(st_controllogic))).
+       (AssocMap.set n (ctrl_vstmnt Vskip) s.(st_controllogic))).
 Proof.
   constructor; intros;
     try (simpl; destruct (peq n n0); subst);
     auto with htlh.
 Qed.
 
+Lemma add_instr_wait_state_incr :
+  forall wait_mod s n n' st,
+    (st_datapath s)!n = None ->
+    (st_controllogic s)!n = None ->
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       s.(st_scldecls)
+       s.(st_arrdecls)
+       (AssocMap.set n st s.(st_datapath))
+       (AssocMap.set n (HTLwait wait_mod s.(st_st) (Vlit (posToValue n'))) s.(st_controllogic))).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
+Definition add_instr_wait (wait_mod : ident) (n : node) (n' : node) (st : datapath_stmnt) : mon unit :=
+  fun s =>
+    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+    | left STM, left TRANS =>
+      OK tt (mkstate
+               s.(st_st)
+               s.(st_freshreg)
+               (st_freshstate s)
+               s.(st_scldecls)
+               s.(st_arrdecls)
+               (AssocMap.set n st s.(st_datapath))
+               (AssocMap.set n (HTLwait wait_mod s.(st_st) (Vlit (posToValue n'))) s.(st_controllogic)))
+         (add_instr_wait_state_incr wait_mod s n n' st STM TRANS)
+    | _, _ => Error (Errors.msg "HTL.add_instr_wait")
+    end.
+
 Definition add_instr_skip (n : node) (st : datapath_stmnt) : mon unit :=
   fun s =>
     match check_empty_node_datapath s n, check_empty_node_controllogic s n with
@@ -222,7 +259,7 @@ Definition add_instr_skip (n : node) (st : datapath_stmnt) : mon unit :=
                s.(st_scldecls)
                s.(st_arrdecls)
                (AssocMap.set n st s.(st_datapath))
-               (AssocMap.set n Vskip s.(st_controllogic)))
+               (AssocMap.set n (ctrl_vstmnt Vskip) s.(st_controllogic)))
          (add_instr_skip_state_incr s n st STM TRANS)
     | _, _ => Error (Errors.msg "HTL.add_instr")
     end.
@@ -238,7 +275,7 @@ Lemma add_node_skip_state_incr :
        (st_freshstate s)
        s.(st_scldecls)
        s.(st_arrdecls)
-       (AssocMap.set n (vstmnt Vskip) s.(st_datapath))
+       (AssocMap.set n (data_vstmnt Vskip) s.(st_datapath))
        (AssocMap.set n st s.(st_controllogic))).
 Proof.
   constructor; intros;
@@ -246,7 +283,7 @@ Proof.
     auto with htlh.
 Qed.
 
-Definition add_node_skip (n : node) (st : stmnt) : mon unit :=
+Definition add_node_skip (n : node) (st : control_stmnt) : mon unit :=
   fun s =>
     match check_empty_node_datapath s n, check_empty_node_controllogic s n with
     | left STM, left TRANS =>
@@ -256,7 +293,7 @@ Definition add_node_skip (n : node) (st : stmnt) : mon unit :=
                (st_freshstate s)
                s.(st_scldecls)
                s.(st_arrdecls)
-               (AssocMap.set n (vstmnt Vskip) s.(st_datapath))
+               (AssocMap.set n (data_vstmnt Vskip) s.(st_datapath))
                (AssocMap.set n st s.(st_controllogic)))
          (add_node_skip_state_incr s n st STM TRANS)
     | _, _ => Error (Errors.msg "HTL.add_instr")
@@ -411,7 +448,7 @@ Lemma add_branch_instr_state_incr:
                 (st_freshstate s)
                 s.(st_scldecls)
                 s.(st_arrdecls)
-                (AssocMap.set n (vstmnt Vskip) (st_datapath s))
+                (AssocMap.set n (data_vstmnt Vskip) (st_datapath s))
                 (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
 Proof.
   intros. apply state_incr_intro; simpl;
@@ -429,7 +466,7 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
                 (st_freshstate s)
                 s.(st_scldecls)
                 s.(st_arrdecls)
-                (AssocMap.set n (vstmnt Vskip) (st_datapath s))
+                (AssocMap.set n (data_vstmnt Vskip) (st_datapath s))
                 (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
          (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS)
     | _, _ => Error (Errors.msg "Htlgen: add_branch_instr")
@@ -475,24 +512,24 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     match i with
     | Inop n' =>
       if Z.leb (Z.pos n') Integers.Int.max_unsigned then
-        add_instr n n' (vstmnt Vskip)
+        add_instr n n' (data_vstmnt Vskip)
       else error (Errors.msg "State is larger than 2^32.")
     | Iop op args dst n' =>
       if Z.leb (Z.pos n') Integers.Int.max_unsigned then
         do instr <- translate_instr op args;
         do _ <- declare_reg None dst 32;
-        add_instr n n' (vstmnt (nonblock dst instr))
+        add_instr n n' (data_vstmnt (nonblock dst instr))
       else error (Errors.msg "State is larger than 2^32.")
     | Iload mem addr args dst n' =>
       if Z.leb (Z.pos n') Integers.Int.max_unsigned then
         do src <- translate_arr_access mem addr args stack;
         do _ <- declare_reg None dst 32;
-        add_instr n n' (vstmnt (nonblock dst src))
+        add_instr n n' (data_vstmnt (nonblock dst src))
       else error (Errors.msg "State is larger than 2^32.")
     | Istore mem addr args src n' =>
       if Z.leb (Z.pos n') Integers.Int.max_unsigned then
         do dst <- translate_arr_access mem addr args stack;
-        add_instr n n' (vstmnt (Vnonblock dst (Vvar src))) (* TODO: Could juse use add_instr? reg exists. *)
+        add_instr n n' (data_vstmnt (Vnonblock dst (Vvar src))) (* TODO: Could juse use add_instr? reg exists. *)
       else error (Errors.msg "State is larger than 2^32.")
     | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.")
     | Icall sig (inr fn) args dst n' =>
@@ -500,7 +537,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
         do _ <- declare_reg None dst 32;
         do join_state <- create_state;
         do _ <- add_instr n join_state (HTLfork fn args);
-        add_instr join_state n' (HTLjoin fn dst)
+        add_instr_wait fn join_state n' (HTLjoin fn dst)
       else error (Errors.msg "State is larger than 2^32.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
@@ -516,9 +553,9 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     | Ireturn r =>
       match r with
       | Some r' =>
-        add_instr_skip n (vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))))
+        add_instr_skip n (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))))
       | None =>
-        add_instr_skip n (vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))))
+        add_instr_skip n (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))))
       end
     end
   end.
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index ccc5ade..c0a8f75 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -390,7 +390,7 @@ Section CORRECTNESS.
   Lemma op_stack_based :
     forall F V sp v m args rs op ge pc' res0 pc f e fin rtrn st stk,
       tr_instr fin rtrn st stk (RTL.Iop op args res0 pc')
-               (vstmnt (Verilog.Vnonblock (Verilog.Vvar res0) e))
+               (data_vstmnt (Verilog.Vnonblock (Verilog.Vvar res0) e))
                (state_goto st pc') ->
       reg_stack_based_pointers sp rs ->
       (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') ->
@@ -966,12 +966,13 @@ Section CORRECTNESS.
     inv CONST; assumption.
     inv CONST; assumption. 
     (* processing of state *)
-    econstructor.
+    constructor.
     crush.
-    econstructor.
-    econstructor.
-    econstructor.
-    econstructor.
+    constructor.
+    constructor.
+    constructor.
+    constructor.
+    constructor.
 
     all: invert MARR; big_tac.
 
@@ -1004,7 +1005,7 @@ Section CORRECTNESS.
     econstructor; simpl; trivial.
     constructor; trivial.
     econstructor; simpl; eauto.
-    simpl. econstructor. econstructor. econstructor.
+    simpl. econstructor. econstructor. econstructor. constructor.
     apply H5. simplify.
 
     all: big_tac.
@@ -1222,7 +1223,7 @@ Section CORRECTNESS.
       econstructor. econstructor. econstructor. crush.
       econstructor. econstructor.
       econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor.
+      econstructor. econstructor. econstructor.
 
       all: big_tac.
 
@@ -1457,7 +1458,7 @@ Section CORRECTNESS.
       eapply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
       econstructor. econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor. econstructor. econstructor. econstructor. crush.
 
       all: big_tac.
 
@@ -1572,7 +1573,7 @@ Section CORRECTNESS.
       eexists. split.
       eapply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
-      econstructor. econstructor. econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor. econstructor.
       eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
       econstructor.
       econstructor.
@@ -1851,7 +1852,7 @@ Section CORRECTNESS.
       eexists. split.
       eapply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
-      econstructor. econstructor. econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor. constructor.
       eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
       econstructor.
       econstructor. econstructor. econstructor. econstructor.
@@ -2104,7 +2105,7 @@ Section CORRECTNESS.
       eexists. split.
       eapply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
-      econstructor. econstructor. econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor. econstructor.
       eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
       econstructor. econstructor. econstructor. econstructor.
 
@@ -2336,7 +2337,7 @@ Section CORRECTNESS.
       eapply HTL.step_module; eauto.
       inv CONST; assumption.
       inv CONST; assumption.
-      econstructor; simpl; trivial.
+      econstructor; econstructor; simpl; trivial.
       constructor; trivial.
       eapply Verilog.erun_Vternary_true; simpl; eauto.
       eapply eval_cond_correct; eauto. intros.
@@ -2353,7 +2354,7 @@ Section CORRECTNESS.
       eapply HTL.step_module; eauto.
       inv CONST; assumption.
       inv CONST; assumption.
-      econstructor; simpl; trivial.
+      econstructor; econstructor; simpl; trivial.
       constructor; trivial.
       eapply Verilog.erun_Vternary_false; simpl; eauto.
       eapply eval_cond_correct; eauto. intros.
@@ -2407,7 +2408,7 @@ Section CORRECTNESS.
       eapply HTL.step_module; eauto.
       inv CONST; assumption.
       inv CONST; assumption.
-      constructor.
+      constructor. econstructor.
       econstructor; simpl; trivial.
       econstructor; simpl; trivial.
       constructor.
@@ -2438,7 +2439,7 @@ Section CORRECTNESS.
       eapply HTL.step_module; eauto.
       inv CONST; assumption.
       inv CONST; assumption.
-      constructor. constructor.
+      constructor. constructor. econstructor.
       econstructor; simpl; trivial.
       econstructor; simpl; trivial.
       constructor. constructor. constructor.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index e1641b3..10e48f7 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -114,16 +114,16 @@ Ltac monadInv H :=
 statemachine that is created by the translation contains the correct
 translations for each of the elements *)
 
-Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt -> stmnt -> Prop :=
+Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt -> control_stmnt -> Prop :=
 | tr_instr_Inop :
     forall n,
       Z.pos n <= Int.max_unsigned ->
-      tr_instr fin rtrn st stk (RTL.Inop n) (vstmnt Vskip) (state_goto st n)
+      tr_instr fin rtrn st stk (RTL.Inop n) (data_vstmnt Vskip) (state_goto st n)
 | tr_instr_Iop :
     forall n op args dst s s' e i,
       Z.pos n <= Int.max_unsigned ->
       translate_instr op args s = OK e s' i ->
-      tr_instr fin rtrn st stk (RTL.Iop op args dst n) (vstmnt (Vnonblock (Vvar dst) e)) (state_goto st n)
+      tr_instr fin rtrn st stk (RTL.Iop op args dst n) (data_vstmnt (Vnonblock (Vvar dst) e)) (state_goto st n)
 | tr_instr_Icall :
     forall n sig fn args dst,
       Z.pos n <= Int.max_unsigned ->
@@ -133,24 +133,24 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt -
       Z.pos n1 <= Int.max_unsigned ->
       Z.pos n2 <= Int.max_unsigned ->
       translate_condition cond args s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) (vstmnt Vskip) (state_cond st c n1 n2)
+      tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) (data_vstmnt Vskip) (state_cond st c n1 n2)
 | tr_instr_Ireturn_None :
-    tr_instr fin rtrn st stk (RTL.Ireturn None) (vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z)))
-                                                  (block rtrn (Vlit (ZToValue 0%Z))))) Vskip
+    tr_instr fin rtrn st stk (RTL.Ireturn None) (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z)))
+                                                  (block rtrn (Vlit (ZToValue 0%Z))))) (ctrl_vstmnt Vskip)
 | tr_instr_Ireturn_Some :
     forall r,
       tr_instr fin rtrn st stk (RTL.Ireturn (Some r))
-               (vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r)))) Vskip
+               (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r)))) (ctrl_vstmnt Vskip)
 | tr_instr_Iload :
     forall mem addr args s s' i c dst n,
       Z.pos n <= Int.max_unsigned ->
       translate_arr_access mem addr args stk s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (vstmnt (nonblock dst c)) (state_goto st n)
+      tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (data_vstmnt (nonblock dst c)) (state_goto st n)
 | tr_instr_Istore :
     forall mem addr args s s' i c src n,
       Z.pos n <= Int.max_unsigned ->
       translate_arr_access mem addr args stk s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (vstmnt (Vnonblock c (Vvar src)))
+      tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (data_vstmnt (Vnonblock c (Vvar src)))
                (state_goto st n).
 (*| tr_instr_Ijumptable :
     forall cexpr tbl r,
@@ -415,6 +415,13 @@ Lemma add_instr_freshreg_trans :
 Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed.
 Hint Resolve add_instr_freshreg_trans : htlspec.
 
+Lemma add_instr_wait_freshreg_trans :
+  forall m n n' st s r s' i,
+  add_instr_wait m n n' st s = OK r s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof. intros. unfold add_instr_wait in H. repeat (unfold_match H). inv H. auto. Qed.
+Hint Resolve add_instr_freshreg_trans : htlspec.
+
 Lemma add_branch_instr_freshreg_trans :
   forall n n0 n1 e s r s' i,
   add_branch_instr e n n0 n1 s = OK r s' i ->
@@ -459,7 +466,7 @@ Proof.
     apply declare_reg_freshreg_trans in EQ.
     apply add_instr_freshreg_trans in EQ0.
     apply create_state_freshreg_trans in EQ1.
-    apply add_instr_freshreg_trans in EQ3.
+    apply add_instr_wait_freshreg_trans in EQ3.
     congruence.
   - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0.
     congruence.
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index b3557fd..5629b1e 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -54,14 +54,18 @@ Definition transl_datapath_fun (a : Verilog.node * HTL.datapath_stmnt) :=
    match s with
    | HTL.HTLfork m args => Verilog.Vskip (* inline_call m args *)
    | HTL.HTLjoin m dst => Verilog.Vskip (* inline_call m args *)
-   | HTL.HTLVstmnt s => s
+   | HTL.HTLDataVstmnt s => s
    end).
 
 Definition transl_datapath st := map transl_datapath_fun st.
 
-Definition transl_ctrl_fun (a : Verilog.node * Verilog.stmnt) :=
-  let (n, stmnt) := a
-  in (Verilog.Vlit (posToValue n), stmnt).
+Definition transl_ctrl_fun (a : Verilog.node * HTL.control_stmnt) :=
+  let (n, s) := a in
+  (Verilog.Vlit (posToValue n),
+   match s with
+   | HTL.HTLwait _ _ _ => Vskip
+   | HTL.HTLCtrlVstmnt s => s
+   end).
 
 Definition transl_ctrl st := map transl_ctrl_fun st.
 
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index d309033..a3a13f2 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -37,10 +37,14 @@ Definition ident := positive.
 Inductive datapath_stmnt :=
 | HTLfork : ident -> list reg -> datapath_stmnt
 | HTLjoin : ident -> reg -> datapath_stmnt
-| HTLVstmnt : Verilog.stmnt -> datapath_stmnt.
+| HTLDataVstmnt : Verilog.stmnt -> datapath_stmnt.
+
+Inductive control_stmnt :=
+| HTLwait : ident -> reg -> Verilog.expr -> control_stmnt
+| HTLCtrlVstmnt : Verilog.stmnt -> control_stmnt.
 
 Definition datapath := PTree.t datapath_stmnt.
-Definition controllogic := PTree.t Verilog.stmnt.
+Definition controllogic := PTree.t control_stmnt.
 
 Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
   forall p0 : positive,
@@ -115,9 +119,19 @@ Inductive datapath_stmnt_runp:
     datapath_stmnt_runp f ar al (HTLfork i args) ar al
 | stmnt_runp_HTLcall : forall f ar al i dst,
     datapath_stmnt_runp f ar al (HTLjoin i dst) ar al
-| stmnt_runp_HTLVstmnt : forall asr0 asa0 asr1 asa1 f stmnt,
+| stmnt_runp_HTLDataVstmnt : forall asr0 asa0 asr1 asa1 f stmnt,
+    Verilog.stmnt_runp f asr0 asa0 stmnt asr1 asa1 ->
+    datapath_stmnt_runp f asr0 asa0 (HTLDataVstmnt stmnt) asr1 asa1.
+
+Inductive control_stmnt_runp:
+  Verilog.fext -> Verilog.reg_associations -> Verilog.arr_associations ->
+  control_stmnt -> Verilog.reg_associations -> Verilog.arr_associations -> Prop :=
+(* TODO give it an actual semantics *)
+| stmnt_runp_HTLwait : forall f ar al i reg expr,
+    control_stmnt_runp f ar al (HTLwait i reg expr) ar al
+| stmnt_runp_HTLCtrlVstmnt : forall asr0 asa0 asr1 asa1 f stmnt,
     Verilog.stmnt_runp f asr0 asa0 stmnt asr1 asa1 ->
-    datapath_stmnt_runp f asr0 asa0 (HTLVstmnt stmnt) asr1 asa1.
+    control_stmnt_runp f asr0 asa0 (HTLCtrlVstmnt stmnt) asr1 asa1.
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
@@ -132,7 +146,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       asr!(m.(mod_st)) = Some (posToValue st) ->
       m.(mod_controllogic)!st = Some ctrl ->
       m.(mod_datapath)!st = Some data ->
-      Verilog.stmnt_runp f
+      control_stmnt_runp f
         (Verilog.mkassociations asr empty_assocmap)
         (Verilog.mkassociations asa (empty_stack m))
         ctrl
diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml
index 430a4b4..aa90dbe 100644
--- a/src/verilog/PrintHTL.ml
+++ b/src/verilog/PrintHTL.ml
@@ -45,7 +45,7 @@ let print_instruction pp (pc, i) =
   fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i)
 
 let pprint_datapath_stmnt i = function
-  | HTLVstmnt s -> pprint_stmnt i s
+  | HTLDataVstmnt s -> pprint_stmnt i s
   | HTLfork (name, args) -> concat [
       "fork "; extern_atom name; "("; concat (intersperse ", " (List.map register args)); ");\n"
     ]
@@ -56,6 +56,17 @@ let pprint_datapath_stmnt i = function
 let print_datapath_instruction pp (pc, i) =
   fprintf pp "%5d:\t%s" pc (pprint_datapath_stmnt 0 i)
 
+let pprint_control_stmnt i = function
+  | HTLCtrlVstmnt s -> pprint_stmnt i s
+  | HTLwait (name, statereg, expr) -> concat [
+      "wait("; extern_atom name; ", ";
+      register statereg; ", ";
+      pprint_expr expr; ");\n"
+    ]
+
+let print_control_instruction pp (pc, i) =
+  fprintf pp "%5d:\t%s" pc (pprint_control_stmnt 0 i)
+
 let ptree_to_list ptree =
   List.sort
     (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
@@ -70,7 +81,7 @@ let print_module pp id f =
   fprintf pp "datapath {\n";
   List.iter (print_datapath_instruction pp) datapath;
   fprintf pp "  }\n\n  controllogic {\n";
-  List.iter (print_instruction pp) controllogic;
+  List.iter (print_control_instruction pp) controllogic;
   fprintf pp "  }\n}\n\n"
 
 let print_globdef pp (id, gd) =
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index 6a15ee9..dbb8ba0 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -18,6 +18,8 @@
 
 val pprint_stmnt : int -> Verilog.stmnt -> string
 
+val pprint_expr : Verilog.expr -> string
+
 val print_value : out_channel -> ValueInt.value -> unit
 
 val print_program : bool -> out_channel -> Verilog.program -> unit