diff options
Diffstat (limited to 'src/hls/Veriloggenproof.v')
-rw-r--r-- | src/hls/Veriloggenproof.v | 198 |
1 files changed, 186 insertions, 12 deletions
diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 5c484d3..ccc0688 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -225,6 +225,116 @@ Proof. Qed. 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. +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. Variable prog: HTL.program. @@ -269,6 +379,12 @@ Section CORRECTNESS. Qed. 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, HTL.step ge S1 t S2 -> @@ -276,13 +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. - Admitted. -(* - econstructor; split. apply Smallstep.plus_one. econstructor. - assumption. assumption. eassumption. apply valueToPos_posToValue. + induction 1; intros R1 MSTATE; inv MSTATE; destruct (HTL.mod_ram m) eqn:?. + - 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. @@ -314,19 +431,76 @@ Section CORRECTNESS. 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. - apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto. - rewrite valueToPos_posToValue. constructor; assumption. lia. + 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 _]. + 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. + + 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. - - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. 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. - Qed.*) + 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. Lemma transl_initial_states : |