diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-12-17 10:02:23 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-12-17 10:02:23 +0000 |
commit | 51e3a17d2e65b095861c243807f4e8d76c60ea0e (patch) | |
tree | e4870fc714b872835d3e04d10954cb4f74d42cac /src/SoftwarePipelining/SoftwarePipelining.ml | |
parent | 4f67aaa8ba8b2b51716896d9be896af385652bc9 (diff) | |
download | vericert-51e3a17d2e65b095861c243807f4e8d76c60ea0e.tar.gz vericert-51e3a17d2e65b095861c243807f4e8d76c60ea0e.zip |
Add Software pipelining stage by tristan et al.
Diffstat (limited to 'src/SoftwarePipelining/SoftwarePipelining.ml')
-rw-r--r-- | src/SoftwarePipelining/SoftwarePipelining.ml | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/src/SoftwarePipelining/SoftwarePipelining.ml b/src/SoftwarePipelining/SoftwarePipelining.ml new file mode 100644 index 0000000..eeb2dfd --- /dev/null +++ b/src/SoftwarePipelining/SoftwarePipelining.ml @@ -0,0 +1,73 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Basic +open IMS +open MVE +open RTL + +let clean t = + + let rec clean_rec i = + match i with + | 0 -> [] + | n -> + begin + match t.(i - 1) with + | None -> clean_rec (i - 1) + | Some inst -> inst :: clean_rec (i - 1) + end + in + let l = List.rev (clean_rec (Array.length t)) in + List.hd l :: (List.filter (fun e -> not (is_cond e)) (List.tl l)) + +let print_nodes = List.iter (fun n -> Printf.printf "%s \n" (string_of_node n)) + +(* random heuristic *) + +let find node schedule opt = + try NI.find node schedule with + | Not_found -> opt + +let random ddg schedule = + let unscheduled = G.fold_vertex (fun node l -> + match find node schedule None with + | Some v -> l + | None -> node :: l + ) ddg [] in + let bound = List.length unscheduled in + Random.self_init (); + List.nth unscheduled (Random.int bound) + +(* tought heuristics *) + +module Topo = Graph.Topological.Make (G) +module Scc = Graph.Components.Make (G) + +let order = ref [] + +let pipeliner ddg = + order := List.flatten (Scc.scc_list ddg); + let (sched,ii) = IMS.pipeliner ddg random in + let (steady,prolog,epilog,min,unroll,entrance,way_out) = MVE.mve ddg sched ii in + let steady_state = clean steady in + if min <= 0 then None + else + Some {steady_state = steady_state; prolog = prolog; epilog = epilog; min = min; unrolling = unroll; + ramp_up = entrance; ramp_down = way_out} + + +let main f = + Basic.apply_pipeliner f pipeliner ~debug:false + + + |