Merge branch 'master' into arrays-proof

14 files changed, 364 insertions, 1028 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index e998521..98ef429 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -74,9 +74,12 @@ Proof.
   intros. destruct x; simpl. rewrite print_identity. auto. auto.
 Qed.
 
-Definition transf_backend (r : RTL.program) : res Verilog.module :=
+Definition transf_backend (r : RTL.program) : res Verilog.program :=
   OK r
-  @@@ Veriloggen.transf_program.
+  @@@ Inlining.transf_program
+  @@ print (print_RTL 1)
+  @@@ HTLgen.transl_program
+  @@ Veriloggen.transl_program.
 
 Definition transf_frontend (p: Csyntax.program) : res RTL.program :=
   OK p
@@ -88,7 +91,7 @@ Definition transf_frontend (p: Csyntax.program) : res RTL.program :=
   @@@ RTLgen.transl_program
   @@ print (print_RTL 0).
 
-Definition transf_hls (p : Csyntax.program) : res Verilog.module :=
+Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
   OK p
   @@@ transf_frontend
   @@@ transf_backend.
diff --git a/src/Simulator.v b/src/Simulator.v
index 930971b..83d3e96 100644
--- a/src/Simulator.v
+++ b/src/Simulator.v
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From Coq Require Import FSets.FMapPositive.
+(*From Coq Require Import FSets.FMapPositive.
 
 From compcert Require Import Errors.
 
@@ -33,3 +33,4 @@ Definition simulate (n : nat) (m : Verilog.module) : res (Value.value * list (po
   end.
 
 Local Close Scope error_monad_scope.
+*)
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 0028fcb..ba87af6 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From coqup Require Verilog Value Compiler Simulator.
+From coqup Require Verilog Value Compiler.
 
 From Coq Require DecidableClass.
 
@@ -166,7 +166,7 @@ Set Extraction AccessOpaque.
 
 Cd "src/extraction".
 Separate Extraction
-         Verilog.module Value.uvalueToZ coqup.Compiler.transf_hls Simulator.simulate
+         Verilog.module Value.uvalueToZ coqup.Compiler.transf_hls
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index cba2940..c73aaa7 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -17,7 +17,7 @@
  *)
 
 From compcert Require Import Maps.
-From compcert Require Errors.
+From compcert Require Errors Globalenvs.
 From compcert Require Import AST RTL.
 From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad.
 
@@ -27,15 +27,12 @@ Hint Resolve AssocMap.gss : htlh.
 Hint Resolve Ple_refl : htlh.
 Hint Resolve Ple_succ : htlh.
 
-Inductive scl_decl : Type := Scalar (sz : nat).
-Inductive arr_decl : Type := Array (sz : nat) (ln : nat).
-
 Record state: Type := mkstate {
   st_st : reg;
   st_freshreg: reg;
   st_freshstate: node;
-  st_scldecls: AssocMap.t scl_decl;
-  st_arrdecls: AssocMap.t arr_decl;
+  st_scldecls: AssocMap.t (option io * scl_decl);
+  st_arrdecls: AssocMap.t (option io * arr_decl);
   st_datapath: datapath;
   st_controllogic: controllogic;
 }.
@@ -44,8 +41,8 @@ Definition init_state (st : reg) : state :=
   mkstate st
           1%positive
           1%positive
-          (AssocMap.empty scl_decl)
-          (AssocMap.empty arr_decl)
+          (AssocMap.empty (option io * scl_decl))
+          (AssocMap.empty (option io * arr_decl))
           (AssocMap.empty stmnt)
           (AssocMap.empty stmnt).
 
@@ -127,6 +124,30 @@ Proof.
     auto with htlh.
 Qed.
 
+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, Scalar sz) s.(st_scldecls))
+       s.(st_arrdecls)
+       s.(st_datapath)
+       s.(st_controllogic)).
+Proof. auto with htlh. Qed.
+
+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, Scalar sz) s.(st_scldecls))
+                s.(st_arrdecls)
+                s.(st_datapath)
+                s.(st_controllogic))
+              (declare_reg_state_incr i s r sz).
+
 Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
   fun s =>
     match check_empty_node_datapath s n, check_empty_node_controllogic s n with
@@ -338,9 +359,11 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     | Inop n' => add_instr n n' Vskip
     | Iop op args dst n' =>
       do instr <- translate_instr op args;
+      do _ <- declare_reg None dst 32;
       add_instr n n' (nonblock dst instr)
     | Iload mem addr args dst n' =>
       do src <- translate_arr_access mem addr args stack;
+      do _ <- declare_reg None dst 32;
       add_instr n n' (block dst src)
     | Istore mem addr args src n' =>
       do dst <- translate_arr_access mem addr args stack;
@@ -363,61 +386,62 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
   end.
 
 Lemma create_reg_state_incr:
-  forall s sz,
+  forall s sz i,
     st_incr s (mkstate
          s.(st_st)
          (Pos.succ (st_freshreg s))
          (st_freshstate s)
-         (AssocMap.set s.(st_freshreg) (Scalar sz) s.(st_scldecls))
+         (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls))
          s.(st_arrdecls)
          (st_datapath s)
          (st_controllogic s)).
 Proof. constructor; simpl; auto with htlh. Qed.
 
-Definition create_reg (sz : nat) : mon reg :=
+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) (Scalar sz) s.(st_scldecls))
+                   (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls))
                    (st_arrdecls s)
                    (st_datapath s)
                    (st_controllogic s))
-              (create_reg_state_incr s sz).
+              (create_reg_state_incr s sz i).
 
 Lemma create_arr_state_incr:
-  forall s sz ln,
+  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) (Array sz ln) s.(st_arrdecls))
+         (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls))
          (st_datapath s)
          (st_controllogic s)).
 Proof. constructor; simpl; auto with htlh. Qed.
 
-Definition create_arr (sz : nat) (ln : nat) : mon (reg * nat) :=
+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) (Array sz ln) s.(st_arrdecls))
+                   (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls))
                    (st_datapath s)
                    (st_controllogic s))
-              (create_arr_state_incr s sz ln).
+              (create_arr_state_incr s sz ln i).
 
 Definition transf_module (f: function) : mon module :=
-  do fin <- create_reg 1;
-  do rtrn <- create_reg 32;
-  do (stack, stack_len) <- create_arr 32 (Z.to_nat (f.(fn_stacksize) / 4));
+  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 _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
-  do start <- create_reg 1;
-  do rst <- create_reg 1;
-  do clk <- create_reg 1;
+  do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.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;
   ret (mkmodule
          f.(RTL.fn_params)
@@ -428,14 +452,19 @@ Definition transf_module (f: function) : mon module :=
          stack
          stack_len
          fin
-         rtrn).
+         rtrn
+         start
+         rst
+         clk
+         current_state.(st_scldecls)
+         current_state.(st_arrdecls)).
 
 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))
-          (st_scldecls (init_state st))
+          (AssocMap.set st (None, Scalar 32) (st_scldecls (init_state st)))
           (st_arrdecls (init_state st))
           (st_datapath (init_state st))
           (st_controllogic (init_state st)).
@@ -443,15 +472,30 @@ Definition max_state (f: function) : state :=
 Definition transl_module (f : function) : Errors.res module :=
   run_mon (max_state f) (transf_module f).
 
