From 57350a8ca5579b65978d7a723a20915e763a2d0b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 3 Mar 2021 21:12:15 +0000 Subject: Add RAM semantics to HTL and fix proof --- src/hls/HTLgenproof.v | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'src/hls/HTLgenproof.v') diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 59ff55b..e3b0147 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1030,6 +1030,7 @@ Section CORRECTNESS. Ltac tac0 := match goal with + | [ |- HTL.exec_ram _ _ _ _ _ ] => constructor | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge @@ -1701,7 +1702,7 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - all: crush. + all: try constructor; crush. (** State Lookup *) unfold Verilog.merge_regs. @@ -1981,7 +1982,7 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - all: crush. + all: try constructor; crush. (** State Lookup *) unfold Verilog.merge_regs. @@ -2229,7 +2230,7 @@ Section CORRECTNESS. eapply Verilog.stmnt_runp_Vnonblock_arr. crush. econstructor. econstructor. econstructor. econstructor. - all: crush. + all: try constructor; crush. (** State Lookup *) unfold Verilog.merge_regs. @@ -2463,7 +2464,7 @@ 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. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. inv MARR. inv CONST. @@ -2480,7 +2481,7 @@ 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. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. inv MARR. inv CONST. @@ -2535,7 +2536,7 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor. - constructor. constructor. + constructor. constructor. constructor. unfold state_st_wf in WF; big_tac; eauto. destruct wf as [HCTRL HDATA]. apply HCTRL. @@ -2564,6 +2565,7 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor. constructor. constructor. constructor. constructor. constructor. + constructor. unfold state_st_wf in WF; big_tac; eauto. -- cgit