diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-03-12 11:09:54 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-03-12 11:09:54 +0000 |
| commit | 1df82be06ecda0e75b48159f525020dd08e7b00b (patch) | |
| tree | 5ce73c35ce8b783714d2ec5d35197094713592c7 | |
| parent | e9109a10aecb53e56c8110dd788495a5b0b3c88c (diff) | |
| download | vericert-1df82be06ecda0e75b48159f525020dd08e7b00b.tar.gz vericert-1df82be06ecda0e75b48159f525020dd08e7b00b.zip | |
Try and fix identity proof in Memorygen
| -rw-r--r-- | src/hls/Memorygen.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 7ce61b3..ed72c11 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -342,7 +342,8 @@ Definition behaviour_correct d c d' c' r' := /\ PTree.get i c' = Some c_s' /\ exec_all_ram r' d_s' c_s' rs1 ar1 trs2 tar2 /\ match_reg_assocs (merge_reg_assocs rs2) (merge_reg_assocs trs2) - /\ match_arr_assocs (merge_arr_assocs ar2 r') (merge_arr_assocs tar2 r'). + /\ match_arr_assocs (merge_arr_assocs (ram_mem r') (ram_size r') ar2) + (merge_arr_assocs (ram_mem r') (ram_size r') tar2). Lemma behaviour_correct_equiv : forall d c r, @@ -361,6 +362,16 @@ Proof. unfold find_assocmap. unfold AssocMapExt.get_default. assert ((assoc_blocking (merge_reg_assocs rs2)) ! (ram_en r) = None) by admit. destruct_match; try discriminate; auto. + constructor; constructor; auto. + constructor; constructor; crush. + assert (Some arr = Some arr'). + { + rewrite <- H3. rewrite <- H5. + symmetry. + assert (s = (ram_mem r)) by admit; subst. + eapply merge_arr_idempotent. + } + subst; auto. Qed. Hint Resolve behaviour_correct_equiv : mgen. |