4 files changed, 53 insertions, 17 deletions
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 :=