Fix code generation in partitioning and scheduling

4 files changed, 54 insertions, 9 deletions

diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index 37273b4..0d4badd 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -243,8 +243,9 @@ Definition empty_trees (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
   end.
 
 Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
-  check (fst (abstract_sequence (empty, nil) bb))
-        (fst (abstract_sequence (empty, nil) (concat (concat bbt)))) &&
+  forallb (fun x => match x with ((_, _, f1), (_, _, f2)) => check f1 f2 end)
+          (combine (snd (abstract_sequence (empty, nil) bb))
+                   (snd (abstract_sequence (empty, nil) (concat (concat bbt))))) &&
   empty_trees bb bbt.
 
 Definition check_scheduled_trees := beq2 schedule_oracle.
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index a058536..560250a 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -663,6 +663,23 @@ Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
       (AssocMap.set n st s.(st_controllogic)))
    (add_control_instr_force_state_incr s n st).
 
+Definition add_control_instr_try (n : node) (st : stmnt) : mon unit :=
+  fun s =>
+    match check_empty_node_controllogic s n with
+    | left CTRL =>
+      OK tt (mkstate
+           s.(st_st)
+           s.(st_freshreg)
+           (st_freshstate s)
+           s.(st_scldecls)
+           s.(st_arrdecls)
+           s.(st_datapath)
+           (AssocMap.set n st s.(st_controllogic)))
+         (add_control_instr_state_incr s n st CTRL)
+    | _ =>
+      OK tt s (st_refl s)
+    end.
+
 Fixpoint pred_expr (preg: reg) (p: pred_op) :=
   match p with
   | Plit (b, pred) =>
@@ -802,17 +819,17 @@ Definition translate_inst_list (fin rtrn preg stack: reg) (ni : node * node * li
     do _ <- collectlist
           (fun l => translate_inst Vblock fin rtrn preg stack n l) (concat li);
     do st <- get;
-    add_control_instr n (state_goto st.(st_st) p)
+    add_control_instr_try n (state_goto st.(st_st) p)
   end.
 
 Definition transf_bblock (fin rtrn preg stack: reg) (ni : node * ParBB.t)
   : mon unit :=
   let (n, bb) := ni in
   do nstate <- create_new_state ((poslength bb))%positive;
-  do _ <- collectlist (translate_inst_list fin rtrn preg stack)
+  do _ <- add_control_instr nstate Vskip;
+  collectlist (translate_inst_list fin rtrn preg stack)
                       (prange n (nstate + poslength bb - 1)%positive
-                                  bb);
-  add_control_instr nstate Vskip.
+                                  bb).
 
 (*Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}.
   refine (match bool_dec ((a <? b) && (b <? c) && (c <? d)
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
index 3b7cdd7..07b1be9 100644
--- a/src/hls/Partition.ml
+++ b/src/hls/Partition.ml
@@ -68,14 +68,14 @@ let rec next_bblock_from_RTL is_start e (c : RTL.code) s i =
   match trans_inst, succ with
   | (None, Some i'), _ ->
     if List.exists (fun x -> x = s) (snd e) && not is_start then
-      Errors.OK [RBnop; RBexit (None, (RBgoto s))]
+      Errors.OK [RBexit (None, (RBgoto s))]
     else
       Errors.OK [RBnop; RBexit (None, i')]
   | (Some i', None), (s', Some i_n)::[] ->
     if List.exists (fun x -> x = s) (fst e) then
       Errors.OK [i'; RBexit (None, (RBgoto s'))]
     else if List.exists (fun x -> x = s) (snd e) && not is_start then
-      Errors.OK [RBnop; RBexit (None, (RBgoto s))]
+      Errors.OK [RBexit (None, (RBgoto s))]
     else begin
       match next_bblock_from_RTL false e c s' i_n with
       | Errors.OK bb ->
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 9d9700a..9ba2b51 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -441,6 +441,7 @@ let get_predicate = function
   | RBload (p, _, _, _, _) -> p
   | RBstore (p, _, _, _, _) -> p
   | RBsetpred (p, _, _, _) -> p
+  | RBexit (p, _) -> p
   | _ -> None
 
 let rec next_setpred p i = function
@@ -465,6 +466,7 @@ let rec next_preduse p i instr=
   | RBstore (Some p', _, _, _, _) :: rst -> next p' rst
   | RBop (Some p', _, _, _) :: rst -> next p' rst
   | RBsetpred (Some p', _, _, _) :: rst -> next p' rst
+  | RBexit (Some p', _) :: rst -> next p' rst
   | _ :: rst -> next_load (i + 1) rst
 
 let accumulate_RAW_pred_deps instrs dfg curri =
@@ -513,6 +515,28 @@ let accumulate_WAW_deps instrs dfg curri =
       | Some i' -> DFG.add_edge dfg (gen_vertex instrs i) (gen_vertex instrs i') )
   | _ -> dfg
 
+let accumulate_pre_exit_deps instrs dfg curri =
+  let i, curr = curri in
+  match curr with
+  | RBexit (_, _) ->
+    List.fold_left (fun ndfg -> function (i', instr') ->
+        if i' < i
+        then DFG.add_edge ndfg (gen_vertex instrs i') (gen_vertex instrs i)
+        else ndfg
+      ) dfg (List.mapi (fun i x -> (i, x)) instrs)
+  | _ -> dfg
+
+let accumulate_post_exit_deps instrs dfg curri =
+  let i, curr = curri in
+  match curr with
+  | RBexit (_, _) ->
+    List.fold_left (fun ndfg -> function (i', instr') ->
+        if i' > i
+        then DFG.add_edge ndfg (gen_vertex instrs i) (gen_vertex instrs i')
+        else ndfg
+      ) dfg (List.mapi (fun i x -> (i, x)) instrs)
+  | _ -> dfg
+
 let accumulate_WAR_deps instrs dfg curri =
   let i, curr = curri in
   let dst_dep dst =
@@ -533,6 +557,7 @@ let assigned_vars vars = function
   | RBload (_, _, _, _, dst) -> dst :: vars
   | RBstore (_, _, _, _, _) -> vars
   | RBsetpred (_, _, _, _) -> vars
+  | RBexit (_, _) -> vars
 
 let get_pred = function
   | RBnop -> None
@@ -581,7 +606,9 @@ let gather_bb_constraints debug bb =
         accumulate_WAW_mem_deps;
         accumulate_RAW_pred_deps;
         accumulate_WAR_pred_deps;
-        accumulate_WAW_pred_deps
+        accumulate_WAW_pred_deps;
+        accumulate_pre_exit_deps;
+        accumulate_post_exit_deps
       ]
   in
   let dfg''' = remove_unnecessary_deps dfg'' in