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 | |
| 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
| -rw-r--r-- | src/hls/Verilog.v | 6 | ||||
| -rw-r--r-- | src/hls/Veriloggenproof.v | 11 |
2 files changed, 10 insertions, 7 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) -> diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 1f7126f..b3a9922 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -43,10 +43,11 @@ Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop := Inductive match_states : HTL.state -> state -> Prop := | match_state : - forall m st reg_assoc arr_assoc hstk vstk, + forall m st reg_assoc_htl reg_assoc_v arr_assoc hstk vstk, match_stacks hstk vstk -> - match_states (HTL.State hstk m st reg_assoc arr_assoc) - (State vstk (transl_module m) st reg_assoc arr_assoc) + (forall i, reg_assoc_htl ! i = reg_assoc_v ! i) -> + match_states (HTL.State hstk m st reg_assoc_htl arr_assoc) + (State vstk (transl_module m) st reg_assoc_v arr_assoc) | match_returnstate : forall v hstk vstk, match_stacks hstk vstk -> @@ -343,9 +344,9 @@ Section CORRECTNESS. unfold ZToValue. rewrite !Int.unsigned_repr; unfold_constants; try lia. econstructor. apply mis_stepp_decl. trivial. trivial. simplify. - unfold merge_regs. unfold_merge. apply AssocMap.gss. auto. auto. + unfold merge_regs. unfold_merge. apply AssocMap.gss. auto. auto. auto. rewrite valueToPos_posToValue. - simplify. unfold merge_regs. unfold_merge. + simplify. unfold merge_regs. unfold_merge. Search Maps.PTree.set. - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. |