From 5d4aed9030565349a83f9ede4bd35c020eb416b5 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 5 May 2020 00:38:19 +0100 Subject: Simplifications to proof --- src/verilog/Test.v | 21 +++++++-------------- src/verilog/Value.v | 2 -- src/verilog/Verilog.v | 10 ++++++++-- 3 files changed, 15 insertions(+), 18 deletions(-) (limited to 'src/verilog') 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. diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 39d1832..61f2652 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -101,8 +101,6 @@ Definition boolToValue (sz : nat) (b : bool) : value := (** ** Arithmetic operations *) -Definition EQ_trivial : forall x, vsize x = vsize x. trivial. Defined. - Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. intros; subst; assumption. Defined. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 756dc12..399bff7 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -281,6 +281,7 @@ Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop := expr_runp fext assoc fs vf -> valueToBool vc = false -> expr_runp fext assoc (Vternary c ts fs) vf. +Hint Constructors expr_runp : verilog. Definition handle_opt {A : Type} (err : errmsg) (val : option A) : res A := @@ -412,11 +413,12 @@ Inductive state_fext_assoc : state -> fext * assoclist -> Prop := | get_state_fext_assoc : forall c assoc nbassoc f cycle pc, state_fext_assoc (State c assoc nbassoc f cycle pc) (f cycle, assoc). +Hint Constructors state_fext_assoc : verilog. Inductive stmnt_runp: state -> stmnt -> state -> Prop := -| stmnt_run_Vskip: +| stmnt_runp_Vskip: forall s, stmnt_runp s Vskip s -| stmnt_run_Vseq: +| stmnt_runp_Vseq: forall st1 st2 s0 s1 s2, stmnt_runp s0 st1 s1 -> stmnt_runp s1 st2 s2 -> @@ -473,6 +475,7 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop := stmnt_runp (State c assoc nbassoc f cycle pc) (Vnonblock lhs rhs) (State c assoc nbassoc' f cycle pc). +Hint Constructors stmnt_runp : verilog. (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := let run := fun st ls => @@ -503,6 +506,7 @@ Inductive mi_stepp : state -> module_item -> state -> Prop := | mi_stepp_Vdecl : forall s lhs rhs, mi_stepp s (Vdecl lhs rhs) s. +Hint Constructors mi_stepp : verilog. Inductive mis_stepp : state -> list module_item -> state -> Prop := | mis_stepp_Cons : @@ -513,6 +517,7 @@ Inductive mis_stepp : state -> list module_item -> state -> Prop := | mis_stepp_Nil : forall s, mis_stepp s nil s. +Hint Constructors mis_stepp : verilog. Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist := PositiveMap.add r v assoc. @@ -614,6 +619,7 @@ Inductive step : state -> state -> Prop := assoc!(fst m.(mod_return)) = Some result -> step (State m assoc empty_assoclist f cycle stvar) (Finishstate result). +Hint Constructors step : verilog. (*Inductive initial_state (m: module): state -> Prop := | initial_state_intro: -- cgit