diff options
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/GiblePargen.v | 5 | ||||
-rw-r--r-- | src/hls/HTLPargen.v | 25 | ||||
-rw-r--r-- | src/hls/Partition.ml | 4 | ||||
-rw-r--r-- | src/hls/Schedule.ml | 29 |
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 |