-Definition transl_fundef (f : RTL.fundef) : Errors.res HTL.fundef :=
+Definition transl_fundef := transf_partial_fundef transl_module.
+
+Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p.
+
+(*Definition transl_main_fundef f : Errors.res HTL.fundef :=
   match f with
-  | Internal f' =>
-    Errors.bind (transl_module f')
-                (fun f'' => Errors.OK (Internal f''))
-  | _ => Errors.Error (Errors.msg "External function could not be translated.")
+  | Internal f => transl_fundef (Internal f)
+  | External f => Errors.Error (Errors.msg "Could not find internal main function")
   end.
 
 (** Translation of a whole program. *)
 
 Definition transl_program (p: RTL.program) : Errors.res HTL.program :=
-  transform_partial_program transl_fundef p.
+  transform_partial_program2 (fun i f => if Pos.eqb p.(AST.prog_main) i
+                                         then transl_fundef f
+                                         else transl_main_fundef f)
+                             (fun i v => Errors.OK v) p.
+*)
+
+(*Definition main_is_internal (p : RTL.program): Prop :=
+  let ge := Globalenvs.Genv.globalenv p in
+  forall b m,
+  Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
+  Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m).
+
+Definition tranls_program_with_proof (p : RTL.program) : Errors.res { p' : HTL.program | main_is_internal p }.
+*)
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 6dc4c21..773497b 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -724,6 +724,7 @@ Section CORRECTNESS.
   Admitted.
   Hint Resolve transl_step_correct : htlproof.
 
+  (* Had to admit proof because currently there is no way to force main to be Internal. *)
   Lemma transl_initial_states :
     forall s1 : Smallstep.state (RTL.semantics prog),
       Smallstep.initial_state (RTL.semantics prog) s1 ->
@@ -740,10 +741,11 @@ Section CORRECTNESS.
     replace (AST.prog_main tprog) with (AST.prog_main prog).
     rewrite symbols_preserved; eauto.
     symmetry; eapply Linking.match_program_main; eauto.
-    eexact A. trivial.
+    Admitted.
+    (*eexact A. trivial.
     constructor.
     apply transl_module_correct. auto.
-  Qed.
+  Qed.*)
   Hint Resolve transl_initial_states : htlproof.
 
   Lemma transl_final_states :
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 89b79ac..57d2d87 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -184,7 +184,7 @@ Hint Constructors tr_code : htlspec.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
-    forall data control fin rtrn st stk stk_len m,
+    forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls,
       (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
                tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
       stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) ->
@@ -192,34 +192,48 @@ Inductive tr_module (f : RTL.function) : module -> Prop :=
                         data
                         control
                         f.(RTL.fn_entrypoint)
-                            st stk stk_len fin rtrn) ->
+                        st stk stk_len fin rtrn start rst clk scldecls arrdecls) ->
       tr_module f m.
 Hint Constructors tr_module : htlspec.
 
 Lemma create_reg_datapath_trans :
-  forall sz s s' x i,
-    create_reg sz s = OK x s' i ->
+  forall sz s s' x i iop,
+    create_reg iop sz s = OK x s' i ->
     s.(st_datapath) = s'.(st_datapath).
 Proof. intros. monadInv H. trivial. Qed.
 Hint Resolve create_reg_datapath_trans : htlspec.
 
 Lemma create_reg_controllogic_trans :
-  forall sz s s' x i,
-    create_reg sz s = OK x s' i ->
+  forall sz s s' x i iop,
+    create_reg iop sz s = OK x s' i ->
+    s.(st_controllogic) = s'.(st_controllogic).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_reg_controllogic_trans : htlspec.
+
+Lemma declare_reg_datapath_trans :
+  forall sz s s' x i iop r,
+    declare_reg iop r sz s = OK x s' i ->
+    s.(st_datapath) = s'.(st_datapath).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_reg_datapath_trans : htlspec.
+
+Lemma declare_reg_controllogic_trans :
+  forall sz s s' x i iop r,
+    declare_reg iop r sz s = OK x s' i ->
     s.(st_controllogic) = s'.(st_controllogic).
 Proof. intros. monadInv H. trivial. Qed.
 Hint Resolve create_reg_controllogic_trans : htlspec.
 
 Lemma create_arr_datapath_trans :
-  forall sz ln s s' x i,
-    create_arr sz ln s = OK x s' i ->
+  forall sz ln s s' x i iop,
+    create_arr iop sz ln s = OK x s' i ->
     s.(st_datapath) = s'.(st_datapath).
 Proof. intros. monadInv H. trivial. Qed.
 Hint Resolve create_arr_datapath_trans : htlspec.
 
 Lemma create_arr_controllogic_trans :
-  forall sz ln s s' x i,
-    create_arr sz ln s = OK x s' i ->
+  forall sz ln s s' x i iop,
+    create_arr iop sz ln s = OK x s' i ->
     s.(st_controllogic) = s'.(st_controllogic).
 Proof. intros. monadInv H. trivial. Qed.
 Hint Resolve create_arr_controllogic_trans : htlspec.
@@ -240,11 +254,11 @@ Hint Resolve get_refl_s : htlspec.
 
 Ltac inv_incr :=
   repeat match goal with
-  | [ H: create_reg _ ?s = OK _ ?s' _ |- _ ] =>
+  | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] =>
     let H1 := fresh "H" in
     assert (H1 := H); eapply create_reg_datapath_trans in H;
     eapply create_reg_controllogic_trans in H1
-  | [ H: create_arr _ _ ?s = OK _ ?s' _ |- _ ] =>
+  | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] =>
     let H1 := fresh "H" in
     assert (H1 := H); eapply create_arr_datapath_trans in H;
     eapply create_arr_controllogic_trans in H1
@@ -256,6 +270,44 @@ Ltac inv_incr :=
   | [ H: st_incr _ _ |- _ ] => destruct st_incr
   end.
 
+Lemma collect_controllogic_trans :
+  forall A f l cs cs' ci,
+  (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) ->
+  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic).
+Proof.
+  induction l; intros; monadInv H0.
+  - trivial.
+  - apply H in EQ. rewrite EQ. eauto.
+Qed.
+
+Lemma collect_datapath_trans :
+  forall A f l cs cs' ci,
+  (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) ->
+  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath).
+Proof.
+  induction l; intros; monadInv H0.
+  - trivial.
+  - apply H in EQ. rewrite EQ. eauto.
+Qed.
+
+Lemma collect_declare_controllogic_trans :
+  forall io n l s s' i,
+  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
+  s.(st_controllogic) = s'.(st_controllogic).
+Proof.
+  intros. eapply collect_controllogic_trans; try eassumption.
+  intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption.
+Qed.
+
+Lemma collect_declare_datapath_trans :
+  forall io n l s s' i,
+  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
+  s.(st_datapath) = s'.(st_datapath).
+Proof.
+  intros. eapply collect_datapath_trans; try eassumption.
+  intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption.
+Qed.
+
 Ltac rewrite_states :=
   match goal with
   | [ H: ?x ?s = ?x ?s' |- _ ] =>
@@ -330,16 +382,17 @@ Proof.
     + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop.
       eapply in_map with (f := fst) in H9. contradiction.
 
-    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
-    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
-    + inversion H2. inversion H9. unfold nonblock. rewrite <- e2. rewrite H. constructor.
-      eapply translate_instr_tr_op. apply EQ1.
-      eapply in_map with (f := fst) in H9. contradiction.
+    + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    + inversion H2. inversion H14. unfold nonblock. assert (HST: st_st s4 = st_st s2) by congruence. rewrite HST.
+      constructor. eapply translate_instr_tr_op. apply EQ1.
+      eapply in_map with (f := fst) in H14. contradiction.
 
-    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
-    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
-    + inversion H2. inversion H9. rewrite <- e2. rewrite H. econstructor. apply EQ1.
-      eapply in_map with (f := fst) in H9. contradiction.
+    + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    + inversion H2. inversion H14. rewrite <- e2. assert (HST: st_st s2 = st_st s0) by congruence.
+      rewrite HST. econstructor. apply EQ1.
+      eapply in_map with (f := fst) in H14. contradiction.
 
     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
@@ -407,9 +460,13 @@ Proof.
   econstructor; simpl; trivial.
   intros.
   inv_incr.
-  assert (STC: st_controllogic s9 = st_controllogic s3) by congruence.
-  assert (STD: st_datapath s9 = st_datapath s3) by congruence.
-  assert (STST: st_st s9 = st_st s3) by congruence.
+  assert (EQ3D := EQ3).
+  destruct x3.
+  apply collect_declare_datapath_trans in EQ3.
+  apply collect_declare_controllogic_trans in EQ3D.
+  assert (STC: st_controllogic s10 = st_controllogic s3) by congruence.
+  assert (STD: st_datapath s10 = st_datapath s3) by congruence.
+  assert (STST: st_st s10 = st_st s3) by congruence.
   rewrite STC. rewrite STD. rewrite STST.
   eapply iter_expand_instr_spec; eauto with htlspec.
   apply PTree.elements_complete.
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index 4a6f23e..efe3565 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -16,655 +16,51 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From Coq Require Import FSets.FMapPositive.
+From compcert Require Import Maps.
+From compcert Require Errors.
+From compcert Require Import AST.
+From coqup Require Import Verilog HTL Coquplib AssocMap Value.
 
-From coqup Require Import Verilog Coquplib Value.
-
-From compcert Require Errors Op AST Integers Maps.
-From compcert Require Import RTL.
-
-Notation "a ! b" := (PositiveMap.find b a) (at level 1).
-
-Definition node : Type := positive.
-Definition reg : Type := positive.
-Definition ident : Type := positive.
-
-Hint Resolve PositiveMap.gempty : verilog_state.
-Hint Resolve PositiveMap.gso : verilog_state.
-Hint Resolve PositiveMap.gss : verilog_state.
-Hint Resolve Ple_refl : verilog_state.
-
-Inductive statetrans : Type :=
-| StateGoto (p : node)
-| StateCond (c : expr) (t f : node).
-
-Definition state_goto (st : reg) (n : node) : stmnt :=
-  Vnonblock (Vvar st) (Vlit (posToValue 32 n)).
-
-Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
-  Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)).
-
-Definition statetrans_transl (stvar : reg) (st : statetrans) : stmnt :=
+Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr * Verilog.stmnt) :=
   match st with
