aboutsummaryrefslogtreecommitdiffstats
path: root/src/SoftwarePipelining/SPIMS.mli
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-11-18 22:10:55 +0000
committerYann Herklotz <git@yannherklotz.com>2021-11-18 22:10:55 +0000
commit82d69d247c7de8387b92936086abdc3d441c8628 (patch)
tree227f7db7e785f1c3affa2028bc2484e0771d54f4 /src/SoftwarePipelining/SPIMS.mli
parentfea7ee4d30aa7597ff5b8e2a2954ed452a1a7a57 (diff)
downloadvericert-82d69d247c7de8387b92936086abdc3d441c8628.tar.gz
vericert-82d69d247c7de8387b92936086abdc3d441c8628.zip
Rename pipelining
Diffstat (limited to 'src/SoftwarePipelining/SPIMS.mli')
-rw-r--r--src/SoftwarePipelining/SPIMS.mli22
1 files changed, 0 insertions, 22 deletions
diff --git a/src/SoftwarePipelining/SPIMS.mli b/src/SoftwarePipelining/SPIMS.mli
deleted file mode 100644
index 7c1d9a7..0000000
--- a/src/SoftwarePipelining/SPIMS.mli
+++ /dev/null
@@ -1,22 +0,0 @@
-(***********************************************************************)
-(* *)
-(* Compcert Extensions *)
-(* *)
-(* Jean-Baptiste Tristan *)
-(* *)
-(* All rights reserved. This file is distributed under the terms *)
-(* described in file ../../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-
-open Graph.Pack.Digraph
-open SPBasic
-
-module NI : Map.S with type key = SPBasic.G.V.t
-
-(* piepeliner takes a data dependency graph and returns a schedule with an initiation interval
- fails if cannot find any schedule *)
-val pipeliner : G.t -> (G.t -> int option NI.t -> G.V.t) -> int NI.t * int
-
-val print_schedule : int NI.t -> unit