Add RTLPar with functional units

3 files changed, 1302 insertions, 0 deletions

diff --git a/src/hls/HTLParFugen.v b/src/hls/HTLParFugen.v
new file mode 100644
index 0000000..a002e15
--- /dev/null
+++ b/src/hls/HTLParFugen.v
@@ -0,0 +1,879 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Require Import Coq.micromega.Lia.
+
+Require Import compcert.common.AST.
+Require compcert.common.Errors.
+Require compcert.common.Globalenvs.
+Require compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Statemonad.
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.HTL.
+Require Import vericert.hls.Predicate.
+Require Import vericert.hls.RTLParFU.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.Verilog.
+
+#[local] Hint Resolve AssocMap.gempty : htlh.
+#[local] Hint Resolve AssocMap.gso : htlh.
+#[local] Hint Resolve AssocMap.gss : htlh.
+#[local] Hint Resolve Ple_refl : htlh.
+#[local] Hint Resolve Ple_succ : htlh.
+
+Definition assignment : Type := expr -> expr -> stmnt.
+
+Record state: Type := mkstate {
+  st_st: reg;
+  st_freshreg: reg;
+  st_freshstate: node;
+  st_scldecls: AssocMap.t (option io * scl_decl);
+  st_arrdecls: AssocMap.t (option io * arr_decl);
+  st_datapath: datapath;
+  st_controllogic: controllogic;
+}.
+
+Definition init_state (st : reg) : state :=
+  mkstate st
+          1%positive
+          1%positive
+          (AssocMap.empty (option io * scl_decl))
+          (AssocMap.empty (option io * arr_decl))
+          (AssocMap.empty stmnt)
+          (AssocMap.empty stmnt).
+
+Module HTLState <: State.
+
+  Definition st := state.
+
+  Inductive st_incr: state -> state -> Prop :=
+    state_incr_intro:
+      forall (s1 s2: state),
+        st_st s1 = st_st s2 ->
+        Ple s1.(st_freshreg) s2.(st_freshreg) ->
+        Ple s1.(st_freshstate) s2.(st_freshstate) ->
+        (forall n,
+            s1.(st_controllogic)!n = None
+            \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) ->
+        st_incr s1 s2.
+  #[local] Hint Constructors st_incr : htlh.
+
+  Definition st_prop := st_incr.
+  #[local] Hint Unfold st_prop : htlh.
+
+  Lemma st_refl : forall s, st_prop s s.
+  Proof. auto with htlh. Qed.
+
+  Lemma st_trans :
+    forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
+  Proof.
+    intros. inv H. inv H0.
+    apply state_incr_intro; eauto using Ple_trans; intros; try congruence.
+    destruct H4 with n; destruct H7 with n; intuition congruence.
+  Qed.
+
+End HTLState.
+Export HTLState.
+
+Module HTLMonad := Statemonad(HTLState).
+Export HTLMonad.
+
+Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
+Import HTLMonadExtra.
+Export MonadNotation.
+
+Definition state_goto (st : reg) (n : node) : stmnt :=
+  Vnonblock (Vvar st) (Vlit (posToValue n)).
+
+Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
+  Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).
+
+Definition check_empty_node_datapath:
+  forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }.
+Proof.
+  intros. case (s.(st_datapath)!n); tauto.
+Defined.
+
+Definition check_empty_node_controllogic:
+  forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }.
+Proof.
+  intros. case (s.(st_controllogic)!n); tauto.
+Defined.
+
+Lemma declare_reg_state_incr :
+  forall i s r sz,
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       s.(st_freshstate)
+       (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
+       s.(st_arrdecls)
+       s.(st_datapath)
+       s.(st_controllogic)).
+Proof. Admitted.
+
+Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
+  fun s => OK tt (mkstate
+                s.(st_st)
+                s.(st_freshreg)
+                s.(st_freshstate)
+                (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
+                s.(st_arrdecls)
+                s.(st_datapath)
+                s.(st_controllogic))
+              (declare_reg_state_incr i s r sz).
+
+Lemma add_instr_state_incr :
+  forall s n n' st,
+    (st_controllogic s)!n = None ->
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       s.(st_scldecls)
+       s.(st_arrdecls)
+       (AssocMap.set n st s.(st_datapath))
+       (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
+Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
+  fun s =>
+    match check_empty_node_controllogic s n with
+    | left TRANS =>
+      OK tt (mkstate
+               s.(st_st)
+               s.(st_freshreg)
+               (st_freshstate s)
+               s.(st_scldecls)
+               s.(st_arrdecls)
+               (AssocMap.set n st s.(st_datapath))
+               (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic)))
+         (add_instr_state_incr s n n' st TRANS)
+    | _ => Error (Errors.msg "HTL.add_instr")
+    end.
+
+Lemma add_instr_skip_state_incr :
+  forall s n st,
+    (st_controllogic s)!n = None ->
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       s.(st_scldecls)
+       s.(st_arrdecls)
+       (AssocMap.set n st s.(st_datapath))
+       (AssocMap.set n Vskip s.(st_controllogic))).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
+Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
+  fun s =>
+    match check_empty_node_controllogic s n with
+    | left TRANS =>
+      OK tt (mkstate
+               s.(st_st)
+               s.(st_freshreg)
+               (st_freshstate s)
+               s.(st_scldecls)
+               s.(st_arrdecls)
+               (AssocMap.set n st s.(st_datapath))
+               (AssocMap.set n Vskip s.(st_controllogic)))
+         (add_instr_skip_state_incr s n st TRANS)
+    | _ => Error (Errors.msg "HTL.add_instr_skip")
+    end.
+
+Lemma add_node_skip_state_incr :
+  forall s n st,
+    (st_controllogic s)!n = None ->
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       s.(st_scldecls)
+       s.(st_arrdecls)
+       (AssocMap.set n Vskip s.(st_datapath))
+       (AssocMap.set n st s.(st_controllogic))).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
+Definition add_node_skip (n : node) (st : stmnt) : mon unit :=
+  fun s =>
+    match check_empty_node_controllogic s n with
+    | left TRANS =>
+      OK tt (mkstate
+               s.(st_st)
+               s.(st_freshreg)
+               (st_freshstate s)
+               s.(st_scldecls)
+               s.(st_arrdecls)
+               (AssocMap.set n Vskip s.(st_datapath))
+               (AssocMap.set n st s.(st_controllogic)))
+         (add_node_skip_state_incr s n st TRANS)
+    | _ => Error (Errors.msg "HTL.add_node_skip")
+    end.
+
+Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
+Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
+
+Definition bop (op : binop) (r1 r2 : reg) : expr :=
+  Vbinop op (Vvar r1) (Vvar r2).
+
+Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=
+  Vbinop op (Vvar r) (Vlit (intToValue l)).
+
+Definition boplitz (op: binop) (r: reg) (l: Z) : expr :=
+  Vbinop op (Vvar r) (Vlit (ZToValue l)).
+
+Definition translate_comparison (c : Integers.comparison) (args : list reg)
+  : mon expr :=
+  match c, args with
+  | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2)
+  | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2)
+  | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2)
+  | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2)
+  | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2)
+  | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2)
+  | _, _ => error (Errors.msg
+                 "Htlgen: comparison instruction not implemented: other")
+  end.
+
+Definition translate_comparison_imm (c : Integers.comparison) (args : list reg)
+           (i: Integers.int) : mon expr :=
+  match c, args with
+  | Integers.Ceq, r1::nil => ret (boplit Veq r1 i)
+  | Integers.Cne, r1::nil => ret (boplit Vne r1 i)
+  | Integers.Clt, r1::nil => ret (boplit Vlt r1 i)
+  | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i)
+  | Integers.Cle, r1::nil => ret (boplit Vle r1 i)
+  | Integers.Cge, r1::nil => ret (boplit Vge r1 i)
+  | _, _ => error (Errors.msg
+                 "Htlgen: comparison_imm instruction not implemented: other")
+  end.
+
+Definition translate_comparisonu (c : Integers.comparison) (args : list reg)
+  : mon expr :=
+  match c, args with
+  | Integers.Clt, r1::r2::nil => ret (bop Vltu r1 r2)
+  | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2)
+  | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2)
+  | Integers.Cge, r1::r2::nil => ret (bop Vgeu r1 r2)
+  | _, _ => error (Errors.msg
+                 "Htlgen: comparison instruction not implemented: other")
+  end.
+
+Definition translate_comparison_immu (c : Integers.comparison)
+           (args : list reg) (i: Integers.int) : mon expr :=
+  match c, args with
+  | Integers.Clt, r1::nil => ret (boplit Vltu r1 i)
+  | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i)
+  | Integers.Cle, r1::nil => ret (boplit Vleu r1 i)
+  | Integers.Cge, r1::nil => ret (boplit Vgeu r1 i)
+  | _, _ => error (Errors.msg
+                 "Htlgen: comparison_imm instruction not implemented: other")
+  end.
+
+Definition translate_condition (c : Op.condition) (args : list reg)
+  : mon expr :=
+  match c, args with
+  | Op.Ccomp c, _ => translate_comparison c args
+  | Op.Ccompu c, _ => translate_comparisonu c args
+  | Op.Ccompimm c i, _ => translate_comparison_imm c args i
+  | Op.Ccompuimm c i, _ => translate_comparison_immu c args i
+  | Op.Cmaskzero n, _ =>
+    error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero")
+  | Op.Cmasknotzero n, _ =>
+    error (Errors.msg
+         "Htlgen: condition instruction not implemented: Cmasknotzero")
+  | _, _ =>
+    error (Errors.msg "Htlgen: condition instruction not implemented: other")
+  end.
+
+Definition check_address_parameter_signed (p : Z) : bool :=
+  Z.leb Integers.Ptrofs.min_signed p
+  && Z.leb p Integers.Ptrofs.max_signed.
+
+Definition check_address_parameter_unsigned (p : Z) : bool :=
+  Z.leb p Integers.Ptrofs.max_unsigned.
+
+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?*)
+  | Op.Aindexed off, r1::nil =>
+    if (check_address_parameter_signed off)
+    then ret (boplitz Vadd r1 off)
+    else error (Errors.msg ("HTLPargen: translate_eff_addressing (Aindexed): address out of bounds"))
+  | Op.Ascaled scale offset, r1::nil =>
+    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
+    then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))
+    else error (Errors.msg "HTLPargen: translate_eff_addressing (Ascaled): address out of bounds")
+  | Op.Aindexed2 offset, r1::r2::nil =>
+    if (check_address_parameter_signed offset)
+    then ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset)))
+    else error (Errors.msg "HTLPargen: translate_eff_addressing (Aindexed2): address out of bounds")
+  | 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 (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset))))
+    else error (Errors.msg "HTLPargen: translate_eff_addressing (Aindexed2scaled): address out of bounds")
+  | 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 (Vlit (ZToValue a))
+    else error (Errors.msg "HTLPargen: translate_eff_addressing (Ainstack): address out of bounds")
+  | _, _ => error (Errors.msg "HTLPargen: translate_eff_addressing unsuported addressing")
+  end.
+
+(** Translate an instruction to a statement. FIX mulhs mulhu *)
+Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
+  match op, args with
+  | Op.Omove, r::nil => ret (Vvar r)
+  | Op.Ointconst n, _ => ret (Vlit (intToValue n))
+  | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r))
+  | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2)
+  | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2)
+  | 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.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)
+  | Op.Oorimm n, r::nil => ret (boplit Vor r n)
+  | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2)
+  | Op.Oxorimm n, r::nil => ret (boplit Vxor r n)
+  | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r))
+  | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2)
+  | Op.Oshlimm n, r::nil => ret (boplit Vshl r n)
+  | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2)
+  | Op.Oshrimm n, r::nil => ret (boplit Vshr r n)
+  | Op.Oshrximm n, r::nil =>
+    ret (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0)))
+                  (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar r)) (Vlit n)))
+                  (Vbinop Vshru (Vvar r) (Vlit n)))
+  | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2)
+  | Op.Oshruimm n, r::nil => ret (boplit Vshru r n)
+  | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm")
+  (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32)))
+                                        (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*)
+  | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n)))
+  | Op.Ocmp c, _ => translate_condition c args
+  | Op.Osel c AST.Tint, r1::r2::rl =>
+    do tc <- translate_condition c rl;
+    ret (Vternary tc (Vvar r1) (Vvar r2))
+  | Op.Olea a, _ => translate_eff_addressing a args
+  | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other")
+  end.
+
+Lemma add_branch_instr_state_incr:
+  forall s e n n1 n2,
+    (st_controllogic s) ! n = None ->
+    st_incr s (mkstate
+                 s.(st_st)
+                (st_freshreg s)
+                (st_freshstate s)
+                s.(st_scldecls)
+                s.(st_arrdecls)
+                (AssocMap.set n Vskip (st_datapath s))
+                (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
+Proof.
+  intros. apply state_incr_intro; simpl;
+            try (intros; destruct (peq n0 n); subst);
+            auto with htlh.
+Qed.
+
+Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
+  fun s =>
+    match check_empty_node_controllogic s n with
+    | left NTRANS =>
+      OK tt (mkstate
+               s.(st_st)
+                (st_freshreg s)
+                (st_freshstate s)
+                s.(st_scldecls)
+                s.(st_arrdecls)
+                (AssocMap.set n Vskip (st_datapath s))
+                (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
+         (add_branch_instr_state_incr s e n n1 n2 NTRANS)
+    | _ => Error (Errors.msg "Htlgen: add_branch_instr")
+    end.
+
+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.
+
+Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=
+  match ns with
+  | n :: ns' => (i, n) :: enumerate (i+1) ns'
+  | nil => nil
+  end.
+
+Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
+  List.map (fun a => match a with
+                    (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n)))
+                  end)
+           (enumerate 0 ns).
+
+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
+         s.(st_st)
+         (Pos.succ (st_freshreg s))
+         (st_freshstate s)
+         s.(st_scldecls)
+         (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
+         (st_datapath s)
+         (st_controllogic s)).
+Proof. constructor; simpl; auto with htlh. Qed.
+
+Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
+  fun s => let r := s.(st_freshreg) in
+           OK (r, ln) (mkstate
+                   s.(st_st)
+                   (Pos.succ r)
+                   (st_freshstate s)
+                   s.(st_scldecls)
+                   (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
+                   (st_datapath s)
+                   (st_controllogic s))
+              (create_arr_state_incr s sz ln i).
+
+Definition max_pc_map (m : Maps.PTree.t stmnt) :=
+  PTree.fold (fun m pc i => Pos.max m pc) m 1%positive.
+
+Lemma max_pc_map_sound:
+  forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m).
+Proof.
+  intros until i.
+  apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m).
+  (* extensionality *)
+  intros. apply H0. rewrite H; auto.
+  (* base case *)
+  rewrite PTree.gempty. congruence.
+  (* inductive case *)
+  intros. rewrite PTree.gsspec in H2. destruct (peq pc k).
+  inv H2. unfold Ple, Plt in *. lia.
+  apply Ple_trans with a. auto.
+  unfold Ple, Plt in *. lia.
+Qed.
+
+Lemma max_pc_wf :
+  forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
+            map_well_formed m.
+Proof.
+  unfold map_well_formed. intros.
+  exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x.
+  apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B.
+  unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst.
+  simplify. transitivity (Z.pos (max_pc_map m)); eauto.
+Qed.
+
+Definition poslength {A : Type} (l : list A) : positive :=
+  match Zlength l with
+  | Z.pos p => p
+  | _ => 1
+  end.
+
+Fixpoint penumerate {A : Type} (p : positive) (l : list A) {struct l}
+  : list (positive * A) :=
+  match l with
+  | x :: xs => (p, x) :: penumerate (Pos.pred p) xs
+  | nil => nil
+  end.
+
+Fixpoint prange {A: Type} (p1 p2: positive) (l: list A) {struct l} :=
+  match l with
+  | x :: xs => (p1, p2, x) :: prange p2 (Pos.pred p2) xs
+  | nil => nil
+  end.
+
+Lemma add_data_instr_state_incr :
+  forall s n st,
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       s.(st_scldecls)
+       s.(st_arrdecls)
+       (AssocMap.set n (Vseq (AssocMapExt.get_default
+                            _ Vskip n s.(st_datapath)) st) s.(st_datapath))
+       s.(st_controllogic)).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
+Definition add_data_instr (n : node) (st : stmnt) : mon unit :=
+  fun s =>
+    OK tt (mkstate
+         s.(st_st)
+         s.(st_freshreg)
+         (st_freshstate s)
+         s.(st_scldecls)
+         s.(st_arrdecls)
+         (AssocMap.set n (Vseq (AssocMapExt.get_default _ Vskip n s.(st_datapath)) st) s.(st_datapath))
+         s.(st_controllogic))
+       (add_data_instr_state_incr s n st).
+
+Lemma add_control_instr_state_incr :
+  forall s n st,
+  (st_controllogic s) ! n = None ->
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       s.(st_scldecls)
+       s.(st_arrdecls)
+       s.(st_datapath)
+       (AssocMap.set n st s.(st_controllogic))).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
+Definition add_control_instr (n : node) (st : stmnt) : mon unit :=
+  fun s =>
+    match check_empty_node_controllogic s n with
+    | left CTRL =>
+      OK tt (mkstate
+           s.(st_st)
+           s.(st_freshreg)
+           (st_freshstate s)
+           s.(st_scldecls)
+           s.(st_arrdecls)
+           s.(st_datapath)
+           (AssocMap.set n st s.(st_controllogic)))
+         (add_control_instr_state_incr s n st CTRL)
+    | _ =>
+      Error (Errors.msg "HTLPargen.add_control_instr: control logic is not empty")
+    end.
+
+Definition add_control_instr_force_state_incr :
+  forall s n st,
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       s.(st_scldecls)
+       s.(st_arrdecls)
+       s.(st_datapath)
+       (AssocMap.set n st s.(st_controllogic))).
+Admitted.
+
+Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
+  fun s =>
+    OK tt (mkstate
+      s.(st_st)
+      s.(st_freshreg)
+      (st_freshstate s)
+      s.(st_scldecls)
+      s.(st_arrdecls)
+      s.(st_datapath)
+      (AssocMap.set n st s.(st_controllogic)))
+   (add_control_instr_force_state_incr s n st).
+
+Fixpoint pred_expr (preg: reg) (p: pred_op) :=
+  match p with
+  | Plit (b, pred) =>
+    if b
+    then Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred))
+    else Vunop Vnot (Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)))
+  | Ptrue => Vlit (ZToValue 1)
+  | Pfalse => Vlit (ZToValue 0)
+  | Pand p1 p2 =>
+    Vbinop Vand (pred_expr preg p1) (pred_expr preg p2)
+  | Por p1 p2 =>
+    Vbinop Vor (pred_expr preg p1) (pred_expr preg p2)
+  end.
+
+Definition translate_predicate (a : assignment)
+           (preg: reg) (p: option pred_op) (dst e: expr) :=
+  match p with
+  | None => ret (a dst e)
+  | Some pos =>
+    ret (a dst (Vternary (pred_expr preg pos) e dst))
+  end.
+
+Definition translate_inst a (fin rtrn stack 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
+  | FUload p chunk addr args dst =>
+    do src <- translate_arr_access chunk addr args stack;
+    do _ <- declare_reg None dst 32;
+    translate_predicate a preg p (Vvar dst) src
+  | FUstore p chunk addr args src =>
+    do dst <- translate_arr_access chunk addr args stack;
+    translate_predicate a preg p dst (Vvar src)
+  | FUsetpred _ c args p =>
+    do cond <- translate_condition c args;
+    ret (a (pred_expr preg (Plit (true, p))) cond)
+  end.
+
+Lemma create_new_state_state_incr:
+  forall s p,
+  st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (s.(st_freshstate) + p)%positive
+       s.(st_scldecls)
+       s.(st_arrdecls)
+       s.(st_datapath)
+       s.(st_controllogic)).
+Admitted.
+
+Definition create_new_state (p: node): mon node :=
+  fun s => OK s.(st_freshstate)
+              (mkstate
+                s.(st_st)
+                s.(st_freshreg)
+                (s.(st_freshstate) + p)%positive
+                s.(st_scldecls)
+                s.(st_arrdecls)
+                s.(st_datapath)
+                s.(st_controllogic))
+              (create_new_state_state_incr s p).
+
+Definition translate_inst_list (fin rtrn stack 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 stack preg n l;
+             add_data_instr n stmnt) (concat li);
+    do st <- get;
+    add_control_instr n (state_goto st.(st_st) p)
+  end.
+
+Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr)
+  : mon (stmnt * stmnt) :=
+  match cfi with
+  | FUgoto n' =>
+    do st <- get;
+    ret (Vskip, state_goto st.(st_st) n')
+  | FUcond 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 =>
+    match r with
+    | Some r' =>
+      ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))),
+           Vskip)
+    | None =>
+      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 stack preg c1;
+    do (tc2s, tc2c) <- translate_cfi' fin rtrn stack preg c2;
+    ret ((Vcond (pred_expr preg p) tc1s tc2s), (Vcond (pred_expr preg p) tc1c tc2c))
+  | FUjumptable 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 =>
+    error (Errors.msg "HTLPargen: RPcall not supported.")
+  | FUtailcall sig ri lr =>
+    error (Errors.msg "HTLPargen: RPtailcall not supported.")
+  | FUbuiltin e lb b n =>
+    error (Errors.msg "HTLPargen: RPbuildin not supported.")
+  end.
+
+Definition translate_cfi (fin rtrn stack preg: reg) (ni: node * cf_instr)
+  : mon unit :=
+  let (n, cfi) := ni in
+  do (s, c) <- translate_cfi' fin rtrn stack preg cfi;
+  do _ <- add_control_instr n c;
+  add_data_instr n s.
+
+Definition transf_bblock (fin rtrn stack preg: reg) (ni : node * bblock)
+  : mon unit :=
+  let (n, bb) := ni in
+  do nstate <- create_new_state ((poslength bb.(bb_body)))%positive;
+  do _ <- collectlist (translate_inst_list fin rtrn stack preg)
+                      (prange n (nstate + poslength bb.(bb_body) - 1)%positive
+                                  bb.(bb_body));
+  match bb.(bb_body) with
+  | nil => translate_cfi fin rtrn stack preg (n, bb.(bb_exit))
+  | _ => translate_cfi fin rtrn stack preg (nstate, bb.(bb_exit))
+  end.
+
+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)
+                          && (d <? e) && (e <? f) && (f <? g))%positive true with
+          | left t => left _
+          | _ => _
+          end); auto.
+  simplify; repeat match goal with
+                   | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H
+                   end; unfold module_ordering; auto.
+Defined.
+
+Definition transf_module (f: function) : mon HTL.module.
+  refine (
+  if stack_correct f.(fn_stacksize) then
+    do fin <- create_reg (Some Voutput) 1;
+    do rtrn <- create_reg (Some Voutput) 32;
+    do (stack, stack_len) <- create_arr None 32
+                                        (Z.to_nat (f.(fn_stacksize) / 4));
+    do preg <- create_reg None 32;
+    do _ <- collectlist (transf_bblock fin rtrn stack preg)
+                        (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;
+    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)))
+              Integers.Int.max_unsigned,
+          decide_order (st_st current_state) fin rtrn stack start rst clk,
+          max_list_dec (fn_params f) (st_st current_state)
+    with
+    | left LEDATA, left LECTRL, left MORD, left WFPARAMS =>
+        ret (HTL.mkmodule
+           f.(fn_params)
+           current_state.(st_datapath)
+           current_state.(st_controllogic)
+           f.(fn_entrypoint)
+           current_state.(st_st)
+           stack
+           stack_len
+           fin
+           rtrn
+           start
+           rst
+           clk
+           current_state.(st_scldecls)
+           current_state.(st_arrdecls)
+           None
+           (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))
+           MORD
+           _
+           WFPARAMS)
+    | _, _, _, _ => error (Errors.msg "More than 2^32 states.")
+    end
+  else error (Errors.msg "Stack size misalignment.")); discriminate.
+Defined.
+
+Definition max_state (f: function) : state :=
+  let st := Pos.succ (max_reg_function f) in
+  mkstate st
+          (Pos.succ st)
+          (Pos.succ (max_pc_function f))
+          (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st)))
+          (st_arrdecls (init_state st))
+          (st_datapath (init_state st))
+          (st_controllogic (init_state st)).
+
+Definition transl_module (f : function) : Errors.res HTL.module :=
+  run_mon (max_state f) (transf_module f).
+
+Definition transl_fundef := transf_partial_fundef transl_module.
+
+Definition main_is_internal (p : RTLParFU.program) : bool :=
+  let ge := Globalenvs.Genv.globalenv p in
+  match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with
+  | Some b =>
+    match Globalenvs.Genv.find_funct_ptr ge b with
+    | Some (AST.Internal _) => true
+    | _ => false
+    end
+  | _ => false
+  end.
+
+Definition transl_program (p : RTLParFU.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/RTLParFU.v b/src/hls/RTLParFU.v
new file mode 100644
index 0000000..3442ff0
--- /dev/null
+++ b/src/hls/RTLParFU.v
@@ -0,0 +1,402 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020-2021 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Require Import compcert.backend.Registers.
+Require Import compcert.common.AST.
+Require Import compcert.common.Events.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.common.Memory.
+Require Import compcert.common.Smallstep.
+Require Import compcert.common.Values.
+Require Import compcert.lib.Coqlib.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require Import compcert.verilog.Op.
+
+Require Import vericert.hls.FunctionalUnits.
+Require Import Predicate.
+Require Import Vericertlib.
+
+Definition node := positive.
+
+Inductive instr : Type :=
+| FUnop : instr
+| FUop : option pred_op -> operation -> list reg -> reg -> instr
+| FUload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
+| FUstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
+| FUsetpred : option pred_op -> condition -> list reg -> predicate -> instr.
+
+Inductive cf_instr : Type :=
+| FUcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr
+| FUtailcall : signature -> reg + ident -> list reg -> cf_instr
+| FUbuiltin : external_function -> list (builtin_arg reg) ->
+              builtin_res reg -> node -> cf_instr
+| FUcond : condition -> list reg -> node -> node -> cf_instr
+| FUjumptable : reg -> list node -> cf_instr
+| FUreturn : option reg -> cf_instr
+| FUgoto : node -> cf_instr
+| FUpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr.
+
+Fixpoint successors_instr (i : cf_instr) : list node :=
+  match i with
+  | FUcall sig ros args res s => s :: nil
+  | FUtailcall sig ros args => nil
+  | FUbuiltin ef args res s => s :: nil
+  | FUcond cond args ifso ifnot => ifso :: ifnot :: nil
+  | FUjumptable arg tbl => tbl
+  | FUreturn optarg => nil
+  | FUgoto n => n :: nil
+  | FUpred_cf p c1 c2 => concat (successors_instr c1 :: successors_instr c2 :: nil)
+  end.
+
+Definition max_reg_instr (m: positive) (i: instr) :=
+  match i with
+  | FUnop => m
+  | FUop p op args res =>
+      fold_left Pos.max args (Pos.max res m)
+  | FUload p chunk addr args dst =>
+      fold_left Pos.max args (Pos.max dst m)
+  | FUstore p chunk addr args src =>
+      fold_left Pos.max args (Pos.max src m)
+  | FUsetpred p' c args p =>
+      fold_left Pos.max args m
+  end.
+
+Fixpoint max_reg_cfi (m : positive) (i : cf_instr) :=
+  match i with
+  | FUcall sig (inl r) args res s =>
+      fold_left Pos.max args (Pos.max r (Pos.max res m))
+  | FUcall sig (inr id) args res s =>
+      fold_left Pos.max args (Pos.max res m)
+  | FUtailcall sig (inl r) args =>
+      fold_left Pos.max args (Pos.max r m)
+  | FUtailcall sig (inr id) args =>
+      fold_left Pos.max args m
+  | FUbuiltin ef args res s =>
+      fold_left Pos.max (params_of_builtin_args args)
+                (fold_left Pos.max (params_of_builtin_res res) m)
+  | FUcond cond args ifso ifnot => fold_left Pos.max args m
+  | FUjumptable arg tbl => Pos.max arg m
+  | FUreturn None => m
+  | FUreturn (Some arg) => Pos.max arg m
+  | FUgoto n => m
+  | FUpred_cf p c1 c2 => Pos.max (max_reg_cfi m c1) (max_reg_cfi m c2)
+  end.
+
+Definition regset := Regmap.t val.
+Definition predset := PMap.t bool.
+
+Definition eval_predf (pr: predset) (p: pred_op) :=
+  sat_predicate p (fun x => pr !! (Pos.of_nat x)).
+
+#[global]
+ Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf.
+Proof.
+  unfold Proper. simplify. unfold "==>".
+  intros.
+  unfold sat_equiv in *. intros. unfold eval_predf. subst. apply H0.
+Qed.
+
+#[local] Open Scope pred_op.
+
+Lemma eval_predf_Pand :
+  forall ps p p',
+    eval_predf ps (p ∧ p') = eval_predf ps p && eval_predf ps p'.
+Proof. unfold eval_predf; split; simplify; auto with bool. Qed.
+
+Lemma eval_predf_Por :
+  forall ps p p',
+    eval_predf ps (p ∨ p') = eval_predf ps p || eval_predf ps p'.
+Proof. unfold eval_predf; split; simplify; auto with bool. Qed.
+
+Lemma eval_predf_pr_equiv :
+  forall p ps ps',
+    (forall x, ps !! x = ps' !! x) ->
+    eval_predf ps p = eval_predf ps' p.
+Proof.
+  induction p; simplify; auto;
+    try (unfold eval_predf; simplify; repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
+    [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por];
+    erewrite IHp1; try eassumption; erewrite IHp2; eauto.
+Qed.
+
+Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
+  match rl, vl with
+  | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
+  | _, _ => Regmap.init Vundef
+  end.
+
+Definition bblock_body := list (list (list instr)).
+
+Record bblock : Type :=
+  mk_bblock {
+      bb_body: bblock_body;
+      bb_exit: cf_instr
+    }.
+
+Definition code: Type := PTree.t bblock.
+
+Record function: Type :=
+  mkfunction {
+      fn_sig: signature;
+      fn_params: list reg;
+      fn_stacksize: Z;
+      fn_code: code;
+      fn_funct_units: funct_unit;
+      fn_entrypoint: node;
+    }.
+
+Definition fundef := AST.fundef function.
+Definition program := AST.program fundef unit.
+
+Definition funsig (fd: fundef) :=
+  match fd with
+  | Internal f => fn_sig f
+  | External ef => ef_sig ef
+  end.
+
+Inductive stackframe : Type :=
+| Stackframe:
+  forall (res: reg)            (**r where to store the result *)
+         (f: function)         (**r calling function *)
+         (sp: val)             (**r stack pointer in calling function *)
+         (pc: node)            (**r program point in calling function *)
+         (rs: regset)          (**r register state in calling function *)
+         (pr: predset),        (**r predicate state of the calling function *)
+    stackframe.
+
+Inductive state : Type :=
+| State:
+  forall (stack: list stackframe) (**r call stack *)
+         (f: function)            (**r current function *)
+         (sp: val)                (**r stack pointer *)
+         (pc: node)               (**r current program point in [c] *)
+         (rs: regset)             (**r register state *)
+         (pr: predset)            (**r predicate register state *)
+         (m: mem),                (**r memory state *)
+    state
+| Callstate:
+  forall (stack: list stackframe) (**r call stack *)
+         (f: fundef)              (**r function to call *)
+         (args: list val)         (**r arguments to the call *)
+         (m: mem),                (**r memory state *)
+    state
+| Returnstate:
+  forall (stack: list stackframe) (**r call stack *)
+         (v: val)                 (**r return value for the call *)
+         (m: mem),                (**r memory state *)
+    state.
+
+Record instr_state := mk_instr_state {
+                         is_rs: regset;
+                         is_ps: predset;
+                         is_mem: mem;
+                       }.
+
+Definition genv := Genv.t fundef unit.
+
+Section RELSEM.
+
+  Context (ge: genv).
+
+  Definition find_function
+             (ros: reg + ident) (rs: regset) : option fundef :=
+    match ros with
+    | inl r => Genv.find_funct ge rs#r
+    | inr symb =>
+        match Genv.find_symbol ge symb with
+        | None => None
+        | Some b => Genv.find_funct_ptr ge b
+        end
+    end.
+
+  Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
+  | eval_pred_true:
+    forall i i' p,
+      eval_predf (is_ps i) p = true ->
+      eval_pred (Some p) i i' i'
+  | eval_pred_false:
+    forall i i' p,
+      eval_predf (is_ps i) p = false ->
+      eval_pred (Some p) i i' i
+  | eval_pred_none:
+    forall i i', eval_pred None i i' i.
+
+  Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop :=
+  | exec_FUnop:
+    forall sp ist,
+      step_instr sp ist FUnop ist
+  | exec_FUop:
+    forall op v res args rs m sp p ist pr,
+      eval_operation ge sp op rs##args m = Some v ->
+      eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#res <- v) pr m) ist ->
+      step_instr sp (mk_instr_state rs pr m) (FUop p op args res) ist
+  | exec_FUload:
+    forall addr rs args a chunk m v dst sp p pr ist,
+      eval_addressing ge sp addr rs##args = Some a ->
+      Mem.loadv chunk m a = Some v ->
+      eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist ->
+      step_instr sp (mk_instr_state rs pr m) (FUload p chunk addr args dst) ist
+  | exec_FUstore:
+    forall addr rs args a chunk m src m' sp p pr ist,
+      eval_addressing ge sp addr rs##args = Some a ->
+      Mem.storev chunk m a rs#src = Some m' ->
+      eval_pred p (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist ->
+      step_instr sp (mk_instr_state rs pr m) (FUstore p chunk addr args src) ist
+  | exec_FUsetpred:
+    forall sp rs pr m p c b args p' ist,
+      Op.eval_condition c rs##args m = Some b ->
+      eval_pred p' (mk_instr_state rs pr m) (mk_instr_state rs (pr#p <- b) m) ist ->
+      step_instr sp (mk_instr_state rs pr m) (FUsetpred p' c args p) ist.
+
+  Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop :=
+  | exec_RBcons:
+    forall state i state' state'' instrs sp,
+      step_instr sp state i state' ->
+      step_instr_list sp state' instrs state'' ->
+      step_instr_list sp state (i :: instrs) state''
+  | exec_RBnil:
+    forall state sp,
+      step_instr_list sp state nil state.
+
+  Inductive step_instr_seq (sp : val)
+    : instr_state -> list (list instr) -> instr_state -> Prop :=
+  | exec_instr_seq_cons:
+    forall state i state' state'' instrs,
+      step_instr_list sp state i state' ->
+      step_instr_seq sp state' instrs state'' ->
+      step_instr_seq sp state (i :: instrs) state''
+  | exec_instr_seq_nil:
+    forall state,
+      step_instr_seq sp state nil state.
+
+  Inductive step_instr_block (sp : val)
+    : instr_state -> bblock_body -> instr_state -> Prop :=
+  | exec_instr_block_cons:
+    forall state i state' state'' instrs,
+      step_instr_seq sp state i state' ->
+      step_instr_block sp state' instrs state'' ->
+      step_instr_block sp state (i :: instrs) state''
+  | exec_instr_block_nil:
+    forall state,
+      step_instr_block sp state nil state.
+
+  Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
+  | exec_FUcall:
+    forall s f sp rs m res fd ros sig args pc pc' pr,
+      find_function ros rs = Some fd ->
+      funsig fd = sig ->
+      step_cf_instr (State s f sp pc rs pr m) (FUcall sig ros args res pc')
+                    E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m)
+  | exec_FUtailcall:
+    forall s f stk rs m sig ros args fd m' pc pr,
+      find_function ros rs = Some fd ->
+      funsig fd = sig ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (FUtailcall sig ros args)
+                    E0 (Callstate s fd rs##args m')
+  | exec_FUbuiltin:
+    forall s f sp rs m ef args res pc' vargs t vres m' pc pr,
+      eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
+      external_call ef ge vargs m t vres m' ->
+      step_cf_instr (State s f sp pc rs pr m) (FUbuiltin ef args res pc')
+                    t (State s f sp pc' (regmap_setres res vres rs) pr m')
+  | exec_FUcond:
+    forall s f sp rs m cond args ifso ifnot b pc pc' pr,
+      eval_condition cond rs##args m = Some b ->
+      pc' = (if b then ifso else ifnot) ->
+      step_cf_instr (State s f sp pc rs pr m) (FUcond cond args ifso ifnot)
+                    E0 (State s f sp pc' rs pr m)
+  | exec_FUjumptable:
+    forall s f sp rs m arg tbl n pc pc' pr,
+      rs#arg = Vint n ->
+      list_nth_z tbl (Int.unsigned n) = Some pc' ->
+      step_cf_instr (State s f sp pc rs pr m) (FUjumptable arg tbl)
+                    E0 (State s f sp pc' rs pr m)
+  | exec_FUreturn:
+    forall s f stk rs m or pc m' pr,
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (FUreturn or)
+                    E0 (Returnstate s (regmap_optget or Vundef rs) m')
+  | exec_FUgoto:
+    forall s f sp pc rs pr m pc',
+      step_cf_instr (State s f sp pc rs pr m) (FUgoto pc') E0 (State s f sp pc' rs pr m)
+  | exec_FUpred_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) (FUpred_cf p cf1 cf2) t st'.
+
+  Inductive step: state -> trace -> state -> Prop :=
+  | exec_bblock:
+    forall s f sp pc rs rs' m m' t s' bb pr pr',
+      f.(fn_code)!pc = Some bb ->
+      step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') ->
+      step_cf_instr (State s f sp pc rs' pr' m') bb.(bb_exit) t s' ->
+      step (State s f sp pc rs pr m) t s'
+  | exec_function_internal:
+    forall s f args m m' stk,
+      Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
+      step (Callstate s (Internal f) args m)
+           E0 (State s
+                     f
+                     (Vptr stk Ptrofs.zero)
+                     f.(fn_entrypoint)
+                         (init_regs args f.(fn_params))
+                         (PMap.init false) m')
+  | exec_function_external:
+    forall s ef args res t m m',
+      external_call ef ge args m t res m' ->
+      step (Callstate s (External ef) args m)
+           t (Returnstate s res m')
+  | exec_return:
+    forall res f sp pc rs s vres m pr,
+      step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m)
+           E0 (State s f sp pc (rs#res <- vres) pr m).
+
+End RELSEM.
+
+Inductive initial_state (p: program): state -> Prop :=
+| initial_state_intro: forall b f m0,
+    let ge := Genv.globalenv p in
+    Genv.init_mem p = Some m0 ->
+    Genv.find_symbol ge p.(prog_main) = Some b ->
+    Genv.find_funct_ptr ge b = Some f ->
+    funsig f = signature_main ->
+    initial_state p (Callstate nil f nil m0).
+
+Inductive final_state: state -> int -> Prop :=
+| final_state_intro: forall r m,
+    final_state (Returnstate nil (Vint r) m) r.
+
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).
+
+Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) :=
+  let max_body := fold_left (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) bb.(bb_body) m in
+  max_reg_cfi max_body bb.(bb_exit).
+
+Definition max_reg_function (f: function) :=
+  Pos.max
+    (PTree.fold max_reg_bblock f.(fn_code) 1%positive)
+    (fold_left Pos.max f.(fn_params) 1%positive).
+
+Definition max_pc_function (f: function) : positive :=
+  PTree.fold (fun m pc i => (Pos.max m
+                                     (pc + match Zlength i.(bb_body)
+                                           with Z.pos p => p | _ => 1 end))%positive)
+             f.(fn_code) 1%positive.
diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v
new file mode 100644
index 0000000..389d76c
--- /dev/null
+++ b/src/hls/RTLParFUgen.v
@@ -0,0 +1,21 @@
+Require Import Coq.micromega.Lia.
+
+Require Import compcert.common.AST.
+Require compcert.common.Errors.
+Require compcert.common.Globalenvs.
+Require compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Statemonad.
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.HTL.
+Require Import vericert.hls.Predicate.
+Require Import vericert.hls.RTLParFU.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.Verilog.
+Require Import vericert.hls.RTLBlockInstr.
+Require Import vericert.hls.RTLPar.
+
+Definition transl_program (p : RTLParFU.program) : Errors.res HTL.program :=
+  transform_partial_program transl_fundef p.