[WIP] Remove extra statements from HTL.

2 files changed, 18 insertions, 73 deletions

diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 3191733..5a55a55 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -44,16 +44,9 @@ Definition reg := positive.
 Definition node := positive.
 Definition ident := positive.
 
-Inductive datapath_stmnt :=
-| HTLfork : ident -> list reg -> datapath_stmnt
-| HTLjoin : ident -> reg -> datapath_stmnt
-| HTLDataVstmnt : Verilog.stmnt -> datapath_stmnt.
-
-Inductive control_stmnt :=
-| HTLwait : ident -> reg -> Verilog.expr -> control_stmnt
-| HTLCtrlVstmnt : Verilog.stmnt -> control_stmnt.
-
+Definition datapath_stmnt := Verilog.stmnt.
 Definition datapath := PTree.t datapath_stmnt.
+Definition control_stmnt := Verilog.stmnt.
 Definition controllogic := PTree.t control_stmnt.
 
 Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
@@ -143,8 +136,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       asr!(mod_reset m) = Some (ZToValue 0) ->
       asr!(mod_finish m) = Some (ZToValue 0) ->
       asr!(m.(mod_st)) = Some (posToValue st) ->
-      m.(mod_controllogic)!st = Some (HTLCtrlVstmnt ctrl_stmnt) ->
-      m.(mod_datapath)!st = Some (HTLDataVstmnt data_stmnt) ->
+      m.(mod_controllogic)!st = Some ctrl_stmnt ->
+      m.(mod_datapath)!st = Some data_stmnt ->
       Verilog.stmnt_runp f
         (Verilog.mkassociations asr empty_assocmap)
         (Verilog.mkassociations asa (empty_stack m))
@@ -163,51 +156,6 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       asr'!(m.(mod_st)) = Some (posToValue pstval) ->
       Z.pos pstval <= Integers.Int.max_unsigned ->
       step g (State sf m st calls asr asa) Events.E0 (State sf m pstval calls asr' asa')
-(** [HTLfork] simply adds the called instruction to the list of active calls*)
-| step_fork :
-    forall g m st sf ctrl_stmnt
-      asr asa
-      basr basa nasr nasa
-      call_ident arg_regs arg_vals
-      calls calls' asr' asa'
-      f pstval,
-      asr!(mod_reset m) = Some (ZToValue 0) ->
-      asr!(mod_finish m) = Some (ZToValue 0) ->
-      asr!(m.(mod_st)) = Some (posToValue st) ->
-      m.(mod_controllogic)!st = Some (HTLCtrlVstmnt ctrl_stmnt) ->
-      m.(mod_datapath)!st = Some (HTLfork call_ident arg_regs) ->
-      Verilog.stmnt_runp f
-        (Verilog.mkassociations asr empty_assocmap)
-        (Verilog.mkassociations asa (empty_stack m))
-        ctrl_stmnt
-        (Verilog.mkassociations basr nasr)
-        (Verilog.mkassociations basa nasa) ->
-      basr!(m.(mod_st)) = Some (posToValue st) ->
-      asr' = Verilog.merge_regs nasr basr ->
-      asa' = Verilog.merge_arrs nasa basa ->
-      arg_vals = List.map (fun r => basr#r) arg_regs ->
-      calls' = (ActiveCall call_ident arg_vals :: calls) ->
-      asr'!(m.(mod_st)) = Some (posToValue pstval) ->
-      Z.pos pstval <= Integers.Int.max_unsigned ->
-      step g (State sf m st calls asr asa) Events.E0 (State sf m pstval calls' asr' asa')
-(** [HTLjoin] acts like a call, using the arguments stored from a previous fork *)
-| step_join :
-    forall g m st sf asr asa
-      calls call_ident call_mod arg_vals dst
-      pstval,
-      asr!(mod_reset m) = Some (ZToValue 0) ->
-      asr!(mod_finish m) = Some (ZToValue 0) ->
-      asr!(mod_st m) = Some (posToValue st) ->
-
-      m.(mod_controllogic)!st = Some (HTLwait call_ident (mod_st m) (Verilog.posToExpr pstval)) ->
-      m.(mod_datapath)!st = Some (HTLjoin call_ident dst) ->
-
-      In (ActiveCall call_ident arg_vals) calls ->
-      find_module call_ident g = Some (AST.Internal call_mod) ->
-
-      Z.pos pstval <= Integers.Int.max_unsigned ->
-      step g (State sf m st calls asr asa) Events.E0
-             (Callstate (Stackframe dst m pstval calls asr asa :: sf) call_mod arg_vals)
 | step_finish :
     forall g m st calls asr asa retval sf,
     asr!(m.(mod_finish)) = Some (ZToValue 1) ->
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index 7d891c3..b417cd6 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -99,14 +99,11 @@ Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
 Import HTLMonadExtra.
 Export MonadNotation.
 
-Definition data_vstmnt : Verilog.stmnt -> HTL.datapath_stmnt := HTLDataVstmnt.
-Definition ctrl_vstmnt : Verilog.stmnt -> HTL.control_stmnt := HTLCtrlVstmnt.
-
 Definition state_goto (st : reg) (n : node) : control_stmnt :=
-  ctrl_vstmnt (Vnonblock (Vvar st) (Vlit (posToValue n))).
+  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))).
+  Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).
 
 Definition nonblock (dst : reg) (e : expr) := (Vnonblock (Vvar dst) e).
 Definition block (dst : reg) (e : expr) := (Vblock (Vvar dst) e).
