From 393c584daba6936f1b4deb68e196e1edc4b753cc Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 18 Nov 2020 10:36:41 +0000 Subject: More work on proving reset signal --- src/hls/Verilog.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/hls/Verilog.v') 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) -> -- cgit