diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-05 01:16:03 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-05 01:16:10 +0100 |
| commit | 4d409fe68c693dd083295f35bd5af8bdec6d2632 (patch) | |
| tree | 0d1eb9ccf70845c3c732a46839c29b29050bd528 /src/verilog/Verilog.v | |
| parent | 5d4aed9030565349a83f9ede4bd35c020eb416b5 (diff) | |
| download | vericert-4d409fe68c693dd083295f35bd5af8bdec6d2632.tar.gz vericert-4d409fe68c693dd083295f35bd5af8bdec6d2632.zip | |
Minimised manual simulation
Diffstat (limited to 'src/verilog/Verilog.v')
| -rw-r--r-- | src/verilog/Verilog.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 399bff7..451b452 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -244,14 +244,14 @@ Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop := | erun_Vlit : forall fext assoc v, expr_runp fext assoc (Vlit v) v - | erun_Vvar : - forall fext assoc v r, - assoc!r = Some v -> - expr_runp fext assoc (Vvar r) v | erun_Vvar_empty : forall fext assoc r sz, assoc!r = None -> expr_runp fext assoc (Vvar r) (ZToValue sz 0) + | erun_Vvar : + forall fext assoc v r, + assoc!r = Some v -> + expr_runp fext assoc (Vvar r) v | erun_Vinputvar : forall fext assoc r v, fext!r = Some v -> @@ -437,21 +437,21 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop := valueToBool vc = false -> stmnt_runp s0 stf s1 -> stmnt_runp s0 (Vcond c stt stf) s1 -| stmnt_runp_Vcase_match: +| stmnt_runp_Vcase_nomatch: forall e ve s0 f assoc s1 me mve sc cs def, state_fext_assoc s0 (f, assoc) -> expr_runp f assoc e ve -> expr_runp f assoc me mve -> - mve = ve -> - stmnt_runp s0 sc s1 -> + mve <> ve -> + stmnt_runp s0 (Vcase e cs def) s1 -> stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1 -| stmnt_runp_Vcase_nomatch: +| stmnt_runp_Vcase_match: forall e ve s0 f assoc s1 me mve sc cs def, state_fext_assoc s0 (f, assoc) -> expr_runp f assoc e ve -> expr_runp f assoc me mve -> - mve <> ve -> - stmnt_runp s0 (Vcase e cs def) s1 -> + mve = ve -> + stmnt_runp s0 sc s1 -> stmnt_runp s0 (Vcase e ((me, sc)::cs) def) s1 | stmnt_runp_Vcase_default: forall s0 f assoc st s1 e ve, |