From 8bc6214e053aa4487abfbd895c00e2da9f21bd8a Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Mon, 30 Aug 2021 22:15:02 +0100 Subject: WIP --- src/hls/ApplyExternctrl.v | 59 ++++++++------ src/hls/HTL.v | 16 +++- src/hls/HTLgen.v | 11 --- src/hls/Renaming.v | 8 +- src/hls/Veriloggen.v | 16 +++- src/hls/Veriloggenproof.v | 190 +++++++++++++++++++++++----------------------- 6 files changed, 160 insertions(+), 140 deletions(-) (limited to 'src/hls') diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v index b024b9e..edd413c 100644 --- a/src/hls/ApplyExternctrl.v +++ b/src/hls/ApplyExternctrl.v @@ -89,14 +89,14 @@ Section APPLY_EXTERNCTRL. end. Definition cases_apply_externctrl_ (stmnt_apply_externctrl_ : Verilog.stmnt -> res Verilog.stmnt) := - fix cases_apply_externctrl (cs : list (Verilog.expr * Verilog.stmnt)) := + fix cases_apply_externctrl (cs : stmnt_expr_list) := match cs with - | nil => OK nil - | (c_e, c_s) :: tl => + | Stmntnil => OK Stmntnil + | Stmntcons c_e c_s tl => do c_e' <- expr_apply_externctrl c_e; do c_s' <- stmnt_apply_externctrl_ c_s; do tl' <- cases_apply_externctrl tl; - OK ((c_e', c_s') :: tl') + OK (Stmntcons c_e' c_s' tl') end. Fixpoint stmnt_apply_externctrl (stmnt : Verilog.stmnt) {struct stmnt} : res Verilog.stmnt := @@ -142,6 +142,12 @@ Section APPLY_EXTERNCTRL. do l <- xassocmap_apply_externctrl (AssocMap.elements regmap); OK (AssocMap_Properties.of_list l). + + Definition decide_ram_wf (clk : reg) (mr : option HTL.ram) : + option (forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive). + destruct mr. + - intros. + Definition module_apply_externctrl : res HTL.module := do mod_start' <- reg_apply_externctrl (HTL.mod_start m); do mod_reset' <- reg_apply_externctrl (HTL.mod_reset m); @@ -159,26 +165,33 @@ Section APPLY_EXTERNCTRL. do mod_externctrl' <- assocmap_apply_externctrl (HTL.mod_externctrl m); match zle (Z.pos (max_pc_map mod_datapath')) Integers.Int.max_unsigned, - zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned with - | left LEDATA, left LECTRL => + zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned, + decide_order mod_st' mod_finish' mod_return' mod_stk' mod_start' mod_reset' mod_clk', + max_list_dec mod_params' mod_st', + decide_ram_wf mod_clk' (HTL.mod_ram m) with + | left LEDATA, left LECTRL, left MORD, left WFPARAMS => OK (HTL.mkmodule - mod_params' - mod_datapath' - mod_controllogic' - (HTL.mod_entrypoint m) - mod_st' - mod_stk' - (HTL.mod_stk_len m) - mod_finish' - mod_return' - mod_start' - mod_reset' - mod_clk' - mod_scldecls' - mod_arrdecls' - mod_externctrl' - (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))) - | _, _ => Error (Errors.msg "More than 2^32 states.") + mod_params' + mod_datapath' + mod_controllogic' + (HTL.mod_entrypoint m) + mod_st' + mod_stk' + (HTL.mod_stk_len m) + mod_finish' + mod_return' + mod_start' + mod_reset' + mod_clk' + mod_scldecls' + mod_arrdecls' + mod_externctrl' + (HTL.mod_ram m) + (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA)) + MORD + (HTL.mod_ram_wf m) + WFPARAMS) + | _, _, _, _ => Error (Errors.msg "ApplyExternctrl") end. End APPLY_EXTERNCTRL. diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 886f86d..c22497f 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -110,7 +110,6 @@ Record module: Type := (** Map from registers in this module to control registers in other modules. These will be mapped to the same verilog register. *) mod_externctrl : AssocMap.t (ident * controlsignal); - mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); mod_ram : option ram; mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath; mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk; @@ -141,7 +140,7 @@ Definition prog_modmap (p : HTL.program) := (AST.prog_defs p)). Lemma max_pc_wf : - forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + forall T m, (Z.pos (max_pc_map m) <= Integers.Int.max_unsigned)%Z -> @map_well_formed T m. Proof. unfold map_well_formed. intros. @@ -257,7 +256,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := asr' = Verilog.merge_regs nasr3 basr3 -> asa' = Verilog.merge_arrs nasa3 basa3 -> asr'!(m.(mod_st)) = Some (posToValue pstval) -> - Z.pos pstval <= Integers.Int.max_unsigned -> + (Z.pos pstval <= Integers.Int.max_unsigned)%Z -> step g (State sf mid m st asr asa) Events.E0 (State sf mid m pstval asr' asa') @@ -437,3 +436,14 @@ Definition max_list_dec (l: list reg) (st: reg) : {Forall (Pos.gt st) l} + {True ); auto. apply max_list_correct. apply Pos.ltb_lt in e. lia. Qed. + +Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}. + refine (match bool_dec ((a left _ + | _ => _ + end); auto. + simplify; repeat match goal with + | H: context[(_ apply Pos.ltb_lt in H + end; unfold module_ordering; auto. +Defined. diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 0b7f3ec..84e1a0f 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -626,17 +626,6 @@ Proof. simplify. transitivity (Z.pos (max_pc_map m)); eauto. Qed. -Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}. - refine (match bool_dec ((a left _ - | _ => _ - end); auto. - simplify; repeat match goal with - | H: context[(_ apply Pos.ltb_lt in H - end; unfold module_ordering; auto. -Defined. - Definition transf_module (f: function) : mon HTL.module. refine ( if stack_correct f.(fn_stacksize) then diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v index b9fbcaa..6c816c2 100644 --- a/src/hls/Renaming.v +++ b/src/hls/Renaming.v @@ -102,12 +102,12 @@ Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) := ret (Vcond e' s1' s2') | Vcase e cs def => do e' <- renumber_expr e; - do cs' <- sequence (map - (fun (c : (Verilog.expr * Verilog.stmnt)) => - let (c_expr, c_stmnt) := c in + do cs_list' <- sequence (map + (fun '(c_expr, c_stmnt) => do expr' <- renumber_expr c_expr; do stmnt' <- renumber_stmnt c_stmnt; - ret (expr', stmnt')) cs); + ret (expr', stmnt')) (stmnt_to_list cs)); + let cs' := list_to_stmnt cs_list' in do def' <- match def with | None => ret None | Some d => do def' <- renumber_stmnt d; ret (Some def') diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index 1ded68a..1e7bb8e 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -62,8 +62,16 @@ Section TRANSLATE. | _ => Some it end. - Definition mod_body (m : HTL.module) := - + Definition inst_ram clk ram := + Valways (Vnegedge clk) + (Vcond (Vbinop Vne (Vvar (ram_u_en ram)) (Vvar (ram_en ram))) + (Vseq (Vcond (Vvar (ram_wr_en ram)) + (Vnonblock (Vvari (ram_mem ram) (Vvar (ram_addr ram))) + (Vvar (ram_d_in ram))) + (Vnonblock (Vvar (ram_d_out ram)) + (Vvari (ram_mem ram) (Vvar (ram_addr ram))))) + (Vnonblock (Vvar (ram_en ram)) (Vvar (ram_u_en ram)))) + Vskip). (* FIXME Remove the fuel parameter (recursion limit)*) Fixpoint transl_module (fuel : nat) (prog : HTL.program) (externclk : option reg) (m : HTL.module) : res Verilog.module := @@ -85,8 +93,8 @@ Section TRANSLATE. translated_modules in - let case_el_ctrl := transl_states (PTree.elements (HTL.mod_controllogic m)) in - let case_el_data := transl_states (PTree.elements (HTL.mod_datapath m)) in + let case_el_ctrl := list_to_stmnt (transl_states (PTree.elements (HTL.mod_controllogic m))) in + let case_el_data := list_to_stmnt (transl_states (PTree.elements (HTL.mod_datapath m))) in let externctrl := HTL.mod_externctrl m in diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index c54f726..8ecab63 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -264,114 +264,114 @@ Admitted. (* 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 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_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_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_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_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_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_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_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_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 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. +(* 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. +(* 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 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. +(* 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. -- cgit