Guard join state with called module finish

Needed to match RTL semantics, since the join state executes once before
the call is initiated, and we need the destination register to not be
affected until after the call has returned.

3 files changed, 14 insertions, 6 deletions

diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index 39146ff..908c627 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -490,8 +490,9 @@ Definition fork (rst : reg) (params : list (reg * reg)) : datapath_stmnt :=
   let assign_params := nonblock_all params in
   Vseq reset_mod assign_params.
 
-Definition join (fn_rtrn fn_rst fn_dst : reg) : datapath_stmnt :=
-  let set_result := Vnonblock (Vvar fn_dst) (Vvar fn_rtrn) in
+Definition join (fn_fin fn_rst fn_rtrn fn_dst : reg) : datapath_stmnt :=
+  let set_result := Vcond (boplitz Veq fn_fin 1)
+                          (Vnonblock (Vvar fn_dst) (Vvar fn_rtrn)) Vskip in
   let stop_reset := Vnonblock (Vvar fn_rst) (Vlit (ZToValue 0)) in
   Vseq stop_reset set_result.
 
@@ -558,7 +559,7 @@ Definition transf_instr (ge : RTL.genv) (fin rtrn stack: reg) (ni: node * instru
              do return_reg <- map_externctrl fn ctrl_return;
 
              let fork_instr := fork reset_reg params in
-             let join_instr := join return_reg reset_reg dst in
+             let join_instr := join finish_reg reset_reg return_reg dst in
 
              do _ <- add_instr n join_state fork_instr;
              add_instr_wait finish_reg join_state n' join_instr
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 5b1dc1b..ae9967f 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -139,7 +139,7 @@ Inductive match_frames (ge : RTL.genv) (current_id : HTL.ident) (mem : Memory.me
       (CONST : match_constants m asr)
       (EXTERN_CALLER : has_externctrl m current_id ret rst fin)
       (JOIN_CTRL : (HTL.mod_controllogic m)!st = Some (state_wait (HTL.mod_st m) fin pc))
-      (JOIN_DATA : (HTL.mod_datapath m)!st = Some (join ret rst dst))
+      (JOIN_DATA : (HTL.mod_datapath m)!st = Some (join fin rst ret dst))
       (TAILS : match_frames ge mid mem rtl_tl htl_tl)
       (DST : Ple dst (RTL.max_reg_function f))
       (PC : (Z.pos pc <= Int.max_unsigned)),
@@ -1566,7 +1566,13 @@ Section CORRECTNESS.
           rewrite assign_all_out by admit.
           rewrite AssocMap.gso by not_control_reg.
           apply AssocMap.gss.
-        * repeat econstructor.
+        * unfold join.
+          econstructor.
+          -- repeat econstructor.
+          -- eapply Verilog.stmnt_runp_Vcond_false.
+             ++ repeat econstructor.
+             ++ big_tac. admit. (* TODO: Externctrl finish is false *)
+             ++ repeat econstructor.
         * constructor.
         * simpl.
           apply AssocMapExt.merge_correct_2.
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index b46fd3b..dbdc8bf 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -102,7 +102,7 @@ Inductive tr_code (ge : RTL.genv) (c : RTL.code) (pc : RTL.node) (stmnts : datap
           Z.pos pc2 <= Int.max_unsigned /\
           stmnts!pc = Some (fork fn_rst (List.combine fn_params args)) /\
           trans!pc = Some (state_goto st pc2) /\
-          stmnts!pc2 = Some (join fn_return fn_rst dst) /\
+          stmnts!pc2 = Some (join fn_finish fn_rst fn_return dst) /\
           trans!pc2 = Some (state_wait st fn_finish n)) ->
 
       tr_code ge c pc stmnts trans externctrl fin rtrn st stk (RTL.Icall sig (inr fn) args dst n)
@@ -410,6 +410,7 @@ Proof.
       * monad_crush.
       * replace x6 with (st_freshreg s7) in * by intro_step.
         replace x5 with (st_freshreg s6) in * by intro_step.
+        replace x4 with (st_freshreg s5) in * by intro_step.
         monad_crush.
       * replace x4 with (st_freshreg s5) in * by intro_step.
         monad_crush.