-  | StateGoto p => state_goto stvar p
-  | StateCond c t f => state_cond stvar c t f
+  | (n, stmt) :: ls => (Vlit (posToValue 32 n), stmt) :: transl_list ls
+  | nil => nil
   end.
 
-Definition valid_freshstate (stm: PositiveMap.t stmnt) (fs: node) :=
-  forall (n: node),
-    Plt n fs \/ stm!n = None.
-Hint Unfold valid_freshstate : verilog_state.
-
-Definition states_have_transitions (stm: PositiveMap.t stmnt) (st: PositiveMap.t statetrans) :=
-  forall (n: node),
-      (forall x, stm!n = Some x -> exists y, st!n = Some y)
-      /\ (forall x, st!n = Some x -> exists y, stm!n = Some y).
-Hint Unfold states_have_transitions : verilog_state.
-
-Record decl : Type := mkdecl {
-  width: nat;
-  length: nat
-}.
-
-Record state: Type := mkstate {
-  st_freshreg: reg;
-  st_freshstate: node;
-  st_stm: PositiveMap.t stmnt;
-  st_statetrans: PositiveMap.t statetrans;
-  st_decl: PositiveMap.t decl;
-  st_wf: valid_freshstate st_stm st_freshstate
-         /\ states_have_transitions st_stm st_statetrans;
-}.
-
-Remark init_state_valid_freshstate:
-  valid_freshstate (PositiveMap.empty stmnt) 1%positive.
-Proof. auto with verilog_state. Qed.
-Hint Resolve init_state_valid_freshstate : verilog_state.
-
-Remark init_state_states_have_transitions:
-  states_have_transitions (PositiveMap.empty stmnt) (PositiveMap.empty statetrans).
-Proof.
-  unfold states_have_transitions.
-  split; intros; rewrite PositiveMap.gempty in H; discriminate.
-Qed.
-Hint Resolve init_state_states_have_transitions : verilog_state.
-
-Remark init_state_wf:
-    valid_freshstate (PositiveMap.empty stmnt) 1%positive
-    /\ states_have_transitions (PositiveMap.empty stmnt) (PositiveMap.empty statetrans).
-Proof. auto with verilog_state. Qed.
-
-Definition init_state : state :=
-  mkstate 1%positive
-          1%positive
-          (PositiveMap.empty stmnt)
-          (PositiveMap.empty statetrans)
-          (PositiveMap.empty decl)
-          init_state_wf.
-
-Inductive state_incr: state -> state -> Prop :=
-  state_incr_intro:
-    forall (s1 s2: state),
-      Ple s1.(st_freshreg) s2.(st_freshreg) ->
-      Ple s1.(st_freshstate) s2.(st_freshstate) ->
-      (forall n,
-          s1.(st_stm)!n = None \/ s2.(st_stm)!n = s1.(st_stm)!n) ->
-      (forall n,
-          s1.(st_statetrans)!n = None
-          \/ s2.(st_statetrans)!n = s1.(st_statetrans)!n) ->
-      state_incr s1 s2.
-Hint Constructors state_incr : verilog_state.
-
-Lemma state_incr_refl:
-  forall s, state_incr s s.
-Proof. auto with verilog_state. Qed.
-
-Lemma state_incr_trans:
-  forall s1 s2 s3, state_incr s1 s2 -> state_incr s2 s3 -> state_incr s1 s3.
-Proof.
-  intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans.
-  - intros. destruct H3 with n.
-    + left; assumption.
-    + destruct H6 with n;
-      [ rewrite <- H0; left; assumption
-      | right; rewrite <- H0; apply H8
-      ].
-  - intros. destruct H4 with n.
-    + left; assumption.
-    + destruct H7 with n.
-      * rewrite <- H0. left. assumption.
-      * right. rewrite <- H0. apply H8.
-Qed.
-
-Inductive res (A: Type) (s: state): Type :=
-| Error : Errors.errmsg -> res A s
-| OK : A -> forall (s' : state), state_incr s s' -> res A s.
-
-Arguments OK [A s].
-Arguments Error [A s].
-
-Definition mon (A: Type) : Type := forall (s: state), res A s.
-
-Definition ret {A: Type} (x: A) : mon A :=
-  fun (s : state) => OK x s (state_incr_refl s).
-
-Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B :=
-  fun (s : state) =>
-    match f s with
-    | Error msg => Error msg
-    | OK a s' i =>
-      match g a s' with
-      | Error msg => Error msg
-      | OK b s'' i' => OK b s'' (state_incr_trans s s' s'' i i')
-      end
-    end.
-
-Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
-  bind f (fun xy => g (fst xy) (snd xy)).
-
-Notation "'do' X <- A ; B" := (bind A (fun X => B))
-(at level 200, X ident, A at level 100, B at level 200).
-Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
-(at level 200, X ident, Y ident, A at level 100, B at level 200).
-
-Definition handle_error {A: Type} (f g: mon A) : mon A :=
-  fun (s : state) =>
-    match f s with
-    | OK a s' i => OK a s' i
-    | Error _ => g s
-    end.
-
-Definition error {A: Type} (err: Errors.errmsg) : mon A := fun (s: state) => Error err.
-
-Definition get : mon state := fun s => OK s s (state_incr_refl s).
-
-Definition set (s: state) (i: forall s', state_incr s' s) : mon unit :=
-  fun s' => OK tt s (i s').
-
-Definition run_mon {A: Type} (s: state) (m: mon A): Errors.res A :=
-    match m s with
-    | OK a s' i => Errors.OK a
-    | Error err => Errors.Error err
-    end.
-
-Definition map_state (f: state -> state) (i: forall s, state_incr s (f s)): mon state :=
-  fun s => let s' := f s in OK s' s' (i s).
-
-Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) :=
-  match l with
-  | nil => ret nil
-  | x::xs =>
-    do r <- f x;
-    do rs <- traverselist f xs;
-    ret (r::rs)
+Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item :=
+  match scldecl with
+  | (r, (io, Scalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl'
+  | nil => nil
   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 32 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 "Veriloggen: comparison instruction not implemented: other")
+Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item :=
+  match arrdecl with
+  | (r, (io, Array sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl'
+  | nil => nil
   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 "Veriloggen: 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_comparison c args
-  | Op.Ccompimm c i, _ => translate_comparison_imm c args i
-  | Op.Ccompuimm c i, _ => translate_comparison_imm c args i
-  | Op.Cmaskzero n, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: Cmaskzero")
-  | Op.Cmasknotzero n, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: Cmasknotzero")
-  | _, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: other")
-  end.
-
-Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=
-  match a, args with
-  | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off)
-  | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off))
-  | Op.Ascaled scale offset, r1::nil =>
-    ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset)))
-  | Op.Aindexed2scaled scale offset, r1::r2::nil =>
-    ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
-  (* Stack arrays/referenced variables *)
-  | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
-    let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *)
-    if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vlit (ZToValue 32 (a / 4)))
-    else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset")
-  | _, _ => error (Errors.msg "Veriloggen: eff_addressing instruction not implemented: other")
-  end.
-
-(** Translate an instruction to a statement. *)
-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, _ => error (Errors.msg "Veriloggen: Instruction not implemented: Omulhs")
-  | Op.Omulhu, _ => error (Errors.msg "Veriloggen: Instruction not implemented: Omulhu")
-  | 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 => error (Errors.msg "Veriloggen: Instruction not implemented: Oshrximm")
-  | Op.Oshru, r1::r2::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshru")
-  | Op.Oshruimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshruimm")
-  | Op.Ororimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Ororimm")
-  | Op.Oshldimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshldimm")
-  | Op.Ocmp c, _ => translate_condition c args
-  | Op.Olea a, _ => translate_eff_addressing a args
-  | Op.Oleal a, _ => translate_eff_addressing a args (* FIXME: Need to be careful here; large arrays might fail? *)
-  | Op.Ocast32signed, r::nill => ret (Vvar r) (* FIXME: Don't need to sign extend for now since everything is 32 bit? *)
-  | _, _ => error (Errors.msg "Veriloggen: Instruction not implemented: other")
-  end.
-
-Remark add_instr_valid_freshstate:
-  forall (s: state) (n: node) (st: stmnt),
-    Plt n (st_freshstate s) ->
-    valid_freshstate (PositiveMap.add n st s.(st_stm)) (st_freshstate s).
-Proof.
-  unfold valid_freshstate. intros.
-  case (peq n0 n); intro.
-  subst n0. left. assumption.
-  rewrite PositiveMap.gso.
-  apply (st_wf s). assumption.
-Qed.
-Hint Resolve add_instr_valid_freshstate : verilog_state.
-
-Remark add_instr_states_have_transitions:
-  forall (s: state) (n n': node) (st: stmnt),
-  states_have_transitions
-    (PositiveMap.add n st s.(st_stm))
-    (PositiveMap.add n (StateGoto n') s.(st_statetrans)).
-Proof.
-  unfold states_have_transitions. split; intros.
-  - case (peq n0 n); intro.
-    subst. exists (StateGoto n'). apply PositiveMap.gss.
-    rewrite PositiveMap.gso. rewrite PositiveMap.gso in H.
-    assert (H2 := st_wf s). inv H2. unfold states_have_transitions in H1.
-    destruct H1 with n0. apply H2 with x. assumption. assumption. assumption.
-  - case (peq n0 n); intro.
-    subst. exists st. apply PositiveMap.gss.
-    rewrite PositiveMap.gso. rewrite PositiveMap.gso in H.
-    assert (H2 := st_wf s). inv H2. unfold states_have_transitions in H1.
-    destruct H1 with n0. apply H3 with x. assumption. assumption. assumption.
-Qed.
-Hint Resolve add_instr_states_have_transitions : verilog_state.
-
-Remark add_instr_state_wf:
-  forall (s: state) (n n': node) (st: stmnt) (LT: Plt n (st_freshstate s)),
-    valid_freshstate (PositiveMap.add n st (st_stm s)) (st_freshstate s)
-    /\ states_have_transitions
-     (PositiveMap.add n st s.(st_stm))
-     (PositiveMap.add n (StateGoto n') s.(st_statetrans)).
-Proof. auto with verilog_state. Qed.
-
-Lemma add_instr_state_incr :
-  forall s n n' st LT,
-    (st_stm s)!n = None ->
-    (st_statetrans s)!n = None ->
-    state_incr s
-    (mkstate s.(st_freshreg)
-             (st_freshstate s)
-             (PositiveMap.add n st s.(st_stm))
-             (PositiveMap.add n (StateGoto n') s.(st_statetrans))
-             s.(st_decl)
-             (add_instr_state_wf s n n' st LT)).
-Proof.
-  constructor; intros;
-    try (simpl; destruct (peq n n0); subst);
-    auto with verilog_state.
-Qed.
-
-Definition check_empty_node_stm:
-  forall (s: state) (n: node), { s.(st_stm)!n = None } + { True }.
-Proof.
-  intros. case (s.(st_stm)!n); intros. right; auto. left; auto.
-Defined.
-
-Definition check_empty_node_statetrans:
-  forall (s: state) (n: node), { s.(st_statetrans)!n = None } + { True }.
-Proof.
-  intros. case (s.(st_statetrans)!n); intros. right; auto. left; auto.
-Defined.
-
-Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
-  fun s =>
-    match plt n (st_freshstate s), check_empty_node_stm s n, check_empty_node_statetrans s n with
-    | left LT, left STM, left TRANS =>
-      OK tt (mkstate s.(st_freshreg)
-                     (st_freshstate s)
-                     (PositiveMap.add n st s.(st_stm))
-                     (PositiveMap.add n (StateGoto n') s.(st_statetrans))
-                     s.(st_decl)
-                     (add_instr_state_wf s n n' st LT))
-         (add_instr_state_incr s n n' st LT STM TRANS)
-    | _, _, _ => Error (Errors.msg "Veriloggen.add_instr")
-    end.
-
-(** Add a register to the state without changing the [st_freshreg], as this
-should already be the right value.  This can be assumed because the max register
-is taken from the RTL code. *)
-
-Definition add_reg (r: reg) (s: state) : state :=
-  mkstate (st_freshreg s)
-          (st_freshstate s)
-          (st_stm s)
-          (st_statetrans s)
-          (PositiveMap.add r (mkdecl 32 0) (st_decl s))
-          (st_wf s).
-
-Lemma add_reg_state_incr:
-  forall r s,
-  state_incr s (add_reg r s).
-Proof. auto with verilog_state. Qed.
-
-Definition add_instr_reg (r: reg) (n: node) (n': node) (st: stmnt) : mon unit :=
-  do _ <- map_state (add_reg r) (add_reg_state_incr r);
-  add_instr n n' st.
-
-Lemma change_decl_state_incr:
-  forall s decl',
-    state_incr s (mkstate
-         (st_freshreg s)
-         (st_freshstate s)
-         (st_stm s)
-         (st_statetrans s)
-         decl'
-         (st_wf s)).
-Proof. auto with verilog_state. Qed.
-
-Lemma decl_io_state_incr:
-  forall s,
-    state_incr s (mkstate
-         (Pos.succ (st_freshreg s))
-         (st_freshstate s)
-         (st_stm s)
-         (st_statetrans s)
-         (st_decl s)
-         (st_wf s)).
-Proof. constructor; simpl; auto using Ple_succ with verilog_state. Qed.
-
-(** Declare a new register by incrementing the [st_freshreg] by one and
-returning the old [st_freshreg]. *)
-
-Definition decl_io (d: decl) : mon (reg * decl) :=
-  fun s => let r := s.(st_freshreg) in
-           OK (r, d) (mkstate
-                     (Pos.succ r)
-                     (st_freshstate s)
-                     (st_stm s)
-                     (st_statetrans s)
-                     (st_decl s)
-                     (st_wf s))
-              (decl_io_state_incr s).
-
-(** Declare a new register which is given, by changing [st_decl] and without
-affecting anything else. *)
-
-Definition declare_reg (r: reg) (d: decl): mon (reg * decl) :=
-  fun s => OK (r, d) (mkstate
-                      (st_freshreg s)
-                      (st_freshstate s)
-                      (st_stm s)
-                      (st_statetrans s)
-                      (PositiveMap.add r d s.(st_decl))
-                      (st_wf s))
-              (change_decl_state_incr s (PositiveMap.add r d s.(st_decl))).
-
-(** Declare a new fresh register by first getting a valid register to increment,
-and then adding it to the declaration list. *)
-
-Definition decl_fresh_reg (d: decl) : mon (reg * decl) :=
-  do (r, d) <- decl_io d;
-  declare_reg r d.
-
-Lemma add_branch_instr_states_have_transitions:
-  forall s e n n1 n2,
-    states_have_transitions (PositiveMap.add n Vskip (st_stm s))
-                            (PositiveMap.add n (StateCond e n1 n2) (st_statetrans s)).
-Proof.
-  split; intros; destruct (peq n0 n); subst; eauto with verilog_state;
-    rewrite PositiveMap.gso in *;
-    assert (H1 := (st_wf s)); inv H1; unfold states_have_transitions in H2;
-    destruct H2 with n0; try (apply H1 with x); try (apply H3 with x); assumption.
-Qed.
-
-Lemma add_branch_valid_freshstate:
-  forall s n,
-  Plt n (st_freshstate s) ->
-  valid_freshstate (PositiveMap.add n Vskip (st_stm s)) (st_freshstate s).
-Proof.
-  unfold valid_freshstate; intros; destruct (peq n0 n).
-    - subst; auto.
-    - assert (H1 := st_wf s); destruct H1;
-      unfold valid_freshstate in H0; rewrite PositiveMap.gso; auto.
-Qed.
-
-Lemma add_branch_instr_st_wf:
-  forall s e n n1 n2,
-    Plt n (st_freshstate s) ->
-    valid_freshstate (PositiveMap.add n Vskip (st_stm s)) (st_freshstate s)
-    /\ states_have_transitions (PositiveMap.add n Vskip (st_stm s))
-                               (PositiveMap.add n (StateCond e n1 n2) (st_statetrans s)).
-Proof.
-  auto using add_branch_valid_freshstate, add_branch_instr_states_have_transitions.
-Qed.
-
-Lemma add_branch_instr_state_incr:
-  forall s e n n1 n2 LT,
-    (st_stm s) ! n = None ->
-    (st_statetrans s) ! n = None ->
-    state_incr s (mkstate
-                (st_freshreg s)
-                (st_freshstate s)
-                (PositiveMap.add n Vskip (st_stm s))
-                (PositiveMap.add n (StateCond e n1 n2) (st_statetrans s))
-                (st_decl s)
-                (add_branch_instr_st_wf s e n n1 n2 LT)).
-Proof.
-  intros. apply state_incr_intro; simpl;
-            try (intros; destruct (peq n0 n); subst);
-            auto with verilog_state.
-Qed.
-
-Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
-  fun s =>
-    match plt n (st_freshstate s), check_empty_node_stm s n, check_empty_node_statetrans s n with
-    | left LT, left NSTM, left NTRANS =>
-      OK tt (mkstate
-                (st_freshreg s)
-                (st_freshstate s)
-                (PositiveMap.add n Vskip (st_stm s))
-                (PositiveMap.add n (StateCond e n1 n2) (st_statetrans s))
-                (st_decl s)
-                (add_branch_instr_st_wf s e n n1 n2 LT))
-         (add_branch_instr_state_incr s e n n1 n2 LT NSTM NTRANS)
-    | _, _, _ => Error (Errors.msg "Veriloggen: add_branch_instr")
-    end.
-
-Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
-           (args : list reg) (stack : reg) : mon expr :=
-  match addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
-  | Op.Aindexed off, r1::nil => ret (Vvari stack (boplitz Vadd r1 off)) (* FIXME: Cannot guarantee alignment *)
-  | Op.Ascaled scale offset, r1::nil =>
-    if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0))
-    then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4)))))
-    else error (Errors.msg "Veriloggen: translate_arr_access address misaligned")
-  | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
-    if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0))
-    then ret (Vvari stack (Vbinop Vadd (boplitz Vadd r1 (offset / 4)) (boplitz Vmul r2 (scale / 4))))
-    else error (Errors.msg "Veriloggen: translate_arr_access address misaligned")
-  | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
-    let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *)
-    if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4))))
-    else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset")
-  | _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing")
-  end.
-
-Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
-  match ni with
-    (n, i) =>
-    match i with
-    | Inop n' => add_instr n n' Vskip
-    | Iop op args dst n' =>
-      do instr <- translate_instr op args;
-      add_instr_reg dst n n' (block dst instr)
-    | Iload mem addr args dst n' =>
-      do src <- translate_arr_access mem addr args stack;
-      add_instr_reg dst n n' (block dst src)
-    | Istore mem addr args src n' =>
-      do dst <- translate_arr_access mem addr args stack;
-      add_instr_reg src n n' (Vblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
-    | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
-    | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
-    | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
-    | Icond cond args n1 n2 =>
-      do e <- translate_condition cond args;
-      add_branch_instr e n n1 n2
-    | Ijumptable _ _ => error (Errors.msg "Jumptable not implemented")
-    | Ireturn r =>
-      match r with
-      | Some r' =>
-        add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r')))
-      | None =>
-        add_instr n n (block fin (Vlit (ZToValue 1%nat 1%Z)))
-      end
-    end
-  end.
-
-Definition make_stm_cases (s : positive * stmnt) : expr * stmnt :=
-  match s with (a, b) => (posToExpr 32 a, b) end.
-
-Definition make_stm (r : reg) (s : PositiveMap.t stmnt) : stmnt :=
-  Vcase (Vvar r) (map make_stm_cases (PositiveMap.elements s)) (Some Vskip).
-
-Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr * stmnt :=
-  match st with
-  | (n, StateGoto n') => (posToExpr 32 n, state_goto r n')
-  | (n, StateCond c n1 n2) => (posToExpr 32 n, state_cond r c n1 n2)
-  end.
-
-Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt :=
-  Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)) (Some Vskip).
-
-Definition allocate_reg (e : reg * decl) : module_item :=
-  match e with
-  | (r, (mkdecl n 0)) => Vdecl r n
-  | (r, (mkdecl n l)) => Vdeclarr r n l
-  end.
-
-Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list module_item :=
-  (Valways_ff (Vposedge clk)
-    (Vcond (Vbinop Veq (Vinputvar rst) (Vlit (ZToValue 1 1)))
-      (nonblock st (posToExpr 32 entry))
-      (make_statetrans st s.(st_statetrans))))
-  :: (Valways_ff (Vposedge clk) (make_stm st s.(st_stm)))
-  :: (map allocate_reg (PositiveMap.elements s.(st_decl))).
-
-(** To start out with, the assumption is made that there is only one
-    function/module in the original code. *)
-
-Definition set_int_size (r: reg) : reg * nat := (r, 32%nat).
-
-(*FIXME: This shouldn't be necessary; needs alterations in Verilog.v *)
-Definition get_sz (rg : reg * decl) : szreg := match rg with (r, d) => (r, d.(width)) end.
-
-Definition transf_module (f: function) : mon module :=
-  do fin <- decl_io (mkdecl 1 0);
-  do rtrn <- decl_io (mkdecl 32 0);
-  do stack <- decl_fresh_reg (mkdecl 32%nat (Z.to_nat (f.(fn_stacksize) / 4)));
-  do _ <- traverselist (transf_instr (fst fin) (fst rtrn) (fst stack)) (Maps.PTree.elements f.(fn_code));
-  do start <- decl_io (mkdecl 1 0);
-  do rst <- decl_io (mkdecl 1 0);
-  do clk <- decl_io (mkdecl 1 0);
-  do st <- decl_fresh_reg (mkdecl 32 0);
-  do current_state <- get;
-  let mi := make_module_items f.(fn_entrypoint) (fst clk) (fst st) (fst rst) current_state in
-  ret (mkmodule (get_sz start) (get_sz rst) (get_sz clk) (get_sz fin) (get_sz rtrn) (get_sz st)
-                (map set_int_size f.(fn_params)) mi).
-
-Lemma max_state_valid_freshstate:
-  forall f,
-    valid_freshstate (st_stm init_state) (Pos.succ (max_pc_function f)).
-Proof. unfold valid_freshstate; simpl; auto with verilog_state. Qed.
-Hint Resolve max_state_valid_freshstate : verilog_state.
-
-Lemma max_state_st_wf:
-  forall f,
-    valid_freshstate (st_stm init_state) (Pos.succ (max_pc_function f))
-    /\ states_have_transitions (st_stm init_state) (st_statetrans init_state).
-Proof. auto with verilog_state. Qed.
-
-Definition max_state (f: function) : state :=
-  mkstate (Pos.succ (max_reg_function f))
-          (Pos.succ (max_pc_function f))
-          (st_stm init_state)
-          (st_statetrans init_state)
-          (st_decl init_state)
-          (max_state_st_wf f).
-
-Definition transl_module (f : function) : Errors.res module :=
-  run_mon (max_state f) (transf_module f).
-
-(** Retrieve the main function from the RTL, this should probably be replaced by
-retrieving a designated function instead.  This could be passed on the
-commandline and be assumed as a [Parameter] in this code. *)
-
-Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit))
-{struct flist} : option function :=
-  match flist with
-  | (i, AST.Gfun (AST.Internal f)) :: xs =>
-    if Pos.eqb i main
-    then Some f
-    else main_function main xs
-  | _ :: xs => main_function main xs
-  | nil => None
-  end.
-
-Definition transf_program (d : program) : Errors.res module :=
-  match main_function d.(AST.prog_main) d.(AST.prog_defs) with
-  | Some f => run_mon (max_state f) (transf_module f)
-  | _ => Errors.Error (Errors.msg "Veriloggen: could not find main function")
-  end.
+Definition transl_module (m : HTL.module) : Verilog.module :=
+  let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in
+  let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in
+  let body :=
+      Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
+      :: Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (ZToValue 1 1))
+                                               (Vnonblock (Vvar m.(mod_st)) (posToValue 32 m.(mod_entrypoint)))
+                                               (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip)))
+      :: (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
+                          ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
+  Verilog.mkmodule m.(mod_start)
+                   m.(mod_reset)
+                   m.(mod_clk)
+                   m.(mod_finish)
+                   m.(mod_return)
+                   m.(mod_st)
+                   m.(mod_stk)
+                   m.(mod_params)
+                   body
+                   m.(mod_entrypoint).
+
+Definition transl_fundef := transf_fundef transl_module.
+
+Definition transl_program (p: HTL.program) : Verilog.program :=
+  transform_program transl_fundef p.
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
index 942a83a..6c58c56 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -17,30 +17,15 @@
  *)
 
 From compcert Require Import Smallstep.