@@ -218,7 +215,7 @@ Lemma add_instr_skip_state_incr :
        s.(st_scldecls)
        s.(st_arrdecls)
        (AssocMap.set n st s.(st_datapath))
-       (AssocMap.set n (ctrl_vstmnt Vskip) s.(st_controllogic))).
+       (AssocMap.set n Vskip s.(st_controllogic))).
 Proof.
   constructor; intros;
     try (simpl; destruct (peq n n0); subst);
@@ -271,7 +268,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 (ctrl_vstmnt Vskip) s.(st_controllogic)))
+               (AssocMap.set n Vskip s.(st_controllogic)))
          (add_instr_skip_state_incr s n st STM TRANS)
     | _, _ => Error (Errors.msg "HTL.add_instr")
     end.
@@ -287,7 +284,7 @@ Lemma add_node_skip_state_incr :
        (st_freshstate s)
        s.(st_scldecls)
        s.(st_arrdecls)
-       (AssocMap.set n (data_vstmnt Vskip) s.(st_datapath))
+       (AssocMap.set n Vskip s.(st_datapath))
        (AssocMap.set n st s.(st_controllogic))).
 Proof.
   constructor; intros;
@@ -305,7 +302,7 @@ Definition add_node_skip (n : node) (st : control_stmnt) : mon unit :=
                (st_freshstate s)
                s.(st_scldecls)
                s.(st_arrdecls)
-               (AssocMap.set n (data_vstmnt Vskip) s.(st_datapath))
+               (AssocMap.set n 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")
@@ -462,7 +459,7 @@ Lemma add_branch_instr_state_incr:
                 (st_freshstate s)
                 s.(st_scldecls)
                 s.(st_arrdecls)
-                (AssocMap.set n (data_vstmnt Vskip) (st_datapath s))
+                (AssocMap.set n 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;
@@ -480,7 +477,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 (data_vstmnt Vskip) (st_datapath s))
+                (AssocMap.set n 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")
@@ -526,24 +523,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' (data_vstmnt Vskip)
+        add_instr n n' 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' (data_vstmnt (nonblock dst instr))
+        add_instr n n' (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' (data_vstmnt (nonblock dst src))
+        add_instr n n' (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' (data_vstmnt (Vnonblock dst (Vvar src))) (* TODO: Could juse use add_instr? reg exists. *)
+        add_instr n n' (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' =>
@@ -570,8 +567,8 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
                     | Some r' => Vvar r'
                     | None => Vlit (ZToValue 0%Z)
                     end in
-      do _ <- add_instr n idle_state (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn retval)));
-      add_instr_skip idle_state (data_vstmnt (nonblock fin (Vlit (ZToValue 0%Z))))
+      do _ <- add_instr n idle_state (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn retval));
+      add_instr_skip idle_state (nonblock fin (Vlit (ZToValue 0%Z)))
     end
   end.