diff options
| -rw-r--r-- | src/hls/HTL.v | 1 | ||||
| -rw-r--r-- | src/hls/HTLgen.v | 12 | ||||
| -rw-r--r-- | src/hls/HTLgenproof.v | 13 | ||||
| -rw-r--r-- | src/hls/HTLgenspec.v | 37 |
4 files changed, 47 insertions, 16 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 4f00c79..8474878 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -59,6 +59,7 @@ Inductive controlsignal : Type := | ctrl_return : controlsignal | ctrl_start : controlsignal | ctrl_reset : controlsignal + | ctrl_clk : controlsignal | ctrl_param (idx : nat) : controlsignal. Definition controlsignal_sz (s : controlsignal) : nat := diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 5400e25..42631ca 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -584,7 +584,7 @@ Proof. simplify. transitivity (Z.pos (max_pc_map m)); eauto. Qed. -Definition transf_module (f: function) : mon HTL.module := +Definition transf_module (main : ident) (f: function) : mon HTL.module := if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; @@ -593,7 +593,7 @@ Definition transf_module (f: function) : mon HTL.module := 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; + do clk <- map_externctrl main ctrl_clk; do current_state <- get; match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with @@ -630,10 +630,10 @@ Definition max_state (f: function) : state := (st_datapath (init_state st)) (st_controllogic (init_state st)). -Definition transl_module (f : function) : Errors.res HTL.module := - run_mon (max_state f) (transf_module f). +Definition transl_module main (f : function) : Errors.res HTL.module := + run_mon (max_state f) (transf_module main f). -Definition transl_fundef := transf_partial_fundef transl_module. +Definition transl_fundef main := transf_partial_fundef (transl_module main). (* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *) @@ -877,5 +877,5 @@ Definition main_is_internal (p : RTL.program) : bool := Definition transl_program (p : RTL.program) : Errors.res HTL.program := if main_is_internal p - then transform_partial_program transl_fundef p + then transform_partial_program (transl_fundef p.(prog_main)) p else Errors.Error (Errors.msg "Main function is not Internal."). diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 2b9fb0a..8c2d4af 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -136,7 +136,7 @@ Inductive match_states : RTL.state -> HTL.state -> Prop := Hint Constructors match_states : htlproof. Definition match_prog (p: RTL.program) (tp: HTL.program) := - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\ + Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main p) f = Errors.OK tf) eq p tp /\ main_is_internal p = true. Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program): @@ -158,7 +158,7 @@ Proof. Qed. Definition match_prog' (p: RTL.program) (tp: HTL.program) := - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main p) f = Errors.OK tf) eq p tp. Lemma match_prog_matches : forall p tp, match_prog p tp -> match_prog' p tp. @@ -355,10 +355,11 @@ Section CORRECTNESS. Variable prog : RTL.program. Variable tprog : HTL.program. + Hypothesis TRANSL : match_prog prog tprog. Lemma TRANSL' : - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. + Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main prog) f = Errors.OK tf) eq prog tprog. Proof. intros; apply match_prog_matches; assumption. Qed. Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. @@ -372,7 +373,7 @@ Section CORRECTNESS. forall (b: Values.block) (f: RTL.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef (AST.prog_main prog) f = Errors.OK tf. Proof. intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. @@ -382,7 +383,7 @@ Section CORRECTNESS. forall (v: Values.val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> exists tf, - Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. + Genv.find_funct tge v = Some tf /\ transl_fundef (AST.prog_main prog) f = Errors.OK tf. Proof. intros. exploit (Genv.find_funct_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. @@ -2759,7 +2760,7 @@ Section CORRECTNESS. apply H6. constructor. - apply transl_module_correct. + apply transl_module_correct with (AST.prog_main prog). assert (Some (AST.Internal x) = Some (AST.Internal m)). replace (AST.fundef HTL.module) with (HTL.fundef). rewrite <- H6. setoid_rewrite <- A. trivial. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 8b4e63b..77e8c3d 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -217,6 +217,24 @@ Lemma create_reg_controllogic_trans : Proof. intros. monadInv H. trivial. Qed. Hint Resolve create_reg_controllogic_trans : htlspec. +Lemma map_externctrl_datapath_trans : + forall s s' x i om sig, + map_externctrl om sig s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. + intros. monadInv H. apply create_reg_datapath_trans in EQ. auto. +Qed. +Hint Resolve map_externctrl_datapath_trans : htlspec. + +Lemma map_externctrl_controllogic_trans : + forall s s' x i om sig, + map_externctrl om sig s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. + intros. monadInv H. apply create_reg_controllogic_trans in EQ. auto. +Qed. +Hint Resolve map_externctrl_datapath_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 -> @@ -272,6 +290,10 @@ Ltac inv_incr := let H1 := fresh "H" in assert (H1 := H); eapply create_reg_datapath_trans in H; eapply create_reg_controllogic_trans in H1 + | [ H: map_externctrl _ _ ?s = OK _ ?s' _ |- _ ] => + let H1 := fresh "H" in + assert (H1 := H); eapply map_externctrl_datapath_trans in H; + eapply map_externctrl_controllogic_trans in H1 | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => let H1 := fresh "H" in assert (H1 := H); eapply create_arr_datapath_trans in H; @@ -633,14 +655,21 @@ Proof. inversion 1; auto. Qed. +Lemma map_externctrl_inv : forall a b s r s' i, + map_externctrl a b s = OK r s' i -> + r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). +Proof. + inversion 1; auto. +Qed. + Theorem transl_module_correct : - forall f m, - transl_module f = Errors.OK m -> tr_module f m. + forall i f m, + transl_module i f = Errors.OK m -> tr_module f m. Proof. intros until m. unfold transl_module. unfold run_mon. - destruct (transf_module f (max_state f)) eqn:?; try discriminate. + destruct (transf_module i f (max_state f)) eqn:?; try discriminate. intros. inv H. inversion s; subst. @@ -663,7 +692,7 @@ Proof. pose proof (collect_declare_freshreg_trans _ _ _ _ _ _ EQ3) as TR_DEC. pose proof (create_reg_inv _ _ _ _ _ _ EQ4) as START_VAL. inv START_VAL. pose proof (create_reg_inv _ _ _ _ _ _ EQ5) as RESET_VAL. inv RESET_VAL. - pose proof (create_reg_inv _ _ _ _ _ _ EQ6) as CLK_VAL. inv CLK_VAL. + pose proof (map_externctrl_inv _ _ _ _ _ _ EQ6) as CLK_VAL. inv CLK_VAL. rewrite H9 in *. rewrite H8 in *. replace (st_freshreg s4) with (st_freshreg s2) in * by congruence. rewrite H6 in *. rewrite H7 in *. rewrite H5 in *. simpl in *. inv_incr. |