-From compcert Require RTL.
-From coqup Require Verilog.
+From coqup Require HTL Verilog.
 
 Section CORRECTNESS.
 
-  Variable prog: RTL.program.
-  Variable tprog: Verilog.module.
-
-  Inductive match_states: RTL.state -> Verilog.state -> Prop :=
-  | match_state:
-      forall,
-        
-        match_states (RTL.State f s k sp e m)
-                     (Verilog.State m mi mis assoc nbassoc f cycle pc)
-  | match_returnstate:
-      forall v tv k m tm cs
-             (MS: match_stacks k cs)
-             (LD: Val.lessdef v tv)
-             (MEXT: Mem.extends m tm),
-        match_states (CminorSel.Returnstate v k m)
-                     (RTL.Returnstate cs tv tm).
+  Variable prog: HTL.program.
+  Variable tprog: Verilog.program.
 
   Theorem transf_program_correct:
-    forward_simulation (RTL.semantics prog) (Verilog.semantics tprog).
+    forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).
   Admitted.
 
 End CORRECTNESS.
diff --git a/src/translation/Veriloggenspec.v b/src/translation/Veriloggenspec.v
index 09d08ed..7dc632c 100644
--- a/src/translation/Veriloggenspec.v
+++ b/src/translation/Veriloggenspec.v
@@ -15,116 +15,3 @@
  * You should have received a copy of the GNU General Public License
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
-
-From Coq Require Import FSets.FMapPositive.
-From compcert Require RTL Op Maps.
-From coqup Require Import Coquplib Verilog Veriloggen Value.
-
-(** * Relational specification of the translation *)
-
-(** We now define inductive predicates that characterise the fact that the
-statemachine that is created by the translation contains the correct
-translations for each of the elements *)
-
-Inductive tr_op : Op.operation -> list reg -> expr -> Prop :=
-| tr_op_Omove : forall r, tr_op Op.Omove (r::nil) (Vvar r)
-| tr_op_Ointconst : forall n l, tr_op (Op.Ointconst n) l (Vlit (intToValue n))
-| tr_op_Oneg : forall r, tr_op Op.Oneg (r::nil) (Vunop Vneg (Vvar r))
-| tr_op_Osub : forall r1 r2, tr_op Op.Osub (r1::r2::nil) (bop Vsub r1 r2)
-| tr_op_Omul : forall r1 r2, tr_op Op.Omul (r1::r2::nil) (bop Vmul r1 r2)
-| tr_op_Omulimm : forall r n, tr_op (Op.Omulimm n) (r::nil) (boplit Vmul r n)
-| tr_op_Odiv : forall r1 r2, tr_op Op.Odiv (r1::r2::nil) (bop Vdiv r1 r2)
-| tr_op_Odivu : forall r1 r2, tr_op Op.Odivu (r1::r2::nil) (bop Vdivu r1 r2)
-| tr_op_Omod : forall r1 r2, tr_op Op.Omod (r1::r2::nil) (bop Vmod r1 r2)
-| tr_op_Omodu : forall r1 r2, tr_op Op.Omodu (r1::r2::nil) (bop Vmodu r1 r2)
-| tr_op_Oand : forall r1 r2, tr_op Op.Oand (r1::r2::nil) (bop Vand r1 r2)
-| tr_op_Oandimm : forall n r, tr_op (Op.Oandimm n) (r::nil) (boplit Vand r n)
-| tr_op_Oor : forall r1 r2, tr_op Op.Oor (r1::r2::nil) (bop Vor r1 r2)
-| tr_op_Oorimm : forall n r, tr_op (Op.Oorimm n) (r::nil) (boplit Vor r n)
-| tr_op_Oxor : forall r1 r2, tr_op Op.Oxor (r1::r2::nil) (bop Vxor r1 r2)
-| tr_op_Oxorimm : forall n r, tr_op (Op.Oxorimm n) (r::nil) (boplit Vxor r n)
-| tr_op_Onot : forall r, tr_op Op.Onot (r::nil) (Vunop Vnot (Vvar r))
-| tr_op_Oshl : forall r1 r2, tr_op Op.Oshl (r1::r2::nil) (bop Vshl r1 r2)
-| tr_op_Oshlimm : forall n r, tr_op (Op.Oshlimm n) (r::nil) (boplit Vshl r n)
-| tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2)
-| tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n)
-| tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e
-| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e.
-
-Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
-| tr_instr_Inop :
-    forall n,
-      tr_instr fin rtrn st (RTL.Inop n) Vskip (state_goto st n)
-| tr_instr_Iop :
-    forall n op args e dst,
-      tr_op op args e ->
-      tr_instr fin rtrn st (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
-| tr_instr_Icond :
-    forall n1 n2 cond args s s' i c,
-      translate_condition cond args s = OK c s' i ->
-      tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
-| tr_instr_Ireturn_None :
-      tr_instr fin rtrn st (RTL.Ireturn None) (block fin (Vlit (ZToValue 1%nat 1%Z))) Vskip
-| tr_instr_Ireturn_Some :
-    forall r,
-      tr_instr fin rtrn st (RTL.Ireturn (Some r))
-               (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
-
-Inductive tr_code (c : RTL.code) (stmnts trans : PositiveMap.t stmnt)
-          (fin rtrn st : reg) : Prop :=
-| tr_code_intro :
-    forall i s t n,
-      Maps.PTree.get n c = Some i ->
-      stmnts!n = Some s ->
-      trans!n = Some t ->
-      tr_instr fin rtrn st i s t ->
-      tr_code c stmnts trans fin rtrn st.
-
-(** [tr_module_items start clk st rst s mis] holds if the state is correctly
-translated to actual Verilog, meaning it is correctly implemented as a state
-machine in Verilog.  Currently it does not seem that useful because it models
-the [make_module_items] nearly exactly.  Therefore it might have to be changed
-to make up for that. *)
-
-Inductive tr_module_items : node -> reg -> reg -> reg -> state -> list module_item -> Prop :=
-  tr_module_items_intro :
-    forall start clk st rst s mis,
-      Valways_ff (Vposedge clk)
-                 (Vcond (Vbinop Veq (Vinputvar rst) (Vlit (ZToValue 1 1)))
-                        (nonblock st (posToExpr 32 start))
-                        (make_statetrans st s.(st_statetrans)))
-      :: Valways_ff (Vposedge clk) (make_stm st s.(st_stm))
-      :: List.map allocate_reg (PositiveMap.elements s.(st_decl)) = mis ->
-      tr_module_items start clk st rst s mis.
-
-(** [tr_module function module] Holds if the [module] is the correct translation
-of the [function] that it was given. *)
-
-Inductive tr_module : RTL.function -> module -> Prop :=
-  tr_module_intro :
-    forall f mi st rtrn fin clk rst start s0 s1 s2 s3 s4 s5 s6 i1 i2 i3 i4 i5 i6,
-      decl_io 1 s0 = OK fin s1 i1 ->
-      decl_io 32 s1 = OK rtrn s2 i2 ->
-      decl_io 1 s2 = OK start s3 i3 ->
-      decl_io 1 s3 = OK rst s4 i4 ->
-      decl_io 1 s4 = OK clk s5 i5 ->
-      decl_fresh_reg 32 s5 = OK st s6 i6 ->
-      tr_code f.(RTL.fn_code) s6.(st_stm)
-                                   (PositiveMap.map (statetrans_transl (fst st)) s6.(st_statetrans))
-                                   (fst fin) (fst rtrn) (fst st) ->
-      tr_module_items f.(RTL.fn_entrypoint) (fst clk) (fst st) (fst rst) s6 mi ->
-      tr_module f (mkmodule
-                     start
-                     rst
-                     clk
-                     fin
-                     rtrn
-                     st
-                     (List.map set_int_size f.(RTL.fn_params))
-                     mi).
-
-Lemma tr_module_correct:
-  forall f m,
-  transl_module f = Errors.OK m ->
-  tr_module f m.
-Admitted.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 82aac41..c509248 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -48,7 +48,12 @@ Record module: Type :=
     mod_stk : reg;
     mod_stk_len : nat;
     mod_finish : reg;
-    mod_return : reg
+    mod_return : reg;
+    mod_start : reg;
+    mod_reset : reg;
+    mod_clk : reg;
+    mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl);
+    mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl);
   }.
 
 Definition fundef := AST.fundef module.
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index bdd8581..700b8e3 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -21,6 +21,7 @@ open Value
 open Datatypes
 
 open Camlcoq
