Rewrite a lot fixing scheduling of Gible

24 files changed, 374 insertions, 656 deletions

diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index e89ff86..f2e0fc3 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -65,9 +65,8 @@ let compile_c_file sourcename ifile ofile =
   set_dest Vericert.PrintClight.destination option_dclight ".light.c";
   set_dest Vericert.PrintCminor.destination option_dcminor ".cm";
   set_dest Vericert.PrintRTL.destination option_drtl ".rtl";
-  set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock";
-  set_dest Vericert.PrintRTLPar.destination option_drtlpar ".rtlpar";
-  set_dest Vericert.PrintRTLParFU.destination option_drtlparfu ".rtlparfu";
+  set_dest Vericert.PrintGibleSeq.destination option_dgblseq ".gblseq";
+  set_dest Vericert.PrintGiblePar.destination option_dgblpar ".gblpar";
   set_dest Vericert.PrintHTL.destination option_dhtl ".htl";
   set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
   set_dest Vericert.PrintLTL.destination option_dltl ".ltl";
@@ -266,7 +265,8 @@ HLS Optimisations:
   -dclight       Save generated Clight in <file>.light.c
   -dcminor       Save generated Cminor in <file>.cm
   -drtl          Save RTL at various optimization points in <file>.rtl.<n>
-  -drtlblock     Save RTLBlock <file>.rtlblock
+  -dgblseq       Save GibleSeq <file>.gblseq
+  -dgblpar       Save GiblePar <file>.gblpar
   -dhtl          Save HTL before Verilog generation <file>.htl
   -dltl          Save LTL after register allocation in <file>.ltl
   -dmach         Save generated Mach code in <file>.mach
@@ -392,9 +392,8 @@ let cmdline_actions =
   Exact "-dclight", Set option_dclight;
   Exact "-dcminor", Set option_dcminor;
   Exact "-drtl", Set option_drtl;
-  Exact "-drtlblock", Set option_drtlblock;
-  Exact "-drtlpar", Set option_drtlpar;
-  Exact "-drtlparfu", Set option_drtlparfu;
+  Exact "-dgblseq", Set option_dgblseq;
+  Exact "-dgblpar", Set option_dgblpar;
   Exact "-dhtl", Set option_dhtl;
   Exact "-dltl", Set option_dltl;
   Exact "-dalloctrace", Set option_dalloctrace;
@@ -407,9 +406,8 @@ let cmdline_actions =
     option_dclight := true;
     option_dcminor := true;
     option_drtl := true;
-    option_drtlblock := true;
-    option_drtlpar := true;
-    option_drtlparfu := true;
+    option_dgblseq := true;
+    option_dgblpar := true;
     option_dhtl := true;
     option_dltl := true;
     option_dalloctrace := true;
diff --git a/src/Compiler.v b/src/Compiler.v
index dc3b1c7..a0b3f24 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -62,8 +62,7 @@ Require vericert.hls.Veriloggenproof.
 Require vericert.hls.HTLgen.
 Require vericert.hls.GibleSeq.
 Require vericert.hls.GibleSeqgen.
-Require vericert.hls.RTLPargen.
-Require vericert.hls.RTLParFUgen.
+Require vericert.hls.GiblePargen.
 Require vericert.hls.HTLPargen.
 (*Require vericert.hls.Pipeline.*)
 Require vericert.hls.IfConversion.
@@ -84,9 +83,8 @@ intermediate steps in the compilation, such as ``print_RTL``, ``print_HTL`` and
 
 Parameter print_RTL: Z -> RTL.program -> unit.
 Parameter print_HTL: Z -> HTL.program -> unit.
-Parameter print_RTLBlock: Z -> RTLBlock.program -> unit.
-Parameter print_RTLPar: Z -> RTLPar.program -> unit.
-Parameter print_RTLParFU: Z -> RTLParFU.program -> unit.
+Parameter print_GibleSeq: Z -> GibleSeq.GibleSeq.program -> unit.
+Parameter print_GiblePar: Z -> GiblePar.GiblePar.program -> unit.
 
 Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
   let unused := printer prog in prog.
@@ -260,14 +258,12 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_RTL 6)
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 7)
-  @@@ RTLBlockgen.transl_program
-   @@ print (print_RTLBlock 0)
+  @@@ GibleSeqgen.transl_program
+   @@ print (print_GibleSeq 0)
    @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program
-   @@ print (print_RTLBlock 1)
-  @@@ RTLPargen.transl_program
-   @@ print (print_RTLPar 0)
-  @@@ RTLParFUgen.transl_program
-   @@ print (print_RTLParFU 0)
+   @@ print (print_GibleSeq 1)
+  @@@ GiblePargen.transl_program
+   @@ print (print_GiblePar 0)
   @@@ HTLPargen.transl_program
    @@ print (print_HTL 0)
    @@ Veriloggen.transl_program.
diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml
index 0402d49..9dccb53 100644
--- a/src/VericertClflags.ml
+++ b/src/VericertClflags.ml
@@ -4,8 +4,8 @@ let option_hls = ref true
 let option_debug_hls = ref false
 let option_initial = ref false
 let option_dhtl = ref false
-let option_drtlblock = ref false
-let option_drtlpar = ref false
+let option_dgblseq = ref false
+let option_dgblpar = ref false
 let option_drtlparfu = ref false
 let option_hls_schedule = ref false
 let option_fif_conv = ref false
diff --git a/src/bourdoncle/BourdoncleAux.ml b/src/bourdoncle/BourdoncleAux.ml
index a35004e..1ea4de6 100644
--- a/src/bourdoncle/BourdoncleAux.ml
+++ b/src/bourdoncle/BourdoncleAux.ml
@@ -4,8 +4,9 @@ open Camlcoq
 open BinNums
 open BinPos
 open Maps
-open RTLBlock
-open RTLBlockInstr
+open Gible
+open GibleSeq
+open GibleSeq
 open BourdoncleIterator
 module B = Bourdoncle
 
@@ -46,7 +47,6 @@ let rec get_exits = function
   | RBbuiltin (_,_,dst,j) -> [(int_of_positive j, Inop)]
   | RBcond (c,args,j,k) -> [(int_of_positive j, Inop);(int_of_positive k, Inop)]
   | RBjumptable (_,tbl) -> List.map (fun j -> (int_of_positive j, Inop)) tbl
-  | RBpred_cf (p, cf1, cf2) -> List.append (get_exits cf1) (get_exits cf2)
   | RBreturn _ -> []
 
 let build_cfg f =
@@ -55,7 +55,8 @@ let build_cfg f =
   (* nodes are between 1 and max+1 *)
   let succ = Array.make (max+1) [] in
   let _ = PTree.fold (fun () n ins ->
-			succ.(int_of_positive n) <- get_exits ins.bb_exit) f.fn_code () in
+			succ.(int_of_positive n) <- List.map (fun j -> (int_of_positive j, Inop))
+       (all_successors ins)) f.fn_code () in
     { entry = entry; succ = succ }
 
 let rec build_bourdoncle' (bl : bourdoncle list) : B.bourdoncle list =
@@ -65,7 +66,7 @@ let rec build_bourdoncle' (bl : bourdoncle list) : B.bourdoncle list =
     | (L ((I h) :: l, _)) :: r -> B.L (positive_of_int h, build_bourdoncle' l) :: (build_bourdoncle' r)
     | _ -> failwith "Assertion error: invalid bourdoncle ist"
 
-let build_bourdoncle'' (f : bb coq_function) : B.bourdoncle =
+let build_bourdoncle'' (f : coq_function) : B.bourdoncle =
   let cfg = build_cfg f in
   match build_bourdoncle' (get_bourdoncle cfg) with
     | [] -> failwith "assertion error: empty bourdoncle"
@@ -102,7 +103,7 @@ let build_order (b : B.bourdoncle) : coq_N PMap.t =
   let bo = build_order' (linearize b) (succ_pos N0) in
   (succ_pos N0, bo)
 
-let build_bourdoncle (f : bb coq_function) : (B.bourdoncle * coq_N PMap.t) =
+let build_bourdoncle (f : coq_function) : (B.bourdoncle * coq_N PMap.t) =
   let b = build_bourdoncle'' f in
   let bo = build_order b in
   (b, bo)
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 395ec47..88bb3e8 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -19,10 +19,10 @@
 From vericert Require
      Verilog
      Compiler
-     RTLBlockgen
-     RTLBlock
-     RTLPar
-     RTLBlockInstr
+     GibleSeqgen
+     GibleSeq
+     GiblePar
+     Gible
      HTLgen
      (*Pipeline*)
      HLSOpts
@@ -145,11 +145,9 @@ Extract Constant Compiler.print_Clight => "PrintClight.print_if".
 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_GibleSeq => "PrintGibleSeq.print_if".
+Extract Constant Compiler.print_GiblePar => "PrintGiblePar.print_if".
 Extract Constant Compiler.print_HTL => "PrintHTL.print_if".
-Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if".
-Extract Constant Compiler.print_RTLParFU => "PrintRTLParFU.print_if".
 Extract Constant Compiler.print_LTL => "PrintLTL.print_if".
 Extract Constant Compiler.print_Mach => "PrintMach.print_if".
 Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x".
@@ -184,8 +182,8 @@ Extract Inlined Constant Binary.round_mode => "fun _ -> assert false".
 Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false".
 
 (*Extract Constant Pipeline.pipeline => "pipelining.pipeline".*)
-Extract Constant RTLBlockgen.partition => "Partition.partition".
-Extract Constant RTLPargen.schedule => "Schedule.schedule_fn".
+Extract Constant GibleSeqgen.partition => "Partition.partition".
+Extract Constant GiblePargen.schedule => "Schedule.schedule_fn".
 
 (* Loop normalization *)
 Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle".
