diff options
Diffstat (limited to 'src/hls/Schedule.ml')
| -rw-r--r-- | src/hls/Schedule.ml | 104 |
1 files changed, 77 insertions, 27 deletions
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index c5443c7..70395e7 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -289,6 +289,7 @@ let comb_delay = function | _ -> 1 let pipeline_stages = function + | RBload _ -> 2 | RBop (_, op, _, _) -> (match op with | Odiv -> 32 @@ -304,7 +305,7 @@ let add_dep map i tree dfg curr = | None -> dfg | Some ip -> let ipv = (List.nth map ip) in - DFG.add_edge_e dfg (ipv, comb_delay (snd ipv), List.nth map i) + DFG.add_edge_e dfg (ipv, comb_delay (snd (List.nth map i)), List.nth map i) (** This function calculates the dependencies of each instruction. The nodes correspond to previous registers that were allocated and show which instruction caused it. @@ -327,6 +328,7 @@ let accumulate_RAW_deps map dfg curr = match curr with | RBop (op, _, rs, dst) -> acc_dep_instruction rs dst | RBload (op, _mem, _addr, rs, dst) -> acc_dep_instruction rs dst + | RBsetpred (_op, _mem, rs, _p) -> acc_dep_instruction_nodst rs | RBstore (op, _mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs) | _ -> (i + 1, dst_map, graph) @@ -407,7 +409,7 @@ let accumulate_WAW_mem_deps instrs dfg curri = | RBstore (_, _, _, _, _) -> ( match next_store 0 (take i instrs |> List.rev) with | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i)) | _ -> dfg (** Predicate dependencies. *) @@ -424,6 +426,7 @@ let get_predicate = function | RBop (p, _, _, _) -> p | RBload (p, _, _, _, _) -> p | RBstore (p, _, _, _, _) -> p + | RBsetpred (p, _, _, _) -> p | _ -> None let rec next_setpred p i = function @@ -447,6 +450,7 @@ let rec next_preduse p i instr= | RBload (Some p', _, _, _, _) :: rst -> next p' rst | RBstore (Some p', _, _, _, _) :: rst -> next p' rst | RBop (Some p', _, _, _) :: rst -> next p' rst + | RBsetpred (Some p', _, _, _) :: rst -> next p' rst | _ :: rst -> next_load (i + 1) rst let accumulate_RAW_pred_deps instrs dfg curri = @@ -571,6 +575,18 @@ let gather_bb_constraints debug bb = let encode_var bbn n i = { sv_type = VarType (bbn, n); sv_num = i } let encode_bb bbn i = { sv_type = BBType bbn; sv_num = i } +let add_initial_sv n dfg constr = + let add_initial_sv' (i, instr) g = + let pipes = pipeline_stages instr in + if pipes > 0 then + List.init pipes (fun i' -> i') + |> List.fold_left (fun g i' -> + G.add_edge_e g (encode_var n i i', -1, encode_var n i (i'+1)) + ) g + else g + in + DFG.fold_vertex add_initial_sv' dfg constr + let add_super_nodes n dfg = DFG.fold_vertex (function v1 -> fun g -> (if DFG.in_degree dfg v1 = 0 @@ -578,12 +594,14 @@ let add_super_nodes n dfg = else g) |> (fun g' -> if DFG.out_degree dfg v1 = 0 - then G.add_edge_e g' (encode_var n (fst v1) 0, 0, encode_bb n 1) + then G.add_edge_e g' (encode_var n (fst v1) (pipeline_stages (snd v1)), + 0, encode_bb n 1) else g')) dfg let add_data_deps n = - DFG.fold_edges_e (function ((i1, _), l, (i2, _)) -> fun g -> - G.add_edge_e g (encode_var n i1 0, 0, encode_var n i2 0) + DFG.fold_edges_e (function ((i1, instr1), _, (i2, _)) -> fun g -> + let end_sv = pipeline_stages instr1 in + G.add_edge_e g (encode_var n i1 end_sv, 0, encode_var n i2 0) ) let add_ctrl_deps n succs constr = @@ -607,17 +625,24 @@ let negate_graph constr = DFG.add_edge_e g (v1, -e, v2) ) constr DFG.empty -let add_cycle_constr max n dfg constr = +let add_cycle_constr maxf n dfg constr = let negated_dfg = negate_graph dfg in + let max_initial_del = DFG.fold_vertex (fun v1 g -> + if DFG.in_degree dfg v1 = 0 + then max g (comb_delay (snd v1)) + else g) dfg 0 in let longest_path v = BFDFG.all_shortest_paths negated_dfg v - |> BFDFG.H.to_seq |> List.of_seq in - let constrained_paths = List.filter (function (v, m) -> - m > max) in + |> BFDFG.H.to_seq |> List.of_seq + |> List.map (function (x, y) -> (x, y - max_initial_del)) in + let constrained_paths = List.filter (function (_, m) -> - m > maxf) in List.fold_left (fun g -> function (v, v', w) -> G.add_edge_e g (encode_var n (fst v) 0, - - (int_of_float (Float.ceil (Float.div (float_of_int w) (float_of_int max))) - 1), + - (int_of_float (Float.ceil (Float.div (float_of_int w) (float_of_int maxf))) - 1), encode_var n (fst v') 0) ) constr (DFG.fold_vertex (fun v l -> - List.append l (longest_path v |> constrained_paths + List.append l (longest_path v (*|> (function l -> List.iter (function (a, x) -> + printf "c: %d %d\n" (fst a) x) l; l)*) |> constrained_paths (* |> (function l -> List.iter (function (a, x) -> + printf "%d %d\n" (fst a) x) l; l)*) |> List.map (function (v', w) -> (v, v', - w))) ) dfg []) @@ -671,6 +696,7 @@ let gather_cfg_constraints c constr curr = | None -> assert false | Some { bb_exit = ctrl; _ } -> add_super_nodes n dfg constr + |> add_initial_sv n dfg |> add_data_deps n dfg |> add_ctrl_deps n (successors_instr ctrl |> List.map P.to_int @@ -703,25 +729,32 @@ let print_lp constr = let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ] -let parse_soln tree s = +let parse_soln (tree, bbtree) s = let r = Str.regexp "var\\([0-9]+\\)n\\([0-9]+\\)_0[ ]+\\([0-9]+\\)" in - if Str.string_match r s 0 then - IMap.update - (Str.matched_group 1 s |> int_of_string) - (update_schedule - ( Str.matched_group 2 s |> int_of_string, - Str.matched_group 3 s |> int_of_string )) - tree - else tree + let bb = Str.regexp "bb\\([0-9]+\\)_\\([0-9]+\\)[ ]+\\([0-9]+\\)" in + let upd s = IMap.update + (Str.matched_group 1 s |> int_of_string) + (update_schedule + ( Str.matched_group 2 s |> int_of_string, + Str.matched_group 3 s |> int_of_string )) + in + if Str.string_match r s 0 + then (upd s tree, bbtree) + else + (if Str.string_match bb s 0 + then (tree, upd s bbtree) + else (tree, bbtree)) let solve_constraints constr = - let oc = open_out "lpsolve.txt" in + let (fn, oc) = Filename.open_temp_file "vericert_" "_lp_solve" in fprintf oc "%s\n" (print_lp constr); close_out oc; - Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt") - |> drop 3 - |> List.fold_left parse_soln IMap.empty + let res = Str.split (Str.regexp_string "\n") (read_process ("lp_solve " ^ fn)) + |> drop 3 + |> List.fold_left parse_soln (IMap.empty, IMap.empty) + in + (*Sys.remove fn;*) res let subgraph dfg l = let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in @@ -763,20 +796,35 @@ let all_dfs dfg = if check_in el a then a else (DFGDfs.fold_component (fun v l -> v :: l) [] dfg' el) :: a) [] roots +let range s e = + List.init (e - s) (fun i -> i) + |> List.map (fun x -> x + s) + (** Should generate the [RTLPar] code based on the input [RTLBlock] description. *) -let transf_rtlpar c c' (schedule : (int * int) list IMap.t) = +let transf_rtlpar c c' schedule = let f i bb : RTLPar.bblock = match bb with | { bb_body = []; bb_exit = c } -> { bb_body = []; bb_exit = c } | { bb_body = bb_body'; bb_exit = ctrl_flow } -> let dfg = match PTree.get i c' with None -> assert false | Some x -> x in - let i_sched = IMap.find (P.to_int i) schedule in + let bb_st_e = + let m = IMap.find (P.to_int i) (snd schedule) in + (List.assq 0 m, List.assq 1 m) in + let i_sched = IMap.find (P.to_int i) (fst schedule) in let i_sched_tree = List.fold_left combine_bb_schedule IMap.empty i_sched in let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) in + let body2 = List.fold_left (fun x b -> + match IMap.find_opt b i_sched_tree with + | Some i -> i :: x + | None -> [] :: x + ) [] (range (fst bb_st_e) (snd bb_st_e + 1)) + |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) + |> List.rev + in (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*) let final_body2 = List.map (fun x -> subgraph dfg x |> (fun x -> @@ -784,7 +832,9 @@ let transf_rtlpar c c' (schedule : (int * int) list IMap.t) = |> List.map (subgraph x) |> List.map (fun y -> TopoDFG.fold (fun i l -> snd i :: l) y [] - |> List.rev))) body + |> List.rev))) body2 + (*|> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x []) + |> List.rev) body2*) in { bb_body = final_body2; bb_exit = ctrl_flow |