+open AST
 
 open Printf
 
@@ -107,21 +108,30 @@ let pprint_edge_top i = function
   | Valledge -> "@*"
   | Voredge (e1, e2) -> concat ["@("; pprint_edge e1; " or "; pprint_edge e2; ")"]
 
-let declare i t =
+let declare t =
   function (r, sz) ->
-    concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
+    concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
              register r; ";\n" ]
 
-let declarearr i t =
+let declarearr t =
   function (r, sz, ln) ->
-    concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
+    concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
              register r;
              " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ]
 
+let print_io = function
+  | Some Vinput -> "input"
+  | Some Voutput -> "output reg"
+  | Some Vinout -> "inout"
+  | None -> "reg"
+
+let decl i = function
+  | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)]
+  | Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)]
+
 (* TODO Fix always blocks, as they currently always print the same. *)
 let pprint_module_item i = function
-  | Vdecl (r, sz) -> declare i "reg" (r, sz)
-  | Vdeclarr (r, sz, ln) -> declarearr i "reg" (r, sz, ln)
+  | Vdeclaration d -> decl i d
   | Valways (e, s) ->
     concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
   | Valways_ff (e, s) ->
@@ -138,10 +148,6 @@ let make_io i io r = concat [indent i; io; " "; register r; ";\n"]
 
 let compose f g x = g x |> f
 
