diff options
Diffstat (limited to 'src/hls/HTL.v')
| -rw-r--r-- | src/hls/HTL.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 620ef14..cfc7aa3 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -120,6 +120,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := ctrl (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) -> + basr1!(mod_reset m) = Some (ZToValue 0) -> + basr1!(mod_finish m) = Some (ZToValue 0) -> basr1!(m.(mod_st)) = Some (posToValue st) -> Verilog.stmnt_runp f (Verilog.mkassociations basr1 nasr1) |