diff options
-rw-r--r-- | driver/CoqupDriver.ml | 8 | ||||
-rw-r--r-- | src/CoqupClflags.ml | 5 | ||||
-rw-r--r-- | src/verilog/PrintVerilog.ml | 10 | ||||
-rw-r--r-- | src/verilog/Value.v | 68 | ||||
-rw-r--r-- | test/loop.c | 6 |
5 files changed, 80 insertions, 17 deletions
diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml index 2932a50..afbe4d0 100644 --- a/driver/CoqupDriver.ml +++ b/driver/CoqupDriver.ml @@ -36,11 +36,7 @@ open Coqup.Frontend open Coqup.Assembler open Coqup.Linker open Coqup.Diagnostics - -(* Coqup flags *) -let option_simulate = ref false -let option_hls = ref true -let option_debug_hls = ref false +open Coqup.CoqupClflags (* Name used for version string etc. *) let tool_name = "C verified high-level synthesis" @@ -215,6 +211,7 @@ Processing options: --no-hls Do not use HLS and generate standard flow. --simulate Simulate the result with the Verilog semantics. --debug-hls Add debug logic to the Verilog. + --initialise-stack initialise the stack to all 0s. |} ^ prepro_help ^ language_support_help ^ @@ -316,6 +313,7 @@ let cmdline_actions = [Exact "--no-hls", Unset option_hls; Exact "--simulate", Set option_simulate; Exact "--debug-hls", Set option_debug_hls; + Exact "--initialise-stack", Set option_initial; ] (* Getting version info *) @ version_options tool_name @ 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, diff --git a/test/loop.c b/test/loop.c index b459e3a..52e4fe9 100644 --- a/test/loop.c +++ b/test/loop.c @@ -1,10 +1,12 @@ int main() { int max = 5; int acc = 0; + int b = 1; + int c = 2; - for (int i = 0; i < max; i++) { + for (int i = 0; i < max; i = i + b) { acc += i; } - return acc + 2; + return acc + c; } |