-let init_inputs i r = declare i "input" r
-
-let init_outputs i r = declare i "output reg" r
-
 let testbench = "module testbench;
    reg start, reset, clk;
    wire finish;
@@ -171,17 +177,12 @@ endmodule
 let pprint_module i n m =
   let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in
   let outputs = [m.mod_finish; m.mod_return] in
-  concat [ indent i; "module "; n;
-           "("; concat (intersperse ", " (List.map (compose register fst) (inputs @ outputs))); ");\n";
-           fold_map (init_inputs (i+1)) inputs;
-           fold_map (init_outputs (i+1)) outputs;
+  concat [ indent i; "module "; (extern_atom n);
+           "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n";
            fold_map (pprint_module_item (i+1)) m.mod_body;
-           indent i; "endmodule\n\n";
-           testbench
+           indent i; "endmodule\n\n"
          ]
 
-let print_program pp v = pstr pp (pprint_module 0 "main" v)
-
 let print_result pp lst =
   let rec print_result_in pp = function
     | [] -> fprintf pp "]\n"
@@ -192,3 +193,12 @@ let print_result pp lst =
   print_result_in pp lst
 
 let print_value pp v = fprintf pp "%s" (literal v)
+
+let print_globdef pp (id, gd) =
+  match gd with
+  | Gfun(Internal f) -> pstr pp (pprint_module 0 id f)
+  | _ -> ()
+
+let print_program pp prog =
+  List.iter (print_globdef pp) prog.prog_defs;
+  pstr pp testbench
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index c9fca8e..0df9d06 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -18,6 +18,6 @@
 
 val print_value : out_channel -> Value.value -> unit
 
-val print_program : out_channel -> Verilog.coq_module -> unit
+val print_program : out_channel -> Verilog.program -> unit
 
 val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit
diff --git a/src/verilog/Test.v b/src/verilog/Test.v
deleted file mode 100644
index 90c5312..0000000
--- a/src/verilog/Test.v
+++ /dev/null
@@ -1,99 +0,0 @@
-(*
- * CoqUp: 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/>.
- *)
-
-From coqup Require Import Verilog Veriloggen Coquplib Value.
-From compcert Require Import AST Errors Maps Op Integers.
-From compcert Require RTL.
-From Coq Require Import FSets.FMapPositive.
-From bbv Require Import Word.
-Import ListNotations.
-Import HexNotationValue.
-Import WordScope.
-
-Local Open Scope word_scope.
-
-Definition test_module : module :=
-  let mods := [
-      Valways (Vposedge 3%positive) (Vseq (Vnonblock (Vvar 6%positive) (Vlit (ZToValue 32 5)))
-                                          (Vnonblock (Vvar 7%positive)
-                                                     (Vvar 6%positive)))
-      ] in
-  mkmodule (1%positive, 1%nat)
-           (2%positive, 1%nat)
-           (3%positive, 1%nat)
-           (4%positive, 1%nat)
-           (5%positive, 32%nat)
-           (6%positive, 32%nat)
-           nil
-           mods.
-
-Definition test_input : RTL.function :=
-  let sig := mksignature nil Tvoid cc_default in
-  let params := nil in
-  let stacksize := 0 in
-  let entrypoint := 3%positive in
-  let code := PTree.set 1%positive (RTL.Ireturn (Some 1%positive))
-               (PTree.set 3%positive (RTL.Iop (Ointconst (Int.repr 5)) nil 1%positive 1%positive)
-                          (PTree.empty RTL.instruction)) in
-  RTL.mkfunction sig params stacksize code entrypoint.
-
-Definition test_input_program : RTL.program :=
-  mkprogram [(1%positive, Gfun (Internal test_input))] nil 1%positive.
-
-Compute transf_program test_input_program.
-
-Definition test_output_module : module :=
-  {| mod_start := (4%positive, 1%nat);
-     mod_reset := (5%positive, 1%nat);
-     mod_clk := (6%positive, 1%nat);
-     mod_finish := (2%positive, 1%nat);
-     mod_return := (3%positive, 32%nat);
-     mod_state := (7%positive, 32%nat);
-     mod_args := [];
-     mod_body :=
-       [Valways_ff (Vposedge 6%positive)
-                   (Vcond (Vbinop Veq (Vinputvar 5%positive) (1'h"1"))
-                          (Vnonblock (Vvar 7%positive) (32'h"3"))
-                          (Vcase (Vvar 7%positive)
-                                 [(Vlit (32'h"1"), Vnonblock (Vvar 7%positive) (32'h"1"));
-                                 (Vlit (32'h"3"), Vnonblock (Vvar 7%positive) (32'h"1"))]
-                                 (Some Vskip)));
-       Valways_ff (Vposedge 6%positive)
-                  (Vcase (Vvar 7%positive)
-                         [(Vlit (32'h"1"), Vseq (Vblock (Vvar 2%positive) (Vlit (1'h"1")))
-                                                (Vblock (Vvar 3%positive) (Vvar 1%positive)));
-                         (Vlit (32'h"3"), Vblock (Vvar 1%positive) (Vlit (32'h"5")))]
-                         (Some Vskip));
-       Vdecl 1%positive 32; Vdecl 7%positive 32] |}.
-
-Lemma valid_test_output :
-  transf_program test_input_program = OK test_output_module.
-Proof. trivial. Qed.
-
-Definition test_fextclk := initial_fextclk test_output_module.
-
-Lemma manual_simulation :
-  step (State test_output_module empty_assocmap empty_assocmap
-              test_fextclk 1 (32'h"1"))
-       (State test_output_module (add_assocmap 7%positive (32'h"3") empty_assocmap)
-              empty_assocmap test_fextclk 2 (32'h"3")).
-Proof.
-  repeat (econstructor; eauto);
-  try (unfold ZToValue; instantiate (1 := eq_refl (vsize (1'h"1"))); auto);
-  apply nevalue; apply weqb_false; trivial. Unshelve. exact 0%nat.
-Qed.
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 0e999de..8b83d49 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -87,6 +87,8 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
 Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
   mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)).
 
+Inductive scl_decl : Type := Scalar (sz : nat).
+Inductive arr_decl : Type := Array (sz : nat) (ln : nat).
 
 (** * Verilog AST
 
@@ -181,9 +183,17 @@ Module items can either be declarations ([Vdecl]) or always blocks ([Valways]).
 The declarations are always register declarations as combinational logic can be
 done using combinational always block instead of continuous assignments. *)
 
+Inductive io : Type :=
+| Vinput : io
+| Voutput : io
+| Vinout : io.
+
+Inductive declaration : Type :=
+| Vdecl : option io -> reg -> nat -> declaration
+| Vdeclarr : option io -> reg -> nat -> nat -> declaration.
+
 Inductive module_item : Type :=
-| Vdecl : reg -> nat -> module_item
-| Vdeclarr : reg -> nat -> nat -> module_item
+| Vdeclaration : declaration -> module_item
 | Valways : edge -> stmnt -> module_item
 | Valways_ff : edge -> stmnt -> module_item
 | Valways_comb : edge -> stmnt -> module_item.
@@ -200,15 +210,22 @@ Inductive module_item : Type :=
 *)
 
 Record module : Type := mkmodule {
-  mod_start : szreg;
-  mod_reset : szreg;
-  mod_clk : szreg;
-  mod_finish : szreg;
-  mod_return : szreg;
-  mod_state : szreg; (**r Variable that defines the current state, it should be internal. *)
-  mod_args : list szreg;
+  mod_start : reg;
+  mod_reset : reg;
+  mod_clk : reg;
+  mod_finish : reg;
+  mod_return : reg;
+  mod_st : reg; (**r Variable that defines the current state, it should be internal. *)
+  mod_stk : reg;
+  mod_args : list reg;
   mod_body : list module_item;
-                        }.
+  mod_entrypoint : node;
+}.
+
+Definition fundef := AST.fundef module.
+
+Definition program := AST.program fundef unit.
+
 (** Convert a [positive] to an expression directly, setting it to the right
     size. *)
 Definition posToLit (p : positive) : expr :=
@@ -241,18 +258,28 @@ retrieved and set appropriately.
   which determines which part of the Verilog is executed.  This is then the part
   of the Verilog that should match with the RTL. *)
 
+Inductive stackframe : Type :=
+  Stackframe :
+    forall  (res : reg)
+            (m : module)
+            (pc : node)
+            (assoc : assocmap),
+      stackframe.
+
 Inductive state : Type :=
-| State:
-    forall (m : module)
-           (assoc : reg_associations)
-           (assoc : arr_associations)
-           (f : fextclk)
-           (cycle : nat)
-           (stvar : value),
-    state
-| Finishstate:
-    forall v : value,
-    state.
+| State :
+    forall (stack : list stackframe)
+           (m : module)
+           (st : node)
+           (reg_assoc : assocmap)
+           (arr_assoc : AssocMap.t (list value)), state
+| Returnstate :
+    forall (res : list stackframe)
+           (v : value), state
+| Callstate :
+    forall (stack : list stackframe)
+           (m : module)
+           (args : list value), state.
 
 Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value :=
   match op with
@@ -383,14 +410,14 @@ Definition access_fext (f : fext) (r : reg) : res value :=
 (** Return the location of the lhs of an assignment. *)
 
 Inductive location : Type :=
-| Reg (_ : reg)
-| Array (_ : reg) (_ : nat).
+| LocReg (_ : reg)
+| LocArray (_ : reg) (_ : nat).
 
 Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop :=
-| Base : forall f asr asa r, location_is f asr asa (Vvar r) (Reg r)
+| Base : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r)
 | Indexed : forall f asr asa r iexp iv,
   expr_runp f asr asa iexp iv ->
-  location_is f asr asa (Vvari r iexp) (Array r (valueToNat iv)).
+  location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)).
 
 (* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l)  (e : expr) : res reg := *)
 (*   match e with *)
@@ -508,28 +535,28 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations ->
     stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1
 | stmnt_runp_Vblock_reg:
     forall lhs r rhs rhsval asr asa f,
-    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Reg r) ->
+    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) ->
     expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
     stmnt_runp f asr asa
                  (Vblock lhs rhs)
                  (block_reg r asr rhsval) asa
 | stmnt_runp_Vnonblock_reg:
     forall lhs r rhs rhsval asr asa f,
-    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Reg r) ->
+    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) ->
     expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
     stmnt_runp f asr asa
                  (Vnonblock lhs rhs)
                  (nonblock_reg r asr rhsval) asa
 | stmnt_runp_Vblock_arr:
     forall lhs r i rhs rhsval asr asa f,
