Merge remote-tracking branch 'origin/dev/divider' into dev/scheduling

11 files changed, 353 insertions, 73 deletions

diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index a36f375..467ae37 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -421,10 +421,10 @@ let cmdline_actions =
   warning_options @
 (* Vericert.Interpreter mode *)
  [ Exact "-interp", Set option_interp;
-  Exact "-quiet", Unit (fun () -> Vericert.Interp.trace := 0);
-  Exact "-trace", Unit (fun () -> Vericert.Interp.trace := 2);
-  Exact "-random", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.Random);
-  Exact "-all", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.All)
+   Exact "-quiet", Unit (fun () -> Vericert.Interp.trace := 0);
+   Exact "-trace", Unit (fun () -> Vericert.Interp.trace := 2);
+   Exact "-random", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.Random);
+   Exact "-all", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.All)
  ]
 (* Optimization options *)
 (* -f options: come in -f and -fno- variants *)
diff --git a/src/Compiler.v b/src/Compiler.v
index 056e404..ff0938e 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -69,6 +69,7 @@ Require vericert.hls.RTLParFUgen.
 Require vericert.hls.HTLPargen.
 Require vericert.hls.Pipeline.
 Require vericert.hls.IfConversion.
+(*Require vericert.hls.PipelineOp.*)
 Require vericert.HLSOpts.
 Require vericert.hls.Memorygen.
 
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 3544f9d..bca8fb5 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -145,6 +145,7 @@ Extract Constant Compiler.print_Cminor => "PrintCminor.print_if".
 Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if".
 Extract Constant Compiler.print_RTL => "PrintRTL.print_if".
 Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if".
+Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if".
 Extract Constant Compiler.print_HTL => "PrintHTL.print_if".
 Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if".
 Extract Constant Compiler.print_LTL => "PrintLTL.print_if".
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index d5a99fc..f4552a5 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -28,19 +28,21 @@ Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.ValueInt.
-Require Import vericert.hls.AssocMap.
 Require Import vericert.hls.Array.
 Require Import vericert.hls.FunctionalUnits.
 Require vericert.hls.Verilog.
+Require Import AssocMap.
+Require Import ValueInt.
 
 Local Open Scope positive.
 
-(** The purpose of the hardware transfer language (HTL) is to create a more
+(*|
+The purpose of the hardware transfer language (HTL) is to create a more
 hardware-like layout that is still similar to the register transfer language
 (RTL) that it came from. The main change is that function calls become module
 instantiations and that we now describe a state machine instead of a
-control-flow graph. *)
+control-flow graph.
+|*)
 
 Local Open Scope assocmap.
 
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 373f704..b66a704 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -27,6 +27,7 @@ Require Import compcert.lib.Maps.
 Require Import vericert.common.Statemonad.
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.FunctionalUnits.
 Require Import vericert.hls.HTL.
 Require Import vericert.hls.Predicate.
 Require Import vericert.hls.RTLBlockInstr.
@@ -329,6 +330,30 @@ Definition check_address_parameter_signed (p : Z) : bool :=
 Definition check_address_parameter_unsigned (p : Z) : bool :=
   Z.leb p Integers.Ptrofs.max_unsigned.
 
+Lemma create_reg_state_incr:
+  forall s sz i,
+    st_incr s (mkstate
+         s.(st_st)
+         (Pos.succ (st_freshreg s))
+         (st_freshstate s)
+         (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
+         s.(st_arrdecls)
+         (st_datapath s)
+         (st_controllogic s)).
+Proof. constructor; simpl; auto with htlh. Qed.
+
+Definition create_reg (i : option io) (sz : nat) : mon reg :=
+  fun s => let r := s.(st_freshreg) in
+           OK r (mkstate
+                   s.(st_st)
+                   (Pos.succ r)
+                   (st_freshstate s)
+                   (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
+                   (st_arrdecls s)
+                   (st_datapath s)
+                   (st_controllogic s))
+              (create_reg_state_incr s sz i).
+
 Definition translate_eff_addressing (a: Op.addressing) (args: list reg)
   : mon expr :=
   match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)
@@ -367,10 +392,10 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   | Op.Omulimm n, r::nil => ret (boplit Vmul r n)
   | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs")
   | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu")
-  | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2)
-  | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2)
-  | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2)
-  | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2)
+  | Op.Odiv, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: div")
+  | Op.Odivu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: divu")
+  | Op.Omod, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mod")
+  | Op.Omodu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: modu")
   | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2)
   | Op.Oandimm n, r::nil => ret (boplit Vand r n)
   | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2)
