From 4d409fe68c693dd083295f35bd5af8bdec6d2632 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 5 May 2020 01:16:03 +0100 Subject: Minimised manual simulation --- src/verilog/Test.v | 39 ++++----------------------------------- 1 file changed, 4 insertions(+), 35 deletions(-) (limited to 'src/verilog/Test.v') 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. -- cgit