-    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Array r i) ->
+    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) ->
     expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
     stmnt_runp f asr asa
                  (Vblock lhs rhs)
                  asr (block_arr r i asa rhsval)
 | stmnt_runp_Vnonblock_arr:
     forall lhs r i rhs rhsval asr asa f,
-    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Array r i) ->
+    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) ->
     expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
     stmnt_runp f asr asa
                  (Vnonblock lhs rhs)
@@ -565,8 +592,8 @@ Inductive mi_stepp : fext -> reg_associations -> arr_associations ->
     stmnt_runp f sr0 sa0 st sr1 sa1 ->
     mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1
 | mi_stepp_Vdecl :
-    forall f sr sa lhs rhs,
-    mi_stepp f sr sa (Vdecl lhs rhs) sr sa.
+    forall f sr sa lhs rhs io,
+    mi_stepp f sr sa (Vdeclaration (Vdecl io lhs rhs)) sr sa.
 Hint Constructors mi_stepp : verilog.
 
 Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
@@ -607,8 +634,8 @@ other arguments to the module are also to be supported. *)
 
 Definition initial_fextclk (m : module) : fextclk :=
   fun x => match x with
-           | S O => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap)
-           | _ => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap)
+           | S O => (AssocMap.set (mod_reset m) (ZToValue 1 1) empty_assocmap)
+           | _ => (AssocMap.set (mod_reset m) (ZToValue 1 0) empty_assocmap)
            end.
 
 (*Definition module_run (n : nat) (m : module) : res assocmap :=
@@ -655,42 +682,60 @@ Qed.
 
  *)
 
