From ea14bf01e909d96590150c0f5271988b2bb2bf38 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 2 Mar 2021 21:17:52 +0000 Subject: Add implementation --- src/hls/HTLgenproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/hls/HTLgenproof.v') diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 9a7e272..59ff55b 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1,4 +1,4 @@ - (* +(* * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz * 2020 James Pollard -- cgit 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 From b9b21b639f4604b7ff0f0ccefa70f4bbde706d54 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 9 Mar 2021 22:19:40 +0000 Subject: Add negative edge reasoning to HTLgenproof --- src/hls/HTLgenproof.v | 88 ++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 76 insertions(+), 12 deletions(-) (limited to 'src/hls/HTLgenproof.v') diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index e3b0147..3b5496f 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1736,15 +1736,36 @@ Section CORRECTNESS. crush. unfold Verilog.merge_arrs. - rewrite AssocMap.gcombine. - 2: { reflexivity. } + rewrite AssocMap.gcombine by reflexivity. + rewrite AssocMap.gss. + erewrite Verilog.merge_arr_empty2. unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gcombine by reflexivity. + rewrite AssocMap.gss. rewrite AssocMap.gss. unfold Verilog.merge_arr. + setoid_rewrite H7. + reflexivity. + + rewrite AssocMap.gcombine by reflexivity. + unfold Verilog.merge_arr. + unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gss. rewrite AssocMap.gss. setoid_rewrite H7. reflexivity. + rewrite combine_length. + rewrite <- array_set_len. + unfold arr_repeat. crush. + symmetry. + apply list_repeat_len. + + rewrite <- array_set_len. + unfold arr_repeat. crush. + rewrite H4. + apply list_repeat_len. + rewrite combine_length. rewrite <- array_set_len. unfold arr_repeat. crush. @@ -1752,8 +1773,8 @@ Section CORRECTNESS. rewrite <- array_set_len. unfold arr_repeat. crush. - rewrite list_repeat_len. - rewrite H4. reflexivity. + rewrite H4. + apply list_repeat_len. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. @@ -2015,11 +2036,21 @@ Section CORRECTNESS. crush. unfold Verilog.merge_arrs. - rewrite AssocMap.gcombine. - 2: { reflexivity. } + rewrite AssocMap.gcombine by reflexivity. + rewrite AssocMap.gss. + erewrite Verilog.merge_arr_empty2. unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gcombine by reflexivity. + rewrite AssocMap.gss. rewrite AssocMap.gss. unfold Verilog.merge_arr. + setoid_rewrite H7. + reflexivity. + + rewrite AssocMap.gcombine by reflexivity. + unfold Verilog.merge_arr. + unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gss. rewrite AssocMap.gss. setoid_rewrite H7. reflexivity. @@ -2027,12 +2058,23 @@ Section CORRECTNESS. rewrite combine_length. rewrite <- array_set_len. unfold arr_repeat. crush. + symmetry. apply list_repeat_len. rewrite <- array_set_len. unfold arr_repeat. crush. - rewrite list_repeat_len. - rewrite H4. reflexivity. + rewrite H4. + apply list_repeat_len. + + rewrite combine_length. + rewrite <- array_set_len. + unfold arr_repeat. crush. + apply list_repeat_len. + + rewrite <- array_set_len. + unfold arr_repeat. crush. + rewrite H4. + apply list_repeat_len. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) (Integers.Ptrofs.of_int @@ -2264,11 +2306,21 @@ Section CORRECTNESS. crush. unfold Verilog.merge_arrs. - rewrite AssocMap.gcombine. - 2: { reflexivity. } + rewrite AssocMap.gcombine by reflexivity. + rewrite AssocMap.gss. + erewrite Verilog.merge_arr_empty2. unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gcombine by reflexivity. rewrite AssocMap.gss. + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H7. + reflexivity. + + rewrite AssocMap.gcombine by reflexivity. unfold Verilog.merge_arr. + unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gss. rewrite AssocMap.gss. setoid_rewrite H7. reflexivity. @@ -2276,12 +2328,23 @@ Section CORRECTNESS. rewrite combine_length. rewrite <- array_set_len. unfold arr_repeat. crush. + symmetry. apply list_repeat_len. rewrite <- array_set_len. unfold arr_repeat. crush. - rewrite list_repeat_len. - rewrite H4. reflexivity. + rewrite H4. + apply list_repeat_len. + + rewrite combine_length. + rewrite <- array_set_len. + unfold arr_repeat. crush. + apply list_repeat_len. + + rewrite <- array_set_len. + unfold arr_repeat. crush. + rewrite H4. + apply list_repeat_len. remember i0 as OFFSET. destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). @@ -2576,6 +2639,7 @@ Section CORRECTNESS. apply HTL.step_finish. unfold Verilog.merge_regs. unfold_merge. + unfold_merge. rewrite AssocMap.gso. apply AssocMap.gss. simpl; lia. apply AssocMap.gss. -- cgit From 8573889ca84a84475761b4d75d55547a2995c831 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 7 Apr 2021 01:11:04 +0100 Subject: Basically done with proof --- src/hls/HTLgenproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/hls/HTLgenproof.v') diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 3b5496f..1aac3b7 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -2602,7 +2602,7 @@ Section CORRECTNESS. constructor. constructor. constructor. unfold state_st_wf in WF; big_tac; eauto. - destruct wf as [HCTRL HDATA]. apply HCTRL. + destruct wf1 as [HCTRL HDATA]. apply HCTRL. apply AssocMapExt.elements_iff. eexists. match goal with H: control ! pc = Some _ |- _ => apply H end. @@ -2632,7 +2632,7 @@ Section CORRECTNESS. unfold state_st_wf in WF; big_tac; eauto. - destruct wf as [HCTRL HDATA]. apply HCTRL. + destruct wf1 as [HCTRL HDATA]. apply HCTRL. apply AssocMapExt.elements_iff. eexists. match goal with H: control ! pc = Some _ |- _ => apply H end. -- cgit