Merge branch 'develop' of github.com:ymherklotz/coqup into arrays-proof

7 files changed, 219 insertions, 113 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 357d487..dc82fb1 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -199,6 +199,41 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
     | _, _ => Error (Errors.msg "HTL.add_instr")
     end.
 
+Lemma add_node_skip_state_incr :
+  forall s n st,
+    (st_datapath s)!n = None ->
+    (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_datapath s n, check_empty_node_controllogic s n with
+    | left STM, 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 STM TRANS)
+    | _, _ => Error (Errors.msg "HTL.add_instr")
+    end.
+
 Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
 Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
 
@@ -219,7 +254,7 @@ Definition translate_comparison (c : Integers.comparison) (args : list reg) : mo
   | 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")
+  | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other")
   end.
 
 Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int)
@@ -231,7 +266,7 @@ Definition translate_comparison_imm (c : Integers.comparison) (args : list reg)
   | 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")
+  | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")
   end.
 
 Definition translate_condition (c : Op.condition) (args : list reg) : mon expr :=
@@ -240,9 +275,9 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr :
   | 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")
+  | 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 (p : Z) : bool :=
@@ -276,7 +311,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex
   | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
   end.
 
-(** Translate an instruction to a statement. *)
+(** 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)
@@ -285,8 +320,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   | 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.Omulhs, r1::r2::nil => ret (bop Vmul r1 r2)
+  | Op.Omulhu, r1::r2::nil => ret (bop Vmul r1 r2)
   | 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)
