diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-25 09:09:23 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-25 09:09:23 +0100 |
| commit | 445aabbcf63e29d68dd0c98dde7f259af0381591 (patch) | |
| tree | fe77b0b489849e60dca1fc221f7c3a301ec776e5 /src/verilog/Verilog.v | |
| parent | 14cd3b8b12e3db17c3842ae9dfdb30ca86b6394c (diff) | |
| download | vericert-kvx-445aabbcf63e29d68dd0c98dde7f259af0381591.tar.gz vericert-kvx-445aabbcf63e29d68dd0c98dde7f259af0381591.zip | |
Work on Veriloggen proof
Diffstat (limited to 'src/verilog/Verilog.v')
| -rw-r--r-- | src/verilog/Verilog.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 7d5e3c0..9c05fc9 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -279,7 +279,8 @@ Inductive stackframe : Type := forall (res : reg) (m : module) (pc : node) - (assoc : assocmap), + (reg_assoc : assocmap_reg) + (arr_assoc : assocmap_arr), stackframe. Inductive state : Type := @@ -735,9 +736,9 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (init_params args m.(mod_args))) (empty_stack m)) | step_return : - forall g m asr i r sf pc mst, + forall g m asr i r sf pc mst asa, mst = mod_st m -> - step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0 + step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) (empty_stack m)). Hint Constructors step : verilog. |