diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-11-18 22:10:55 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-18 22:10:55 +0000 |
commit | 82d69d247c7de8387b92936086abdc3d441c8628 (patch) | |
tree | 227f7db7e785f1c3affa2028bc2484e0771d54f4 /src/pipelining/SPBasic.mli | |
parent | fea7ee4d30aa7597ff5b8e2a2954ed452a1a7a57 (diff) | |
download | vericert-82d69d247c7de8387b92936086abdc3d441c8628.tar.gz vericert-82d69d247c7de8387b92936086abdc3d441c8628.zip |
Rename pipelining
Diffstat (limited to 'src/pipelining/SPBasic.mli')
-rw-r--r-- | src/pipelining/SPBasic.mli | 57 |
1 files changed, 57 insertions, 0 deletions
diff --git a/src/pipelining/SPBasic.mli b/src/pipelining/SPBasic.mli new file mode 100644 index 0000000..f16e524 --- /dev/null +++ b/src/pipelining/SPBasic.mli @@ -0,0 +1,57 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Graph.Pack.Digraph + +(* DATA DEPENDENCY GRAPHS *) +module G : Graph.Sig.P + +(* We abstract the register type to make sure that the user won't mess up *) +type reg + +(* The scheduling should return a value of type pipeline *) +type pipeline = { + steady_state : G.V.t list; + prolog : G.V.t list; + epilog : G.V.t list; + min : int; + unrolling : int; + ramp_up : (reg * reg) list; + ramp_down : (reg * reg) list +} + +(* Operations on ddg *) + +val display : G.t -> string -> unit +val apply_pipeliner : RTL.coq_function -> (G.t -> pipeline option) -> ?debug:bool -> RTL.coq_function +val get_succs_raw : G.t -> G.V.t -> G.V.t list + +(* Operations on instructions, the nodes of the data dependency graph *) + +val string_of_node : G.V.t -> string +val latency : G.V.t -> int +val reforge_reads : G.V.t -> reg -> reg -> G.V.t +val reforge_writes : G.V.t -> reg -> G.V.t +val written : G.V.t -> reg option +val is_cond : G.V.t -> bool + +(* Operations on dependencies, the edges of the data dependency graph *) + +type et = IntraRAW | IntraWAW | IntraWAR | InterRAW | InterWAW | InterWAR + +val edge_type : G.E.t -> et +val distance : G.E.t -> int + +(* Getting fresh registers, int is the number of required registers *) + +val fresh_regs : int -> reg array +val print_reg : reg -> unit |