diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-11-18 10:36:41 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-18 10:36:41 +0000 |
| commit | 393c584daba6936f1b4deb68e196e1edc4b753cc (patch) | |
| tree | 60e2db9faf426451e375c6e86bea774987459678 /src/hls/Verilog.v | |
| parent | 2a5b73153060ff9f69403ca81d29c9c9761623d8 (diff) | |
| download | vericert-kvx-wip/reset-signals.tar.gz vericert-kvx-wip/reset-signals.zip | |
More work on proving reset signalwip/reset-signals
Diffstat (limited to 'src/hls/Verilog.v')
| -rw-r--r-- | src/hls/Verilog.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 6b4004f..db21d01 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -730,7 +730,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := valueToPos stval = pstval -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') | step_reset : - forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf g, + forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf g mrst, asr!(m.(mod_reset)) = Some (ZToValue 1) -> asr!(m.(mod_finish)) = Some (ZToValue 0) -> mis_stepp f (mkassociations asr empty_assocmap) @@ -742,7 +742,9 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := asa' = merge_arrs nasa1 basa1 -> asr'!(m.(mod_st)) = Some stval -> valueToPos stval = pstval -> - step g (Resetstate sf m asr asa) Events.E0 (State sf m pstval asr' asa') + mrst = (m.(mod_reset)) -> + step g (Resetstate sf m asr asa) Events.E0 + (State sf m pstval (asr' # mrst <- (ZToValue 0)) asa') | step_finish : forall asr asa sf retval m st g, asr!(m.(mod_finish)) = Some (ZToValue 1) -> |