Merge branch 'develop' into dev/divider

16 files changed, 1187 insertions, 276 deletions

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index cacf7fa..a4a954c 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -36,11 +36,3 @@ jobs:
 
     - name: Build
       run: nix-shell --run "make -j8"
-
-    - name: Generate Documentation
-      run: nix-shell --run "make -j8 doc"
-
-    - uses: actions/upload-artifact@v2
-      with:
-        name: html-documentation
-        path: html/
diff --git a/Makefile b/Makefile
index e50a543..763c892 100644
--- a/Makefile
+++ b/Makefile
@@ -21,7 +21,7 @@ COQMAKE := $(COQBIN)coq_makefile
 
 COQDOCFLAGS := --no-lib-name -l
 
-VS := src/Compiler.v src/Simulator.v $(foreach d, common hls, src/$(d)/*.v)
+VS := src/Compiler.v src/Simulator.v src/HLSOpts.v $(foreach d, common hls, src/$(d)/*.v)
 
 PREFIX ?= .
 
diff --git a/default.nix b/default.nix
index b004643..8308389 100644
--- a/default.nix
+++ b/default.nix
@@ -1,5 +1,4 @@
-with import <nixpkgs> {};
-
+with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/269fc4ddb896c1c5994eb4bb8c750ec18cb3db82.tar.gz") {};
 let
   ncoq = coq_8_12;
   ncoqPackages = coqPackages_8_12;
@@ -28,7 +27,7 @@ stdenv.mkDerivation {
   name = "vericert";
   src = ./.;
 
-  buildInputs = [ ncoq dune gcc
+  buildInputs = [ ncoq dune_2 gcc
                   ocaml ocamlPackages.findlib ocamlPackages.menhir
                   ocamlPackages.ocamlgraph
                 ];
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 6887b56..d2c301f 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -249,7 +249,8 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)
   -fcommon       Put uninitialized globals in the common section [on].
 
 HLS Optimisations:
-  -fschedule     Schedule the resulting hardware [off].
+  -fschedule      Schedule the resulting hardware [off].
+  -fif-conversion If-conversion optimisation [off].
 |} ^
  target_help ^
  toolchain_help ^
@@ -434,6 +435,7 @@ let cmdline_actions =
   @ f_opt "fpu" option_ffpu
   @ f_opt "sse" option_ffpu (* backward compatibility *)
   @ f_opt "schedule" option_hls_schedule
+  @ f_opt "if-conv" option_fif_conv
   @ [
 (* Catch options that are not handled *)
   Prefix "-", Self (fun s ->
diff --git a/src/Compiler.v b/src/Compiler.v
index 27cb80c..d99ce56 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -68,6 +68,7 @@ Require vericert.hls.RTLPargen.
 Require vericert.hls.HTLPargen.
 Require vericert.hls.Pipeline.
 Require vericert.hls.IfConversion.
+Require vericert.HLSOpts.
 
 Require Import vericert.hls.HTLgenproof.
 
@@ -235,7 +236,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_RTL 7)
   @@@ RTLBlockgen.transl_program
    @@ print (print_RTLBlock 1)
-   @@ IfConversion.transf_program
+   @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program
    @@ print (print_RTLBlock 2)
   @@@ RTLPargen.transl_program
   @@@ HTLPargen.transl_program
diff --git a/src/HLSOpts.v b/src/HLSOpts.v
new file mode 100644
index 0000000..173300d
--- /dev/null
+++ b/src/HLSOpts.v
@@ -0,0 +1,19 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2019-2020 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
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Parameter optim_if_conversion: unit -> bool.
diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml
index 26b4053..534962b 100644
--- a/src/VericertClflags.ml
+++ b/src/VericertClflags.ml
@@ -6,3 +6,4 @@ let option_initial = ref false
 let option_dhtl = ref false
 let option_drtlblock = ref false
 let option_hls_schedule = ref false
+let option_fif_conv = ref false
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index f2754be..b58ebd4 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -29,7 +29,6 @@ Require Import Coq.micromega.Lia.
 Require Export compcert.lib.Coqlib.
 Require Import compcert.lib.Integers.
 
-Require Export vericert.common.VericertTactics.
 Require Import vericert.common.Show.
 
 (* Depend on CompCert for the basic library, as they declare and prove some
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index a4d0bde..8aec96e 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -24,7 +24,8 @@ From vericert Require
      RTLPar
      RTLBlockInstr
      HTLgen
-     Pipeline.
+     Pipeline
+     HLSOpts.
 
 From Coq Require DecidableClass.
 
@@ -131,6 +132,9 @@ Extract Constant Compopts.thumb =>
 Extract Constant Compopts.debug =>
   "fun _ -> !Clflags.option_g".
 
+Extract Constant HLSOpts.optim_if_conversion =>
+  "fun _ -> !VericertClflags.option_fif_conv".
+
 (* Compiler *)
 Extract Constant Compiler.print_Clight => "PrintClight.print_if".
 Extract Constant Compiler.print_Cminor => "PrintCminor.print_if".
diff --git a/src/hls/FunctionalUnits.v b/src/hls/FunctionalUnits.v
new file mode 100644
index 0000000..019cf15
--- /dev/null
+++ b/src/hls/FunctionalUnits.v
@@ -0,0 +1,41 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2021 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
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Require Import compcert.backend.Registers.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Vericertlib.
+
+Inductive funct_unit: Type :=
+| SignedDiv (size: positive) (numer denom quot rem: reg): funct_unit
+| UnsignedDiv (size: positive) (numer denom quot rem: reg): funct_unit.
+
+Record funct_units := mk_avail_funct_units {
+    avail_sdiv: option positive;
+    avail_udiv: option positive;
+    avail_units: PTree.t funct_unit;
+  }.
+
+Definition initial_funct_units :=
+  mk_avail_funct_units None None (PTree.empty funct_unit).
+
+Definition funct_unit_stages (f: funct_unit) : positive :=
+  match f with
+  | SignedDiv s _ _ _ _ => s
+  | UnsignedDiv s _ _ _ _ => s
+  end.
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 88fb9b4..01588f6 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -40,6 +40,8 @@ Hint Resolve AssocMap.gss : htlh.
 Hint Resolve Ple_refl : htlh.
 Hint Resolve Ple_succ : htlh.
 
+Definition assignment : Type := expr -> expr -> stmnt.
+
 Record state: Type := mkstate {
   st_st: reg;
   st_freshreg: reg;
@@ -673,35 +675,33 @@ Fixpoint pred_expr (preg: reg) (p: pred_op) :=
     Vbinop Vor (pred_expr preg p1) (pred_expr preg p2)
   end.
 
-Definition translate_predicate (preg: reg) (p: option pred_op) (dst e: expr) :=
+Definition translate_predicate (a : assignment)
+           (preg: reg) (p: option pred_op) (dst e: expr) :=
   match p with
-  | None => ret (Vnonblock dst e)
+  | None => ret (a dst e)
   | Some pos =>
-    ret (Vnonblock dst (Vternary (pred_expr preg pos) e dst))
+    ret (a dst (Vternary (pred_expr preg pos) e dst))
   end.
 
-Definition translate_inst (fin rtrn stack preg : reg) (n : node) (i : instr)
-  : mon unit :=
+Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr)
+  : mon stmnt :=
   match i with
   | RBnop =>
-    add_data_instr n Vskip
+    ret Vskip
   | RBop p op args dst =>
     do instr <- translate_instr op args;
     do _ <- declare_reg None dst 32;
-    do pred <- translate_predicate preg p (Vvar dst) instr;
-    add_data_instr n pred
+    translate_predicate a preg p (Vvar dst) instr
   | RBload p chunk addr args dst =>
     do src <- translate_arr_access chunk addr args stack;
     do _ <- declare_reg None dst 32;
-    do pred <- translate_predicate preg p (Vvar dst) src;
-    add_data_instr n pred
+    translate_predicate a preg p (Vvar dst) src
   | RBstore p chunk addr args src =>
     do dst <- translate_arr_access chunk addr args stack;
-    do pred <- translate_predicate preg p dst (Vvar src);
-    add_data_instr n pred
+    translate_predicate a preg p dst (Vvar src)
   | RBsetpred c args p =>
     do cond <- translate_condition c args;
-    add_data_instr n (Vnonblock (pred_expr preg (Pvar p)) cond)
+    ret (a (pred_expr preg (Pvar p)) cond)
   end.
 
 Lemma create_new_state_state_incr:
@@ -731,10 +731,13 @@ Definition create_new_state (p: node): mon node :=
                 s.(st_funct_units))
               (create_new_state_state_incr s p).
 
-Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list instr) :=
+Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list (list instr)) :=
   match ni with
   | (n, p, li) =>
-    do _ <- collectlist (translate_inst fin rtrn stack preg n) li;
+    do _ <- collectlist
+          (fun l =>
+             do stmnt <- translate_inst Vblock fin rtrn stack preg n l;
+             add_data_instr n stmnt) (concat li);
     do st <- get;
     add_control_instr n (state_goto st.(st_st) p)
   end.
diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml
index e9020ac..8c9f20e 100644
--- a/src/hls/PrintVerilog.ml
+++ b/src/hls/PrintVerilog.ml
@@ -192,6 +192,7 @@ let testbench = "module testbench;
    reg start, reset, clk;
    wire finish;
    wire [31:0] return_val;
+   reg [31:0] cycles;
 
    main m(start, reset, clk, finish, return_val);
 
@@ -201,20 +202,23 @@ let testbench = "module testbench;
       reset = 0;
       @(posedge clk) reset = 1;
       @(posedge clk) reset = 0;
+      cycles = 0;
    end
 
    always #5 clk = ~clk;
 
    always @(posedge clk) begin
       if (finish == 1) begin
+         $display(\"cycles: %0d\", cycles);
          $display(\"finished: %0d\", return_val);
          $finish;
       end
+      cycles <= cycles + 1;
    end
 endmodule
 "
 
-let debug_always i clk state = concat [
+let debug_always_verbose i clk state = concat [
     indent i; "reg [31:0] count;\n";
     indent i; "initial count = 0;\n";
     indent i; "always @(posedge " ^ register clk ^ ") begin\n";
@@ -226,6 +230,15 @@ let debug_always i clk state = concat [
     indent i; "end\n"
   ]
 
+let debug_always i clk finish = concat [
+    indent i; "reg [31:0] count;\n";
+    indent i; "initial count = 0;\n";
+    indent i; "always @(posedge " ^ register clk ^ ") begin\n";
+    indent (i+2); "if(" ^ register finish ^ ") $display(\"Cycles: %0d\", count);\n";
+    indent (i+1); "count <= count + 1;\n";
+    indent i; "end\n"
+  ]
+
 let print_initial i n stk = concat [
     indent i; "integer i;\n";
     indent i; "initial for(i = 0; i < "; sprintf "%d" n; "; i++)\n";
@@ -246,7 +259,7 @@ let pprint_module debug i n m =
              fold_map (pprint_module_item (i+1)) m.mod_body;
              concat (List.map (print_funct_units m.mod_clk) m.mod_funct_units);
              if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else "";
-             if debug then debug_always i m.mod_clk m.mod_st else "";
+             if debug then debug_always_verbose i m.mod_clk m.mod_st else "";
              indent i; "endmodule\n\n"
            ]
   else ""
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index be9ff22..2e78d36 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -30,7 +30,7 @@ Require Import compcert.verilog.Op.
 
 Require Import vericert.hls.RTLBlockInstr.
 
-Definition bb := list (list instr).
+Definition bb := list (list (list instr)).
 
 Definition bblock := @bblock bb.
 Definition code := @code bb.
@@ -56,11 +56,22 @@ Section RELSEM.
         forall state sp,
         step_instr_list sp state nil state.
 
+  Inductive step_instr_seq (sp : val)
+    : instr_state -> list (list instr) -> instr_state -> Prop :=
+  | exec_instr_seq_cons:
+    forall state i state' state'' instrs,
+      step_instr_list sp state i state' ->
+      step_instr_seq sp state' instrs state'' ->
+      step_instr_seq sp state (i :: instrs) state''
+  | exec_instr_seq_nil:
+    forall state,
+      step_instr_seq sp state nil state.
+
   Inductive step_instr_block (sp : val)
     : instr_state -> bb -> instr_state -> Prop :=
   | exec_instr_block_cons:
     forall state i state' state'' instrs,
-      step_instr_list sp state i state' ->
+      step_instr_seq sp state i state' ->
       step_instr_block sp state' instrs state'' ->
       step_instr_block sp state (i :: instrs) state''
   | exec_instr_block_nil:
@@ -113,7 +124,7 @@ Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
 Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) :=
-  let max_body := fold_left (fun x l => fold_left max_reg_instr l x) bb.(bb_body) m in
+  let max_body := fold_left (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) bb.(bb_body) m in
   max_reg_cfi max_body bb.(bb_exit).
 
 Definition max_reg_function (f: function) :=
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 39c57df..e2e9a90 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -591,12 +591,6 @@ Fixpoint abstract_sequence (f : forest) (b : list instr) : forest :=
   | i :: l => update (abstract_sequence f l) i
   end.
 
-Fixpoint abstract_sequence_par (f : forest) (b : list (list instr)) : forest :=
-  match b with
-  | nil => f
-  | i :: l => abstract_sequence (abstract_sequence_par f l) i
-  end.
-
 (*|
 Check equivalence of control flow instructions.  As none of the basic blocks should have been moved,
 none of the labels should be different, meaning the control-flow instructions should match exactly.
@@ -622,7 +616,7 @@ Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool :=
 
 Definition schedule_oracle (bb: RTLBlock.bblock) (bbt: RTLPar.bblock) : bool :=
   check (abstract_sequence empty (bb_body bb))
-        (abstract_sequence_par empty (bb_body bbt)) &&
+        (abstract_sequence empty (concat (concat (bb_body bbt)))) &&
   check_control_flow_instr (bb_exit bb) (bb_exit bbt) &&
   empty_trees (bb_body bb) (bb_body bbt).
 
diff --git a/src/hls/Sat.v b/src/hls/Sat.v
new file mode 100644
index 0000000..9549947
--- /dev/null
+++ b/src/hls/Sat.v
@@ -0,0 +1,580 @@
+(** Homework Assignment 6#<br>#
+#<a href="http://www.cs.berkeley.edu/~adamc/itp/">#Interactive Computer Theorem
+Proving#</a><br>#
+CS294-9, Fall 2006#<br>#
+UC Berkeley *)
+
+(** Submit your solution file for this assignment as an attachment
+  #<a href="mailto:adamc@cs.berkeley.edu?subject=ICTP HW6">#by e-mail#</a># with
+  the subject "ICTP HW6" by the start of class on October 12.
+  You should write your solutions entirely on your own, which includes not
+  consulting any solutions to these problems that may be posted on the web.
+
+  #<a href="HW6.v">#Template source file#</a>#
+  *)
+
+Require Import Arith Bool List.
+
+(** This assignment involves building a certified boolean satisfiability solver
+  based on the DPLL algorithm.  Your certified procedure will take as input a
+  boolean formula in conjunctive normal form (CNF) and either return a
+  satisfying assignment to the variables or a value signifying that the input
+  formula is unsatisfiable.  Moreover, the procedure will be implemented with a
+  rich specification, so you'll know that the answer it gives is correct.  By
+  the end of the assignment, you'll have extracted OCaml code that can be used
+  to solve some of the more modest classes of problems in the SATLIB archive.
+
+  If you need to page in the relevant background material, try the Wikipedia
+  pages on
+  #<a href="http://en.wikipedia.org/wiki/Boolean_satisfiability_problem">#SAT#</a>#
+  and
+  #<a href="http://en.wikipedia.org/wiki/DPLL_algorithm">#the DPLL
+  algorithm#</a>#.  The implementation we'll develop here omits the pure literal
+  heuristic mentioned on the Wikipedia page but is otherwise identical.
+  *)
+
+
+(** * Problem Definition *)
+
+Definition var := nat.
+(** We identify propositional variables with natural numbers. *)
+
+Definition lit := (bool * var)%type.
+(** A literal is a combination of a truth value and a variable. *)
+
+Definition clause := list lit.
+(** A clause is a list (disjunction) of literals. *)
+
+Definition formula := list clause.
+(** A formula is a list (conjunction) of clauses. *)
+
+Definition asgn := var -> bool.
+(** An assignment is a function from variables to their truth values. *)
+
+Definition satLit (l : lit) (a : asgn) :=
+  a (snd l) = fst l.
+(** An assignment satisfies a literal if it maps it to true. *)
+
+Fixpoint satClause (cl : clause) (a : asgn) {struct cl} : Prop :=
+  match cl with
+    | nil => False
+    | l :: cl' => satLit l a \/ satClause cl' a
+  end.
+(** An assignment satisfies a clause if it satisfies at least one of its
+  literals.
+  *)
+
+Fixpoint satFormula (fm: formula) (a: asgn) {struct fm} : Prop :=
+  match fm with
+    | nil => True
+    | cl :: fm' => satClause cl a /\ satFormula fm' a
+  end.
+(** An assignment satisfies a formula if it satisfies all of its clauses. *)
+
+(** * Subroutines *)
+
+(** This is the only section of this assignment where you need to provide your
+  own solutions.  You will be implementing four crucial subroutines used by
+  DPLL.
+
+  I've provided a number of useful definitions and lemmas which you should feel
+  free to take advantage of in your definitions.  A few tips to keep in mind
+  while writing these strongly specified functions:
+  - You have a case-by-case choice of a "programming" approach, based around the
+    [refine] tactic; or a "proving" approach, where the "code" parts of your
+    definitions are constructed step by step with tactics.  The former is often
+    harder to get started with, but it tends to be more maintainable.
+  - When you use [refine] with a [fix] expression, it's usually a good idea to
+    use the [clear] tactic to remove the recursive function name from the
+    context immediately afterward.  This is because Coq won't check that you
+    call this function with strictly smaller arguments until the whole proof is
+    done, and it's a real downer to be told you had an invalid recursion
+    somewhere after you finally "finish" a proof.  Instead, make all recursive
+    calls explicit in the [refine] argument and clear the function name
+    afterward.
+  - You'll probably end up with a lot of proof obligations to discharge, and you
+    definitely won't want to prove most of them manually.  These tactics will
+    probably be your best friends here: [intuition], [firstorder], [eauto],
+    [simpl], [subst], ....  You will probably want to follow your [refine] tactics
+    with semicolons and strings of semicolon-separated tactics.  These strings
+    should probably start out with basic simplifiers like [intros], [simpl], and
+    [subst].
+  - A word of warning about the [firstorder] tactic: When it works, it works
+    really well!  However, this tactic has a way of running forever on
+    complicated enough goals.  Be ready to cancel its use (e.g., press the
+    "Stop" button in Proof General) if it takes more than a few seconds.  If
+    you do things the way I have, be prepared to mix and match all sorts of
+    different combinations of the automating tactics to get a proof script that
+    solves the problem quickly enough.
+  - The dependent type families that we use with rich specifications are all
+    defined in #<a href="http://coq.inria.fr/library/Coq.Init.Specif.html">#the
+    Specif module#</a># of the Coq standard library.  One potential gotcha when
+    using them comes from the fact that they are defined inductively with
+    parameters; that is, some arguments to these type families are defined
+    before the colon in the [Inductive] command.  Compared to general arguments
+    stemming from function types after that colon, usage of parameters is
+    restricted; they aren't allowed to vary in recursive occurrences of the
+    type being defined, for instance.  Because of this, parameters are ignored
+    for the purposes of pattern-matching, while they must be passed when
+    actually constructing new values.  For instance, one would pattern-match a
+    value of a [sig] type with a pattern like [exist x pf], while one would
+    construct a new value of the same type like [exist _ x pf].  The parameter
+    [P] is passed in the second case, and we use an underscore when the Coq
+    type-checker ought to be able to infer its value.  When this inference isn't
+    possible, you may need to specify manually the predicate defining the [sig]
+    type you want.
+
+  You can also consult the sizeable example at the end of this file, which ties
+  together the pieces you are supposed to write.
+  *)
+
+(** You'll probably want to compare booleans for equality at some point. *)
+Definition bool_eq_dec : forall (x y : bool), {x = y} + {x <> y}.
+  decide equality.
+Defined.
+
+(** A literal and its negation can't be true simultaneously. *)
+Lemma contradictory_assignment : forall s l cl a,
+  s <> fst l
+  -> satLit l a
+  -> satLit (s, snd l) a
+  -> satClause cl a.
+  intros.
+  red in H0, H1.
+  simpl in H1.
+  subst.
+  tauto.
+Qed.
+
+Local Hint Resolve contradictory_assignment : core.
+
+(** Augment an assignment with a new mapping. *)
+Definition upd (a : asgn) (l : lit) : asgn :=
+  fun v : var =>
+    if eq_nat_dec v (snd l)
+      then fst l
+      else a v.
+
+(** Some lemmas about [upd] *)
+
+Lemma satLit_upd_eq : forall l a,
+  satLit l (upd a l).
+  unfold satLit, upd; simpl; intros.
+  destruct (eq_nat_dec (snd l) (snd l)); tauto.
+Qed.
+
+Local Hint Resolve satLit_upd_eq : core.
+
+Lemma satLit_upd_neq : forall v l s a,
+  v <> snd l
+  -> satLit (s, v) (upd a l)
+  -> satLit (s, v) a.
+  unfold satLit, upd; simpl; intros.
+  destruct (eq_nat_dec v (snd l)); tauto.
+Qed.
+
+Local Hint Resolve satLit_upd_neq : core.
+
+Lemma satLit_upd_neq2 : forall v l s a,
+  v <> snd l
+  -> satLit (s, v) a
+  -> satLit (s, v) (upd a l).
+  unfold satLit, upd; simpl; intros.
+  destruct (eq_nat_dec v (snd l)); tauto.
+Qed.
+
+Local Hint Resolve satLit_upd_neq2 : core.
+
+Lemma satLit_contra : forall s l a cl,
+  s <> fst l
+  -> satLit (s, snd l) (upd a l)
+  -> satClause cl a.
+  unfold satLit, upd; simpl; intros.
+  destruct (eq_nat_dec (snd l) (snd l)); intuition.
+  assert False; intuition.
+Qed.
+
+Local Hint Resolve satLit_contra : core.
+
+(** Here's the tactic that I used to discharge #<i>#all#</i># proof obligations
+  in my implementations of the four functions you will define.
+  It comes with no warranty, as different implementations may lead to
+  obligations that it can't solve, or obligations that it takes 42 years to
+  solve.
+  However, if you think enough like me, each of the four definitions you fill in
+  should read like: [[
+refine some_expression_with_holes; clear function_name; magic_solver.
+]] leaving out the [clear] invocation for non-recursive function definitions.
+  *)
+Ltac magic_solver := simpl; intros; subst; intuition eauto; firstorder;
+  match goal with
+    | [ H1 : satLit ?l ?a, H2 : satClause ?cl ?a |- _ ] =>
+      assert (satClause cl (upd a l)); firstorder
+  end.
+
+(** OK, here's your first challenge.  Write this strongly-specified function to
+  update a clause to reflect the effect of making a particular literal true.
+  *)
+Definition setClause : forall (cl : clause) (l : lit),
+  {cl' : clause |
+    forall a, satClause cl (upd a l) <-> satClause cl' a}
+  + {forall a, satLit l a -> satClause cl a}.
+  refine (fix setClause (cl: clause) (l: lit) {struct cl} :=
+            match cl with
+            | nil => inleft (exist _ nil _)
+            | x :: xs =>
+              match setClause xs l with
+              | inright p => inright _
+              | inleft (exist _ cl' H) =>
+                match eq_nat_dec (snd x) (snd l), bool_eq_dec (fst x) (fst l) with
+                | left nat_eq, left bool_eq => inright _
+                | left eq, right ne => inleft (exist _ cl' _)
+                | right neq, _ => inleft (exist _ (x :: cl') _)
+                end
+              end
+            end); clear setClause; try magic_solver.
+  - intros; simpl; left; apply injective_projections in bool_eq; subst; auto.
+  - split; intros. simpl in H0. inversion H0. eapply satLit_contra; eauto.
+    destruct x; simpl in *; subst. auto.
+    apply H. eauto.
+    simpl. right. apply H; eauto.
+  - split; intros; simpl in *. inversion H0. destruct x; simpl in *; subst.
+    left. eauto.
+    right. apply H. eauto.
+    inversion H0. left. apply satLit_upd_neq2. auto. auto.
+    right. apply H. auto.
+Defined.
+
+(** For testing purposes, we define a weakly-specified function as a thin
+  wrapper around [setClause].
+  *)
+Definition setClauseSimple (cl : clause) (l : lit) :=
+  match setClause cl l with
+    | inleft (exist _ cl' _) => Some cl'
+    | inright _ => None
+  end.
+
+(** When your [setClause] implementation is done, you should be able to
+  uncomment these test cases and verify that each one yields the correct answer.
+  Be sure that your [setClause] definition ends in [Defined] and not [Qed], as
+  the former exposes the definition for use in computational reduction, while
+  the latter doesn't.
+  *)
+
+(*Eval compute in setClauseSimple ((false, 1%nat) :: nil) (true, 1%nat).*)
+(*Eval compute in setClauseSimple nil (true, 0).
+Eval compute in setClauseSimple ((true, 0) :: nil) (true, 0).
+Eval compute in setClauseSimple ((true, 0) :: nil) (false, 0).
+Eval compute in setClauseSimple ((true, 0) :: nil) (true, 1).
+Eval compute in setClauseSimple ((true, 0) :: nil) (false, 1).
+Eval compute in setClauseSimple ((true, 0) :: (true, 1) :: nil) (true, 1).
+Eval compute in setClauseSimple ((true, 0) :: (true, 1) :: nil) (false, 1).
+Eval compute in setClauseSimple ((true, 0) :: (false, 1) :: nil) (true, 1).
+Eval compute in setClauseSimple ((true, 0) :: (false, 1) :: nil) (false, 1).*)
+
+(** It's useful to have this strongly-specified nilness check. *)
+Definition isNil : forall (A : Set) (ls : list A), {ls = nil} + {True}.
+  destruct ls; [left|right]; eauto.
+Defined.
+Arguments isNil [A].
+
+(** Some more lemmas that I found helpful.... *)
+
+Lemma satLit_idem_lit : forall l a l',
+  satLit l a
+  -> satLit l' a
+  -> satLit l' (upd a l).
+  unfold satLit, upd; simpl; intros.
+  destruct (eq_nat_dec (snd l') (snd l)); congruence.
+Qed.
+
+Local Hint Resolve satLit_idem_lit : core.
+
+Lemma satLit_idem_clause : forall l a cl,
+  satLit l a
+  -> satClause cl a
+  -> satClause cl (upd a l).
+  induction cl; simpl; intuition.
+Qed.
+
+Local Hint Resolve satLit_idem_clause : core.
+
+Lemma satLit_idem_formula : forall l a fm,
+  satLit l a
+  -> satFormula fm a
+  -> satFormula fm (upd a l).
+  induction fm; simpl; intuition.
+Qed.
+
+Local Hint Resolve satLit_idem_formula : core.
+
+(** Challenge 2: Write this function that updates an entire formula to reflect
+  setting a literal to true.
+  *)
+Definition setFormula : forall (fm : formula) (l : lit),
+  {fm' : formula |
+    forall a, satFormula fm (upd a l) <-> satFormula fm' a}
+  + {forall a, satLit l a -> ~satFormula fm a}.
+  refine (fix setFormula (fm: formula) (l: lit) {struct fm} :=
+            match fm with
+            | nil => inleft (exist _ nil _)
+            | cl' :: fm' =>
+              match setFormula fm' l with
+              | inright p => inright _
+              | inleft (exist _ fm'' H) =>
+                match setClause cl' l with
+                | inright H' => inleft (exist _ fm'' _)
+                | inleft (exist _ cl'' _) =>
+                  if isNil cl''
+                  then inright _
+                  else inleft (exist _ (cl'' :: fm'') _)
+                end
+              end
+            end); clear setFormula; try solve [magic_solver].
+Defined.
+
+(** Here's some code for testing your implementation. *)
+
+Definition setFormulaSimple (fm : formula) (l : lit) :=
+  match setFormula fm l with
+    | inleft (exist _ fm' _) => Some fm'
+    | inright _ => None
+  end.
+
+(*Eval compute in setFormulaSimple (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil) (true, 1%nat).
+Eval compute in setFormulaSimple nil (true, 0).
+Eval compute in setFormulaSimple (((true, 0) :: nil) :: nil) (true, 0).
+Eval compute in setFormulaSimple (((false, 0) :: nil) :: nil) (true, 0).
+Eval compute in setFormulaSimple (((false, 1) :: nil) :: nil) (true, 0).
+Eval compute in setFormulaSimple (((false, 1) :: (true, 0) :: nil) :: nil) (true, 0).
+Eval compute in setFormulaSimple (((false, 1) :: (false, 0) :: nil) :: nil) (true, 0).*)
+
+Local Hint Extern 1 False => discriminate : core.
+
+Local Hint Extern 1 False =>
+  match goal with
+    | [ H : In _ (_ :: _) |- _ ] => inversion H; clear H; subst
+  end : core.
+
+(** Challenge 3: Write this code that either finds a unit clause in a formula
+  or declares that there are none.
+  *)
+Definition findUnitClause : forall (fm: formula),
+  {l : lit | In (l :: nil) fm}
+  + {forall l, ~In (l :: nil) fm}.
+  refine (fix findUnitClause (fm: formula) {struct fm} :=
+            match fm with
+            | nil => inright _
+            | (l :: nil) :: fm' => inleft (exist _ l _)
+            | cl :: fm' =>
+              match findUnitClause fm' with
+              | inleft (exist _ l _) => inleft (exist _ l _)
+              | inright H => inright _
+              end
+            end
+         ); clear findUnitClause; magic_solver.
+Defined.
+
+(** The literal in a unit clause must always be true in a satisfying
+  assignment.
+  *)
+Lemma unitClauseTrue : forall l a fm,
+  In (l :: nil) fm
+  -> satFormula fm a
+  -> satLit l a.
+  induction fm; intuition.
+  inversion H.
+  inversion H; subst; simpl in H0; intuition.
+Qed.
+
+Local Hint Resolve unitClauseTrue : core.
+
+(** Final challenge: Implement unit propagation.  The return type of
+  [unitPropagate] signifies that three results are possible:
+  - [None]: There are no unit clauses.
+  - [Some (inleft _)]: There is a unit clause, and here is a formula reflecting
+    setting its literal to true.
+  - [Some (inright _)]: There is a unit clause, and propagating it reveals that
+    the formula is unsatisfiable.
+  *)
+Definition unitPropagate : forall (fm : formula), option (sigT (fun fm' : formula =>
+  {l : lit |
+    (forall a, satFormula fm a -> satLit l a)
+    /\ forall a, satFormula fm (upd a l) <-> satFormula fm' a})
++ {forall a, ~satFormula fm a}).
+  refine (fix unitPropagate (fm: formula) {struct fm} :=
+            match findUnitClause fm with
+            | inright H => None
+            | inleft (exist _ l _) =>
+              match setFormula fm l with
+              | inright _ => Some (inright _)
+              | inleft (exist _ fm' _) =>
+                Some (inleft (existT _ fm' (exist _ l _)))
+              end
+            end
+         ); clear unitPropagate; magic_solver.
+Defined.
+
+
+Definition unitPropagateSimple (fm : formula) :=
+  match unitPropagate fm with
+    | None => None
+    | Some (inleft (existT _ fm' (exist _ l _))) => Some (Some (fm', l))
+    | Some (inright _) => Some None
+  end.
+
+(*Eval compute in unitPropagateSimple (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil).
+Eval compute in unitPropagateSimple nil.
+Eval compute in unitPropagateSimple (((true, 0) :: nil) :: nil).
+Eval compute in unitPropagateSimple (((true, 0) :: nil) :: ((false, 0) :: nil) :: nil).
+Eval compute in unitPropagateSimple (((true, 0) :: nil) :: ((false, 1) :: nil) :: nil).
+Eval compute in unitPropagateSimple (((true, 0) :: nil) :: ((false, 0) :: (false, 1) :: nil) :: nil).
+Eval compute in unitPropagateSimple (((false, 0) :: (false, 1) :: nil) :: ((true, 0) :: nil) :: nil).*)
+
+
+(** * The SAT Solver *)
+
+(** This section defines a DPLL SAT solver in terms of the subroutines you've
+  written.
+  *)
+
+(** An arbitrary heuristic to choose the next variable to split on *)
+Definition chooseSplit (fm : formula) :=
+  match fm with
+    | ((l :: _) :: _) => l
+    | _ => (true, 0)
+  end.
+
+Definition negate (l : lit) := (negb (fst l), snd l).
+
+Local Hint Unfold satFormula : core.
+
+Lemma satLit_dec : forall l a,
+  {satLit l a} + {satLit (negate l) a}.
+  destruct l.
+  unfold satLit; simpl; intro.
+  destruct b; destruct (a v); simpl; auto.
+Qed.
+
+(** We'll represent assignments as lists of literals instead of functions. *)
+Definition alist := list lit.
+
+Fixpoint interp_alist (al : alist) : asgn :=
+  match al with
+    | nil => fun _ => true
+    | l :: al' => upd (interp_alist al') l
+  end.
+
+(** Here's the final definition!  This is not the way you should write proof
+  scripts. ;-)
+
+  This implementation isn't #<i>#quite#</i># what you would expect, since it
+  takes an extra parameter expressing a search tree depth.  Writing the function
+  without that parameter would be trickier when it came to proving termination.
+  In practice, you can just seed the bound with one plus the number of variables
+  in the input, but the function's return type still indicates a possibility for
+  a "time-out" by returning [None].
+  *)
+Definition boundedSat: forall (bound : nat) (fm : formula),
+  option ({al : alist | satFormula fm (interp_alist al)}
+    + {forall a, ~satFormula fm a}).
+  refine (fix boundedSat (bound : nat) (fm : formula) {struct bound}
+    : option ({al : alist | satFormula fm (interp_alist al)}
+      + {forall a, ~satFormula fm a}) :=
+    match bound with
+      | O => None
+      | S bound' =>
+        if isNil fm
+          then Some (inleft _ (exist _ nil _))
+          else match unitPropagate fm with
+                 | Some (inleft (existT _ fm' (exist _ l _))) =>
+                   match boundedSat bound' fm' with
+                     | None => None
+                     | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (l :: al) _))
+                     | Some (inright _) => Some (inright _ _)
+                   end
+                 | Some (inright _) => Some (inright _ _)
+                 | None =>
+                   let l := chooseSplit fm in
+                     match setFormula fm l with
+                       | inleft (exist _ fm' _) =>
+                         match boundedSat bound' fm' with
+                           | None => None
+                           | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (l :: al) _))
+                           | Some (inright _) =>
+                             match setFormula fm (negate l) with
+                               | inleft (exist _ fm' _) =>
+                                 match boundedSat bound' fm' with
+                                   | None => None
+                                   | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _))
+                                   | Some (inright _) => Some (inright _ _)
+                                 end
+                               | inright _ => Some (inright _ _)
+                             end
+                         end
+                       | inright _ =>
+                         match setFormula fm (negate l) with
+                           | inleft (exist _ fm' _) =>
+                             match boundedSat bound' fm' with
+                               | None => None
+                               | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _))
+                               | Some (inright _) => Some (inright _ _)
+                             end
+                           | inright _ => Some (inright _ _)
+                         end
+                     end
+               end
+    end); simpl; intros; subst; intuition; try generalize dependent (interp_alist al).
+  firstorder.
+  firstorder.
+  firstorder.
+  firstorder.
+  assert (satFormula fm (upd a0 l)); firstorder.
+  assert (satFormula fm (upd a0 l)); firstorder.
+  firstorder.
+  firstorder.
+  firstorder.
+  firstorder.
+  firstorder.
+  firstorder.
+  firstorder.
+  firstorder.
+  firstorder.
+  firstorder.
+  destruct (satLit_dec l a);
+    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
+  destruct (satLit_dec l a);
+    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
+  destruct (satLit_dec l a);
+    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
+  destruct (satLit_dec l a);
+    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
+  destruct (satLit_dec l a); intuition eauto;
+    assert (satFormula fm (upd a l)); firstorder.
+  destruct (satLit_dec l a); intuition eauto;
+    assert (satFormula fm (upd a l)); firstorder.
+  firstorder.
+  firstorder.
+  destruct (satLit_dec l a); intuition eauto;
+    assert (satFormula fm (upd a (negate l))); firstorder.
+  destruct (satLit_dec l a); intuition eauto;
+    assert (satFormula fm (upd a (negate l))); firstorder.
+  destruct (satLit_dec l a);
+    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
+Defined.
+
+Definition boundedSatSimple (bound : nat) (fm : formula) :=
+  match boundedSat bound fm with
+  | None => None
+  | Some (inleft (exist _ a _)) => Some (Some a)
+  | Some (inright _) => Some None
+  end.
+
+(*Eval compute in boundedSatSimple 100 nil.
+Eval compute in boundedSatSimple 100 (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil).
+Eval compute in boundedSatSimple 100 (((true, 0) :: nil) :: nil).
+Eval compute in boundedSatSimple 100 (((true, 0) :: nil) :: ((false, 0) :: nil) :: nil).
+Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((true, 1) :: nil) :: nil).
+Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((true, 1) :: (false, 0) :: nil) :: nil).
+Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((false, 0) :: (false, 0) :: nil) :: ((true, 1) :: nil) :: nil).
+Eval compute in boundedSatSimple 100 (((false, 0) :: (true, 1) :: nil) :: ((false, 1) :: (true, 0) :: nil) :: nil).*)
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index b9ee741..c6c8bf4 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -35,13 +35,182 @@ open HTLMonadExtra
 
 module SS = Set.Make(P)
 
+type svtype =
+  | BBType of int
+  | VarType of int * int
+
+type sv = {
+  sv_type: svtype;
+  sv_num: int;
+}
+
+let print_sv v =
+  match v with
+  | { sv_type = BBType bbi; sv_num = n } -> sprintf "bb%d_%d" bbi n
+  | { sv_type = VarType (bbi, i); sv_num = n } -> sprintf "var%dn%d_%d" bbi i n
+
+module G = Graph.Persistent.Digraph.ConcreteLabeled(struct
+  type t = sv
+  let compare = compare
+  let equal = (=)
+  let hash = Hashtbl.hash
+end)(struct
+  type t = int
+  let compare = compare
+  let hash = Hashtbl.hash
+  let equal = (=)
+  let default = 0
+end)
+
+module GDot = Graph.Graphviz.Dot(struct
+    let graph_attributes _ = []
+    let default_vertex_attributes _ = []
+    let vertex_name = print_sv
+    let vertex_attributes _ = []
+    let get_subgraph _ = None
+    let default_edge_attributes _ = []
+    let edge_attributes _ = []
+
+    include G
+  end)
+
+module DFG = Graph.Persistent.Digraph.ConcreteLabeled(struct
+  type t = int * instr
+  let compare = compare
+  let equal = (=)
+  let hash = Hashtbl.hash
+end)(struct
+  type t = int
+  let compare = compare
+  let hash = Hashtbl.hash
+  let equal = (=)
+  let default = 0
+end)
+
+let reg r = sprintf "r%d" (P.to_int r)
+let print_pred r = sprintf "p%d" (Nat.to_int r)
+
+let print_instr = function
+  | RBnop -> ""
+  | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r)
+  | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r)
+  | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p)
+  | RBop (_, op, args, d) ->
+    (match op, args with
+    | Omove, _ -> "mov"
+    | Ointconst n, _ -> sprintf "%s=%ld" (reg d) (camlint_of_coqint n)
+    | Olongconst n, _ -> sprintf "%s=%LdL" (reg d) (camlint64_of_coqint n)
+    | Ofloatconst n, _ -> sprintf "%s=%.15F" (reg d) (camlfloat_of_coqfloat n)
+    | Osingleconst n, _ -> sprintf "%s=%.15Ff" (reg d) (camlfloat_of_coqfloat32 n)
+    | Oindirectsymbol id, _ -> sprintf "%s=&%s" (reg d) (extern_atom id)
+    | Ocast8signed, [r1] -> sprintf "%s=int8signed(%s)" (reg d) (reg r1)
+    | Ocast8unsigned, [r1] -> sprintf "%s=int8unsigned(%s)" (reg d) (reg r1)
+    | Ocast16signed, [r1] -> sprintf "%s=int16signed(%s)" (reg d) (reg r1)
+    | Ocast16unsigned, [r1] -> sprintf "%s=int16unsigned(%s)" (reg d) (reg r1)
+    | Oneg, [r1] -> sprintf "%s=-%s" (reg d) (reg r1)
+    | Osub, [r1;r2] -> sprintf "%s=%s-%s" (reg d) (reg r1) (reg r2)
+    | Omul, [r1;r2] -> sprintf "%s=%s*%s" (reg d) (reg r1) (reg r2)
+    | Omulimm n, [r1] -> sprintf "%s=%s*%ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Omulhs, [r1;r2] -> sprintf "%s=mulhs(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Omulhu, [r1;r2] -> sprintf "%s=mulhu(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Odiv, [r1;r2] -> sprintf "%s=%s /s %s" (reg d) (reg r1) (reg r2)
+    | Odivu, [r1;r2] -> sprintf "%s=%s /u %s" (reg d) (reg r1) (reg r2)
+    | Omod, [r1;r2] -> sprintf "%s=%s %%s %s" (reg d) (reg r1) (reg r2)
+    | Omodu, [r1;r2] -> sprintf "%s=%s %%u %s" (reg d) (reg r1) (reg r2)
+    | Oand, [r1;r2] -> sprintf "%s=%s & %s" (reg d) (reg r1) (reg r2)
+    | Oandimm n, [r1] -> sprintf "%s=%s & %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oor, [r1;r2] -> sprintf "%s=%s | %s" (reg d) (reg r1) (reg r2)
+    | Oorimm n, [r1] ->  sprintf "%s=%s | %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oxor, [r1;r2] -> sprintf "%s=%s ^ %s" (reg d) (reg r1) (reg r2)
+    | Oxorimm n, [r1] -> sprintf "%s=%s ^ %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Onot, [r1] -> sprintf "%s=not(%s)" (reg d) (reg r1)
+    | Oshl, [r1;r2] -> sprintf "%s=%s << %s" (reg d) (reg r1) (reg r2)
+    | Oshlimm n, [r1] -> sprintf "%s=%s << %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshr, [r1;r2] -> sprintf "%s=%s >>s %s" (reg d) (reg r1) (reg r2)
+    | Oshrimm n, [r1] -> sprintf "%s=%s >>s %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshrximm n, [r1] -> sprintf "%s=%s >>x %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshru, [r1;r2] -> sprintf "%s=%s >>u %s" (reg d) (reg r1) (reg r2)
+    | Oshruimm n, [r1] -> sprintf "%s=%s >>u %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Ororimm n, [r1] -> sprintf "%s=%s ror %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshldimm n, [r1;r2] -> sprintf "%s=(%s, %s) << %ld" (reg d) (reg r1) (reg r2) (camlint_of_coqint n)
+    | Olea addr, args -> sprintf "%s=addr" (reg d)
+    | Omakelong, [r1;r2] -> sprintf "%s=makelong(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Olowlong, [r1] -> sprintf "%s=lowlong(%s)" (reg d) (reg r1)
+    | Ohighlong, [r1] -> sprintf "%s=highlong(%s)" (reg d) (reg r1)
+    | Ocast32signed, [r1] -> sprintf "%s=long32signed(%s)" (reg d) (reg r1)
+    | Ocast32unsigned, [r1] -> sprintf "%s=long32unsigned(%s)" (reg d) (reg r1)
+    | Onegl, [r1] -> sprintf "%s=-l %s" (reg d) (reg r1)
+    | Osubl, [r1;r2] -> sprintf "%s=%s -l %s" (reg d) (reg r1) (reg r2)
+    | Omull, [r1;r2] -> sprintf "%s=%s *l %s" (reg d) (reg r1) (reg r2)
+    | Omullimm n, [r1] -> sprintf "%s=%s *l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+    | Omullhs, [r1;r2] -> sprintf "%s=mullhs(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Omullhu, [r1;r2] -> sprintf "%s=mullhu(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Odivl, [r1;r2] -> sprintf "%s=%s /ls %s" (reg d) (reg r1) (reg r2)
+    | Odivlu, [r1;r2] -> sprintf "%s=%s /lu %s" (reg d) (reg r1) (reg r2)
+    | Omodl, [r1;r2] -> sprintf "%s=%s %%ls %s" (reg d) (reg r1) (reg r2)
+    | Omodlu, [r1;r2] -> sprintf "%s=%s %%lu %s" (reg d) (reg r1) (reg r2)
+    | Oandl, [r1;r2] -> sprintf "%s=%s &l %s" (reg d) (reg r1) (reg r2)
+    | Oandlimm n, [r1] -> sprintf "%s=%s &l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+    | Oorl, [r1;r2] -> sprintf "%s=%s |l %s" (reg d) (reg r1) (reg r2)
+    | Oorlimm n, [r1] ->  sprintf "%s=%s |l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+    | Oxorl, [r1;r2] -> sprintf "%s=%s ^l %s" (reg d) (reg r1) (reg r2)
+    | Oxorlimm n, [r1] -> sprintf "%s=%s ^l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+    | Onotl, [r1] -> sprintf "%s=notl(%s)" (reg d) (reg r1)
+    | Oshll, [r1;r2] -> sprintf "%s=%s <<l %s" (reg d) (reg r1) (reg r2)
+    | Oshllimm n, [r1] -> sprintf "%s=%s <<l %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshrl, [r1;r2] -> sprintf "%s=%s >>ls %s" (reg d) (reg r1) (reg r2)
+    | Oshrlimm n, [r1] -> sprintf "%s=%s >>ls %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshrxlimm n, [r1] -> sprintf "%s=%s >>lx %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshrlu, [r1;r2] -> sprintf "%s=%s >>lu %s" (reg d) (reg r1) (reg r2)
+    | Oshrluimm n, [r1] -> sprintf "%s=%s >>lu %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Ororlimm n, [r1] -> sprintf "%s=%s rorl %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oleal addr, args -> sprintf "%s=addr" (reg d)
+    | Onegf, [r1] -> sprintf "%s=negf(%s)" (reg d) (reg r1)
+    | Oabsf, [r1] -> sprintf "%s=absf(%s)" (reg d) (reg r1)
+    | Oaddf, [r1;r2] -> sprintf "%s=%s +f %s" (reg d) (reg r1) (reg r2)
+    | Osubf, [r1;r2] -> sprintf "%s=%s -f %s" (reg d) (reg r1) (reg r2)
+    | Omulf, [r1;r2] -> sprintf "%s=%s *f %s" (reg d) (reg r1) (reg r2)
+    | Odivf, [r1;r2] -> sprintf "%s=%s /f %s" (reg d) (reg r1) (reg r2)
+    | Onegfs, [r1] -> sprintf "%s=negfs(%s)" (reg d) (reg r1)
+    | Oabsfs, [r1] -> sprintf "%s=absfs(%s)" (reg d) (reg r1)
+    | Oaddfs, [r1;r2] -> sprintf "%s=%s +fs %s" (reg d) (reg r1) (reg r2)
+    | Osubfs, [r1;r2] -> sprintf "%s=%s -fs %s" (reg d) (reg r1) (reg r2)
+    | Omulfs, [r1;r2] -> sprintf "%s=%s *fs %s" (reg d) (reg r1) (reg r2)
+    | Odivfs, [r1;r2] -> sprintf "%s=%s /fs %s" (reg d) (reg r1) (reg r2)
+    | Osingleoffloat, [r1] -> sprintf "%s=singleoffloat(%s)" (reg d) (reg r1)
+    | Ofloatofsingle, [r1] -> sprintf "%s=floatofsingle(%s)" (reg d) (reg r1)
+    | Ointoffloat, [r1] -> sprintf "%s=intoffloat(%s)" (reg d) (reg r1)
+    | Ofloatofint, [r1] -> sprintf "%s=floatofint(%s)" (reg d) (reg r1)
+    | Ointofsingle, [r1] -> sprintf "%s=intofsingle(%s)" (reg d) (reg r1)
+    | Osingleofint, [r1] -> sprintf "%s=singleofint(%s)" (reg d) (reg r1)
+    | Olongoffloat, [r1] -> sprintf "%s=longoffloat(%s)" (reg d) (reg r1)
+    | Ofloatoflong, [r1] -> sprintf "%s=floatoflong(%s)" (reg d) (reg r1)
+    | Olongofsingle, [r1] -> sprintf "%s=longofsingle(%s)" (reg d) (reg r1)
+    | Osingleoflong, [r1] -> sprintf "%s=singleoflong(%s)" (reg d) (reg r1)
+    | Ocmp c, args -> sprintf "%s=cmp" (reg d)
+    | Osel (c, ty), r1::r2::args -> sprintf "%s=sel" (reg d)
+    | _, _ -> sprintf "N/a")
+
+module DFGDot = Graph.Graphviz.Dot(struct
+    let graph_attributes _ = []
+    let default_vertex_attributes _ = []
+    let vertex_name = function (i, instr) -> sprintf "\"%d:%s\"" i (print_instr instr)
+    let vertex_attributes _ = []
+    let get_subgraph _ = None
+    let default_edge_attributes _ = []
+    let edge_attributes _ = []
+
+    include DFG
+  end)
+
 module IMap = Map.Make (struct
   type t = int
 
   let compare = compare
 end)
 
-type dfg = { nodes : instr list; edges : (int * int) list }
+let gen_vertex instrs i = (i, List.nth instrs i)
+
 (** The DFG type defines a list of instructions with their data dependencies as [edges], which are
    the pairs of integers that represent the index of the instruction in the [nodes].  The edges
    always point from left to right. *)
@@ -55,10 +224,12 @@ let print_tuple out_chan a =
   let l, r = a in
   fprintf out_chan "(%d,%d)" l r
 
-let print_dfg out_chan dfg =
+(*let print_dfg out_chan dfg =
   fprintf out_chan "{ nodes = %a, edges = %a }"
     (print_list PrintRTLBlockInstr.print_bblock_body)
-    dfg.nodes (print_list print_tuple) dfg.edges
+    dfg.nodes (print_list print_tuple) dfg.edges*)
+
+let print_dfg = DFGDot.output_graph
 
 let read_process command =
   let buffer_size = 2048 in
@@ -73,38 +244,77 @@ let read_process command =
   ignore (Unix.close_process_in in_channel);
   Buffer.contents buffer
 
+let comb_delay = function
+  | RBnop -> 0
+  | RBop (_, op, _, _) ->
+    (match op with
+     | Omove -> 0
+     | Ointconst _ -> 0
+     | Olongconst _ -> 0
+     | Ocast8signed -> 0
+     | Ocast8unsigned -> 0
+     | Ocast16signed -> 0
+     | Ocast16unsigned -> 0
+     | Oneg -> 0
+     | Onot -> 0
+     | Oor -> 0
+     | Oorimm _ -> 0
+     | Oand -> 0
+     | Oandimm _ -> 0
+     | Oxor -> 0
+     | Oxorimm _ -> 0
+     | Omul -> 8
+     | Omulimm _ -> 8
+     | Omulhs -> 8
+     | Omulhu -> 8
+     | Odiv -> 72
+     | Odivu -> 72
+     | Omod -> 72
+     | Omodu -> 72
+     | _ -> 1)
+  | _ -> 1
+
+let pipeline_stages = function
+  | RBop (_, op, _, _) ->
+    (match op with
+     | Odiv -> 32
+     | Odivu -> 32
+     | Omod -> 32
+     | Omodu -> 32
+     | _ -> 0)
+  | _ -> 0
+
 (** Add a dependency if it uses a register that was written to previously. *)
-let add_dep i tree deps curr =
-  match PTree.get curr tree with None -> deps | Some ip -> (ip, i) :: deps
+let add_dep map i tree dfg curr =
+  match PTree.get curr tree with
+  | 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)
 
 (** This function calculates the dependencies of each instruction.  The nodes correspond to previous
    registers that were allocated and show which instruction caused it.
 
    This function only gathers the RAW constraints, and will therefore only be active for operations
    that modify registers, which is this case only affects loads and operations. *)
-let accumulate_RAW_deps dfg curr =
-  let i, dst_map, { edges; nodes } = dfg in
+let accumulate_RAW_deps map dfg curr =
+  let i, dst_map, graph = dfg in
   let acc_dep_instruction rs dst =
     ( i + 1,
       PTree.set dst i dst_map,
-      {
-        nodes;
-        edges = List.append (List.fold_left (add_dep i dst_map) [] rs) edges;
-      } )
+      List.fold_left (add_dep map i dst_map) graph rs
+    )
   in
   let acc_dep_instruction_nodst rs =
     ( i + 1,
       dst_map,
-      {
-        nodes;
-        edges = List.append (List.fold_left (add_dep i dst_map) [] rs) edges;
-      } )
+    List.fold_left (add_dep map i dst_map) graph rs)
   in
   match curr with
   | RBop (op, _, rs, dst) -> acc_dep_instruction rs dst
   | RBload (op, _mem, _addr, rs, dst) -> acc_dep_instruction rs dst
   | RBstore (op, _mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs)
-  | _ -> (i + 1, dst_map, { edges; nodes })
+  | _ -> (i + 1, dst_map, graph)
 
 (** Finds the next write to the [dst] register.  This is a small optimisation so that only one
    dependency is generated for a data dependency. *)
@@ -159,32 +369,32 @@ let rec next_load i = function
   | RBload (_, _, _, _, _) :: _ -> Some i
   | _ :: rst -> next_load (i + 1) rst
 
-let accumulate_RAW_mem_deps dfg curr =
-  let i, { nodes; edges } = dfg in
+let accumulate_RAW_mem_deps instrs dfg curri =
+  let i, curr = curri in
   match curr with
   | RBload (_, _, _, _, _) -> (
-      match next_store 0 (take i nodes |> List.rev) with
-      | None -> (i + 1, { nodes; edges })
-      | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) )
-  | _ -> (i + 1, { nodes; edges })
+      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) )
+  | _ -> dfg
 
-let accumulate_WAR_mem_deps dfg curr =
-  let i, { nodes; edges } = dfg in
+let accumulate_WAR_mem_deps instrs dfg curri =
+  let i, curr = curri in
   match curr with
   | RBstore (_, _, _, _, _) -> (
-      match next_load 0 (take i nodes |> List.rev) with
-      | None -> (i + 1, { nodes; edges })
-      | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) )
-  | _ -> (i + 1, { nodes; edges })
+      match next_load 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) )
+  | _ -> dfg
 
-let accumulate_WAW_mem_deps dfg curr =
-  let i, { nodes; edges } = dfg in
+let accumulate_WAW_mem_deps instrs dfg curri =
+  let i, curr = curri in
   match curr with
   | RBstore (_, _, _, _, _) -> (
-      match next_store 0 (take i nodes |> List.rev) with
-      | None -> (i + 1, { nodes; edges })
-      | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) )
-  | _ -> (i + 1, { nodes; edges })
+      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) )
+  | _ -> dfg
 
 (** Predicate dependencies. *)
 
@@ -195,7 +405,7 @@ let rec in_predicate p p' =
   | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2
   | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2
 
-let rec get_predicate = function
+let get_predicate = function
   | RBop (p, _, _, _) -> p
   | RBload (p, _, _, _, _) -> p
   | RBstore (p, _, _, _, _) -> p
@@ -224,64 +434,65 @@ let rec next_preduse p i instr=
   | RBop (Some p', _, _, _) :: rst -> next p' rst
   | _ :: rst -> next_load (i + 1) rst
 
-let accumulate_RAW_pred_deps dfg curr =
-  let i, { nodes; edges } = dfg in
+let accumulate_RAW_pred_deps instrs dfg curri =
+  let i, curr = curri in
   match get_predicate curr with
   | Some p -> (
-      match next_setpred p 0 (take i nodes |> List.rev) with
-      | None -> (i + 1, { nodes; edges })
-      | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) )
-  | _ -> (i + 1, { nodes; edges })
+      match next_setpred p 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) )
+  | _ -> dfg
 
-let accumulate_WAR_pred_deps dfg curr =
-  let i, { nodes; edges } = dfg in
+let accumulate_WAR_pred_deps instrs dfg curri =
+  let i, curr = curri in
   match curr with
   | RBsetpred (_, _, p) -> (
-      match next_preduse p 0 (take i nodes |> List.rev) with
-      | None -> (i + 1, { nodes; edges })
-      | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) )
-  | _ -> (i + 1, { nodes; edges })
+      match next_preduse p 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) )
+  | _ -> dfg
 
-let accumulate_WAW_pred_deps dfg curr =
-  let i, { nodes; edges } = dfg in
+let accumulate_WAW_pred_deps instrs dfg curri =
+  let i, curr = curri in
   match curr with
   | RBsetpred (_, _, p) -> (
-      match next_setpred (Pvar p) 0 (take i nodes |> List.rev) with
-      | None -> (i + 1, { nodes; edges })
-      | Some d -> (i + 1, { nodes; edges = (i - d - 1, i) :: edges }) )
-  | _ -> (i + 1, { nodes; edges })
+      match next_setpred (Pvar p) 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) )
+  | _ -> dfg
 
 (** This function calculates the WAW dependencies, which happen when two writes are ordered one
    after another and therefore have to be kept in that order.  This accumulation might be redundant
    if register renaming is done before hand, because then these dependencies can be avoided. *)
-let accumulate_WAW_deps dfg curr =
-  let i, { edges; nodes } = dfg in
+let accumulate_WAW_deps instrs dfg curri =
+  let i, curr = curri in
   let dst_dep dst =
-    match find_next_dst_write i dst (i + 1) (drop (i + 1) nodes) with
-    | Some d -> (i + 1, { nodes; edges = d :: edges })
-    | _ -> (i + 1, { nodes; edges })
+    match find_next_dst_write i dst (i + 1) (drop (i + 1) instrs) with
+    | Some (a, b) -> DFG.add_edge dfg (gen_vertex instrs a) (gen_vertex instrs b)
+    | _ -> dfg
   in
   match curr with
   | RBop (_, _, _, dst) -> dst_dep dst
   | RBload (_, _, _, _, dst) -> dst_dep dst
   | RBstore (_, _, _, _, _) -> (
-      match next_store (i + 1) (drop (i + 1) nodes) with
-      | None -> (i + 1, { nodes; edges })
-      | Some i' -> (i + 1, { nodes; edges = (i, i') :: edges }) )
-  | _ -> (i + 1, { nodes; edges })
+      match next_store (i + 1) (drop (i + 1) instrs) with
+      | None -> dfg
+      | Some i' -> DFG.add_edge dfg (gen_vertex instrs i) (gen_vertex instrs i') )
+  | _ -> dfg
 
-let accumulate_WAR_deps dfg curr =
-  let i, { edges; nodes } = dfg in
+let accumulate_WAR_deps instrs dfg curri =
+  let i, curr = curri in
   let dst_dep dst =
-    let dep_list = find_all_next_dst_read i dst 0 (take i nodes |> List.rev)
+    let dep_list = find_all_next_dst_read i dst 0 (take i instrs |> List.rev)
         |> List.map (function (d, d') -> (i - d' - 1, d))
     in
-    (i + 1, { nodes; edges = List.append dep_list edges })
+    List.fold_left (fun g ->
+        function (d, d') -> DFG.add_edge g (gen_vertex instrs d) (gen_vertex instrs d')) dfg dep_list
   in
   match curr with
   | RBop (_, _, _, dst) -> dst_dep dst
   | RBload (_, _, _, _, dst) -> dst_dep dst
-  | _ -> (i + 1, { nodes; edges })
+  | _ -> dfg
 
 let assigned_vars vars = function
   | RBnop -> vars
@@ -307,124 +518,178 @@ let check_dependent op1 op2 =
   | Some p, Some p' -> not (independant_pred p p')
   | _, _ -> true
 
-let remove_unnecessary_deps dfg =
-  let { edges; nodes } = dfg in
-  let is_dependent = function (i1, i2) ->
-    let instr1 = List.nth nodes i1 in
-    let instr2 = List.nth nodes i2 in
-    check_dependent (get_pred instr1) (get_pred instr2)
+let remove_unnecessary_deps graph =
+  let is_dependent v1 v2 g =
+    let (_, instr1) = v1 in
+    let (_, instr2) = v2 in
+    if check_dependent (get_pred instr1) (get_pred instr2)
+    then g
+    else DFG.remove_edge g v1 v2
   in
-  { edges = List.filter is_dependent edges; nodes }
+  DFG.fold_edges is_dependent graph graph
 
 (** All the nodes in the DFG have to come after the source of the basic block, and should terminate
    before the sink of the basic block.  After that, there should be constraints for data
    dependencies between nodes. *)
 let gather_bb_constraints debug bb =
-  let _, _, dfg =
-    List.fold_left accumulate_RAW_deps
-      (0, PTree.empty, { nodes = bb.bb_body; edges = [] })
+  let ibody = List.mapi (fun i a -> (i, a)) bb.bb_body in
+  let dfg = List.fold_left (fun dfg v -> DFG.add_vertex dfg v) DFG.empty ibody in
+  let _, _, dfg' =
+    List.fold_left (accumulate_RAW_deps ibody)
+      (0, PTree.empty, dfg)
       bb.bb_body
   in
-  if debug then printf "DFG : %a\n" print_dfg dfg else ();
-  let _, dfg1 = List.fold_left accumulate_WAW_deps (0, dfg) bb.bb_body in
-  if debug then printf "DFG': %a\n" print_dfg dfg1 else ();
-  let _, dfg2 = List.fold_left accumulate_WAR_deps (0, dfg1) bb.bb_body in
-  if debug then printf "DFG'': %a\n" print_dfg dfg2 else ();
-  let _, dfg3 =
-    List.fold_left accumulate_RAW_mem_deps (0, dfg2) bb.bb_body
-  in
-  if debug then printf "DFG''': %a\n" print_dfg dfg3 else ();
-  let _, dfg4 =
-    List.fold_left accumulate_WAR_mem_deps (0, dfg3) bb.bb_body
-  in
-  if debug then printf "DFG'''': %a\n" print_dfg dfg4 else ();
-  let _, dfg5 =
-    List.fold_left accumulate_WAW_mem_deps (0, dfg4) bb.bb_body
-  in
-  let _, dfg6 =
-    List.fold_left accumulate_RAW_pred_deps (0, dfg5) bb.bb_body
+  let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb.bb_body) dfg ibody) dfg'
+      [ accumulate_WAW_deps;
+        accumulate_WAR_deps;
+        accumulate_RAW_mem_deps;
+        accumulate_WAR_mem_deps;
+        accumulate_WAW_mem_deps;
+        accumulate_RAW_pred_deps;
+        accumulate_WAR_pred_deps;
+        accumulate_WAW_pred_deps
+      ]
   in
-  let _, dfg7 =
-    List.fold_left accumulate_WAR_pred_deps (0, dfg6) bb.bb_body
+  let dfg''' = remove_unnecessary_deps dfg'' in
+  (List.length bb.bb_body, dfg''', successors_instr bb.bb_exit)
+
+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_super_nodes n dfg =
+  DFG.fold_vertex (function v1 -> fun g ->
+      (if DFG.in_degree dfg v1 = 0
+       then G.add_edge_e g (encode_bb n 0, 0, encode_var n (fst v1) 0)
+       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)
+         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)
+    )
+
+let add_ctrl_deps n succs constr =
+  List.fold_left (fun g n' ->
+      G.add_edge_e g (encode_bb n 1, -1, encode_bb n' 0)
+    ) constr succs
+
+module BFDFG = Graph.Path.BellmanFord(DFG)(struct
+    include DFG
+    type t = int
+    let weight = DFG.E.label
+    let compare = compare
+    let add = (+)
+    let zero = 0
+  end)
+
+module TopoDFG = Graph.Topological.Make(DFG)
+
+let negate_graph constr =
+  DFG.fold_edges_e (function (v1, e, v2) -> fun g ->
+      DFG.add_edge_e g (v1, -e, v2)
+    ) constr DFG.empty
+
+let add_cycle_constr max n dfg constr =
+  let negated_dfg = negate_graph dfg 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
+  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),
+                      encode_var n (fst v') 0)
+    ) constr (DFG.fold_vertex (fun v l ->
+      List.append l (longest_path v |> constrained_paths
+                     |> List.map (function (v', w) -> (v, v', - w)))
+    ) dfg [])
+
+type resource =
+  | Mem
+  | SDiv
+  | UDiv
+
+type resources = {
+  res_mem: DFG.V.t list;
+  res_udiv: DFG.V.t list;
+  res_sdiv: DFG.V.t list;
+}
+
+let find_resource = function
+  | RBload _ -> Some Mem
+  | RBstore _ -> Some Mem
+  | RBop (_, op, _, _) ->
+    ( match op with
+      | Odiv -> Some SDiv
+      | Odivu -> Some UDiv
+      | Omod -> Some SDiv
+      | Omodu -> Some UDiv
+      | _ -> None )
+  | _ -> None
+
+let add_resource_constr n dfg constr =
+  let res = TopoDFG.fold (function (i, instr) ->
+    function {res_mem = ml; res_sdiv = sdl; res_udiv = udl} as r ->
+    match find_resource instr with
+    | Some SDiv -> {r with res_sdiv = (i, instr) :: sdl}
+    | Some UDiv -> {r with res_udiv = (i, instr) :: udl}
+    | Some Mem -> {r with res_mem = (i, instr) :: ml}
+    | None -> r
+    ) dfg {res_mem = []; res_sdiv = []; res_udiv = []}
   in
-  let _, dfg8 =
-    List.fold_left accumulate_WAW_pred_deps (0, dfg7) bb.bb_body
+  let get_constraints l g = List.fold_left (fun gv v' ->
+      match gv with
+      | (g, None) -> (g, Some v')
+      | (g, Some v) ->
+        (G.add_edge_e g (encode_var n (fst v) 0, -1, encode_var n (fst v') 0), Some v')
+    ) (g, None) l |> fst
   in
-  let dfg9 = remove_unnecessary_deps dfg8 in
-  if debug then printf "DFG''''': %a\n" print_dfg dfg9 else ();
-  (List.length bb.bb_body, dfg9, successors_instr bb.bb_exit)
-
-let gen_bb_name s i = sprintf "bb%d%s" (P.to_int i) s
-
-let gen_bb_name_ssrc = gen_bb_name "ssrc"
-
-let gen_bb_name_ssnk = gen_bb_name "ssnk"
-
-let gen_var_name s c i = sprintf "v%d%s_%d" (P.to_int i) s c
-
-let gen_var_name_b = gen_var_name "b"
-
-let gen_var_name_e = gen_var_name "e"
-
-let print_lt0 = sprintf "%s - %s <= 0;\n"
-
-let print_bb_order i c = if P.to_int c < P.to_int i then
-    print_lt0 (gen_bb_name_ssnk i) (gen_bb_name_ssrc c) else
-    ""
-
-let print_src_order i c =
-  print_lt0 (gen_bb_name_ssrc i) (gen_var_name_b c i)
-  ^ print_lt0 (gen_var_name_e c i) (gen_bb_name_ssnk i)
-  ^ sprintf "%s - %s = 1;\n" (gen_var_name_e c i) (gen_var_name_b c i)
-
-let print_src_type i c =
-  sprintf "int %s;\n" (gen_var_name_e c i)
-  ^ sprintf "int %s;\n" (gen_var_name_b c i)
-
-let print_data_dep_order c (i, j) =
-  print_lt0 (gen_var_name_e i c) (gen_var_name_b j c)
-
-let gather_cfg_constraints (completed, (bvars, constraints, types)) c curr =
-  if List.exists (P.eq curr) completed then
-    (completed, (bvars, constraints, types))
-  else
-    match PTree.get curr c with
-    | None -> assert false
-    | Some (num_iters, dfg, next) ->
-        let constraints' =
-          constraints
-          ^ String.concat "" (List.map (print_bb_order curr) next)
-          ^ String.concat ""
-              (List.map (print_src_order curr)
-                 (List.init num_iters (fun x -> x)))
-          ^ String.concat "" (List.map (print_data_dep_order curr) dfg.edges)
-        in
-        let types' =
-          types
-          ^ String.concat ""
-              (List.map (print_src_type curr)
-                 (List.init num_iters (fun x -> x)))
-          ^ sprintf "int %s;\n" (gen_bb_name_ssrc curr)
-          ^ sprintf "int %s;\n" (gen_bb_name_ssnk curr)
-        in
-        let bvars' =
-          List.append
-            (List.map
-               (fun x -> gen_var_name_b x curr)
-               (List.init num_iters (fun x -> x)))
-            bvars
-        in
-        (curr :: completed, (bvars', constraints', types'))
+  get_constraints (List.rev res.res_mem) constr
+  |> get_constraints (List.rev res.res_udiv)
+  |> get_constraints (List.rev res.res_sdiv)
+
+let gather_cfg_constraints c constr curr =
+  let (n, dfg) = curr in
+  match PTree.get (P.of_int n) c with
+  | None -> assert false
+  | Some { bb_exit = ctrl; _ } ->
+    add_super_nodes n dfg constr
+    |> add_data_deps n dfg
+    |> add_ctrl_deps n (successors_instr ctrl
+                        |> List.map P.to_int
+                        |> List.filter (fun n' -> n' < n))
+    |> add_cycle_constr 8 n dfg
+    |> add_resource_constr n dfg
 
 let rec intersperse s = function
   | [] -> []
   | [ a ] -> [ a ]
   | x :: xs -> x :: s :: intersperse s xs
 
+let print_objective constr =
+  let vars = G.fold_vertex (fun v1 l ->
+      match v1 with
+      | { sv_type = VarType _; sv_num = 0 } -> print_sv v1 :: l
+      | _ -> l
+    ) constr []
+  in
+  "min: " ^ String.concat "" (intersperse " + " vars) ^ ";\n"
+
+let print_lp constr =
+  print_objective constr ^
+  (G.fold_edges_e (function (e1, w, e2) -> fun s ->
+       s ^ sprintf "%s - %s <= %d;\n" (print_sv e1) (print_sv e2) w
+     ) constr "" |>
+   G.fold_vertex (fun v1 s ->
+       s ^ sprintf "int %s;\n" (print_sv v1)
+     ) constr)
+
 let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ]
 
 let parse_soln tree s =
-  let r = Str.regexp "v\\([0-9]+\\)b_\\([0-9]+\\)[ ]+\\([0-9]+\\)" in
+  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)
@@ -434,96 +699,83 @@ let parse_soln tree s =
       tree
   else tree
 
-let solve_constraints vars constraints types =
+let solve_constraints constr =
   let oc = open_out "lpsolve.txt" in
-  fprintf oc "min: ";
-  List.iter (fprintf oc "%s") (intersperse " + " vars);
-  fprintf oc ";\n";
-  fprintf oc "%s" constraints;
-  fprintf oc "%s" types;
+  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 find_min = function
-  | [] -> assert false
-  | l :: ls ->
-      let rec find_min' current = function
-        | [] -> current
-        | l' :: ls' ->
-            if snd l' < current then find_min' (snd l') ls'
-            else find_min' current ls'
-      in
-      find_min' (snd l) ls
-
-let find_max = function
-  | [] -> assert false
-  | l :: ls ->
-      let rec find_max' current = function
-        | [] -> current
-        | l' :: ls' ->
-            if snd l' > current then find_max' (snd l') ls'
-            else find_max' current ls'
-      in
-      find_max' (snd l) ls
-
-let ( >>= ) = bind
+let subgraph dfg l =
+  let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in
+  List.fold_left (fun g v ->
+      List.fold_left (fun g' v' ->
+          let edges = DFG.find_all_edges dfg v v' in
+          List.fold_left (fun g'' e ->
+              DFG.add_edge_e g'' e
+            ) g' edges
+        ) g l
+    ) dfg' l
+
+let rec all_successors dfg v =
+  List.concat (List.fold_left (fun l v ->
+      all_successors dfg v :: l
+    ) [] (DFG.succ dfg v))
+
+let order_instr dfg =
+  DFG.fold_vertex (fun v li ->
+      if DFG.in_degree dfg v = 0
+      then (List.map snd (v :: all_successors dfg v)) :: li
+      else li
+    ) dfg []
 
 let combine_bb_schedule schedule s =
   let i, st = s in
   IMap.update st (update_schedule i) schedule
 
-let compare_tuple (a, _) (b, _) = compare a b
-
 (** Should generate the [RTLPar] code based on the input [RTLBlock] description. *)
-let transf_rtlpar c (schedule : (int * int) list IMap.t) =
+let transf_rtlpar c c' (schedule : (int * int) list IMap.t) =
   let f i bb : RTLPar.bblock =
     match bb with
-    | { bb_body = []; bb_exit = c } ->
-      { bb_body = [];
-        bb_exit = c
-      }
+    | { bb_body = []; bb_exit = c } -> { bb_body = []; bb_exit = c }
     | { bb_body = bb_body'; bb_exit = ctrl_flow } ->
-        let i_sched =
-          try IMap.find (P.to_int i) schedule
-          with Not_found -> (
-            printf "Could not find %d\n" (P.to_int i);
-            IMap.iter
-              (fun d -> printf "%d: %a\n" d (print_list print_tuple))
-              schedule;
-            assert false
-          )
-        in
-        let min_state = find_min i_sched in
-        let max_state = find_max i_sched in
-        let i_sched_tree =
-          List.fold_left combine_bb_schedule IMap.empty i_sched
-        in
-        (*printf "--------------- curr: %d, max: %d, min: %d, next: %d\n" (P.to_int i) max_state min_state (P.to_int i - max_state + min_state - 1);
-        printf "HIIIII: %d orig: %d\n" (P.to_int i - max_state + min_state - 1) (P.to_int i);*)
-        { bb_body = (IMap.to_seq i_sched_tree |> List.of_seq |> List.sort compare_tuple |> List.map snd
-                           |> List.map (List.map (fun x -> List.nth bb_body' x)));
-          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 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 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 -> TopoDFG.fold (fun i l -> snd i :: l) x [])
+                                           |> List.rev) body
+      in
+      { bb_body = List.map (fun x -> [x]) final_body2;
+        bb_exit = ctrl_flow
+      }
   in
   PTree.map f c
 
-let second = function (_, a, _) -> a
-
 let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
-  let debug = false in
-  let c' = PTree.map1 (gather_bb_constraints false) c in
+  let debug = true in
+  let transf_graph (_, dfg, _) = dfg in
+  let c' = PTree.map1 (fun x -> gather_bb_constraints false x |> transf_graph) c in
   (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in*)
-  let _, (vars, constraints, types) =
-    List.map fst (PTree.elements c') |>
-    List.fold_left (fun compl ->
-        gather_cfg_constraints compl c') ([], ([], "", ""))
+  let cgraph = PTree.elements c'
+               |> List.map (function (x, y) -> (P.to_int x, y))
+               |> List.fold_left (gather_cfg_constraints c) G.empty
   in
-  let schedule' = solve_constraints vars constraints types in
-  (*IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*)
+  let graph = open_out "constr_graph.dot" in
+  fprintf graph "%a\n" GDot.output_graph cgraph;
+  close_out graph;
+  let schedule' = solve_constraints cgraph in
+  (**IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*)
   (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*)
-  transf_rtlpar c schedule'
+  transf_rtlpar c c' schedule'
 
 let rec find_reachable_states c e =
   match PTree.get e c with