diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-05 00:38:19 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-05 00:38:26 +0100 |
| commit | 5d4aed9030565349a83f9ede4bd35c020eb416b5 (patch) | |
| tree | 57f284d6277ebfdf8294dc8737075ab08c48a69a /src/verilog/Test.v | |
| parent | 2df5dc835efa3ac7552363e81ef9af5d3145cc7e (diff) | |
| download | vericert-5d4aed9030565349a83f9ede4bd35c020eb416b5.tar.gz vericert-5d4aed9030565349a83f9ede4bd35c020eb416b5.zip | |
Simplifications to proof
Diffstat (limited to 'src/verilog/Test.v')
| -rw-r--r-- | src/verilog/Test.v | 21 |
1 files changed, 7 insertions, 14 deletions
diff --git a/src/verilog/Test.v b/src/verilog/Test.v index 5fd6d07..9e13bf6 100644 --- a/src/verilog/Test.v +++ b/src/verilog/Test.v @@ -95,20 +95,14 @@ 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. - 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")). + eapply step_module; auto. + eapply mis_stepp_Cons; auto. apply mi_stepp_Valways_ff. - apply stmnt_runp_Vcond_true with (f := test_fextclk 1%nat) - (assoc := empty_assoclist) - (vc := 1'h"1"); auto. + eapply stmnt_runp_Vcond_true; 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 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. @@ -135,6 +129,5 @@ Proof. eapply mis_stepp_Cons. apply mi_stepp_Vdecl. apply mis_stepp_Nil. - Unshelve. - exact 0%nat. + auto. Unshelve. exact 0%nat. Qed. |