Refine the semantics

3 files changed, 130 insertions, 56 deletions

diff --git a/src/verilog/Test.v b/src/verilog/Test.v
index 7a31865..5c22ef2 100644
--- a/src/verilog/Test.v
+++ b/src/verilog/Test.v
@@ -64,10 +64,35 @@ Lemma valid_test_output :
   transf_program test_input_program = OK test_output_module.
 Proof. trivial. Qed.
 
+Definition test_fextclk := initial_fextclk test_output_module.
+
 Lemma manual_simulation :
-  forall f,
-  step (State test_output_module empty_assoclist
-              (initial_fextclk test_output_module)
-              1%nat 1%positive)
-       (State test_output_module test_output_module (add_assoclist 7 (32'h"3") empty_assoclist)
-              2%nat 3%positive).
+  step (State test_output_module empty_assoclist empty_assoclist
+              test_fextclk 1 (32'h"1"))
+       (State test_output_module (add_assoclist 7%positive (32'h"3") empty_assoclist)
+              empty_assoclist test_fextclk 2 (32'h"3")).
+Proof.
+  apply step_module with (assoc1 := empty_assoclist)
+                         (nbassoc := (add_assoclist 7%positive (32'h"3") empty_assoclist)); auto.
+  apply mis_stepp_Cons with (s1 := State test_output_module empty_assoclist (add_assoclist 7%positive (32'h"3") empty_assoclist) test_fextclk 1%nat (32'h"1")).
+  apply mi_stepp_Valways_ff.
+  apply stmnt_runp_Vcond_true with (f := test_fextclk 1%nat)
+                                   (assoc := empty_assoclist)
+                                   (vc := 1'h"1"); auto.
+  apply get_state_fext_assoc.
+  apply erun_Vbinop with (lv := 1'h"1")
+                         (rv := 1'h"1")
+                         (oper := veq)
+                         (EQ := EQ_trivial (1'h"1")); auto.
+  apply erun_Vinputvar; auto.
+  apply erun_Vlit.
+  eapply stmnt_runp_Vnonblock. simpl. auto.
+  apply erun_Vlit.
+  auto.
+  eapply mis_stepp_Cons.
+  apply mi_stepp_Valways_ff.
+  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.
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 1d31110..21e59be 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -60,13 +60,6 @@ Definition valueToN (v : value) : N :=
 Definition NToValue sz (n : N) : value :=
   mkvalue sz (NToWord sz n).
 
-Definition posToValue sz (p : positive) : value :=
-  mkvalue sz (posToWord sz p).
-
-Definition posToValueAuto (p : positive) : value :=
-  let size := Z.to_nat (Z.succ (log_inf p)) in
-  mkvalue size (Word.posToWord size p).
-
 Definition ZToValue (s : nat) (z : Z) : value :=
   mkvalue s (ZToWord s z).
 
@@ -76,6 +69,19 @@ Definition valueToZ (v : value) : Z :=
 Definition uvalueToZ (v : value) : Z :=
   uwordToZ (vword v).
 
+Definition posToValue sz (p : positive) : value :=
+  mkvalue sz (posToWord sz p).
+
+Definition posToValueAuto (p : positive) : value :=
+  let size := Z.to_nat (Z.succ (log_inf p)) in
+  mkvalue size (Word.posToWord size p).
+
+Definition valueToPos (v : value) : positive :=
+  match valueToZ v with
+  | Zpos p => p
+  | _ => 1
+  end.
+
 Definition intToValue (i : Integers.int) : value :=
   ZToValue Int.wordsize (Int.unsigned i).
 
@@ -95,8 +101,10 @@ Definition boolToValue (sz : nat) (b : bool) : value :=
 
 (** ** Arithmetic operations *)
 
+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. Qed.
+Proof. intros; subst; assumption. Defined.
 
 Definition value_eq_size:
   forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }.
@@ -141,6 +149,26 @@ 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. intros. subst. reflexivity. Qed.
+
+Lemma nevalue {sz : nat} (x y : word sz) : x <> y -> (mkvalue sz x <> mkvalue sz y).
+Proof. Admitted.
+
+Definition valueEqCheck (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 (eqvalue x y eq)
+  | right ne => right (nevalue x y ne)
+  end.
+
+Definition valueEq (x y : value) (EQ : vsize x = vsize y): {x = y} + {x <> y} :=
+  let unif_y := unify_word (vsize x) (vsize y) (vword y) EQ in
+  match weq (vword x) unif_y with
+  | left _ => left _
+  | right _ => right _
+  end.
+
 (** Arithmetic operations over [value], interpreting them as signed or unsigned
 depending on the operation.
 
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 7a3982c..a927eac 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -31,6 +31,8 @@ From coqup Require Import common.Coquplib common.Show verilog.Value.
 From compcert Require Integers Events.
 From compcert Require Import Errors Smallstep Globalenvs.
 
+Import HexNotationValue.
+
 Notation "a ! b" := (PositiveMap.find b a) (at level 1).
 
 Definition reg : Type := positive.
@@ -196,13 +198,11 @@ retrieved and set appropriately.
 Inductive state : Type :=
 | State:
     forall (m : module)
-           (mi : module_item)
-           (mis : list module_item)
            (assoc : assoclist)
            (nbassoc : assoclist)
            (f : fextclk)
            (cycle : nat)
-           (pc : positive),
+           (stvar : value),
     state
 | Finishstate:
     forall v : value,
@@ -248,21 +248,27 @@ Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop :=
       forall fext assoc v r,
       assoc!r = Some v ->
       expr_runp fext assoc (Vvar r) v
+  | erun_Vvar_empty :
+      forall fext assoc r sz,
+      assoc!r = None ->
+      expr_runp fext assoc (Vvar r) (ZToValue sz 0)
   | erun_Vinputvar :
       forall fext assoc r v,
       fext!r = Some v ->
       expr_runp fext assoc (Vinputvar r) v
   | erun_Vbinop :
-      forall fext assoc op l r lv rv oper EQ,
+      forall fext assoc op l r lv rv oper EQ resv,
       expr_runp fext assoc l lv ->
       expr_runp fext assoc r rv ->
       oper = binop_run op ->
-      expr_runp fext assoc (Vbinop op l r) (oper lv rv EQ)
+      resv = oper lv rv EQ ->
+      expr_runp fext assoc (Vbinop op l r) resv
   | erun_Vunop :
-      forall fext assoc u vu op oper,
+      forall fext assoc u vu op oper resv,
       expr_runp fext assoc u vu ->
       oper = unop_run op ->
-      expr_runp fext assoc (Vunop op u) (oper vu)
+      resv = oper vu ->
+      expr_runp fext assoc (Vunop op u) resv
   | erun_Vternary_true :
       forall fext assoc c ts fs vc vt,
       expr_runp fext assoc c vc ->
@@ -402,17 +408,10 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
 Definition stmnt_run (s : state) (st : stmnt) : res state :=
   stmnt_run' (stmnt_height st) s st. *)
 
-Inductive not_matched : state -> value -> expr * stmnt -> Prop :=
-  not_in:
-    forall caseval curr currval m mi c assoc nbassoc f cycle pc,
-    expr_runp (f cycle) assoc (fst curr) currval ->
-    caseval <> currval ->
-    not_matched (State m mi c assoc nbassoc f cycle pc) caseval curr.
-
 Inductive state_fext_assoc : state -> fext * assoclist -> Prop :=
 | get_state_fext_assoc :
-  forall m mi c assoc nbassoc f cycle pc,
-  state_fext_assoc (State m mi c assoc nbassoc f cycle pc) (f cycle, assoc).
+  forall c assoc nbassoc f cycle pc,
+  state_fext_assoc (State c assoc nbassoc f cycle pc) (f cycle, assoc).
 
 Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
 | stmnt_run_Vskip:
@@ -436,38 +435,44 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
     valueToBool vc = false ->
     stmnt_runp s0 stf s1 ->
     stmnt_runp s0 (Vcond c stt stf) s1
-| stmnt_runp_Vcase:
-    forall e ve s0 f assoc s1 me mve sc clst def,
+| stmnt_runp_Vcase_match:
+    forall e ve s0 f assoc s1 me mve sc cs def,
     state_fext_assoc s0 (f, assoc) ->
     expr_runp f assoc e ve ->
     expr_runp f assoc me mve ->
     mve = ve ->
-    In (me, sc) clst ->
     stmnt_runp s0 sc s1 ->
-    stmnt_runp s0 (Vcase e clst def) s1
+    stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1
+| stmnt_runp_Vcase_nomatch:
+    forall e ve s0 f assoc s1 me mve sc cs def,
+    state_fext_assoc s0 (f, assoc) ->
+    expr_runp f assoc e ve ->
+    expr_runp f assoc me mve ->
+    mve <> ve ->
+    stmnt_runp s0 (Vcase e cs def) s1 ->
+    stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1
 | stmnt_runp_Vcase_default:
-    forall s0 f assoc st s1 e ve clst,
+    forall s0 f assoc st s1 e ve,
     state_fext_assoc s0 (f, assoc) ->
     expr_runp f assoc e ve ->
-    Forall (not_matched s0 ve) clst ->
     stmnt_runp s0 st s1 ->
-    stmnt_runp s0 (Vcase e clst (Some st)) s1
+    stmnt_runp s0 (Vcase e nil (Some st)) s1
 | stmnt_runp_Vblock:
-    forall lhs name rhs rhsval m mi c assoc assoc' nbassoc f cycle pc,
+    forall lhs name rhs rhsval c assoc assoc' nbassoc f cycle pc,
     assign_name lhs = OK name ->
     expr_runp (f cycle) assoc rhs rhsval ->
     assoc' = (PositiveMap.add name rhsval assoc) ->
-    stmnt_runp (State m mi c assoc nbassoc f cycle pc)
+    stmnt_runp (State c assoc nbassoc f cycle pc)
                (Vblock lhs rhs)
-               (State m mi c assoc' nbassoc f cycle pc)
+               (State c assoc' nbassoc f cycle pc)
 | stmnt_runp_Vnonblock:
-    forall lhs name rhs rhsval m mi c assoc nbassoc nbassoc' f cycle pc,
+    forall lhs name rhs rhsval c assoc nbassoc nbassoc' f cycle pc,
     assign_name lhs = OK name ->
     expr_runp (f cycle) assoc rhs rhsval ->
     nbassoc' = (PositiveMap.add name rhsval nbassoc) ->
-    stmnt_runp (State m mi c assoc nbassoc f cycle pc)
-               (Vblock lhs rhs)
-               (State m mi c assoc nbassoc' f cycle pc).
+    stmnt_runp (State c assoc nbassoc f cycle pc)
+               (Vnonblock lhs rhs)
+               (State c assoc nbassoc' f cycle pc).
 
 (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
   let run := fun st ls =>
@@ -499,6 +504,16 @@ Inductive mi_stepp : state -> module_item -> state -> Prop :=
     forall s lhs rhs,
     mi_stepp s (Vdecl lhs rhs) s.
 
+Inductive mis_stepp : state -> list module_item -> state -> Prop :=
+| mis_stepp_Cons :
+    forall mi mis s0 s1 s2,
+    mi_stepp s0 mi s1 ->
+    mis_stepp s1 mis s2 ->
+    mis_stepp s0 (mi :: mis) s2
+| mis_stepp_Nil :
+    forall s,
+    mis_stepp s nil s.
+
 Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist :=
   PositiveMap.add r v assoc.
 
@@ -583,19 +598,24 @@ Qed.
 
 Definition genv := Genv.t unit unit.
 
-
-Inductive step : genv -> state -> Events.trace -> state -> Prop :=
+Inductive step : state -> state -> Prop :=
 | step_module :
-    forall g m mi hmi tmi assoc nbassoc f cycle pc e,
-    step_cc g (State m mi (hmi::tmi) assoc nbassoc f cycle pc) e
-            (State m hmi tmi assoc nbassoc f cycle pc)
-| step_module_empty :
-    forall g tmi hmi m mi assoc nbassoc f cycle pc e,
-    hmi::tmi = mod_body m ->
-    step_cc g (State m mi nil assoc nbassoc f cycle pc) e
-            (State m hmi tmi assoc nbassoc f (S cycle) pc).
-
-Inductive initial_state (m: module): state -> Prop :=
+    forall m stvar stvar' cycle f assoc0 assoc1 assoc2 nbassoc,
+    mis_stepp (State m assoc0 empty_assoclist f cycle stvar)
+              m.(mod_body)
+              (State m assoc1 nbassoc f cycle stvar) ->
+    assoc2 = merge_assoclist nbassoc assoc1 ->
+    Some stvar' = assoc2!(fst m.(mod_state)) ->
+    step (State m assoc0 empty_assoclist f cycle stvar)
+         (State m assoc2 empty_assoclist f (S cycle) stvar')
+| step_finish :
+    forall m assoc f cycle stvar result,
+    assoc!(fst m.(mod_finish)) = Some (1'h"1") ->
+    assoc!(fst m.(mod_return)) = Some result ->
+    step (State m assoc empty_assoclist f cycle stvar)
+         (Finishstate result).
+
+(*Inductive initial_state (m: module): state -> Prop :=
 | initial_state_intro:
     forall hmi tmi,
     hmi::tmi = mod_body m ->
@@ -611,3 +631,4 @@ Inductive final_state: state -> Integers.int -> Prop :=
 
 Definition semantics (p: module) :=
   Semantics step (initial_state p) final_state (Genv.empty_genv unit unit nil).
+*)