@@ -302,16 +337,21 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   | 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.Oshrximm n, r::nil => ret (Vbinop Vdiv (Vvar r)
+                                         (Vbinop Vshl (Vlit (ZToValue 32 1))
+                                                 (Vlit (intToValue 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 => ret (Vbinop Vor (boplit Vshr r n) (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) n)))
+  | 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
   | Op.Oleal a, _ => translate_eff_addressing a args (* FIXME: Need to be careful here; large arrays might fail? *)
   | Op.Ocast32signed, r::nil => 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")
+  | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other")
   end.
 
 Lemma add_branch_instr_state_incr:
@@ -345,7 +385,7 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
                 (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 NSTM NTRANS)
-    | _, _ => Error (Errors.msg "Veriloggen: add_branch_instr")
+    | _, _ => Error (Errors.msg "Htlgen: add_branch_instr")
     end.
 
 Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
@@ -354,26 +394,38 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
   | Mint32, Op.Aindexed off, r1::nil =>
     if (check_address_parameter off)
     then ret (Vvari stack (Vbinop Vdiv (boplitz Vadd r1 off) (Vlit (ZToValue 32 4))))
-    else error (Errors.msg "Veriloggen: translate_arr_access address misaligned")
+    else error (Errors.msg "HTLgen: translate_arr_access address misaligned")
   | Mint32, Op.Ascaled scale offset, r1::nil =>
     if (check_address_parameter scale) && (check_address_parameter offset)
     then ret (Vvari stack (Vbinop Vdiv (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) (Vlit (ZToValue 32 4))))
-    else error (Errors.msg "Veriloggen: translate_arr_access address misaligned")
+    else error (Errors.msg "HTLgen: translate_arr_access address misaligned")
   | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
     if (check_address_parameter scale) && (check_address_parameter offset)
     then ret (Vvari stack
                     (Vbinop Vdiv
                             (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
                             (ZToValue 32 4)))
-    else error (Errors.msg "Veriloggen: translate_arr_access address misaligned")
+    else error (Errors.msg "HTLgen: translate_arr_access address misaligned")
   | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
     let a := Integers.Ptrofs.signed a in
     if (check_address_parameter a)
     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")
+    else error (Errors.msg "HTLgen: eff_addressing misaligned 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 32 i), Vnonblock (Vvar st) (Vlit (posToValue 32 n)))
+                  end)
+           (enumerate 0 ns).
+
 Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
   match ni with
     (n, i) =>
@@ -396,7 +448,9 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     | 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")
+    | Ijumptable r tbl =>
+      do s <- get;
+      add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))
     | Ireturn r =>
       match r with
       | Some r' =>
@@ -501,7 +555,7 @@ Definition transl_module (f : function) : Errors.res module :=
 
 Definition transl_fundef := transf_partial_fundef transl_module.
 
-Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p.
+(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *)
 
 (*Definition transl_main_fundef f : Errors.res HTL.fundef :=
   match f with
@@ -518,11 +572,19 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program :=
                              (fun i v => Errors.OK v) p.
 *)
 
-(*Definition main_is_internal (p : RTL.program): Prop :=
+Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := true.
+(*
   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).
+  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 tranls_program_with_proof (p : RTL.program) : Errors.res { p' : HTL.program | main_is_internal p }.
-*)
+Definition transl_program (p : RTL.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/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index a502453..24191ae 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -113,12 +113,23 @@ Inductive match_states : RTL.state -> HTL.state -> Prop :=
 Hint Constructors match_states : htlproof.
 
 Definition match_prog (p: RTL.program) (tp: HTL.program) :=
-  Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
+  Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\
+  main_is_internal p = true.
+
+Definition match_prog_matches :
+  forall p tp,
+    match_prog p tp ->
+    Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
+  Proof. intros. unfold match_prog in H. tauto. Qed.
 
 Lemma transf_program_match:
   forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp.
 Proof.
-  intros. apply Linking.match_transform_partial_program; auto.
+  intros. unfold transl_program in H.
+  destruct (main_is_internal p) eqn:?; try discriminate.
+  unfold match_prog. split.
+  apply Linking.match_transform_partial_program; auto.
+  assumption.
 Qed.
 
 Lemma regs_lessdef_add_greater :
@@ -258,13 +269,16 @@ Section CORRECTNESS.
 
   Hypothesis TRANSL : match_prog prog tprog.
 
+  Lemma TRANSL' :
+    Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog.
+  Proof. intros; apply match_prog_matches; assumption. Qed.
+
   Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
   Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog.
 
   Lemma symbols_preserved:
     forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-  Proof
-    (Genv.find_symbol_transf_partial TRANSL).
+  Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed.
 
   Lemma function_ptr_translated:
     forall (b: Values.block) (f: RTL.fundef),
@@ -272,7 +286,7 @@ Section CORRECTNESS.
       exists tf,
         Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf.
   Proof.
-    intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
+    intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto.
     intros (cu & tf & P & Q & R); exists tf; auto.
   Qed.
 
@@ -282,21 +296,21 @@ Section CORRECTNESS.
       exists tf,
         Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf.
   Proof.
-    intros. exploit (Genv.find_funct_match TRANSL); eauto.
+    intros. exploit (Genv.find_funct_match TRANSL'); eauto.
     intros (cu & tf & P & Q & R); exists tf; auto.
   Qed.
 
   Lemma senv_preserved:
     Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
   Proof
-    (Genv.senv_transf_partial TRANSL).
+    (Genv.senv_transf_partial TRANSL').
   Hint Resolve senv_preserved : htlproof.
 
   Lemma eval_correct :
-    forall sp op rs args m v v' e asr asa f,
+    forall sp op rs args m v v' e asr asa f s s' i,
       Op.eval_operation ge sp op
 (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
-      tr_op op args e ->
+      translate_instr op args s = OK e s' i ->
       val_value_lessdef v v' ->
       Verilog.expr_runp f asr asa e v'.
   Admitted.
@@ -380,7 +394,7 @@ Section CORRECTNESS.
       2: { reflexivity. }
       rewrite AssocMap.gss.
       unfold Verilog.merge_arr.
-      setoid_rewrite H3.
+      setoid_rewrite H5.
       reflexivity.
 
       rewrite combine_length.
@@ -1155,6 +1169,7 @@ Section CORRECTNESS.
 
       assumption.
 
+    - admit.
     - (* Return *)
       econstructor. split.
       eapply Smallstep.plus_two.
@@ -1269,6 +1284,17 @@ Section CORRECTNESS.
   Admitted.
   Hint Resolve transl_step_correct : htlproof.
 
+  Lemma main_tprog_internal :
+    forall b f,
+      Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b ->
+      Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f).
+  Admitted.
+
+  Lemma option_inv :
+    forall A x y,
+      @Some A x = Some y -> x = y.
+    Proof. intros. inversion H. trivial. Qed.
+
   (* 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),
@@ -1277,20 +1303,33 @@ Section CORRECTNESS.
         Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2.
   Proof.
     induction 1.
+    destruct TRANSL. unfold main_is_internal in H4.
+    repeat (unfold_match H4).
+    assert (f = AST.Internal f1). apply option_inv.
+    rewrite <- Heqo0. rewrite <- H1. replace b with b0.
+    auto. apply option_inv. rewrite <- H0. rewrite <- Heqo.
+    trivial.
     exploit function_ptr_translated; eauto.
     intros [tf [A B]].
     unfold transl_fundef, Errors.bind in B.
+    unfold AST.transf_partial_fundef, Errors.bind in B.
     repeat (unfold_match B). inversion B. subst.
     econstructor; split. econstructor.
-    apply (Genv.init_mem_transf_partial TRANSL); eauto.
+    apply (Genv.init_mem_transf_partial TRANSL'); eauto.
     replace (AST.prog_main tprog) with (AST.prog_main prog).
     rewrite symbols_preserved; eauto.
     symmetry; eapply Linking.match_program_main; eauto.
-    Admitted.
-    (*eexact A. trivial.
+    apply main_tprog_internal. replace ge0 with ge in * by auto.
+    replace b0 with b in *. rewrite symbols_preserved.
+    replace (AST.prog_main tprog) with (AST.prog_main prog).
+    assumption.
+    symmetry; eapply Linking.match_program_main; eauto.
+    apply option_inv. rewrite <- H0. rewrite <- Heqo.
+    trivial.
+
     constructor.
-    apply transl_module_correct. auto.
-  Qed.*)
+    apply transl_module_correct. eassumption.
+  Qed.
   Hint Resolve transl_initial_states : htlproof.
 
   Lemma transl_final_states :
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 42de96b..a78256b 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -113,41 +113,13 @@ Ltac monadInv H :=
 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
-| tr_op_Oleal : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Oleal a) l e
-| tr_op_Ocast32signed : forall r, tr_op (Op.Ocast32signed) (r::nil) (Vvar r).
-Hint Constructors tr_op : htlspec.
-
 Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
 | tr_instr_Inop :
     forall n,
       tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n)
 | tr_instr_Iop :
-    forall n op args e dst,
-      tr_op op args e ->
+    forall n op args dst s s' e i,
+      translate_instr op args s = OK e s' i ->
       tr_instr fin rtrn st stk (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,
@@ -168,7 +140,11 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
     forall mem addr args s s' i c src n,
       translate_arr_access mem addr args stk s = OK c s' i ->
       tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src))
-               (state_goto st n).
+               (state_goto st n)
+| tr_instr_Ijumptable :
+    forall cexpr tbl r,
+    cexpr = tbl_to_case_expr st tbl ->
+    tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).
 Hint Constructors tr_instr : htlspec.
 
 Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
@@ -318,21 +294,6 @@ Ltac rewrite_states :=
     remember (?x ?s) as c1; remember (?x ?s') as c2; try subst
   end.
 
-Lemma translate_instr_tr_op :
-  forall op args s s' e i,
-    translate_instr op args s = OK e s' i ->
-    tr_op op args e.
-Proof.
-  intros.
-  destruct op eqn:?; eauto with htlspec; try discriminate; simpl in *;
-    try (match goal with
-           [ H: match ?args with _ => _ end _ = _ _ _ |- _ ] =>
-           repeat (destruct args; try discriminate)
-         end);
-    monadInv H; constructor.
-Qed.
-Hint Resolve translate_instr_tr_op : htlspec.
-
 Ltac unfold_match H :=
   match type of H with
   | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate
@@ -346,7 +307,7 @@ Ltac inv_add_instr' H :=
   end; repeat unfold_match H; inversion H.
 
 Ltac inv_add_instr :=
-  match goal with
+  lazymatch goal with
   | H: context[add_instr_skip _ _ _] |- _ =>
     inv_add_instr' H
   | H: context[add_instr_skip _ _] |- _ =>
@@ -359,6 +320,10 @@ Ltac inv_add_instr :=
     inv_add_instr' H
   | H: context[add_branch_instr _ _ _ _] |- _ =>
     monadInv H; inv_incr; inv_add_instr
+  | H: context[add_node_skip _ _ _] |- _ =>
+    inv_add_instr' H
+  | H: context[add_node_skip _ _] |- _ =>
+    monadInv H; inv_incr; inv_add_instr
   end.
 
 Ltac destruct_optional :=
@@ -386,15 +351,13 @@ Proof.
 
     + 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.
+    + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence.
+      econstructor. apply EQ1. eapply in_map with (f := fst) in H14. 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.
+    + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence.
+      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.
@@ -412,6 +375,12 @@ Proof.
         eauto with htlspec.
       * apply in_map with (f := fst) in H2. 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. constructor. congruence.
+      * apply 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.
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 700b8e3..5dc0386 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -58,7 +58,8 @@ let pprint_binop l r =
   | Vor -> unsigned "|"
   | Vxor -> unsigned "^"
   | Vshl -> unsigned "<<"
-  | Vshr -> unsigned ">>"
+  | Vshr -> signed ">>>"
+  | Vshru -> unsigned ">>"
 
 let unop = function
   | Vneg -> " ~ "
@@ -174,14 +175,29 @@ let testbench = "module testbench;
 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 "; (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"
-         ]
+let debug_always i clk state = concat [
+    indent i; "reg [31:0] count;\n";
+    indent i; "initial count = 0;\n";
+    indent i; "always @(posedge " ^ register clk ^ ") begin\n";
+    indent (i+1); "if(count[0:0] == 10'd0) begin\n";
+    indent (i+2); "$display(\"Cycle count %d\", count);\n";
+    indent (i+2); "$display(\"State %d\\n\", " ^ register state ^ ");\n";
+    indent (i+1); "end\n";
+    indent (i+1); "count <= count + 1;\n";
+    indent i; "end\n"
+  ]
+
+let pprint_module debug i n m =
+  if (extern_atom n) = "main" then
+    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 "; (extern_atom n);
+             "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n";
+             fold_map (pprint_module_item (i+1)) m.mod_body;
+             if debug then debug_always i m.mod_clk m.mod_st else "";
+             indent i; "endmodule\n\n"
+           ]
+  else ""
 
 let print_result pp lst =
   let rec print_result_in pp = function
@@ -194,11 +210,11 @@ let print_result pp lst =
 
 let print_value pp v = fprintf pp "%s" (literal v)
 
-let print_globdef pp (id, gd) =
+let print_globdef debug pp (id, gd) =
   match gd with
-  | Gfun(Internal f) -> pstr pp (pprint_module 0 id f)
+  | Gfun(Internal f) -> pstr pp (pprint_module debug 0 id f)
   | _ -> ()
 
-let print_program pp prog =
-  List.iter (print_globdef pp) prog.prog_defs;
+let print_program debug pp prog =
+  List.iter (print_globdef debug pp) prog.prog_defs;
   pstr pp testbench
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index 0df9d06..6544e52 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.program -> unit
+val print_program : bool -> out_channel -> Verilog.program -> unit
 
 val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 818f625..becc44c 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -19,7 +19,7 @@
 (* begin hide *)
 From bbv Require Import Word.
 From bbv Require HexNotation WordScope.
-From Coq Require Import ZArith.ZArith FSets.FMapPositive.
+From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
 From compcert Require Import lib.Integers common.Values.
 (* end hide *)
 
@@ -340,7 +340,7 @@ Proof.
   rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z.
   split. apply Zle_0_pos.
 
-  assert (p < 2 ^ (Pos.size p))%positive. apply Pos.size_gt.
+  assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt.
   inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1.
   simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.
 Qed.
@@ -371,3 +371,21 @@ Lemma boolToValue_ValueToBool :
   forall b,
   valueToBool (boolToValue 32 b) = b.
 Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed.
+
+Lemma ZToValue_valueToNat :
+  forall x sz,
+  sz > 0 ->
+  (x < 2^(Z.of_nat sz))%Z ->
+  valueToNat (ZToValue sz x) = Z.to_nat x.
+Proof.
+  destruct x; intros; unfold ZToValue, valueToNat; simpl.
+  - rewrite wzero'_def. apply wordToNat_wzero.
+  - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial.
+    unfold Z.of_nat in *. destruct sz eqn:?. omega. simpl in H0.
+    rewrite <- Pos2Z.inj_pow_pos in H0. Search (Z.pos _ < Z.pos _)%Z.
+    Search Pos.to_nat (_ < _). (* Pos2Nat.inj_lt *)
+    Search Pos.to_nat.
+    (* Pos2Nat.is_succ: forall p : positive, exists n : nat, Pos.to_nat p = S n *)
+    Search S Pos.to_nat. Search (_ < _ <-> _)%positive. assert (exists p, Pos.to_nat p = S n).
+    econstructor. Search Pos2Nat.is_succ. Search Pos.of_succ_nat.
+Admitted.
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 4144632..7d5e3c0 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -144,7 +144,8 @@ Inductive binop : Type :=
 | Vor : binop   (** or (binary [|]) *)
 | Vxor : binop  (** xor (binary [^|]) *)
 | Vshl : binop  (** shift left ([<<]) *)
-| Vshr : binop. (** shift right ([>>]) *)
+| Vshr : binop (** shift right ([>>>]) *)
+| Vshru : binop. (** shift right unsigned ([>>]) *)
 
 (** ** Unary Operators *)
 
@@ -320,6 +321,7 @@ Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 ->
   | Vxor => vxor
   | Vshl => vshl
   | Vshr => vshr
+  | Vshru => vshr (* FIXME: should not be the same operation. *)
   end.
 
 Definition unop_run (op : unop) : value -> value :=