@@ -197,7 +195,7 @@ Cd "src/extraction".
 Separate Extraction
          Verilog.module vericert.Compiler.transf_hls
          vericert.Compiler.transf_hls_temp
-         RTLBlockgen.transl_program RTLBlockInstr.successors_instr
+         GibleSeqgen.transl_program Gible.successors_instr
          HTLgen.tbl_to_case_expr
          Predicate.sat_pred_simple
          Verilog.stmnt_to_list
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 9d310fb..ab0511f 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -29,11 +29,12 @@ Require Import compcert.lib.Maps.
 Require compcert.verilog.Op.
 
 Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.RTLBlock.
-Require Import vericert.hls.RTLPar.
-Require Import vericert.hls.RTLBlockInstr.
+Require Import vericert.hls.GibleSeq.
+Require Import vericert.hls.GiblePar.
+Require Import vericert.hls.Gible.
 Require Import vericert.hls.HashTree.
 Require Import vericert.hls.Predicate.
+Require Import vericert.common.DecEq.
 
 #[local] Open Scope positive.
 #[local] Open Scope pred_op.
@@ -65,121 +66,6 @@ Proof.
   decide equality; apply Pos.eq_dec.
 Defined.
 
-Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}.
-Proof.
-  decide equality.
-Defined.
-
-Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}.
-Proof.
-  generalize comparison_eq; intro.
-  generalize Int.eq_dec; intro.
-  generalize Int64.eq_dec; intro.
-  decide equality.
-Defined.
-
-Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}.
-Proof.
-  generalize Int.eq_dec; intro.
-  generalize AST.ident_eq; intro.
-  generalize Z.eq_dec; intro.
-  generalize Ptrofs.eq_dec; intro.
-  decide equality.
-Defined.
-
-Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}.
-Proof.
-  decide equality.
-Defined.
-
-Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}.
-Proof.
-  generalize Int.eq_dec; intro.
-  generalize Int64.eq_dec; intro.
-  generalize Float.eq_dec; intro.
-  generalize Float32.eq_dec; intro.
-  generalize AST.ident_eq; intro.
-  generalize condition_eq; intro.
-  generalize addressing_eq; intro.
-  generalize typ_eq; intro.
-  decide equality.
-Defined.
-
-Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}.
-Proof.
-  decide equality.
-Defined.
-
-Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}.
-Proof.
-  generalize typ_eq; intro.
-  decide equality.
-Defined.
-
-Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}.
-Proof.
-  generalize typ_eq; intro.
-  decide equality.
-Defined.
-
-Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}.
-Proof.
-  repeat decide equality.
-Defined.
-
-Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}.
-Proof.
-  generalize operation_eq; intro.
-  decide equality.
-Defined.
-
-Lemma list_reg_eq : forall (x y : list reg), {x = y} + {x <> y}.
-Proof.
-  generalize Pos.eq_dec; intros.
-  decide equality.
-Defined.
-
-Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}.
-Proof.
-  repeat decide equality.
-Defined.
-
-Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}.
-Proof.
-  generalize Pos.eq_dec; intro.
-  generalize typ_eq; intro.
-  generalize Int.eq_dec; intro.
-  generalize memory_chunk_eq; intro.
-  generalize addressing_eq; intro.
-  generalize operation_eq; intro.
-  generalize condition_eq; intro.
-  generalize signature_eq; intro.
-  generalize list_operation_eq; intro.
-  generalize list_reg_eq; intro.
-  generalize AST.ident_eq; intro.
-  repeat decide equality.
-Defined.
-
-Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}.
-Proof.
-  generalize Pos.eq_dec; intro.
-  generalize typ_eq; intro.
-  generalize Int.eq_dec; intro.
-  generalize Int64.eq_dec; intro.
-  generalize Float.eq_dec; intro.
-  generalize Float32.eq_dec; intro.
-  generalize Ptrofs.eq_dec; intro.
-  generalize memory_chunk_eq; intro.
-  generalize addressing_eq; intro.
-  generalize operation_eq; intro.
-  generalize condition_eq; intro.
-  generalize signature_eq; intro.
-  generalize list_operation_eq; intro.
-  generalize list_reg_eq; intro.
-  generalize AST.ident_eq; intro.
-  repeat decide equality.
-Defined.
-
 (*|
 We then create equality lemmas for a resource and a module to index resources
 uniquely.  The indexing is done by setting Mem to 1, whereas all other
@@ -945,8 +831,8 @@ Qed.*)
 
 Section CORRECT.
 
-  Definition fd := @fundef RTLBlock.bb.
-  Definition tfd := @fundef RTLPar.bb.
+  Definition fd := GibleSeq.fundef.
+  Definition tfd := GiblePar.fundef.
 
   Context (ictx: @ctx fd) (octx: @ctx tfd) (HSIM: similar ictx octx).
 
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index 22d25f8..e7378ea 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -68,7 +68,7 @@ These are the instructions that count as control-flow, and will be placed at the
 end of the basic blocks.
 |*)
 
-Inductive cf_instr : Type :=
+Variant cf_instr : Type :=
 | RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr
 | RBtailcall : signature -> reg + ident -> list reg -> cf_instr
 | RBbuiltin : external_function -> list (builtin_arg reg) ->
@@ -76,10 +76,9 @@ Inductive cf_instr : Type :=
 | RBcond : condition -> list reg -> node -> node -> cf_instr
 | RBjumptable : reg -> list node -> cf_instr
 | RBreturn : option reg -> cf_instr
-| RBgoto : node -> cf_instr
-| RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr.
+| RBgoto : node -> cf_instr.
 
-Inductive instr : Type :=
+Variant instr : Type :=
 | RBnop : instr
 | RBop :
   option pred_op -> operation -> list reg -> reg -> instr
@@ -96,7 +95,7 @@ Helper Functions
 ================
 |*)
 
-Fixpoint successors_instr (i : cf_instr) : list node :=
+Definition successors_instr (i : cf_instr) : list node :=
   match i with
   | RBcall sig ros args res s => s :: nil
   | RBtailcall sig ros args => nil
@@ -105,11 +104,9 @@ Fixpoint successors_instr (i : cf_instr) : list node :=
   | RBjumptable arg tbl => tbl
   | RBreturn optarg => nil
   | RBgoto n => n :: nil
-  | RBpred_cf p c1 c2 =>
-      concat (successors_instr c1 :: successors_instr c2 :: nil)
   end.
 
-Fixpoint max_reg_cfi (m : positive) (i : cf_instr) :=
+Definition max_reg_cfi (m : positive) (i : cf_instr) :=
   match i with
   | RBcall sig (inl r) args res s =>
       fold_left Pos.max args (Pos.max r (Pos.max res m))
@@ -127,7 +124,6 @@ Fixpoint max_reg_cfi (m : positive) (i : cf_instr) :=
   | RBreturn None => m
   | RBreturn (Some arg) => Pos.max arg m
   | RBgoto n => m
-  | RBpred_cf p c1 c2 => Pos.max (max_reg_cfi m c1) (max_reg_cfi m c2)
   end.
 
 Definition max_reg_instr (m: positive) (i: instr) :=
@@ -304,15 +300,12 @@ Top-Level Type Definitions
 Module Type BlockType.
 
   Parameter t: Type.
-
-  Section STEP.
-    Context {A B : Type}.
-    Parameter step: Genv.t A B -> val -> istate -> t -> istate -> Prop.
-  End STEP.
-
-  Parameter max_reg : positive -> node -> t -> positive.
-
+  Parameter foldl : forall A, (A -> instr -> A) -> t -> A -> A.
   Parameter length : t -> nat.
+  Parameter step: forall A B, Genv.t A B -> val -> istate -> t -> istate -> Prop.
+
+  Arguments step [A B].
+  Arguments foldl [A].
 
 End BlockType.
 
@@ -502,15 +495,7 @@ support if-conversion.
     | exec_RBgoto:
       forall s f sp pc rs pr m pc',
         step_cf_instr (State s f sp pc rs pr m)
-                      (RBgoto pc') E0 (State s f sp pc' rs pr m)
-    | exec_RBpred_cf:
-      forall s f sp pc rs pr m cf1 cf2 st' p t,
-        step_cf_instr
-          (State s f sp pc
-                 rs pr m) (if eval_predf pr p then cf1 else cf2) t st' ->
-        step_cf_instr
-          (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2)
-          t st'.
+                      (RBgoto pc') E0 (State s f sp pc' rs pr m).
 
 (*|
 Top-level step
@@ -579,9 +564,11 @@ type ~genv~ which was declared earlier.
   Definition semantics (p: program) :=
     Semantics step (initial_state p) final_state (Genv.globalenv p).
 
+  Definition max_reg_block (m: positive) (n: node) (i: B.t) := B.foldl max_reg_instr i m.
+
   Definition max_reg_function (f: function) :=
     Pos.max
-      (PTree.fold B.max_reg f.(fn_code) 1%positive)
+      (PTree.fold max_reg_block f.(fn_code) 1%positive)
       (fold_left Pos.max f.(fn_params) 1%positive).
 
   Definition max_pc_function (f: function) : positive :=
@@ -592,4 +579,12 @@ type ~genv~ which was declared earlier.
                         with Z.pos p => p | _ => 1 end))%positive)
       f.(fn_code) 1%positive.
 
+  Definition all_successors (b: B.t) : list node :=
+    B.foldl (fun ns i =>
+               match i with
+               | RBexit _ cf => successors_instr cf ++ ns
+               | _ => ns
+               end
+            ) b nil.
+
 End Gible.
diff --git a/src/hls/GiblePar.v b/src/hls/GiblePar.v
index 8eb06ae..9600d16 100644
--- a/src/hls/GiblePar.v
+++ b/src/hls/GiblePar.v
@@ -35,10 +35,17 @@ RTLBlock
 ========
 |*)
 
-Module BB <: BlockType.
+Module ParBB <: BlockType.
 
   Definition t := list (list (list instr)).
 
