From 0f9ab38389000edfa2376fabace69d2366d32647 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 12 Jun 2020 13:18:40 +0100 Subject: Fix declaring function arguments correctly --- src/translation/HTLgen.v | 13 +++++----- src/translation/HTLgenspec.v | 62 +++++++++++++++++++++++++++++++++++++++++--- src/verilog/PrintVerilog.ml | 6 ++--- 3 files changed, 69 insertions(+), 12 deletions(-) diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 15100bf..bbce47c 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -125,28 +125,28 @@ Proof. Qed. Lemma declare_reg_state_incr : - forall s r sz, + forall i s r sz, st_incr s (mkstate s.(st_st) s.(st_freshreg) s.(st_freshstate) - (AssocMap.set r (None, Scalar sz) s.(st_scldecls)) + (AssocMap.set r (i, Scalar sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)). Proof. auto with htlh. Qed. -Definition declare_reg (r : reg) (sz : nat) : mon unit := +Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := fun s => OK tt (mkstate s.(st_st) s.(st_freshreg) s.(st_freshstate) - (AssocMap.set r (None, Scalar sz) s.(st_scldecls)) + (AssocMap.set r (i, Scalar sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)) - (declare_reg_state_incr s r sz). + (declare_reg_state_incr i s r sz). Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := fun s => @@ -359,7 +359,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Inop n' => add_instr n n' Vskip | Iop op args dst n' => do instr <- translate_instr op args; - do _ <- declare_reg dst 32; + do _ <- declare_reg None dst 32; add_instr n n' (nonblock dst instr) | Iload mem addr args dst n' => do src <- translate_arr_access mem addr args stack; @@ -437,6 +437,7 @@ Definition transf_module (f: function) : mon module := do rtrn <- create_reg (Some Voutput) 32; do stack <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); + do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); do start <- create_reg (Some Vinput) 1; do rst <- create_reg (Some Vinput) 1; do clk <- create_reg (Some Vinput) 1; diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 8bb90c6..770b372 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -209,6 +209,20 @@ Lemma create_reg_controllogic_trans : Proof. intros. monadInv H. trivial. Qed. Hint Resolve create_reg_controllogic_trans : htlspec. +Lemma declare_reg_datapath_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_datapath_trans : htlspec. + +Lemma declare_reg_controllogic_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_controllogic_trans : htlspec. + Lemma create_arr_datapath_trans : forall sz ln s s' x i iop, create_arr iop sz ln s = OK x s' i -> @@ -255,6 +269,44 @@ Ltac inv_incr := | [ H: st_incr _ _ |- _ ] => destruct st_incr end. +Lemma collect_controllogic_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_datapath_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_declare_controllogic_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. + intros. eapply collect_controllogic_trans; try eassumption. + intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. +Qed. + +Lemma collect_declare_datapath_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. + intros. eapply collect_datapath_trans; try eassumption. + intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. +Qed. + Ltac rewrite_states := match goal with | [ H: ?x ?s = ?x ?s' |- _ ] => @@ -395,9 +447,13 @@ Proof. econstructor; simpl; trivial. intros. inv_incr. - assert (STC: st_controllogic s9 = st_controllogic s3) by congruence. - assert (STD: st_datapath s9 = st_datapath s3) by congruence. - assert (STST: st_st s9 = st_st s3) by congruence. + assert (EQ3D := EQ3). + destruct x3. + apply collect_declare_datapath_trans in EQ3. + apply collect_declare_controllogic_trans in EQ3D. + assert (STC: st_controllogic s10 = st_controllogic s3) by congruence. + assert (STD: st_datapath s10 = st_datapath s3) by congruence. + assert (STST: st_st s10 = st_st s3) by congruence. rewrite STC. rewrite STD. rewrite STST. eapply iter_expand_instr_spec; eauto with htlspec. apply PTree.elements_complete. diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index d81bf18..700b8e3 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -180,8 +180,7 @@ let pprint_module i n m = concat [ indent i; "module "; (extern_atom n); "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n"; fold_map (pprint_module_item (i+1)) m.mod_body; - indent i; "endmodule\n\n"; - testbench + indent i; "endmodule\n\n" ] let print_result pp lst = @@ -201,4 +200,5 @@ let print_globdef pp (id, gd) = | _ -> () let print_program pp prog = - List.iter (print_globdef pp) prog.prog_defs + List.iter (print_globdef pp) prog.prog_defs; + pstr pp testbench -- cgit