diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-10-18 17:05:46 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-18 17:05:46 +0100 |
commit | fbfa988072ce2eba808b9a6631af5f8e86cd9df0 (patch) | |
tree | 5146e558d5c9c6e9a399225eed0784b8dc12558f /src/hls/Verilog.v | |
parent | 603768a49eac2005729dd03e723ff6c5a6b292f7 (diff) | |
parent | fe06668f0de56635efe55310d7a64289a37c1d90 (diff) | |
download | vericert-dev/michalis.tar.gz vericert-dev/michalis.zip |
Merge branch 'master' into dev/michalisdev/michalis
Diffstat (limited to 'src/hls/Verilog.v')
-rw-r--r-- | src/hls/Verilog.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 0df8b7e..39504a2 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -428,7 +428,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop expr_runp fext reg stack fs vf -> valueToBool vc = false -> expr_runp fext reg stack (Vternary c ts fs) vf. -Hint Constructors expr_runp : verilog. +#[export] Hint Constructors expr_runp : verilog. Definition handle_opt {A : Type} (err : errmsg) (val : option A) : res A := @@ -526,7 +526,7 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> stmnt_runp f asr asa (Vnonblock lhs rhs) asr (nonblock_arr r i asa rhsval). -Hint Constructors stmnt_runp : verilog. +#[export] Hint Constructors stmnt_runp : verilog. Inductive mi_stepp : fext -> reg_associations -> arr_associations -> module_item -> reg_associations -> arr_associations -> Prop := @@ -540,7 +540,7 @@ Inductive mi_stepp : fext -> reg_associations -> arr_associations -> | mi_stepp_Vdecl : forall f sr0 sa0 d, mi_stepp f sr0 sa0 (Vdeclaration d) sr0 sa0. -Hint Constructors mi_stepp : verilog. +#[export] Hint Constructors mi_stepp : verilog. Inductive mi_stepp_negedge : fext -> reg_associations -> arr_associations -> module_item -> reg_associations -> arr_associations -> Prop := @@ -554,7 +554,7 @@ Inductive mi_stepp_negedge : fext -> reg_associations -> arr_associations -> | mi_stepp_negedge_Vdecl : forall f sr0 sa0 d, mi_stepp_negedge f sr0 sa0 (Vdeclaration d) sr0 sa0. -Hint Constructors mi_stepp : verilog. +#[export] Hint Constructors mi_stepp : verilog. Inductive mis_stepp : fext -> reg_associations -> arr_associations -> list module_item -> reg_associations -> arr_associations -> Prop := @@ -566,7 +566,7 @@ Inductive mis_stepp : fext -> reg_associations -> arr_associations -> | mis_stepp_Nil : forall f sr sa, mis_stepp f sr sa nil sr sa. -Hint Constructors mis_stepp : verilog. +#[export] Hint Constructors mis_stepp : verilog. Inductive mis_stepp_negedge : fext -> reg_associations -> arr_associations -> list module_item -> reg_associations -> arr_associations -> Prop := @@ -578,7 +578,7 @@ Inductive mis_stepp_negedge : fext -> reg_associations -> arr_associations -> | mis_stepp_negedge_Nil : forall f sr sa, mis_stepp_negedge f sr sa nil sr sa. -Hint Constructors mis_stepp : verilog. +#[export] Hint Constructors mis_stepp : verilog. Local Close Scope error_monad_scope. @@ -634,7 +634,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := mst = mod_st m -> step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). -Hint Constructors step : verilog. +#[export] Hint Constructors step : verilog. Inductive initial_state (p: program): state -> Prop := | initial_state_intro: forall b m0 m, @@ -692,7 +692,7 @@ Proof. learn (H1 _ H2) end; crush). Qed. -Hint Resolve expr_runp_determinate : verilog. +#[export] Hint Resolve expr_runp_determinate : verilog. Lemma location_is_determinate : forall f asr asa e l, @@ -741,7 +741,7 @@ Lemma stmnt_runp_determinate : learn (H1 _ _ H2) end; crush). Qed. -Hint Resolve stmnt_runp_determinate : verilog. +#[export] Hint Resolve stmnt_runp_determinate : verilog. Lemma mi_stepp_determinate : forall f asr0 asa0 m asr1 asa1, |