@@ -470,30 +495,6 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
 Definition stack_correct (sz : Z) : bool :=
   (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
 
-Lemma create_reg_state_incr:
-  forall s sz i,
-    st_incr s (mkstate
-         s.(st_st)
-         (Pos.succ (st_freshreg s))
-         (st_freshstate s)
-         (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
-         s.(st_arrdecls)
-         (st_datapath s)
-         (st_controllogic s)).
-Proof. constructor; simpl; auto with htlh. Qed.
-
-Definition create_reg (i : option io) (sz : nat) : mon reg :=
-  fun s => let r := s.(st_freshreg) in
-           OK r (mkstate
-                   s.(st_st)
-                   (Pos.succ r)
-                   (st_freshstate s)
-                   (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
-                   (st_arrdecls s)
-                   (st_datapath s)
-                   (st_controllogic s))
-              (create_reg_state_incr s sz i).
-
 Lemma create_arr_state_incr:
   forall s sz ln i,
     st_incr s (mkstate
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index 3f4e513..b879c8d 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -32,6 +32,7 @@ Require Import vericert.hls.AssocMap.
 Require Import vericert.hls.HTL.
 Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.Verilog.
+Require Import vericert.hls.FunctionalUnits.
 
 #[local] Hint Resolve AssocMap.gempty : htlh.
 #[local] Hint Resolve AssocMap.gso : htlh.
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index 8746ba2..75d5321 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -31,6 +31,7 @@ Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.HTL.
 Require Import vericert.hls.HTLgen.
 Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.FunctionalUnits.
 
 #[local] Hint Resolve Maps.PTree.elements_keys_norepet : htlspec.
 #[local] Hint Resolve Maps.PTree.elements_correct : htlspec.
diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v
new file mode 100644
index 0000000..793b752
--- /dev/null
+++ b/src/hls/PipelineOp.v
@@ -0,0 +1,192 @@
+(*
+ * 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 Coq.Lists.List.
+
+Require Import compcert.backend.Registers.
+Require Import compcert.common.AST.
+Require Import compcert.common.Errors.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require Import compcert.verilog.Op.
+
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.RTLBlockInstr.
+Require Import vericert.hls.RTLPar.
+Require Import vericert.hls.FunctionalUnits.
+
+Import Option.Notation.
+
+Local Open Scope positive.
+
+Definition div_pos (il: nat * list nat) x :=
+  let (i, l) := il in
+  match x with
+  | RBop _ Odiv _ _ => (S i, i :: l)
+  | RBop _ Odivu _ _ => (S i, i :: l)
+  | RBop _ Omod _ _ => (S i, i :: l)
+  | RBop _ Omodu _ _ => (S i, i :: l)
+  | _ => (S i, l)
+  end.
+
+Definition div_pos_in_list (il: nat * list (nat * nat)) bb :=
+  let (i, l) := il in
+  let dp := snd (List.fold_left div_pos bb (0%nat, nil)) in
+  (S i, (List.map (fun x => (i, x)) dp) ++ l).
+
+Definition div_pos_in_block (il: nat * list (nat * nat * nat)) bb :=
+  let (i, l) := il in
+  let dp := snd (List.fold_left div_pos_in_list bb (0%nat, nil)) in
+  (S i, (List.map (fun (yx : nat * nat) => let (y, x) := yx in (i, y, x)) dp) ++ l).
+
+Definition find_divs (bb: bblock) :=
+  snd (List.fold_left div_pos_in_block bb.(bb_body) (0%nat, nil)).
+
+Fixpoint mapi' {A B: Type} (n: nat) (f: nat -> A -> B) (l: list A): list B :=
+  match l with
+  | nil => nil
+  | a :: b => f n a :: mapi' (S n) f b
+  end.
+
+Definition mapi {A B: Type} := @mapi' A B 0.
+
+Definition map_at {A: Type} (n: nat) (f: A -> A) (l: list A): list A :=
+  mapi (fun i il =>
+          if Nat.eqb n i
+          then f il
+          else il
+       ) l.
+
+Definition map_at_err {A: Type} (n: nat) (f: A -> A) (l: list A): option (list A) :=
+  if (Datatypes.length l <=? n)%nat
+  then None
+  else Some (map_at n f l).
+
+Definition replace_div' sdiv udiv (d: instr) :=
+  match d with
+  | RBop op Odiv args dst => RBpiped op sdiv args
+  | RBop op Odivu args dst => RBpiped op udiv args
+  | RBop op Omod args dst => RBpiped op sdiv args
+  | RBop op Omodu args dst => RBpiped op udiv args
+  | _ => d
+  end.
+
+Definition get_sdiv (fu: funct_unit) : option (reg * reg * reg) :=
+  match fu with
+  | SignedDiv s a b d _ => Some (a, b, d)
+  | _ => None
+  end.
+
+Definition get_udiv (fu: funct_unit) : option (reg * reg * reg) :=
+  match fu with
+  | UnsignedDiv s a b d _ => Some (a, b, d)
+  | _ => None
+  end.
+
+Definition get_smod (fu: funct_unit) : option (reg * reg * reg) :=
+  match fu with
+  | SignedDiv s a b _ d => Some (a, b, d)
+  | _ => None
+  end.
+
+Definition get_umod (fu: funct_unit) : option (reg * reg * reg) :=
+  match fu with
+  | UnsignedDiv s a b _ d => Some (a, b, d)
+  | _ => None
+  end.
+
+Definition bind3 {A B C D: Type}
+           (f: option (A * B * C))
+           (g: A -> B -> C -> option D) : option D :=
+  match f with
+  | Some (a, b, c) => g a b c
+  | None => None
+  end.
+
+Notation "'do' ( X , Y , Z ) <- A ; B" := (bind3 A (fun X Y Z => B))
+   (at level 200, X ident, Y ident, Z ident, A at level 100, B at level 200).
+
+Definition replace_div_error (fu: funct_units) (bb: bb) (loc: nat * nat * nat) :=
+  match loc with
+  | (z, y, x) =>
+    do sdiv <- fu.(avail_sdiv);
+    do udiv <- fu.(avail_udiv);
+    do sfu <- PTree.get sdiv fu.(avail_units);
+    do ufu <- PTree.get udiv fu.(avail_units);
+    do z' <- List.nth_error bb z;
+    do y' <- List.nth_error z' y;
+    do x' <- List.nth_error y' x;
+    let transf := map_at z (map_at y (map_at x (replace_div' sdiv udiv))) bb in
+    match x' with
+    | RBop op Odiv args dst =>
+      do (s1, s2, src) <- get_sdiv sfu;
+      map_at_err (z + 32)%nat (fun x => (RBassign op sdiv src dst :: nil) :: x) transf
+    | RBop op Odivu args dst =>
+      do (s1, s2, src) <- get_udiv ufu;
+      map_at_err (z + 32)%nat (fun x => (RBassign op sdiv src dst :: nil) :: x) transf
+    | RBop op Omod args dst =>
+      do (s1, s2, src) <- get_smod sfu;
+      map_at_err (z + 32)%nat (fun x => (RBassign op sdiv src dst :: nil) :: x) transf
+    | RBop op Omodu args dst =>
+      do (s1, s2, src) <- get_umod ufu;
+      map_at_err (z + 32)%nat (fun x => (RBassign op sdiv src dst :: nil) :: x) transf
+    | _ => None
+    end
+  end.
+
+Definition replace_div (fu: funct_units) (bb: bb) loc :=
+  match replace_div_error fu bb loc with
+  | Some bb' => bb'
+  | _ => bb
+  end.
+
+Definition transf_code (i: code * funct_units) (bbn: node * bblock) :=
+  let (c, fu) := i in
+  let (n, bb) := bbn in
+  let divs := find_divs bb in
+  match divs with
+  | nil => (PTree.set n bb c, fu)
+  | _ =>
+    (PTree.set n (mk_bblock (List.fold_left (replace_div fu) divs bb.(bb_body)) bb.(bb_exit)) c, fu)
+  end.
+
+Definition create_fu (r: reg) :=
+  let fu := PTree.set 2 (UnsignedDiv 32 (r+5) (r+6) (r+7) (r+8))
+      (PTree.set 1 (SignedDiv 32 (r+1) (r+2) (r+3) (r+4)) (PTree.empty _)) in
+  mk_avail_funct_units (Some 1) (Some 2) fu.
+
+Definition transf_function (f: function) : function :=
+  let fu := create_fu (max_reg_function f) in
+  let (c, fu') := List.fold_left transf_code
+                                (PTree.elements f.(fn_code))
+                                (PTree.empty bblock, fu) in
+  mkfunction
+    f.(fn_sig)
+    f.(fn_params)
+    f.(fn_stacksize)
+    c
+    fu'
+    f.(fn_entrypoint).
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.
diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml
index fbb26c5..46b001e 100644
--- a/src/hls/PrintVerilog.ml
+++ b/src/hls/PrintVerilog.ml
@@ -28,6 +28,7 @@ open Clflags
 open Printf
 
 open VericertClflags
+open FunctionalUnits
 
 module PMap = Map.Make (struct
   type t = P.t
@@ -152,9 +153,9 @@ let declarearr (t, _) =
 
 let print_io = function
   | Some Vinput -> "input", false
-  | Some Voutput -> "output reg", true
+  | Some Voutput -> "output logic", true
   | Some Vinout -> "inout", false
-  | None -> "reg", true
+  | None -> "logic", true
 
 let decl i = function
   | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)]
@@ -180,6 +181,20 @@ let rec intersperse c = function
 
 let make_io i io r = concat [indent i; io; " "; register r; ";\n"]
 
+(**let print_funct_units clk = function
+  | SignedDiv (stages, numer, denom, quot, rem) ->
+    sprintf ("div_signed #(.stages(%d)) divs(.clk(%s), " ^^
+             ".clken(1'b1), .numer(%s), .denom(%s), " ^^
+             ".quotient(%s), .remain(%s))\n")
+      (P.to_int stages)
+      (register clk) (register numer) (register denom) (register quot) (register rem)
+  | UnsignedDiv (stages, numer, denom, quot, rem) ->
+    sprintf ("div_unsigned #(.stages(%d)) divs(.clk(%s), " ^^
+             ".clken(1'b1), .numer(%s), .denom(%s), " ^^
+             ".quotient(%s), .remain(%s))\n")
+      (P.to_int stages)
+      (register clk) (register numer) (register denom) (register quot) (register rem)*)
+
 let compose f g x = g x |> f
 
 let testbench = "module testbench;
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 84fbcc3..94225fa 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -571,6 +571,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 +590,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 =
@@ -611,7 +625,7 @@ 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
+  let constrained_paths = List.filter (function (_, 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),
@@ -671,6 +685,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,16 +718,21 @@ 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 (fn, oc) = Filename.open_temp_file "vericert_" "_lp_solve" in
@@ -721,7 +741,7 @@ let solve_constraints constr =
 
   let res = Str.split (Str.regexp_string "\n") (read_process ("lp_solve " ^ fn))
             |> drop 3
-            |> List.fold_left parse_soln IMap.empty
+            |> List.fold_left parse_soln (IMap.empty, IMap.empty)
   in
   Sys.remove fn; res
 
@@ -765,20 +785,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 ->
@@ -787,6 +822,8 @@ let transf_rtlpar c c' (schedule : (int * int) list IMap.t) =
                                                |> List.map (fun y ->
                                                    TopoDFG.fold (fun i l -> snd i :: l) y []
                                                    |> List.rev))) body
+                                           (*|> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x [])
+                                           |> List.rev) body2*)
       in
       { bb_body = final_body2;
         bb_exit = ctrl_flow
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index cee1d60..3a2c81d 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -142,23 +142,30 @@ Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
 Inductive scl_decl : Type := VScalar (sz : nat).
 Inductive arr_decl : Type := VArray (sz : nat) (ln : nat).
 
-(** * Verilog AST
+(*|
+Verilog AST
+===========
 
 The Verilog AST is defined here, which is the target language of the
 compilation.
 
-** Value
+Value
+-----
 
 The Verilog [value] is a bitvector containg a size and the actual bitvector. In
 this case, the [Word.word] type is used as many theorems about that bitvector
-have already been proven. *)
+have already been proven.
+|*)
 
-(** ** Binary Operators
+(*|
+Binary Operators
+----------------
 
 These are the binary operations that can be represented in Verilog. Ideally,
 multiplication and division would be done by custom modules which could al so be
 scheduled properly. However, for now every Verilog operator is assumed to take
-one clock cycle. *)
+one clock cycle.
+|*)
 
 Inductive binop : Type :=
 | Vadd : binop  (** addition (binary [+]) *)
@@ -186,13 +193,19 @@ Inductive binop : Type :=
 | Vshru : binop. (** shift right unsigned ([>>]) *)
 (*| Vror : binop (** shift right unsigned ([>>]) *)*)
 
-(** ** Unary Operators *)
+(*|
+Unary Operators
+---------------
+|*)
 
 Inductive unop : Type :=
 | Vneg  (** negation ([-]) *)
 | Vnot. (** not operation [!] *)
 
-(** ** Expressions *)
+(*|
+Expressions
+-----------
+|*)
 
 Inductive expr : Type :=
 | Vlit : value -> expr
@@ -207,7 +220,10 @@ Inductive expr : Type :=
 Definition posToExpr (p : positive) : expr :=
   Vlit (posToValue p).
 
-(** ** Statements *)
+(*|
+Statements
+----------
+|*)
 
 Inductive stmnt : Type :=
 | Vskip : stmnt
@@ -220,14 +236,17 @@ with stmnt_expr_list : Type :=
 | Stmntnil : stmnt_expr_list
 | Stmntcons : expr -> stmnt -> stmnt_expr_list -> stmnt_expr_list.
 
-(** ** Edges
+(*|
+Edges
+-----
 
 These define when an always block should be triggered, for example if the always
 block should be triggered synchronously at the clock edge, or asynchronously for
 combinational logic.
 
 [edge] is not part of [stmnt] in this formalisation because is closer to the
-semantics that are used. *)
+semantics that are used.
+|*)
 
 Inductive edge : Type :=
 | Vposedge : reg -> edge
@@ -235,11 +254,14 @@ Inductive edge : Type :=
 | Valledge : edge
 | Voredge : edge -> edge -> edge.
 
-(** ** Module Items
+(*|
+Module Items
+------------
 
 Module items can either be declarations ([Vdecl]) or always blocks ([Valways]).
 The declarations are always register declarations as combinational logic can be
-done using combinational always block instead of continuous assignments. *)
+done using combinational always block instead of continuous assignments.
+|*)
 
 Inductive io : Type :=
 | Vinput : io
@@ -256,7 +278,8 @@ Inductive module_item : Type :=
 | Valways_ff : edge -> stmnt -> module_item
 | Valways_comb : edge -> stmnt -> module_item.
 
-(** The main module type containing all the important control signals
+(*|
+The main module type containing all the important control signals
 
 - [mod_start] If set, starts the computations in the module.
 - [mod_reset] If set, reset the state in the module.
@@ -265,7 +288,7 @@ Inductive module_item : Type :=
 - [mod_finish] Bit that is set if the result is ready.
 - [mod_return] The return value that was computed.
 - [mod_body] The body of the module, including the state machine.
-*)
+|*)
 
 Record module : Type := mkmodule {
   mod_start : reg;
@@ -285,15 +308,18 @@ Definition fundef := AST.fundef module.
 
 Definition program := AST.program fundef unit.
 
-(** Convert a [positive] to an expression directly, setting it to the right
-    size. *)
+(*|
+Convert a [positive] to an expression directly, setting it to the right size.
+|*)
 Definition posToLit (p : positive) : expr :=
   Vlit (posToValue p).
 
 Definition fext := unit.
 Definition fextclk := nat -> fext.
 
-(** ** State
+(*|
+State
+-----
 
 The [state] contains the following items:
 n
@@ -312,7 +338,8 @@ retrieved and set appropriately.
   Verilog, as the Verilog was generated by the RTL, which means that we have to
   make an assumption about how it looks.  In this case, that it contains state
   which determines which part of the Verilog is executed.  This is then the part
-  of the Verilog that should match with the RTL. *)
+  of the Verilog that should match with the RTL.
+|*)
 
 Inductive stackframe : Type :=
   Stackframe :
@@ -432,7 +459,9 @@ Definition handle_def {A : Type} (a : A) (val : option A)
 
 Local Open Scope error_monad_scope.
 
-(** Return the location of the lhs of an assignment. *)
+(*|
+Return the location of the lhs of an assignment.
+|*)
 
 Inductive location : Type :=
 | LocReg (_ : reg)