diff options
Diffstat (limited to 'src/hls/DMemorygen.v')
| -rw-r--r-- | src/hls/DMemorygen.v | 56 |
1 files changed, 0 insertions, 56 deletions
diff --git a/src/hls/DMemorygen.v b/src/hls/DMemorygen.v index bef9f3d..d6c4fe8 100644 --- a/src/hls/DMemorygen.v +++ b/src/hls/DMemorygen.v @@ -2133,62 +2133,6 @@ Proof. apply Forall_forall. apply IHl. Qed. -(* Lemma transf_code_fold_correct: *) -(* forall l m state ram d' c' n, *) -(* fold_right (transf_maps state ram) (mod_datapath m, mod_controllogic m) l = (d', c') -> *) -(* Forall (fun x => x < n) (map fst l) -> *) -(* Forall (Pos.le n) (map snd l) -> *) -(* list_norepet (map fst l) -> *) -(* list_norepet (map snd l) -> *) -(* (forall p i c_s rs1 ar1 rs2 ar2 trs1 tar1 d_s, *) -(* i < n -> *) -(* all_match_empty_size m ar1 -> *) -(* all_match_empty_size m tar1 -> *) -(* match_module_to_ram m ram -> *) -(* (mod_datapath m)!i = Some d_s -> *) -(* (mod_controllogic m)!i = Some c_s -> *) -(* match_reg_assocs p rs1 trs1 -> *) -(* match_arr_assocs ar1 tar1 -> *) -(* max_reg_module m < p -> *) -(* exec_all d_s c_s rs1 ar1 rs2 ar2 -> *) -(* exists d_s' c_s' trs2 tar2, *) -(* d'!i = Some d_s' /\ c'!i = Some c_s' *) -(* /\ exec_all_ram ram d_s' c_s' trs1 tar1 trs2 tar2 *) -(* /\ match_reg_assocs p (merge_reg_assocs rs2) (merge_reg_assocs trs2) *) -(* /\ match_arr_assocs (merge_arr_assocs (ram_mem ram) (ram_size ram) ar2) *) -(* (merge_arr_assocs (ram_mem ram) (ram_size ram) tar2)). *) -(* Proof. *) -(* induction l as [| a l IHl]; simplify. *) -(* - match goal with *) -(* | H: (_, _) = (_, _) |- _ => inv H *) -(* end; *) -(* unfold exec_all in *; repeat inv_exists; simplify. *) -(* exploit match_states_same; *) -(* try match goal with *) -(* | H: stmnt_runp _ _ _ ?c _ _, H2: (mod_controllogic _) ! _ = Some ?c |- _ => apply H *) -(* end; eauto; mgen_crush; *) -(* try match goal with *) -(* | H: (mod_controllogic _) ! _ = Some ?c |- _ => *) -(* apply max_reg_stmnt_le_stmnt_tree in H; unfold max_reg_module in *; lia *) -(* end; intros; *) -(* exploit match_states_same; *) -(* try match goal with *) -(* | H: stmnt_runp _ _ _ ?c _ _, H2: (mod_datapath _) ! _ = Some ?c |- _ => apply H *) -(* end; eauto; mgen_crush; *) -(* try match goal with *) -(* | H: (mod_datapath _) ! _ = Some ?c |- _ => *) -(* apply max_reg_stmnt_le_stmnt_tree in H; unfold max_reg_module in *; lia *) -(* end; intros; *) -(* repeat match goal with *) -(* | |- exists _, _ => eexists *) -(* end; simplify; eauto; *) -(* unfold exec_all_ram; *) -(* repeat match goal with *) -(* | |- exists _, _ => eexists *) -(* end; simplify; eauto. *) -(* constructor. admit. *) -(* Abort. *) - Lemma empty_stack_transf : forall m, empty_stack (transf_module m) = empty_stack m. Proof. unfold empty_stack, transf_module; intros; repeat destruct_match; crush. Qed. |