From 8a260a8b81617e192fc929e0189fd3df1327f80a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 30 Jun 2020 00:04:39 +0100 Subject: Add equivalence between int add value add --- src/verilog/Value.v | 64 ++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 54 insertions(+), 10 deletions(-) diff --git a/src/verilog/Value.v b/src/verilog/Value.v index c380ca7..3c5ed04 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,58 @@ 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 eq_op H := + intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold; + rewrite <- H; rewrite uwordToZ_ZToWord; auto. + Lemma zadd_vplus : forall z1 z2, - valueToZ (vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 + z2. + 0 <= z1 + z2 < 2 ^ 32 -> + uvalueToZ (vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 + z2. +Proof. eq_op ZToWord_plus. Qed. + +Lemma zadd_vplus2 : + forall z1 z2, + vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl = ZToValue 32 (z1 + z2). Proof. - intros. unfold valueToZ, ZToValue. simpl. - Admitted. + intros. unfold vplus, ZToValue, map_word2. rewrite unify_word_unfold. simpl. + rewrite ZToWord_plus; 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_vplus2. + rewrite uvalueToZ_ZToValue_full. rewrite <- Int.unsigned_repr_eq. + rewrite Int.repr_unsigned. auto. omega. +Qed. + +Lemma zsub_vminus : + forall z1 z2, + 0 <= z1 - z2 < 2 ^ 32 -> + uvalueToZ (vminus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 - z2. +Proof. eq_op ZToWord_minus. Qed. + +Lemma zmul_vmul : + forall z1 z2, + 0 <= z1 * z2 < 2 ^ 32 -> + uvalueToZ (vmul (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 * z2. +Proof. eq_op 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 valueToN, NToValue; simpl; rewrite unify_word_unfold. unfold wdiv. + unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto. +Qed. (*Lemma ZToValue_valueToNat : forall x sz, -- cgit From 9a640d4f50b93a9d5f9b48e10b0c4cbfa7f0680f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 30 Jun 2020 00:29:41 +0100 Subject: Make the proofs more concise --- src/verilog/Value.v | 38 +++++++++++++++++++++----------------- 1 file changed, 21 insertions(+), 17 deletions(-) diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 3c5ed04..8ba5138 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -397,15 +397,15 @@ Proof. destruct b; auto. Qed. Local Open Scope Z. -Ltac eq_op H := +Ltac word_op_value H := intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold; - rewrite <- H; rewrite uwordToZ_ZToWord; auto. + rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega. Lemma zadd_vplus : - forall z1 z2, - 0 <= z1 + z2 < 2 ^ 32 -> - uvalueToZ (vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 + z2. -Proof. eq_op ZToWord_plus. Qed. + 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, @@ -415,26 +415,30 @@ Proof. 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_vplus2. - rewrite uvalueToZ_ZToValue_full. rewrite <- Int.unsigned_repr_eq. - rewrite Int.repr_unsigned. auto. omega. + 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 z1 z2, - 0 <= z1 - z2 < 2 ^ 32 -> - uvalueToZ (vminus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 - z2. -Proof. eq_op ZToWord_minus. Qed. + 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 z1 z2, - 0 <= z1 * z2 < 2 ^ 32 -> - uvalueToZ (vmul (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 * z2. -Proof. eq_op ZToWord_mult. Qed. + 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 : -- cgit From f26f3887d0b0ac286c317a5425a3a4781871cfc2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 30 Jun 2020 12:34:35 +0100 Subject: Add command line flags for initial block --- driver/CoqupDriver.ml | 8 +++----- src/CoqupClflags.ml | 5 +++++ src/verilog/PrintVerilog.ml | 10 ++++++++++ test/loop.c | 6 ++++-- 4 files changed, 22 insertions(+), 7 deletions(-) create mode 100644 src/CoqupClflags.ml 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/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; } -- cgit