diff options
Diffstat (limited to 'src/verilog/HTL.v')
| -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 3ba5b59..b3d1442 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -141,8 +141,10 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := forall g m args res, step g (Callstate res m args) Events.E0 (State res m m.(mod_entrypoint) - (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) - (init_regs args m.(mod_params))) + (AssocMap.set (mod_reset m) (ZToValue 0) + (AssocMap.set (mod_finish m) (ZToValue 0) + (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) + (init_regs args m.(mod_params))))) (empty_stack m)) | step_return : forall g m asr asa i r sf pc mst, |