diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-20 10:51:33 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-20 10:51:33 +0100 |
| commit | d76ea8e7a52f01a1be2f5b2ec1c5367a42aa0f65 (patch) | |
| tree | aabf67c1f3dc2b0cbbad455b4fa622db4fde43e2 /src/verilog | |
| parent | 43f766ea8aff8309d94173cc1e2670eb8ddce68f (diff) | |
| download | vericert-d76ea8e7a52f01a1be2f5b2ec1c5367a42aa0f65.tar.gz vericert-d76ea8e7a52f01a1be2f5b2ec1c5367a42aa0f65.zip | |
Fix the semantics to properly evaluate the state
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/HTL.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 147d24b..36e4434 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -63,7 +63,7 @@ Inductive state : Type := Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall g t m st ctrl data assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f, + forall g t m st ctrl data assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f stval pstval, m.(mod_controllogic)!st = Some ctrl -> m.(mod_datapath)!st = Some data -> Verilog.stmnt_runp f @@ -75,7 +75,9 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := data (Verilog.mkassociations assoc2 nbassoc1) -> assoc3 = merge_assocmap nbassoc1 assoc2 -> - step g (State m st assoc0) t (State m st assoc3) + assoc3!(m.(mod_st)) = Some stval -> + valueToPos stval = pstval -> + step g (State m st assoc0) t (State m pstval assoc3) | step_finish : forall g t m st assoc retval, assoc!(m.(mod_finish)) = Some (1'h"1") -> |