-Definition genv := Genv.t unit unit.
-
-Inductive step : state -> state -> Prop :=
-| step_module :
-    forall m stvar stvar' cycle f
-      asr0 asa0 asr1 asa1
-      asr' asa',
-    mis_stepp (f cycle) asr0 asa0
-              m.(mod_body) asr1 asa1 ->
-    asr' = merge_associations asr1 ->
-    asa' = merge_associations asa1 ->
-    Some stvar' = asr'.(assoc_blocking)!(fst m.(mod_state)) ->
-    step (State m asr0 asa0 f cycle stvar)
-         (State m asr' asa' f (S cycle) stvar')
+Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} :=
+  match rl, vl with
+  | r :: rl', v :: vl' => AssocMap.set r v (init_params vl' rl')
+  | _, _ => empty_assocmap
+  end.
+
+Definition genv := Globalenvs.Genv.t fundef unit.
+
+Inductive step : genv -> state -> Events.trace -> state -> Prop :=
+  | step_module :
+      forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g,
+      mis_stepp f (mkassociations asr empty_assocmap)
+                  (mkassociations asa (AssocMap.empty (list value)))
+                  m.(mod_body)
+                  (mkassociations basr1 nasr1)
+                  (mkassociations basa1 nasa1)->
+      asr' = merge_assocmap nasr1 basr1 ->
+      asa' = AssocMapExt.merge (list value) nasa1 basa1 ->
+      asr'!(m.(mod_st)) = Some stval ->
+      valueToPos stval = pstval ->
+      step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
 | step_finish :
-    forall m asr asa f cycle stvar result,
-    asr.(assoc_blocking)!(fst m.(mod_finish)) = Some (1'h"1") ->
-    asr.(assoc_blocking)!(fst m.(mod_return)) = Some result ->
-    step (State m asr asa f cycle stvar)
-         (Finishstate result).
+    forall asr asa sf retval m st g,
+    asr!(m.(mod_finish)) = Some (1'h"1") ->
+    asr!(m.(mod_return)) = Some retval ->
+    step g (State sf m st asr asa) Events.E0 (Returnstate sf retval)
+| step_call :
+    forall g res m args,
+    step g (Callstate res m args) Events.E0
+         (State res m m.(mod_entrypoint)
+          (AssocMap.set m.(mod_st) (posToValue 32 m.(mod_entrypoint))
+           (init_params args m.(mod_args)))
+          (AssocMap.empty (list value)))
+| step_return :
+    forall g m asr i r sf pc mst,
+    mst = mod_st m ->
+    step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0
+         (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
+                (AssocMap.empty (list value))).
 Hint Constructors step : verilog.
 
-(*Inductive initial_state (m: module): state -> Prop :=
-| initial_state_intro:
-    forall hmi tmi,
-    hmi::tmi = mod_body m ->
-    initial_state m (State m hmi tmi empty_assocmap empty_assocmap (initial_fextclk m) O xH).
-
-(** A final state is a [Returnstate] with an empty call stack. *)
-
-Inductive final_state: state -> Integers.int -> Prop :=
-  | final_state_intro: forall v,
-      final_state (Finishstate v) (valueToInt v).
-
-(** The small-step semantics for a module. *)
-
-Definition semantics (p: module) :=
-  Semantics step (initial_state p) final_state (Genv.empty_genv unit unit nil).
-*)
+Inductive initial_state (p: program): state -> Prop :=
+  | initial_state_intro: forall b m0 m,
+      let ge := Globalenvs.Genv.globalenv p in
+      Globalenvs.Genv.init_mem p = Some m0 ->
+      Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
+      Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) ->
+      initial_state p (Callstate nil m nil).
+
+Inductive final_state : state -> Integers.int -> Prop :=
+| final_state_intro : forall retval retvali,
+    retvali = valueToInt retval ->
+    final_state (Returnstate nil retval) retvali.
+
+Definition semantics (m : program) :=
+  Smallstep.Semantics step (initial_state m) final_state
+                      (Globalenvs.Genv.globalenv m).