+  Definition foldl (A: Type) (f: A -> instr -> A) (bb : t) (m : A): A :=
+    fold_left
+      (fun x l => fold_left (fun x' l' => fold_left f l' x') l x)
+      bb m.
+
+  Definition length : t -> nat := @length (list (list instr)).
+
   Section RELSEM.
 
     Context {A B: Type} (ge: Genv.t A B).
@@ -63,13 +70,7 @@ function that can execute lists of things, given their execution rule.
 
   End RELSEM.
 
-  Definition max_reg (m : positive) (pc : node) (bb : t) :=
-    fold_left
-      (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x)
-      bb m.
-
-  Definition length : t -> nat := @length (list (list instr)).
-
-End BB.
+End ParBB.
 
-Module GiblePar := Gible(BB).
+Module GiblePar := Gible(ParBB).
+Export GiblePar.
diff --git a/src/hls/RTLPargen.v b/src/hls/GiblePargen.v
index d425049..37273b4 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/GiblePargen.v
@@ -27,11 +27,12 @@ Require Import compcert.lib.Maps.
 Require compcert.verilog.Op.
 
 Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.RTLBlock.
-Require Import vericert.hls.RTLPar.
-Require Import vericert.hls.RTLBlockInstr.
+Require Import vericert.hls.GibleSeq.
+Require Import vericert.hls.GiblePar.
+Require Import vericert.hls.Gible.
 Require Import vericert.hls.Predicate.
 Require Import vericert.hls.Abstr.
+Require Import vericert.common.DecEq.
 Import NE.NonEmptyNotation.
 
 #[local] Open Scope positive.
@@ -166,37 +167,41 @@ This is done by multiplying the predicates together, and assigning the negation
 of the expression to the other predicates.
 |*)
 
-Definition update (f : forest) (i : instr) : forest :=
+Definition forest_state : Type := forest * list (cf_instr * option pred_op * forest).
+
+Definition update (flist : forest_state) (i : instr): forest_state :=
+  let (f, fl) := flist in
   match i with
-  | RBnop => f
+  | RBnop => flist
   | RBop p op rl r =>
-    f # (Reg r) <-
+    (f # (Reg r) <-
     (app_predicated p
        (f # (Reg r))
-       (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f))))
+       (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f)))), fl)
   | RBload p chunk addr rl r =>
