Finish manual simulation

2 files changed, 68 insertions, 5 deletions

diff --git a/src/verilog/Test.v b/src/verilog/Test.v
index 5c22ef2..5fd6d07 100644
--- a/src/verilog/Test.v
+++ b/src/verilog/Test.v
@@ -1,9 +1,30 @@
+(*
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
 From coqup Require Import Verilog Veriloggen Coquplib Value.
 From compcert Require Import AST Errors Maps Op Integers.
 From compcert Require RTL.
 From Coq Require Import FSets.FMapPositive.
+From bbv Require Import Word.
 Import ListNotations.
 Import HexNotationValue.
+Import WordScope.
+
 Local Open Scope word_scope.
 
 Definition test_module : module :=
@@ -60,6 +81,8 @@ Definition test_output_module : module :=
                          (Some Vskip));
        Vdecl 1%positive 32; Vdecl 7%positive 32] |}.
 
+Search (_ <> _ -> _ = _).
+
 Lemma valid_test_output :
   transf_program test_input_program = OK test_output_module.
 Proof. trivial. Qed.
@@ -95,4 +118,23 @@ Proof.
   apply get_state_fext_assoc.
   apply erun_Vvar_empty. auto.
   apply erun_Vlit.
-  unfold ZToValue. instantiate (1 := 32%nat). simpl.
+  unfold ZToValue. instantiate (1 := 32%nat). simpl. apply nevalue. simpl.
+  apply weqb_false. simpl. trivial.
+  eapply stmnt_runp_Vcase_nomatch.
+  apply get_state_fext_assoc.
+  apply erun_Vvar_empty. auto.
+  apply erun_Vlit.
+  unfold ZToValue. instantiate (1 := 32%nat). simpl. apply nevalue. simpl.
+  apply weqb_false. simpl. trivial.
+  eapply stmnt_runp_Vcase_default.
+  apply get_state_fext_assoc.
+  apply erun_Vvar_empty. auto.
+  apply stmnt_run_Vskip.
+  eapply mis_stepp_Cons.
+  apply mi_stepp_Vdecl.
+  eapply mis_stepp_Cons.
+  apply mi_stepp_Vdecl.
+  apply mis_stepp_Nil.
+  Unshelve.
+  exact 0%nat.
+Qed.
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 4cacab5..39d1832 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -103,8 +103,8 @@ Definition boolToValue (sz : nat) (b : bool) : value :=
 
 Definition EQ_trivial : forall x, vsize x = vsize x. trivial. Defined.
 
-Lemma unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
-Proof. intros; subst; assumption. Defined.
+Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
+intros; subst; assumption. Defined.
 
 Definition value_eq_size:
   forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }.
@@ -149,7 +149,6 @@ Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value)
   | _ => None
   end.
 
-
 Lemma eqvalue {sz : nat} (x y : word sz) : x = y <-> mkvalue sz x = mkvalue sz y.
 Proof.
   split; intros.
@@ -168,13 +167,35 @@ Qed.
 Lemma nevaluef {sz : nat} (x y : word sz) : x <> y -> mkvalue sz x <> mkvalue sz y.
 Proof. apply nevalue. Qed.
 
-Definition valueEq (sz : nat) (x y : word sz) :
+(*Definition rewrite_word_size (initsz finalsz : nat) (w : word initsz)
+  : option (word finalsz) :=
+  match Nat.eqb initsz finalsz return option (word finalsz) with
+  | true => Some _
+  | false => None
+  end.*)
+
+Definition valueeq (sz : nat) (x y : word sz) :
   {mkvalue sz x = mkvalue sz y} + {mkvalue sz x <> mkvalue sz y} :=
   match weq x y with
   | left eq => left (eqvaluef x y eq)
   | right ne => right (nevaluef x y ne)
   end.
 
+Definition valueeqb (x y : value) : bool :=
+  match value_eq_size x y with
+  | left EQ =>
+    weqb (vword x) (unify_word (vsize x) (vsize y) (vword y) EQ)
+  | right _ => false
+  end.
+
+Theorem valueeqb_true_iff :
+  forall v1 v2,
+  valueeqb v1 v2 = true <-> v1 = v2.
+Proof.
+  split; intros.
+  unfold valueeqb in H. destruct (value_eq_size v1 v2).
+  Admitted.
+
 (** Arithmetic operations over [value], interpreting them as signed or unsigned
 depending on the operation.