Minimised manual simulation

2 files changed, 14 insertions, 45 deletions

diff --git a/src/verilog/Test.v b/src/verilog/Test.v
index 9e13bf6..d94467d 100644
--- a/src/verilog/Test.v
+++ b/src/verilog/Test.v
@@ -95,39 +95,8 @@ Lemma manual_simulation :
        (State test_output_module (add_assoclist 7%positive (32'h"3") empty_assoclist)
               empty_assoclist test_fextclk 2 (32'h"3")).
 Proof.
-  eapply step_module; auto.
-  eapply mis_stepp_Cons; auto.
-  apply mi_stepp_Valways_ff.
-  eapply stmnt_runp_Vcond_true; auto.
-  apply get_state_fext_assoc.
-  eapply erun_Vbinop; auto.
-  apply erun_Vinputvar; simpl. auto.
-  apply erun_Vlit. simpl. unfold ZToValue. simpl. instantiate (1 := eq_refl (vsize (1'h"1"))). auto.
-  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. 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.
-  auto. Unshelve. exact 0%nat.
+  repeat (econstructor; eauto);
+  try (simpl; unfold ZToValue; simpl; instantiate (1 := eq_refl (vsize (1'h"1"))); auto);
+  apply nevalue; apply weqb_false; trivial.
+  Unshelve. exact 0%nat.
 Qed.
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 399bff7..451b452 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -244,14 +244,14 @@ Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop :=
   | erun_Vlit :
       forall fext assoc v,
       expr_runp fext assoc (Vlit v) v
-  | erun_Vvar :
-      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_Vvar :
+      forall fext assoc v r,
+      assoc!r = Some v ->
+      expr_runp fext assoc (Vvar r) v
   | erun_Vinputvar :
       forall fext assoc r v,
       fext!r = Some v ->
@@ -437,21 +437,21 @@ 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_match:
+| 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 sc s1 ->
+    mve <> ve ->
+    stmnt_runp s0 (Vcase e cs def) s1 ->
     stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1
-| stmnt_runp_Vcase_nomatch:
+| 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 ->
-    stmnt_runp s0 (Vcase e cs def) s1 ->
+    mve = ve ->
+    stmnt_runp s0 sc s1 ->
     stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1
 | stmnt_runp_Vcase_default:
     forall s0 f assoc st s1 e ve,