diff options
Diffstat (limited to 'src/hls/Veriloggenproof.v')
| -rw-r--r-- | src/hls/Veriloggenproof.v | 218 |
1 files changed, 197 insertions, 21 deletions
diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 9abbd4b..d1494ec 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -115,7 +115,7 @@ Lemma Zle_relax : p < q <= r -> p <= q <= r. Proof. lia. Qed. -Hint Resolve Zle_relax : verilogproof. +#[local] Hint Resolve Zle_relax : verilogproof. Lemma transl_in : forall l p, @@ -178,7 +178,7 @@ Lemma transl_list_correct : stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} - (Vcase (Vvar ev) (transl_list l) (Some Vskip)) + (Vcase (Vvar ev) (list_to_stmnt (transl_list l)) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). Proof. @@ -202,7 +202,7 @@ Proof. eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H. trivial. assumption. Qed. -Hint Resolve transl_list_correct : verilogproof. +#[local] Hint Resolve transl_list_correct : verilogproof. Lemma pc_wf : forall A m p v, @@ -223,7 +223,117 @@ Proof. - intros. constructor. - intros. simplify. econstructor. constructor. auto. Qed. -Hint Resolve mis_stepp_decl : verilogproof. +#[local] Hint Resolve mis_stepp_decl : verilogproof. + +Lemma mis_stepp_negedge_decl : + forall l asr asa f, + mis_stepp_negedge f asr asa (map Vdeclaration l) asr asa. +Proof. + induction l. + - intros. constructor. + - intros. simplify. econstructor. constructor. auto. +Qed. +#[local] Hint Resolve mis_stepp_negedge_decl : verilogproof. + +Lemma mod_entrypoint_equiv m : mod_entrypoint (transl_module m) = HTL.mod_entrypoint m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_st_equiv m : mod_st (transl_module m) = HTL.mod_st m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_stk_equiv m : mod_stk (transl_module m) = HTL.mod_stk m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_stk_len_equiv m : mod_stk_len (transl_module m) = HTL.mod_stk_len m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_finish_equiv m : mod_finish (transl_module m) = HTL.mod_finish m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_reset_equiv m : mod_reset (transl_module m) = HTL.mod_reset m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_clk_equiv m : mod_clk (transl_module m) = HTL.mod_clk m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_return_equiv m : mod_return (transl_module m) = HTL.mod_return m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma mod_params_equiv m : mod_args (transl_module m) = HTL.mod_params m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Lemma empty_stack_equiv m : empty_stack (transl_module m) = HTL.empty_stack m. +Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. + +Ltac rewrite_eq := rewrite mod_return_equiv + || rewrite mod_clk_equiv + || rewrite mod_reset_equiv + || rewrite mod_finish_equiv + || rewrite mod_stk_len_equiv + || rewrite mod_stk_equiv + || rewrite mod_st_equiv + || rewrite mod_entrypoint_equiv + || rewrite mod_params_equiv + || rewrite empty_stack_equiv. + +Lemma find_assocmap_get r i v : r ! i = Some v -> r # i = v. +Proof. + intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. auto. +Qed. + +Lemma ram_exec_match : + forall f asr asa asr' asa' r clk, + HTL.exec_ram asr asa (Some r) asr' asa' -> + mi_stepp_negedge f asr asa (inst_ram clk r) asr' asa'. +Proof. + inversion 1; subst; simplify. + { unfold inst_ram. econstructor. + eapply stmnt_runp_Vcond_false. + econstructor. econstructor. econstructor. auto. + econstructor. auto. + simplify. + unfold boolToValue, natToValue, valueToBool. + rewrite Int.eq_sym. rewrite H3. simplify. + auto. constructor. } + { unfold inst_ram. econstructor. econstructor. econstructor. + econstructor. econstructor. auto. + econstructor. auto. + simplify. + unfold boolToValue, natToValue, valueToBool. + pose proof H4 as X. apply find_assocmap_get in X. + rewrite X. rewrite Int.eq_sym. rewrite H1. auto. + econstructor. econstructor. econstructor. econstructor. + pose proof H5 as X. apply find_assocmap_get in X. + rewrite X. + unfold valueToBool. unfold ZToValue in *. + unfold Int.eq in H2. + unfold uvalueToZ. + assert (Int.unsigned wr_en =? 0 = false). + apply Z.eqb_neq. rewrite Int.unsigned_repr in H2 by (simplify; lia). + destruct (zeq (Int.unsigned wr_en) 0); crush. + rewrite H0. auto. + apply stmnt_runp_Vnonblock_arr. econstructor. econstructor. auto. + econstructor. econstructor. + apply find_assocmap_get in H9. rewrite H9. + apply find_assocmap_get in H6. rewrite H6. + repeat econstructor. apply find_assocmap_get; auto. + } + { econstructor. econstructor. econstructor. econstructor. auto. + econstructor. auto. + econstructor. + unfold boolToValue, natToValue, valueToBool. + apply find_assocmap_get in H3. rewrite H3. + rewrite Int.eq_sym. rewrite H1. auto. + econstructor. + eapply stmnt_runp_Vcond_false. econstructor. auto. + simplify. apply find_assocmap_get in H4. rewrite H4. + auto. + repeat (econstructor; auto). apply find_assocmap_get in H5. + rewrite H5. eassumption. + repeat econstructor. simplify. apply find_assocmap_get; auto. + } +Qed. + Section CORRECTNESS. @@ -238,7 +348,7 @@ Section CORRECTNESS. Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed. - Hint Resolve symbols_preserved : verilogproof. + #[local] Hint Resolve symbols_preserved : verilogproof. Lemma function_ptr_translated: forall (b: Values.block) (f: HTL.fundef), @@ -249,7 +359,7 @@ Section CORRECTNESS. intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. - Hint Resolve function_ptr_translated : verilogproof. + #[local] Hint Resolve function_ptr_translated : verilogproof. Lemma functions_translated: forall (v: Values.val) (f: HTL.fundef), @@ -260,14 +370,20 @@ Section CORRECTNESS. intros. exploit (Genv.find_funct_match TRANSL); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. - Hint Resolve functions_translated : verilogproof. + #[local] Hint Resolve functions_translated : verilogproof. Lemma senv_preserved: Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). Proof. intros. eapply (Genv.senv_match TRANSL). Qed. - Hint Resolve senv_preserved : verilogproof. + #[local] Hint Resolve senv_preserved : verilogproof. + + Ltac unfold_replace := + match goal with + | H: HTL.mod_ram _ = _ |- context[transl_module] => + unfold transl_module; rewrite H + end. Theorem transl_step_correct : forall (S1 : HTL.state) t S2, @@ -276,12 +392,14 @@ Section CORRECTNESS. match_states S1 R1 -> exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. Proof. - induction 1; intros R1 MSTATE; inv MSTATE. + induction 1; intros R1 MSTATE; inv MSTATE; destruct (HTL.mod_ram m) eqn:?. - econstructor; split. apply Smallstep.plus_one. econstructor. - assumption. assumption. eassumption. apply valueToPos_posToValue. + unfold_replace. assumption. unfold_replace. assumption. + unfold_replace. eassumption. apply valueToPos_posToValue. split. lia. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. split. lia. apply HP. eassumption. eassumption. + unfold_replace. econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. simpl. unfold find_assocmap. unfold AssocMapExt.get_default. rewrite H. trivial. @@ -303,7 +421,40 @@ Section CORRECTNESS. econstructor. econstructor. eapply transl_list_correct. - intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. + intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. + auto. apply Maps.PTree.elements_keys_norepet. eassumption. + 2: { apply valueToPos_inj. apply unsigned_posToValue_le. + eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. + apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. + destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. trivial. + } + apply Maps.PTree.elements_correct. eassumption. eassumption. + econstructor. econstructor. + apply mis_stepp_decl. simplify. unfold_replace. simplify. + econstructor. econstructor. econstructor. econstructor. + econstructor. + apply ram_exec_match. eauto. + apply mis_stepp_negedge_decl. simplify. auto. auto. + rewrite_eq. eauto. auto. + rewrite valueToPos_posToValue. econstructor. auto. + simplify; lia. + - inv H7. econstructor; split. apply Smallstep.plus_one. econstructor. + unfold_replace. assumption. unfold_replace. assumption. + unfold_replace. eassumption. apply valueToPos_posToValue. + split. lia. + eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. + unfold_replace. + econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. + simpl. unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite H. trivial. + + econstructor. simpl. auto. auto. + + eapply transl_list_correct. + intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto. apply Maps.PTree.elements_keys_norepet. eassumption. 2: { apply valueToPos_inj. apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. @@ -314,19 +465,44 @@ Section CORRECTNESS. } apply Maps.PTree.elements_correct. eassumption. eassumption. - apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto. - rewrite valueToPos_posToValue. constructor; assumption. lia. + econstructor. econstructor. - - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption. + eapply transl_list_correct. + intros. split. lia. pose proof (HTL.mod_wf m) as HP. + destruct HP as [_ HP]; auto. + apply Maps.PTree.elements_keys_norepet. eassumption. + 2: { apply valueToPos_inj. apply unsigned_posToValue_le. + eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. + apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. + destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. trivial. + } + apply Maps.PTree.elements_correct. eassumption. eassumption. + + apply mis_stepp_decl. simplify. + unfold_replace. + repeat econstructor. apply mis_stepp_negedge_decl. trivial. trivial. + simpl. unfold_replace. eassumption. auto. simplify. + rewrite valueToPos_posToValue. constructor; eassumption. simplify; lia. + - econstructor; split. apply Smallstep.plus_one. apply step_finish. + rewrite_eq. assumption. + rewrite_eq. eassumption. + econstructor; auto. + - econstructor; split. apply Smallstep.plus_one. apply step_finish. + unfold transl_module. rewrite Heqo. simplify. + assumption. unfold_replace. eassumption. constructor; assumption. - econstructor; split. apply Smallstep.plus_one. constructor. - - constructor. constructor. + repeat rewrite_eq. constructor. constructor. + - econstructor; split. apply Smallstep.plus_one. constructor. + repeat rewrite_eq. constructor. constructor. - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. - - apply match_state. assumption. + repeat rewrite_eq. apply match_state. assumption. + - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. + repeat rewrite_eq. apply match_state. assumption. Qed. - Hint Resolve transl_step_correct : verilogproof. + #[local] Hint Resolve transl_step_correct : verilogproof. Lemma transl_initial_states : forall s1 : Smallstep.state (HTL.semantics prog), @@ -344,7 +520,7 @@ Section CORRECTNESS. inv B. eauto. constructor. Qed. - Hint Resolve transl_initial_states : verilogproof. + #[local] Hint Resolve transl_initial_states : verilogproof. Lemma transl_final_states : forall (s1 : Smallstep.state (HTL.semantics prog)) @@ -356,7 +532,7 @@ Section CORRECTNESS. Proof. intros. inv H0. inv H. inv H3. constructor. reflexivity. Qed. - Hint Resolve transl_final_states : verilogproof. + #[local] Hint Resolve transl_final_states : verilogproof. Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). |