-    f # (Reg r) <-
+    (f # (Reg r) <-
       (app_predicated p
          (f # (Reg r))
          (map_predicated
             (map_predicated (pred_ret (Eload chunk addr))
                             (merge (list_translation rl f)))
-            (f # Mem)))
+            (f # Mem))), fl)
   | RBstore p chunk addr rl r =>
-    f # Mem <-
+    (f # Mem <-
       (app_predicated p
          (f # Mem)
          (map_predicated
             (map_predicated
                (predicated_apply2 (map_predicated (pred_ret Estore)
                                                   (f # (Reg r))) chunk addr)
-               (merge (list_translation rl f))) (f # Mem)))
+               (merge (list_translation rl f))) (f # Mem))), fl)
   | RBsetpred p' c args p =>
-    f # (Pred p) <-
+    (f # (Pred p) <-
     (app_predicated p'
        (f # (Pred p))
        (map_predicated (pred_ret (Esetpred c))
-                       (merge (list_translation args f))))
+                       (merge (list_translation args f)))), fl)
+  | RBexit p c => (f, (c, p, f) :: fl)
   end.
 
 (*|
@@ -207,7 +212,7 @@ code than in the RTLBlock code.
 Get a sequence from the basic block.
 |*)
 
-Fixpoint abstract_sequence (f : forest) (b : list instr) : forest :=
+Fixpoint abstract_sequence (f : forest_state) (b : list instr) : forest_state :=
   match b with
   | nil => f
   | i :: l => abstract_sequence (update f i) l
@@ -227,7 +232,7 @@ We define the top-level oracle that will check if two basic blocks are
 equivalent after a scheduling transformation.
 |*)
 
-Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool :=
+Definition empty_trees (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
   match bb with
   | nil =>
     match bbt with
@@ -237,11 +242,10 @@ Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool :=
   | _ => true
   end.
 
-Definition schedule_oracle (bb: RTLBlock.bblock) (bbt: RTLPar.bblock) : bool :=
-  check (abstract_sequence empty (bb_body bb))
-        (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).
+Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
+  check (fst (abstract_sequence (empty, nil) bb))
+        (fst (abstract_sequence (empty, nil) (concat (concat bbt)))) &&
+  empty_trees bb bbt.
 
 Definition check_scheduled_trees := beq2 schedule_oracle.
 
@@ -271,22 +275,22 @@ Top-level Functions
 ===================
 |*)
 
-Parameter schedule : RTLBlock.function -> RTLPar.function.
+Parameter schedule : GibleSeq.function -> GiblePar.function.
 
-Definition transl_function (f: RTLBlock.function)
-  : Errors.res RTLPar.function :=
+Definition transl_function (f: GibleSeq.function)
+  : Errors.res GiblePar.function :=
   let tfcode := fn_code (schedule f) in
-  if check_scheduled_trees f.(fn_code) tfcode then
-    Errors.OK (mkfunction f.(fn_sig)
-                          f.(fn_params)
-                          f.(fn_stacksize)
+  if check_scheduled_trees f.(GibleSeq.fn_code) tfcode then
+    Errors.OK (mkfunction f.(GibleSeq.fn_sig)
+                          f.(GibleSeq.fn_params)
+                          f.(GibleSeq.fn_stacksize)
                           tfcode
-                          f.(fn_entrypoint))
+                          f.(GibleSeq.fn_entrypoint))
   else
     Errors.Error
       (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").
 
 Definition transl_fundef := transf_partial_fundef transl_function.
 
-Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program :=
+Definition transl_program (p : GibleSeq.program) : Errors.res GiblePar.program :=
   transform_partial_program transl_fundef p.
diff --git a/src/hls/RTLPargenproof.v b/src/hls/GiblePargenproof.v
index f975601..2abbea4 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -26,10 +26,10 @@ Require Import compcert.common.Values.
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.RTLBlock.
-Require Import vericert.hls.RTLPar.
-Require Import vericert.hls.RTLBlockInstr.
-Require Import vericert.hls.RTLPargen.
+Require Import vericert.hls.GibleSeq.
+Require Import vericert.hls.GiblePar.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GiblePargen.
 Require Import vericert.hls.Predicate.
 Require Import vericert.hls.Abstr.
 
@@ -89,7 +89,7 @@ Proof. induction l; crush. Qed.
 Lemma check_dest_l_dec i r : {check_dest_l i r = true} + {check_dest_l i r = false}.
 Proof. destruct (check_dest_l i r); tauto. Qed.
 
-Lemma check_dest_update :
+(*Lemma check_dest_update :
   forall f i r,
   check_dest i r = false ->
   (update f i) # (Reg r) = f # (Reg r).
@@ -1145,3 +1145,4 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
   Qed.
 
 End CORRECTNESS.
+*)
diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v
index 1ba28bc..9444f28 100644
--- a/src/hls/GibleSeq.v
+++ b/src/hls/GibleSeq.v
@@ -36,13 +36,13 @@ RTLBlock
 ========
 |*)
 
-Module BB <: BlockType.
+Module SeqBB <: BlockType.
 
   Definition t := list instr.
 
-  Section RELSEM.
+  Definition foldl {A: Type}: (A -> instr -> A) -> t -> A -> A := @fold_left A instr.
 
-    Context {A B: Type} (ge: Genv.t A B).
+  Definition length : t -> nat := @length instr.
 
 (*|
 Instruction list step
@@ -56,16 +56,9 @@ This is simply using the high-level function ``step_list``, which is a general
 function that can execute lists of things, given their execution rule.
 |*)
 
-    Definition step := step_list (step_instr ge).
-
-  End RELSEM.
-
-  Definition max_reg (m : positive) (n: node) (i : t) : positive :=
-    fold_left max_reg_instr i m.
-
-  Definition length : t -> nat := @length instr.
+  Definition step {A B: Type} (ge: Genv.t A B) := step_list (step_instr ge).
 
-End BB.
+End SeqBB.
 
-Module GibleSeq := Gible(BB).
+Module GibleSeq := Gible(SeqBB).
 Export GibleSeq.
diff --git a/src/hls/GibleSeqgen.v b/src/hls/GibleSeqgen.v
index 8d52339..31dabf8 100644
--- a/src/hls/GibleSeqgen.v
+++ b/src/hls/GibleSeqgen.v
@@ -42,7 +42,7 @@ Definition check_valid_node (tc: code) (e: node) :=
   | _ => false
   end.
 
-Fixpoint check_code (c: RTL.code) (tc: code) (pc: node) (b: BB.t) :=
+Fixpoint check_code (c: RTL.code) (tc: code) (pc: node) (b: SeqBB.t) :=
   match c ! pc, b with
   | Some (RTL.Inop pc'), RBnop :: (_ :: _ :: _) as b' =>
       check_code c tc pc' b'
diff --git a/src/hls/GibleSeqgenproof.v b/src/hls/GibleSeqgenproof.v
index 55b25d1..8fd859b 100644
--- a/src/hls/GibleSeqgenproof.v
+++ b/src/hls/GibleSeqgenproof.v
@@ -104,7 +104,7 @@ finding is actually done at that higher level already.
 
   Definition valid_succ (tc: code) (pc: node) : Prop := exists b, tc ! pc = Some b.
 
-  Inductive match_block (c: RTL.code) (tc: code) (pc: node): BB.t -> Prop :=
+  Inductive match_block (c: RTL.code) (tc: code) (pc: node): SeqBB.t -> Prop :=
   (*
    * Basic Block Instructions
    *)
@@ -195,9 +195,9 @@ the basic block.
 
   Definition sem_extrap f pc sp in_s in_s' block :=
     forall out_s block2,
-      BB.step tge sp in_s block out_s ->
+      SeqBB.step tge sp in_s block out_s ->
       f.(fn_code) ! pc = Some block2 ->
-      BB.step tge sp in_s' block2 out_s.
+      SeqBB.step tge sp in_s' block2 out_s.
 
   Lemma match_block_exists_instr :
     forall c tc pc a,
@@ -224,7 +224,7 @@ proof inside of the ``match_states`` that shows that the execution from the
 whole execution (in one big step) of the basic block.
 |*)
 
-  Variant match_states : option BB.t -> RTL.state -> state -> Prop :=
+  Variant match_states : option SeqBB.t -> RTL.state -> state -> Prop :=
     | match_state :
       forall stk stk' f tf sp pc rs m pc0 b rs0 m0
         (TF: transl_function f = OK tf)
@@ -282,7 +282,7 @@ whole execution (in one big step) of the basic block.
     inv H; auto.
   Qed.
 
-  Definition measure (b: option BB.t): nat :=
+  Definition measure (b: option SeqBB.t): nat :=
     match b with
     | None => 0
     | Some b' => 1 + length b'
@@ -528,7 +528,7 @@ whole execution (in one big step) of the basic block.
       (RTL.fn_code f) ! pc = Some (RTL.Iop op args res pc') ->
       Op.eval_operation ge sp op rs ## args m = Some v ->
       transl_function f = OK tf ->
-      (forall (pc0 : positive) (b : BB.t),
+      (forall (pc0 : positive) (b : SeqBB.t),
           (fn_code tf) ! pc0 = Some b -> match_block (RTL.fn_code f) (fn_code tf) pc0 b) ->
       Forall2 match_stackframe s stk' ->
       star RTL.step ge (RTL.State s f sp pc1 rs1 m1) E0 (RTL.State s f sp pc rs m) ->
@@ -737,7 +737,7 @@ whole execution (in one big step) of the basic block.
       forall b s2,
         match_states b (RTL.State s f (Vptr stk Integers.Ptrofs.zero) pc rs m) s2 ->
         exists b' s2',
-          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option SeqBB.t) measure b' b) /\
             match_states b' (RTL.Callstate s fd rs ## args m') s2'.
   Proof.
     intros * H H0 H1 H2.
@@ -802,7 +802,7 @@ whole execution (in one big step) of the basic block.
       forall b s2,
         match_states b (RTL.Callstate s (Internal f) args m) s2 ->
         exists b' s2',
-          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option SeqBB.t) measure b' b) /\
             match_states b'
                          (RTL.State s f (Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) (RTL.init_regs args (RTL.fn_params f)) m') s2'.
   Proof.
@@ -845,7 +845,7 @@ whole execution (in one big step) of the basic block.
       forall b s2,
         match_states b (RTL.Callstate s (External ef) args m) s2 ->
         exists b' s2',
-          (plus step tge s2 t s2' \/ star step tge s2 t s2' /\ ltof (option BB.t) measure b' b) /\
+          (plus step tge s2 t s2' \/ star step tge s2 t s2' /\ ltof (option SeqBB.t) measure b' b) /\
             match_states b' (RTL.Returnstate s res m') s2'.
   Proof.
     intros * H.
@@ -861,7 +861,7 @@ whole execution (in one big step) of the basic block.
     forall res f sp pc rs s vres m b s2,
       match_states b (RTL.Returnstate (RTL.Stackframe res f sp pc rs :: s) vres m) s2 ->
       exists b' s2',
-        (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
+        (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option SeqBB.t) measure b' b) /\
           match_states b' (RTL.State s f sp pc rs # res <- vres m) s2'.
   Proof.
     intros.
@@ -884,7 +884,7 @@ whole execution (in one big step) of the basic block.
       forall b0 s2,
         match_states b0 (RTL.State s f sp pc rs m) s2 ->
         exists b' s2',
-          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b0) /\
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option SeqBB.t) measure b' b0) /\
             match_states b' (RTL.State s f sp pc' rs m) s2'.
   Proof.
     intros * H H0 H1.
@@ -920,7 +920,7 @@ whole execution (in one big step) of the basic block.
       forall b s2,
         match_states b (RTL.State s f sp pc rs m) s2 ->
         exists b' s2',
-          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option SeqBB.t) measure b' b) /\
             match_states b' (RTL.State s f sp pc' rs m) s2'.
   Proof.
     intros * H H0 H1.
@@ -947,7 +947,7 @@ whole execution (in one big step) of the basic block.
       forall b s2,
         match_states b (RTL.State s f (Vptr stk Integers.Ptrofs.zero) pc rs m) s2 ->
         exists b' s2',
-          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option SeqBB.t) measure b' b) /\
             match_states b' (RTL.Returnstate s (regmap_optget or Vundef rs) m') s2'.
   Proof.
     intros * H H0.
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 8960ef9..a058536 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -30,8 +30,8 @@ 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.
-Require Import vericert.hls.RTLParFU.
+Require Import vericert.hls.GiblePar.
+Require Import vericert.hls.Gible.
 Require Import vericert.hls.FunctionalUnits.
 Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.Verilog.
@@ -685,20 +685,26 @@ Definition translate_predicate (a : assignment)
     ret (a dst (Vternary (pred_expr preg pos) e dst))
   end.
 
-Definition translate_inst a (fin rtrn preg : reg) (n : node) (i : instr)
-  : mon stmnt :=
-  match i with
-  | FUnop =>
-    ret Vskip
-  | FUop p op args dst =>
-    do instr <- translate_instr op args;
-    do _ <- declare_reg None dst 32;
-    translate_predicate a preg p (Vvar dst) instr
-  | FUread p1 p2 r => ret Vskip
-  | FUwrite p1 p2 r => ret Vskip
-  | FUsetpred _ c args p =>
-    do cond <- translate_condition c args;
-    ret (a (pred_expr preg (Plit (true, p))) cond)
+Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
+           (args : list reg) (stack : reg) : mon expr :=
+  match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
+  | Mint32, Op.Aindexed off, r1::nil =>
+    if (check_address_parameter_signed off)
+    then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4))))
+    else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")
+  | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
+    then ret (Vvari stack
+                    (Vbinop Vdivu
+                            (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
+                            (Vlit (ZToValue 4))))
+    else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")
+  | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
+    let a := Integers.Ptrofs.unsigned a in
+    if (check_address_parameter_unsigned a)
+    then ret (Vvari stack (Vlit (ZToValue (a / 4))))
+    else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset")
+  | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing")
   end.
 
 Lemma create_new_state_state_incr:
@@ -726,28 +732,17 @@ Definition create_new_state (p: node): mon node :=
                 s.(st_controllogic))
               (create_new_state_state_incr s p).
 
-Definition translate_inst_list (fin rtrn preg: reg) (ni : node * node * list (list instr)) :=
-  match ni with
-  | (n, p, li) =>
-    do _ <- collectlist
-          (fun l =>
-             do stmnt <- translate_inst Vblock fin rtrn preg n l;
-             add_data_instr n stmnt) (concat li);
-    do st <- get;
-    add_control_instr n (state_goto st.(st_st) p)
-  end.
-
-Fixpoint translate_cfi' (fin rtrn preg: reg) (cfi: cf_instr)
+Definition translate_cfi' (fin rtrn preg: reg) (cfi: cf_instr)
   : mon (stmnt * stmnt) :=
   match cfi with
-  | FUgoto n' =>
+  | RBgoto n' =>
     do st <- get;
     ret (Vskip, state_goto st.(st_st) n')
-  | FUcond c args n1 n2 =>
+  | RBcond c args n1 n2 =>
     do st <- get;
     do e <- translate_condition c args;
     ret (Vskip, state_cond st.(st_st) e n1 n2)
-  | FUreturn r =>
+  | RBreturn r =>
     match r with
     | Some r' =>
       ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))),
@@ -756,18 +751,14 @@ Fixpoint translate_cfi' (fin rtrn preg: reg) (cfi: cf_instr)
       ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))),
            Vskip)
     end
-  | FUpred_cf p c1 c2 =>
-    do (tc1s, tc1c) <- translate_cfi' fin rtrn preg c1;
-    do (tc2s, tc2c) <- translate_cfi' fin rtrn preg c2;
-    ret ((Vcond (pred_expr preg p) tc1s tc2s), (Vcond (pred_expr preg p) tc1c tc2c))
-  | FUjumptable r tbl =>
+  | RBjumptable r tbl =>
     do s <- get;
     ret (Vskip, Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr s.(st_st) tbl)) (Some Vskip))
-  | FUcall sig ri rl r n =>
+  | RBcall sig ri rl r n =>
     error (Errors.msg "HTLPargen: RPcall not supported.")
-  | FUtailcall sig ri lr =>
+  | RBtailcall sig ri lr =>
     error (Errors.msg "HTLPargen: RPtailcall not supported.")
-  | FUbuiltin e lb b n =>
+  | RBbuiltin e lb b n =>
     error (Errors.msg "HTLPargen: RPbuildin not supported.")
   end.
 
@@ -778,17 +769,50 @@ Definition translate_cfi (fin rtrn preg: reg) (ni: node * cf_instr)
   do _ <- add_control_instr n c;
   add_data_instr n s.
 
-Definition transf_bblock (fin rtrn preg: reg) (ni : node * bblock)
+Definition translate_inst a (fin rtrn preg stack : reg) (n : node) (i : instr) :=
+  match i with
+  | RBnop =>
+    do stmnt <- ret Vskip;
+    add_data_instr n stmnt
+  | RBop p op args dst =>
+    do instr <- translate_instr op args;
+    do _ <- declare_reg None dst 32;
+    do stmnt <- translate_predicate a preg p (Vvar dst) instr;
+    add_data_instr n stmnt
+  | RBload p mem addr args dst =>
+      do src <- translate_arr_access mem addr args stack;
+      do _ <- declare_reg None dst 32;
+      do stmnt <- translate_predicate a preg p (Vvar dst) src;
+      add_data_instr n stmnt
+  | RBstore p mem addr args src =>
+      do dst <- translate_arr_access mem addr args stack;
+      do stmnt <- translate_predicate a preg p dst (Vvar src);
+      add_data_instr n stmnt
+  | RBsetpred _ c args p =>
+    do cond <- translate_condition c args;
+    do stmnt <- ret (a (pred_expr preg (Plit (true, p))) cond);
+    add_data_instr n stmnt
+  | RBexit p cf =>
+      translate_cfi fin rtrn preg (n, cf)
+  end.
+
+Definition translate_inst_list (fin rtrn preg stack: reg) (ni : node * node * list (list instr)) :=
+  match ni with
+  | (n, p, li) =>
+    do _ <- collectlist
+          (fun l => translate_inst Vblock fin rtrn preg stack n l) (concat li);
+    do st <- get;
+    add_control_instr n (state_goto st.(st_st) p)
+  end.
+
+Definition transf_bblock (fin rtrn preg stack: reg) (ni : node * ParBB.t)
   : mon unit :=
   let (n, bb) := ni in
-  do nstate <- create_new_state ((poslength bb.(bb_body)))%positive;
-  do _ <- collectlist (translate_inst_list fin rtrn preg)
-                      (prange n (nstate + poslength bb.(bb_body) - 1)%positive
-                                  bb.(bb_body));
-  match bb.(bb_body) with
-  | nil => translate_cfi fin rtrn preg (n, bb.(bb_exit))
-  | _ => translate_cfi fin rtrn preg (nstate, bb.(bb_exit))
-  end.
+  do nstate <- create_new_state ((poslength bb))%positive;
+  do _ <- collectlist (translate_inst_list fin rtrn preg stack)
+                      (prange n (nstate + poslength bb - 1)%positive
+                                  bb);
+  add_control_instr nstate Vskip.
 
 (*Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}.
   refine (match bool_dec ((a <? b) && (b <? c) && (c <? d)
@@ -821,41 +845,43 @@ Definition transf_module (f: function) : mon HTL.module :=
     do fin <- create_reg (Some Voutput) 1;
     do rtrn <- create_reg (Some Voutput) 32;
     do preg <- create_reg None 32;
-    do _ <- collectlist (transf_bblock fin rtrn preg)
+    do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
+    do _ <- collectlist (transf_bblock fin rtrn preg stack)
                         (Maps.PTree.elements f.(fn_code));
     do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32)
                         f.(fn_params);
     do start <- create_reg (Some Vinput) 1;
     do rst <- create_reg (Some Vinput) 1;
     do clk <- create_reg (Some Vinput) 1;
-    match get_ram 0 (fn_funct_units f) with
-    | Some (_, r) =>
-        do _ <- declare_ram r;
-        do current_state <- get;
-        match zle (Z.pos (max_pc_map current_state.(st_datapath)))
-                  Integers.Int.max_unsigned,
-          zle (Z.pos (max_pc_map current_state.(st_controllogic)))
+    do r_en <- create_reg None 1;
+    do r_u_en <- create_reg None 1;
+    do r_addr <- create_reg None 32;
+    do r_wr_en <- create_reg None 1;
+    do r_d_in <- create_reg None 32;
+    do r_d_out <- create_reg None 32;
+    do current_state <- get;
+    match zle (Z.pos (max_pc_map current_state.(st_datapath)))
               Integers.Int.max_unsigned,
-          max_list_dec (fn_params f) (st_st current_state)
-        with
-        | left LEDATA, left LECTRL, left WFPARAMS =>
-          ret (HTL.mkmodule
-             f.(fn_params)
-             current_state.(st_datapath)
-             current_state.(st_controllogic)
-             f.(fn_entrypoint)
-             current_state.(st_st)
-             fin
-             rtrn
-             start
-             rst
-             clk
-             current_state.(st_scldecls)
-             current_state.(st_arrdecls)
-             r)
-        | _, _, _=> error (Errors.msg "More than 2^32 states.")
-        end
-    | _ => error (Errors.msg "Stack RAM not found.")
+      zle (Z.pos (max_pc_map current_state.(st_controllogic)))
+          Integers.Int.max_unsigned,
+      max_list_dec (fn_params f) (st_st current_state)
+    with
+    | left LEDATA, left LECTRL, left WFPARAMS =>
+        ret (HTL.mkmodule
+        f.(fn_params)
+        current_state.(st_datapath)
+        current_state.(st_controllogic)
+        f.(fn_entrypoint)
+        current_state.(st_st)
+        fin
+        rtrn
+        start
+        rst
+        clk
+        current_state.(st_scldecls)
+        current_state.(st_arrdecls)
+        (mk_ram stack_len stack r_en r_u_en r_addr r_wr_en r_d_in r_d_out))
+    | _, _, _=> error (Errors.msg "More than 2^32 states.")
     end
   else error (Errors.msg "Stack size misalignment.").
 
@@ -874,7 +900,7 @@ Definition transl_module (f : function) : Errors.res HTL.module :=
 
 Definition transl_fundef := transf_partial_fundef transl_module.
 
-Definition main_is_internal (p : RTLParFU.program) : bool :=
+Definition main_is_internal (p : GiblePar.program) : bool :=
   let ge := Globalenvs.Genv.globalenv p in
   match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with
   | Some b =>
@@ -885,7 +911,7 @@ Definition main_is_internal (p : RTLParFU.program) : bool :=
   | _ => false
   end.
 
-Definition transl_program (p : RTLParFU.program) : Errors.res HTL.program :=
+Definition transl_program (p : GiblePar.program) : Errors.res HTL.program :=
   if main_is_internal p
   then transform_partial_program transl_fundef p
   else Errors.Error (Errors.msg "Main function is not Internal.").
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 4e62a68..1825ee7 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -23,8 +23,8 @@ Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.RTLBlockInstr.
-Require Import vericert.hls.RTLBlock.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GibleSeq.
 Require Import vericert.hls.Predicate.
 Require Import vericert.bourdoncle.Bourdoncle.
 
@@ -52,30 +52,39 @@ Definition map_if_convert (p: pred_op) (i: instr) :=
     RBload (Some (combine_pred p p')) chunk addr args dst
   | RBstore p' chunk addr args src =>
     RBstore (Some (combine_pred p p')) chunk addr args src
+  | RBsetpred p' c l pred =>
+      RBsetpred (Some (combine_pred p p')) c l pred
+  | RBexit p' cf => RBexit (Some (combine_pred p p')) cf
   | _ => i
   end.
 
-Definition if_convert_block (c: code) (p: predicate) (bb: bblock) : bblock :=
-  let cfi := bb_exit bb in
-  match cfi with
-  | RBcond cond args n1 n2 =>
+Definition get_unconditional_exit (bb: SeqBB.t) := List.nth_error bb (length bb - 1).
+
+Definition if_convert_block (c: code) (p: predicate) (bb: SeqBB.t) : SeqBB.t :=
+  match get_unconditional_exit bb with
+  | Some (RBexit None (RBcond cond args n1 n2)) =>
     match PTree.get n1 c, PTree.get n2 c with
     | Some bb1, Some bb2 =>
-      let bb1' := List.map (map_if_convert (Plit (true, p))) bb1.(bb_body) in
-      let bb2' := List.map (map_if_convert (Plit (false, p))) bb2.(bb_body) in
-      mk_bblock (List.concat (bb.(bb_body) :: ((RBsetpred None cond args p) :: bb1') :: bb2' :: nil))
-                (RBpred_cf (Plit (true, p)) bb1.(bb_exit) bb2.(bb_exit))
+      let bb1' := List.map (map_if_convert (Plit (true, p))) bb1 in
+      let bb2' := List.map (map_if_convert (Plit (false, p))) bb2 in
+      List.concat (bb :: ((RBsetpred None cond args p) :: bb1') :: bb2' :: nil)
     | _, _ => bb
     end
   | _ => bb
   end.
 
-Definition is_cond_cfi (cfi: cf_instr) :=
+Definition is_cond_cfi' (cfi: cf_instr) :=
   match cfi with
   | RBcond _ _ _ _ => true
   | _ => false
   end.
 
+Definition is_cond_cfi (b: SeqBB.t) :=
+  match get_unconditional_exit b with
+  | Some (RBexit None (RBcond _ _ _ _)) => true
+  | _ => false
+  end.
+
 Fixpoint any {A: Type} (f: A -> bool) (a: list A) :=
   match a with
   | x :: xs => f x || any f xs
@@ -88,9 +97,9 @@ Fixpoint all {A: Type} (f: A -> bool) (a: list A) :=
   | nil => true
   end.
 
-Definition find_backedge (nb: node * bblock) :=
+Definition find_backedge (nb: node * SeqBB.t) :=
   let (n, b) := nb in
-  let succs := successors_instr b.(bb_exit) in
+  let succs := all_successors b in
   filter (fun x => Pos.ltb n x) succs.
 
 Definition find_all_backedges (c: code) : list node :=
@@ -108,29 +117,31 @@ Fixpoint get_loops (b: bourdoncle): list node :=
 Definition is_loop (b: list node) (n: node) :=
   any (Pos.eqb n) b.
 
-Definition is_flat_cfi (n: cf_instr) :=
+Definition is_flat_cfi' (n: cf_instr) :=
   match n with
   | RBcond _ _ _ _ => false
   | RBjumptable _ _ => false
-  | RBpred_cf _ _ _ => false
   | _ => true
   end.
 
+Definition is_flat_cfi (n: SeqBB.t) :=
+  (length (all_successors n) =? 1)%nat.
+
 Definition is_flat (c: code) (succ: node) :=
   match c ! succ with
-  | Some bblock => is_flat_cfi bblock.(bb_exit)
+  | Some bblock => is_flat_cfi bblock
   | None => false
   end.
 
-Definition find_blocks_with_cond ep (b: list node) (c: code) : list (node * bblock) :=
+Definition find_blocks_with_cond ep (b: list node) (c: code) : list (node * SeqBB.t) :=
   let backedges := find_all_backedges c in
-  List.filter (fun x => is_cond_cfi (snd x).(bb_exit) &&
+  List.filter (fun x => is_cond_cfi (snd x) &&
                         (negb (is_loop b (fst x)) || Pos.eqb (fst x) ep) &&
                         all (fun x' => is_flat c x')
-                            (successors_instr (snd x).(bb_exit))
+                            (all_successors (snd x))
               ) (PTree.elements c).
 
-Definition if_convert_code (p: nat * code) (nb: node * bblock) :=
+Definition if_convert_code (p: nat * code) (nb: node * SeqBB.t) :=
   let nbb := if_convert_block (snd p) (Pos.of_nat (fst p)) (snd nb) in
   (S (fst p), PTree.set (fst nb) nbb (snd p)).
 
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
index 4e699e6..3b7cdd7 100644
--- a/src/hls/Partition.ml
+++ b/src/hls/Partition.ml
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(* [[file:../../docs/basic-block-generation.org::partition-main][partition-main]] *)
 open Printf
 open Clflags
 open Camlcoq
@@ -26,8 +25,9 @@ open Maps
 open AST
 open Kildall
 open Op
-open RTLBlockInstr
-open RTLBlock
+open Gible
+open GibleSeq
+open GibleSeq
 
 (** Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass
    [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *)
@@ -41,8 +41,10 @@ let find_edges c =
       let f = find_edge i n in
       (List.append (fst f) (fst l), List.append (snd f) (snd l))) c ([], [])
 
-let prepend_instr i = function
-  | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e}
+(* let prepend_instr i = function *)
+(*   | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e} *)
+
+let prepend_instr i b = i :: b
 
 let translate_inst = function
   | RTL.Inop _ -> Some RBnop
@@ -66,14 +68,14 @@ let rec next_bblock_from_RTL is_start e (c : RTL.code) s i =
   match trans_inst, succ with
   | (None, Some i'), _ ->
     if List.exists (fun x -> x = s) (snd e) && not is_start then
-      Errors.OK { bb_body = [RBnop]; bb_exit = RBgoto s }
+      Errors.OK [RBnop; RBexit (None, (RBgoto s))]
     else
-      Errors.OK { bb_body = [RBnop]; bb_exit = i' }
+      Errors.OK [RBnop; RBexit (None, i')]
   | (Some i', None), (s', Some i_n)::[] ->
     if List.exists (fun x -> x = s) (fst e) then
-      Errors.OK { bb_body = [i']; bb_exit = RBgoto s' }
+      Errors.OK [i'; RBexit (None, (RBgoto s'))]
     else if List.exists (fun x -> x = s) (snd e) && not is_start then
-      Errors.OK { bb_body = []; bb_exit = RBgoto s }
+      Errors.OK [RBnop; RBexit (None, (RBgoto s))]
     else begin
       match next_bblock_from_RTL false e c s' i_n with
       | Errors.OK bb ->
@@ -102,12 +104,12 @@ let rec translate_all edge c s res =
      | Some i ->
        match next_bblock_from_RTL true edge c s i with
        | Errors.Error msg -> Errors.Error msg
-       | Errors.OK {bb_body = bb; bb_exit = e} ->
-         let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in
+       | Errors.OK bb ->
+         let succ = List.filter (fun x -> P.lt x s) (all_successors bb) in
          (match traverseacc (translate_all edge c) succ (c_bb, s :: translated) with
           | Errors.Error msg -> Errors.Error msg
           | Errors.OK (c', t') ->
-            Errors.OK (PTree.set s {bb_body = bb; bb_exit = e} c', t')))
+            Errors.OK (PTree.set s bb c', t')))
 
 (* Partition a function and transform it into RTLBlock. *)
 let function_from_RTL f =
@@ -123,4 +125,3 @@ let function_from_RTL f =
               }
 
 let partition = function_from_RTL
-(* partition-main ends here *)
diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v
index bb01ff9..63d7d5a 100644
--- a/src/hls/PipelineOp.v
+++ b/src/hls/PipelineOp.v
@@ -28,8 +28,8 @@ Require Import compcert.verilog.Op.
 
 
 Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.RTLBlockInstr.
-Require Import vericert.hls.RTLPar.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GiblePar.
 Require Import vericert.hls.FunctionalUnits.
 
 Import Option.Notation.
@@ -56,8 +56,8 @@ Definition div_pos_in_block (il: nat * list (nat * nat * nat)) bb :=
   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)).
+Definition find_divs (bb: ParBB.t) :=
+  snd (List.fold_left div_pos_in_block bb (0%nat, nil)).
 
 Fixpoint mapi' {A B: Type} (n: nat) (f: nat -> A -> B) (l: list A): list B :=
   match l with
diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintGible.ml
index b8e1e2e..16d91af 100644
--- a/src/hls/PrintRTLBlockInstr.ml
+++ b/src/hls/PrintGible.ml
@@ -3,7 +3,7 @@ open Camlcoq
 open Datatypes
 open Maps
 open AST
-open RTLBlockInstr
+open Gible
 open Predicate
 open PrintAST
 
@@ -33,31 +33,7 @@ let print_pred_option pp = function
   | Some x -> fprintf pp "(%a)" print_pred_op x
   | None -> ()
 
-let print_bblock_body pp i =
-  fprintf pp "\t\t";
-  match i with
-  | RBnop -> fprintf pp "nop\n"
-  | RBop(p, op, ls, dst) ->
-     fprintf pp "%a %a = %a\n"
-       print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls)
-  | RBload(p, chunk, addr, args, dst) ->
-     fprintf pp "%a %a = %s[%a]\n"
-       print_pred_option p reg dst (name_of_chunk chunk)
-       (PrintOp.print_addressing reg) (addr, args)
-  | RBstore(p, chunk, addr, args, src) ->
-     fprintf pp "%a %s[%a] = %a\n"
-       print_pred_option p
-       (name_of_chunk chunk)
-       (PrintOp.print_addressing reg) (addr, args)
-       reg src
-  | RBsetpred (p', c, args, p) ->
-    fprintf pp "%a %a = %a\n"
-      print_pred_option p'
-      pred p
-      (PrintOp.print_condition reg) (c, args)
-
-let rec print_bblock_exit pp i =
-  fprintf pp "\t\t";
+let print_bblock_exit pp i =
   match i with
   | RBcall(_, fn, args, res, _) ->
       fprintf pp "%a = %a(%a)\n"
@@ -86,5 +62,28 @@ let rec print_bblock_exit pp i =
       fprintf pp "return %a\n" reg arg
   | RBgoto n ->
      fprintf pp "goto %d\n" (P.to_int n)
-  | RBpred_cf (p, c1, c2) ->
-    fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2
+
+let print_bblock_body pp i =
+  fprintf pp "\t\t";
+  match i with
+  | RBnop -> fprintf pp "nop\n"
+  | RBop(p, op, ls, dst) ->
+     fprintf pp "%a %a = %a\n"
+       print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls)
+  | RBload(p, chunk, addr, args, dst) ->
+     fprintf pp "%a %a = %s[%a]\n"
+       print_pred_option p reg dst (name_of_chunk chunk)
+       (PrintOp.print_addressing reg) (addr, args)
+  | RBstore(p, chunk, addr, args, src) ->
+     fprintf pp "%a %s[%a] = %a\n"
+       print_pred_option p
+       (name_of_chunk chunk)
+       (PrintOp.print_addressing reg) (addr, args)
+       reg src
+  | RBsetpred (p', c, args, p) ->
+    fprintf pp "%a %a = %a\n"
+      print_pred_option p'
+      pred p
+      (PrintOp.print_condition reg) (c, args)
+  | RBexit (p, cf) ->
+    fprintf pp "%a %a" print_pred_option p print_bblock_exit cf
diff --git a/src/hls/PrintRTLPar.ml b/src/hls/PrintGiblePar.ml
index ab93fa5..11bea67 100644
--- a/src/hls/PrintRTLPar.ml
+++ b/src/hls/PrintGiblePar.ml
@@ -17,10 +17,11 @@ open Camlcoq
 open Datatypes
 open Maps
 open AST
-open RTLBlockInstr
-open RTLPar
+open Gible
+open GiblePar
+open GiblePar
 open PrintAST
-open PrintRTLBlockInstr
+open PrintGible
 
 (* Printing of RTL code *)
 
@@ -40,8 +41,7 @@ let print_bblock pp (pc, i) =
   fprintf pp "%5d:{\n" pc;
   List.iter (fun x -> fprintf pp "{\n";
               List.iter (fun x -> fprintf pp "( "; List.iter (print_bblock_body pp) x; fprintf pp " )") x;
-              fprintf pp "}\n") i.bb_body;
-  print_bblock_exit pp i.bb_exit;
+              fprintf pp "}\n") i;
   fprintf pp "\t}\n\n"
 
 let print_function pp id f =
diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintGibleSeq.ml
index 8fef401..155f98e 100644
--- a/src/hls/PrintRTLBlock.ml
+++ b/src/hls/PrintGibleSeq.ml
@@ -17,10 +17,11 @@ open Camlcoq
 open Datatypes
 open Maps
 open AST
-open RTLBlockInstr
-open RTLBlock
+open Gible
+open GibleSeq
+open GibleSeq
 open PrintAST
-open PrintRTLBlockInstr
+open PrintGible
 
 (* Printing of RTL code *)
 
@@ -38,8 +39,7 @@ let ros pp = function
 
 let print_bblock pp (pc, i) =
   fprintf pp "%5d:{\n" pc;
-  List.iter (print_bblock_body pp) i.bb_body;
-  print_bblock_exit pp i.bb_exit;
+  List.iter (print_bblock_body pp) i;
   fprintf pp "\t}\n\n"
 
 let print_function pp id f =
diff --git a/src/hls/PrintRTLParFU.ml b/src/hls/PrintRTLParFU.ml
deleted file mode 100644
index ec4d851..0000000
--- a/src/hls/PrintRTLParFU.ml
+++ /dev/null
@@ -1,120 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Pretty-printers for RTL code *)
-
-open Printf
-open Camlcoq
-open Datatypes
-open Maps
-open AST
-open PrintRTLBlockInstr
-open RTLParFU
-open PrintAST
-
-(* Printing of RTL code *)
-
-let reg pp r =
-  fprintf pp "x%d" (P.to_int r)
-
-let rec regs pp = function
-  | [] -> ()
-  | [r] -> reg pp r
-  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
-
-let ros pp = function
-  | Coq_inl r -> reg pp r
-  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
-
-let print_bblock_body pp i =
-  fprintf pp "\t\t";
-  match i with
-  | FUnop -> fprintf pp "nop\n"
-  | FUop(p, op, ls, dst) ->
-     fprintf pp "%a %a = %a\n"
-       print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls)
-  | FUsetpred (p', c, args, p) ->
-    fprintf pp "%a %a = %a\n"
-      print_pred_option p'
-      pred p
-      (PrintOp.print_condition reg) (c, args)
-  | _ -> assert false
-
-let rec print_bblock_exit pp i =
-  fprintf pp "\t\t";
-  match i with
-  | FUcall(_, fn, args, res, _) ->
-      fprintf pp "%a = %a(%a)\n"
-        reg res ros fn regs args;
-  | FUtailcall(_, fn, args) ->
-      fprintf pp "tailcall %a(%a)\n"
-        ros fn regs args
-  | FUbuiltin(ef, args, res, _) ->
-      fprintf pp "%a = %s(%a)\n"
-        (print_builtin_res reg) res
-        (name_of_external ef)
-        (print_builtin_args reg) args
-  | FUcond(cond, args, s1, s2) ->
-      fprintf pp "if (%a) goto %d else goto %d\n"
-        (PrintOp.print_condition reg) (cond, args)
-        (P.to_int s1) (P.to_int s2)
-  | FUjumptable(arg, tbl) ->
-      let tbl = Array.of_list tbl in
-      fprintf pp "jumptable (%a)\n" reg arg;
-      for i = 0 to Array.length tbl - 1 do
-        fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i))
-      done
-  | FUreturn None ->
-      fprintf pp "return\n"
-  | FUreturn (Some arg) ->
-      fprintf pp "return %a\n" reg arg
-  | FUgoto n ->
-     fprintf pp "goto %d\n" (P.to_int n)
-  | FUpred_cf (p, c1, c2) ->
-    fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2
-
-let print_bblock pp (pc, i) =
-  fprintf pp "%5d:{\n" pc;
-  List.iter (fun x -> fprintf pp "{\n";
-              List.iter (fun x -> fprintf pp "( "; List.iter (print_bblock_body pp) x; fprintf pp " )") x;
-              fprintf pp "}\n") i.bb_body;
-  print_bblock_exit pp i.bb_exit;
-  fprintf pp "\t}\n\n"
-
-let print_function pp id f =
-  fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
-  let instrs =
-    List.sort
-      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
-      (List.rev_map
-        (fun (pc, i) -> (P.to_int pc, i))
-        (PTree.elements f.fn_code)) in
-  List.iter (print_bblock pp) instrs;
-  fprintf pp "}\n\n"
-
-let print_globdef pp (id, gd) =
-  match gd with
-  | Gfun(Internal f) -> print_function pp id f
-  | _ -> ()
-
-let print_program pp (prog: program) =
-  List.iter (print_globdef pp) prog.prog_defs
-
-let destination : string option ref = ref None
-
-let print_if passno prog =
-  match !destination with
-  | None -> ()
-  | Some f ->
-     let oc = open_out (f ^ "." ^ Z.to_string passno) in
-     print_program oc prog;
-     close_out oc
diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v
deleted file mode 100644
index 886c23d..0000000
--- a/src/hls/RICtransf.v
+++ /dev/null
@@ -1,86 +0,0 @@
-(*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2022 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.common.AST.
-Require Import compcert.common.Errors.
-Require Import compcert.common.Globalenvs.
-Require Import compcert.lib.Integers.
-Require Import compcert.lib.Maps.
-
-Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.RTLBlockInstr.
-Require Import vericert.hls.RTLPar.
-Require Import vericert.hls.Predicate.
-
-(*|
-=====================
-Reverse If-Conversion
-=====================
-
-This transformation takes a scheduling RTLPar block and removes any predicates
-from it.  It can then be trivially transformed into linear code again.  It works
-by iteratively selecting a predicate, then creating a branch based on it and
-placing subsequent instructions in one branch or the other.
-|*)
-
-Fixpoint existsb_val {A B} (f: A -> option B) (l : list A) : option B :=
-  match l with
-  | nil => None
-  | a :: l0 =>
-      match f a, existsb_val f l0 with
-      | _, Some v => Some v
-      | Some v, _ => Some v
-      | _, _ => None
-      end
-  end.
-
-Definition includes_setpred (bb: bb) :=
-  existsb_val (existsb_val (existsb_val (fun x => match x with RBsetpred a _ _ _ => Some a | _ => None end))) bb.
-
-Definition add_bb (should_split: bool) (i: bb) (bbc: list bb * list bb) :=
-  match bbc with
-  | (a, b) => if should_split then (a, i::b) else (i::a, b)
-  end.
-
-Fixpoint first_split (saw_pred: bool) (bb: list bb) :=
-  match bb with
-  | a :: b =>
-      match includes_setpred a with
-      | Some v =>
-          let (_, res) := first_split true b in
-          (Some v, add_bb saw_pred a res)
-      | _ =>
-          let (v, res) := first_split saw_pred b in
-          (v, add_bb saw_pred a res)
-      end
-  | nil => (None, (nil, nil))
-  end.
-
-Definition split_bb (fresh: node) (b: list bb) : list bb * list bb * list bb :=
-  match first_split false b with
-  | (Some p, (bb1, bb2)) => (bb1 ++ bb2, nil, nil)
-  | (None, (bb1, bb2)) => (bb1 ++ bb2, nil, nil)
-  end.
-
-Definition transf_function (f: function) : function := f.
-
-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/RTLParFUgen.v b/src/hls/RTLParFUgen.v
index 49ee6e7..a15be1c 100644
--- a/src/hls/RTLParFUgen.v
+++ b/src/hls/RTLParFUgen.v
@@ -30,8 +30,8 @@ Require Import vericert.hls.AssocMap.
 Require Import vericert.hls.Predicate.
 Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.Verilog.
-Require Import vericert.hls.RTLBlockInstr.
-Require Import vericert.hls.RTLPar.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GiblePar.
 Require Import vericert.hls.RTLParFU.
 Require Import vericert.hls.FunctionalUnits.
 
@@ -43,7 +43,7 @@ Definition update {A: Type} (i: positive) (f: option A -> A) (pt: PTree.t A) :=
 Definition add_instr (instr_: instr) x :=
   match x with Some i => instr_ :: i | None => instr_ :: nil end.
 
-Definition transl_instr (res: resources) (cycle: positive) (i: RTLBlockInstr.instr)
+Definition transl_instr (res: resources) (cycle: positive) (i: Gible.instr)
            (li: Errors.res (list instr * PTree.t (list instr))):
   Errors.res (list instr * PTree.t (list instr)) :=
   do (instr_list, d_tree) <- li;
@@ -74,9 +74,10 @@ Definition transl_instr (res: resources) (cycle: positive) (i: RTLBlockInstr.ins
       | _ => Errors.Error (Errors.msg "Could not find RAM")
       end
   | RBsetpred op c args p => Errors.OK (FUsetpred op c args p :: instr_list, d_tree)
+  | RBexit po cf => Errors.Error (Errors.msg "Wrong.")
   end.
 
-Fixpoint transl_cf_instr (i: RTLBlockInstr.cf_instr): RTLParFU.cf_instr :=
+Definition transl_cf_instr (i: Gible.cf_instr): RTLParFU.cf_instr :=
   match i with
   | RBcall sig r args d n => FUcall sig r args d n
   | RBtailcall sig r args => FUtailcall sig r args
@@ -85,7 +86,6 @@ Fixpoint transl_cf_instr (i: RTLBlockInstr.cf_instr): RTLParFU.cf_instr :=
   | RBjumptable r ns => FUjumptable r ns
   | RBreturn r => FUreturn r
   | RBgoto n => FUgoto n
-  | RBpred_cf po c1 c2 => FUpred_cf po (transl_cf_instr c1) (transl_cf_instr c2)
   end.
 
 Definition list_split {A:Type} (l: list (Z * A)) : (list (Z * A)) * (list (Z * A)) :=
@@ -101,7 +101,7 @@ Fixpoint map_error {A B : Type} (f : A -> res B) (l : list A) {struct l} : res (
     OK (y::ys)
   end.
 
-Definition transl_op_chain_block (res: resources) (cycle: positive) (instrs: list RTLBlockInstr.instr)
+Definition transl_op_chain_block (res: resources) (cycle: positive) (instrs: list Gible.instr)
            (state: Errors.res (list (list instr) * PTree.t (list instr)))
   : Errors.res (list (list instr) * PTree.t (list instr)) :=
   do (li, tr) <- state;
@@ -110,7 +110,7 @@ Definition transl_op_chain_block (res: resources) (cycle: positive) (instrs: lis
 
 (*Compute transl_op_chain_block initial_resources 10%nat (RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::RBnop::RBnop::nil) (OK (nil, PTree.empty _)).*)
 
-Definition transl_par_block (res: resources) (cycle: positive) (instrs: list (list RTLBlockInstr.instr))
+Definition transl_par_block (res: resources) (cycle: positive) (instrs: list (list Gible.instr))
            (state: Errors.res (list (list (list instr)) * PTree.t (list instr)))
   : Errors.res (list (list (list instr)) * PTree.t (list instr)) :=
   do (li, tr) <- state;
@@ -119,7 +119,7 @@ Definition transl_par_block (res: resources) (cycle: positive) (instrs: list (li
 
 (*Compute transl_par_block initial_resources 10%nat ((RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::nil)::(RBop None (Op.Ointconst (Int.repr 2)) nil 2%positive::RBnop::nil)::nil) (OK (((FUnop::nil)::nil)::nil, PTree.empty _)).*)
 
-Definition transl_seq_block (res: resources) (b: list (list RTLBlockInstr.instr))
+Definition transl_seq_block (res: resources) (b: list (list Gible.instr))
            (a: Errors.res (list (list (list instr)) * PTree.t (list instr) * positive)) :=
   do (litr, n) <- a;
   let (li, tr) := litr in
@@ -134,14 +134,13 @@ Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr))
   | None => ((cycle + 1)%positive, curr :: bb)
   end.
 
-Definition transl_bb (res: resources) (bb: RTLPar.bb): Errors.res RTLParFU.bblock_body :=
+Definition transl_bb (res: resources) (bb: ParBB.t): Errors.res RTLParFU.bblock_body :=
   do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb;
   let (li, tr) := litr in
   OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)).
 
-Definition transl_bblock (res: resources) (bb: RTLPar.bblock): Errors.res bblock :=
-  do bb' <- transl_bb res (RTLBlockInstr.bb_body bb);
-  OK (mk_bblock bb' (transl_cf_instr (RTLBlockInstr.bb_exit bb))).
+(*Definition transl_bblock (res: resources) (bb: ParBB.t): Errors.res ParBB.t :=
+  transl_bb res bb.
 
 Definition error_map_ptree {A B: Type} (f: positive -> A -> res B) (pt: PTree.t A) :=
   do ptl' <- map_error (fun x => do x' <- uncurry f x; OK (fst x, x')) (PTree.elements pt);
@@ -175,3 +174,4 @@ Definition transl_fundef p :=
 
 Definition transl_program (p : RTLPar.program) : Errors.res RTLParFU.program :=
   transform_partial_program transl_fundef p.
+*)
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 70395e7..9d9700a 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -25,9 +25,12 @@ open Maps
 open AST
 open Kildall
 open Op
-open RTLBlockInstr
+open Gible
 open Predicate
-open RTLBlock
+open GibleSeq
+open GibleSeq
+open GiblePar
+open GiblePar
 open HTL
 open Verilog
 open HTLgen
@@ -286,6 +289,7 @@ let comb_delay = function
      | Omod -> 72
      | Omodu -> 72
      | _ -> 1)
+  | RBexit _ -> 8
   | _ -> 1
 
 let pipeline_stages = function
@@ -330,6 +334,11 @@ let accumulate_RAW_deps map dfg curr =
   | RBload (op, _mem, _addr, rs, dst) -> acc_dep_instruction rs dst
   | RBsetpred (_op, _mem, rs, _p) -> acc_dep_instruction_nodst rs
   | RBstore (op, _mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs)
+  | RBexit (_, RBcall (_, _, rs, _, _)) -> acc_dep_instruction_nodst rs
+  | RBexit (_, RBtailcall (_, _, rs)) -> acc_dep_instruction_nodst rs
+  | RBexit (_, RBcond (_, rs, _, _)) -> acc_dep_instruction_nodst rs
+  | RBexit (_, RBjumptable (r, _)) -> acc_dep_instruction_nodst [r]
+  | RBexit (_, RBreturn (Some r)) -> acc_dep_instruction_nodst [r]
   | _ -> (i + 1, dst_map, graph)
 
 (** Finds the next write to the [dst] register.  This is a small optimisation so that only one
@@ -356,8 +365,13 @@ let rec find_all_next_dst_read i dst i' curr =
   | RBop (_, _, rs, _) :: curr' -> check_dst rs curr'
   | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr'
   | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr'
-  | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr'
   | RBsetpred (_, _, rs, _) :: curr' -> check_dst rs curr'
+  | RBexit (_, RBcall (_, _, rs, _, _)) :: curr' -> check_dst rs curr'
+  | RBexit (_, RBtailcall (_, _, rs)) :: curr' -> check_dst rs curr'
+  | RBexit (_, RBcond (_, rs, _, _)) :: curr' -> check_dst rs curr'
+  | RBexit (_, RBjumptable (r, _)) :: curr' -> check_dst [r] curr'
+  | RBexit (_, RBreturn (Some r)) :: curr' -> check_dst [r] curr'
+  | _ :: curr' -> check_dst [] curr'
 
 let drop i lst =
   let rec drop' i' lst' =
@@ -525,6 +539,7 @@ let get_pred = function
   | RBop (op, _, _, _) -> op
   | RBload (op, _, _, _, _) -> op
   | RBstore (op, _, _, _, _) -> op
+  | RBexit (op, _) -> op
   | RBsetpred (_, _, _, _) -> None
 
 let independant_pred p p' =
@@ -551,14 +566,14 @@ let remove_unnecessary_deps graph =
    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 ibody = List.mapi (fun i a -> (i, a)) bb.bb_body in
+  let ibody = List.mapi (fun i a -> (i, a)) bb 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
+      bb
   in
-  let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb.bb_body) dfg ibody) dfg'
+  let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb) dfg ibody) dfg'
       [ accumulate_WAW_deps;
         accumulate_WAR_deps;
         accumulate_RAW_mem_deps;
@@ -570,7 +585,7 @@ let gather_bb_constraints debug bb =
       ]
   in
   let dfg''' = remove_unnecessary_deps dfg'' in
-  (List.length bb.bb_body, dfg''', successors_instr bb.bb_exit)
+  (List.length bb, dfg''', GibleSeq.all_successors 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 }
@@ -690,15 +705,15 @@ let add_resource_constr n dfg constr =
   |> get_constraints (List.rev res.res_udiv)
   |> get_constraints (List.rev res.res_sdiv)
 
-let gather_cfg_constraints c constr curr =
+let gather_cfg_constraints (c: GibleSeq.code) constr curr =
   let (n, dfg) = curr in
   match PTree.get (P.of_int n) c with
   | None -> assert false
-  | Some { bb_exit = ctrl; _ } ->
+  | Some bb ->
     add_super_nodes n dfg constr
     |> add_initial_sv n dfg
     |> add_data_deps n dfg
-    |> add_ctrl_deps n (successors_instr ctrl
+    |> add_ctrl_deps n (GibleSeq.all_successors bb
                         |> List.map P.to_int
                         |> List.filter (fun n' -> n' < n))
     |> add_cycle_constr 8 n dfg
@@ -802,10 +817,10 @@ let range s e =
 
 (** Should generate the [RTLPar] code based on the input [RTLBlock] description. *)
 let transf_rtlpar c c' schedule =
-  let f i bb : RTLPar.bblock =
+  let f i bb : ParBB.t =
     match bb with
-    | { bb_body = []; bb_exit = c } -> { bb_body = []; bb_exit = c }
-    | { bb_body = bb_body'; bb_exit = ctrl_flow } ->
+    | bb_body' ->
+    (* | { bb_body = bb_body'; bb_exit = ctrl_flow } -> *)
       let dfg = match PTree.get i c' with None -> assert false | Some x -> x in
       let bb_st_e =
         let m = IMap.find (P.to_int i) (snd schedule) in
@@ -836,13 +851,12 @@ let transf_rtlpar c c' schedule =
                                            (*|> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x [])
                                            |> List.rev) body2*)
       in
-      { bb_body = final_body2;
-        bb_exit = ctrl_flow
-      }
+      final_body2
+    | _ -> List.map (fun i -> [[i]]) bb
   in
   PTree.map f c
 
-let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
+let schedule entry (c : GibleSeq.code) =
   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
@@ -859,22 +873,22 @@ let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
   (**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 c' schedule'
 
-let rec find_reachable_states c e =
-  match PTree.get e c with
-  | Some { bb_exit = ex; _ } ->
-    e :: List.fold_left (fun x a -> List.concat [x; find_reachable_states c a]) []
-      (successors_instr ex |> List.filter (fun x -> P.lt x e))
-  | None -> assert false
+(* let rec find_reachable_states c e = *)
+(*   match PTree.get e c with *)
+(*   | Some bb -> *)
+(*     e :: List.fold_left (fun x a -> List.concat [x; find_reachable_states c a]) [] *)
+(*       (all_successors bb |> List.filter (fun x -> P.lt x e)) *)
+(*   | None -> assert false *)
 
 let add_to_tree c nt i =
   match PTree.get i c with
   | Some p -> PTree.set i p nt
   | None -> assert false
 
-let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function =
+let schedule_fn (f : GibleSeq.coq_function) : GiblePar.coq_function =
   let scheduled = schedule f.fn_entrypoint f.fn_code in
-  let reachable = find_reachable_states scheduled f.fn_entrypoint
-                  |> List.to_seq |> SS.of_seq |> SS.to_seq |> List.of_seq in
+  (* let reachable = find_reachable_states scheduled f.fn_entrypoint *)
+  (*                 |> List.to_seq |> SS.of_seq |> SS.to_seq |> List.of_seq in *)
   { fn_sig = f.fn_sig;
     fn_params = f.fn_params;
     fn_stacksize = f.fn_stacksize;