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/Verilog.v | |
| parent | 2df5dc835efa3ac7552363e81ef9af5d3145cc7e (diff) | |
| download | vericert-5d4aed9030565349a83f9ede4bd35c020eb416b5.tar.gz vericert-5d4aed9030565349a83f9ede4bd35c020eb416b5.zip | |
Simplifications to proof
Diffstat (limited to 'src/verilog/Verilog.v')
| -rw-r--r-- | src/verilog/Verilog.v | 10 |
1 files changed, 8 insertions, 2 deletions
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: |