From 2a5b73153060ff9f69403ca81d29c9c9761623d8 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 17 Nov 2020 13:14:56 +0000 Subject: Add changes for proof of reset signals with Resetstate --- src/hls/HTL.v | 2 ++ src/hls/HTLgenproof.v | 28 +++++++++++++++++++++------- src/hls/Verilog.v | 32 +++++++++++++++++++++++++------- src/hls/Veriloggen.v | 4 +++- src/hls/Veriloggenproof.v | 32 +++++++++++++++++++++++++++++--- 5 files changed, 80 insertions(+), 18 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) diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index afc827d..1fbc361 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1080,12 +1080,13 @@ Section CORRECTNESS. crush. econstructor. econstructor. - econstructor. - - all: invert MARR; big_tac. - inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia. + all: try constructor; invert MARR; big_tac. + inv CONST. simplify. assumption. + inv CONST. simplify. assumption. + inv CONST. constructor. simplify; rewrite AssocMap.gso; auto; lia. + simplify; rewrite AssocMap.gso; auto; lia. Unshelve. exact tt. Qed. Hint Resolve transl_inop_correct : htlproof. @@ -1113,7 +1114,10 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor; trivial. econstructor; simpl; eauto. - simpl. econstructor. econstructor. + simpl. + inv CONST. assumption. + inv CONST. assumption. + econstructor. econstructor. apply H5. simplify. all: big_tac. @@ -2448,7 +2452,10 @@ Section CORRECTNESS. eapply eval_cond_correct; eauto. intros. intros. eapply RTL.max_reg_function_use. apply H22. auto. econstructor. auto. - simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. + simpl. + inv CONST. assumption. + inv CONST. assumption. + econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. inv MARR. inv CONST. @@ -2465,7 +2472,10 @@ Section CORRECTNESS. eapply eval_cond_correct; eauto. intros. intros. eapply RTL.max_reg_function_use. apply H22. auto. econstructor. auto. - simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. + simpl. + inv CONST. assumption. + inv CONST. assumption. + econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. inv MARR. inv CONST. @@ -2514,6 +2524,8 @@ Section CORRECTNESS. inv CONST; assumption. inv CONST; assumption. constructor. + inv CONST. assumption. + inv CONST. assumption. econstructor; simpl; trivial. econstructor; simpl; trivial. constructor. @@ -2545,6 +2557,8 @@ Section CORRECTNESS. inv CONST; assumption. inv CONST; assumption. constructor. + inv CONST. assumption. + inv CONST. assumption. econstructor; simpl; trivial. econstructor; simpl; trivial. constructor. constructor. constructor. diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index e5f86d5..6b4004f 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -286,6 +286,11 @@ Inductive state : Type := (st : node) (reg_assoc : assocmap_reg) (arr_assoc : assocmap_arr), state +| Resetstate : + forall (stack : list stackframe) + (m : module) + (reg_assoc : assocmap_reg) + (arr_assoc : assocmap_arr), state | Returnstate : forall (res : list stackframe) (v : value), state @@ -724,6 +729,20 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := asr'!(m.(mod_st)) = Some stval -> 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, + asr!(m.(mod_reset)) = Some (ZToValue 1) -> + asr!(m.(mod_finish)) = Some (ZToValue 0) -> + mis_stepp f (mkassociations asr empty_assocmap) + (mkassociations asa (empty_stack m)) + m.(mod_body) + (mkassociations basr1 nasr1) + (mkassociations basa1 nasa1) -> + asr' = merge_regs nasr1 basr1 -> + 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') | step_finish : forall asr asa sf retval m st g, asr!(m.(mod_finish)) = Some (ZToValue 1) -> @@ -732,11 +751,10 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_call : forall g res m args, step g (Callstate res m args) Events.E0 - (State res m m.(mod_entrypoint) - (AssocMap.set (mod_reset m) (ZToValue 0) + (Resetstate res m + (AssocMap.set (mod_reset m) (ZToValue 1) (AssocMap.set (mod_finish m) (ZToValue 0) - (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint)) - (init_params args m.(mod_args))))) + (init_params args m.(mod_args)))) (empty_stack m)) | step_return : forall g m asr i r sf pc mst asa, @@ -883,9 +901,9 @@ Lemma semantics_determinate : Proof. intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. - invert H; invert H0; constructor. (* Traces are always empty *) - - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst. - pose proof (mis_stepp_determinate H5 H15). - crush. + - invert H; invert H0; crush; assert (f = f0) by (destruct f; destruct f0; auto); subst. + pose proof (mis_stepp_determinate H5 H15). crush. + pose proof (mis_stepp_determinate H3 H10). crush. - constructor. invert H; crush. - invert H; invert H0; unfold ge0, ge1 in *; crush. - red; simplify; intro; invert H0; invert H; crush. diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index a0be0fa..b497115 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -44,7 +44,9 @@ Definition transl_module (m : HTL.module) : Verilog.module := Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1))) (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint)))) (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip))) - :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) + :: Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 0))) + (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) + Vskip) :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in Verilog.mkmodule m.(mod_start) diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 9abbd4b..1f7126f 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -300,7 +300,12 @@ Section CORRECTNESS. } apply Maps.PTree.elements_correct. eassumption. eassumption. - econstructor. econstructor. + econstructor. econstructor. econstructor. + econstructor. econstructor. simplify. + unfold find_assocmap, AssocMapExt.get_default. + rewrite H5. trivial. + constructor. simplify. unfold valueToBool, boolToValue, Int.eq, uvalueToZ, natToValue. + rewrite zeq_true. rewrite Int.unsigned_repr. auto. lia. eapply transl_list_correct. intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. @@ -319,9 +324,30 @@ Section CORRECTNESS. - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption. constructor; assumption. - - econstructor; split. apply Smallstep.plus_one. constructor. + - econstructor; split. eapply Smallstep.plus_two. constructor. + econstructor. + apply AssocMap.gss. + rewrite AssocMap.gso. + apply AssocMap.gss. admit. + econstructor. + constructor. eapply stmnt_runp_Vcond_true. econstructor. econstructor. simplify. + unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gss. auto. + econstructor. simplify. unfold valueToBool, boolToValue, Int.eq, uvalueToZ, natToValue. + rewrite zeq_true. rewrite Int.unsigned_repr. auto. simpl. unfold_constants. lia. + econstructor. econstructor. econstructor. + econstructor. econstructor. + eapply stmnt_runp_Vcond_false. econstructor. econstructor. simplify. + unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gss. auto. + econstructor. simplify. unfold valueToBool, boolToValue, Int.eq, uvalueToZ, natToValue. + rewrite zeq_false. rewrite Int.unsigned_repr. auto. simpl. unfold_constants. lia. + 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. + rewrite valueToPos_posToValue. + simplify. unfold merge_regs. unfold_merge. + - constructor. constructor. - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. apply match_state. assumption. -- cgit