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

3 files changed, 73 insertions, 10 deletions

diff --git a/src/CoqupClflags.ml b/src/CoqupClflags.ml
new file mode 100644
index 0000000..83dd31d
--- /dev/null
+++ b/src/CoqupClflags.ml
@@ -0,0 +1,5 @@
+(* Coqup flags *)
+let option_simulate = ref false
+let option_hls = ref true
+let option_debug_hls = ref false
+let option_initial = ref false
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 5dc0386..6d10887 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -22,9 +22,12 @@ open Datatypes
 
 open Camlcoq
 open AST
+open Clflags
 
 open Printf
 
+open CoqupClflags
+
 let concat = String.concat ""
 
 let indent i = String.make (2 * i) ' '
@@ -187,6 +190,12 @@ let debug_always i clk state = concat [
     indent i; "end\n"
   ]
 
+let print_initial i n stk = concat [
+    indent i; "integer i;\n";
+    indent i; "initial for(i = 0; i < "; sprintf "%d" n; "; i++)\n";
+    indent (i+1); register stk; "[i] = 0;\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
@@ -194,6 +203,7 @@ let pprint_module debug i n m =
     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 !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else "";
              if debug then debug_always i m.mod_clk m.mod_st else "";
              indent i; "endmodule\n\n"
            ]
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index c380ca7..8ba5138 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -111,8 +111,7 @@ intros; subst; assumption. Defined.
 Lemma unify_word_unfold :
   forall sz w,
   unify_word sz sz w eq_refl = w.
-Proof.
-  intros. unfold unify_word. Admitted.
+Proof. auto. Qed.
 
 Definition value_eq_size:
   forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }.
@@ -330,6 +329,12 @@ Proof.
   auto using uwordToZ_ZToWord.
 Qed.
 
+Lemma uvalueToZ_ZToValue_full :
+  forall sz : nat,
+  (0 < sz)%nat ->
+  forall z : Z, uvalueToZ (ZToValue sz z) = (z mod 2 ^ Z.of_nat sz)%Z.
+Proof. unfold uvalueToZ, ZToValue. simpl. auto using uwordToZ_ZToWord_full. Qed.
+
 Lemma ZToValue_uvalueToZ :
   forall v,
   ZToValue (vsize v) (uvalueToZ v) = v.
@@ -390,19 +395,62 @@ Lemma boolToValue_ValueToBool :
   valueToBool (boolToValue 32 b) = b.
 Proof. destruct b; auto. Qed.
 
-Lemma intToValue_eq_size :
-  forall n1 n2,
-  vsize (intToValue n1) = vsize (intToValue n2).
-Proof. auto. Qed.
-
 Local Open Scope Z.
 
+Ltac word_op_value H :=
+  intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold;
+  rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega.
+
 Lemma zadd_vplus :
+  forall sz z1 z2,
+  (sz > 0)%nat ->
+  uvalueToZ (vplus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 + z2) mod 2 ^ Z.of_nat sz.
+Proof. word_op_value ZToWord_plus. Qed.
+
+Lemma zadd_vplus2 :
   forall z1 z2,
-  valueToZ (vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 + z2.
+  vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl = ZToValue 32 (z1 + z2).
+Proof.
+  intros. unfold vplus, ZToValue, map_word2. rewrite unify_word_unfold. simpl.
+  rewrite ZToWord_plus; auto.
+Qed.
+
+Lemma wordsize_32 :
+  Int.wordsize = 32%nat.
+Proof. auto. Qed.
+
+Lemma intadd_vplus :
+  forall i1 i2,
+  valueToInt (vplus (intToValue i1) (intToValue i2) eq_refl) = Int.add i1 i2.
+Proof.
+  intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus.
+  rewrite <- Int.unsigned_repr_eq.
+  rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega.
+Qed.
+
+Lemma zsub_vminus :
+  forall sz z1 z2,
+  (sz > 0)%nat ->
+  uvalueToZ (vminus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 - z2) mod 2 ^ Z.of_nat sz.
+Proof. word_op_value ZToWord_minus. Qed.
+
+Lemma zmul_vmul :
+  forall sz z1 z2,
+  (sz > 0)%nat ->
+  uvalueToZ (vmul (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 * z2) mod 2 ^ Z.of_nat sz.
+Proof. word_op_value ZToWord_mult. Qed.
+
+Local Open Scope N.
+Lemma zdiv_vdiv :
+  forall n1 n2,
+  n1 < 2 ^ 32 ->
+  n2 < 2 ^ 32 ->
+  n1 / n2 < 2 ^ 32 ->
+  valueToN (vdiv (NToValue 32 n1) (NToValue 32 n2) eq_refl) = n1 / n2.
 Proof.
-  intros. unfold valueToZ, ZToValue. simpl.
-  Admitted.
+  intros; unfold valueToN, NToValue; simpl; rewrite unify_word_unfold. unfold wdiv.
+  unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto.
+Qed.
 
 (*Lemma ZToValue_valueToNat :
   forall x sz,