diff options
Diffstat (limited to 'src/hls/HTLPargen.v')
-rw-r--r-- | src/hls/HTLPargen.v | 155 |
1 files changed, 83 insertions, 72 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 9213514..01588f6 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -27,6 +27,7 @@ Require Import compcert.lib.Maps. Require Import vericert.common.Statemonad. Require Import vericert.common.Vericertlib. Require Import vericert.hls.AssocMap. +Require Import vericert.hls.FunctionalUnits. Require Import vericert.hls.HTL. Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLPar. @@ -49,6 +50,7 @@ Record state: Type := mkstate { st_arrdecls: AssocMap.t (option io * arr_decl); st_datapath: datapath; st_controllogic: controllogic; + st_funct_units: funct_units; }. Definition init_state (st : reg) : state := @@ -58,7 +60,8 @@ Definition init_state (st : reg) : state := (AssocMap.empty (option io * scl_decl)) (AssocMap.empty (option io * arr_decl)) (AssocMap.empty stmnt) - (AssocMap.empty stmnt). + (AssocMap.empty stmnt) + initial_funct_units. Module HTLState <: State. @@ -128,7 +131,8 @@ Lemma declare_reg_state_incr : (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_datapath) - s.(st_controllogic)). + s.(st_controllogic) + s.(st_funct_units)). Proof. auto with htlh. Qed. Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := @@ -139,7 +143,8 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_datapath) - s.(st_controllogic)) + s.(st_controllogic) + s.(st_funct_units)) (declare_reg_state_incr i s r sz). Lemma add_instr_state_incr : @@ -153,7 +158,8 @@ Lemma add_instr_state_incr : s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic)) + s.(st_funct_units)). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -171,7 +177,8 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic)) + s.(st_funct_units)) (add_instr_state_incr s n n' st TRANS) | _ => Error (Errors.msg "HTL.add_instr") end. @@ -187,7 +194,8 @@ Lemma add_instr_skip_state_incr : s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n Vskip s.(st_controllogic))). + (AssocMap.set n Vskip s.(st_controllogic)) + s.(st_funct_units)). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -205,7 +213,8 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit := s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n Vskip s.(st_controllogic))) + (AssocMap.set n Vskip s.(st_controllogic)) + s.(st_funct_units)) (add_instr_skip_state_incr s n st TRANS) | _ => Error (Errors.msg "HTL.add_instr_skip") end. @@ -221,7 +230,8 @@ Lemma add_node_skip_state_incr : s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n Vskip s.(st_datapath)) - (AssocMap.set n st s.(st_controllogic))). + (AssocMap.set n st s.(st_controllogic)) + s.(st_funct_units)). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -239,7 +249,8 @@ Definition add_node_skip (n : node) (st : stmnt) : mon unit := s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n Vskip s.(st_datapath)) - (AssocMap.set n st s.(st_controllogic))) + (AssocMap.set n st s.(st_controllogic)) + s.(st_funct_units)) (add_node_skip_state_incr s n st TRANS) | _ => Error (Errors.msg "HTL.add_node_skip") end. @@ -327,6 +338,32 @@ Definition check_address_parameter_signed (p : Z) : bool := Definition check_address_parameter_unsigned (p : Z) : bool := Z.leb p Integers.Ptrofs.max_unsigned. +Lemma create_reg_state_incr: + forall s sz i, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + (st_datapath s) + (st_controllogic s) + s.(st_funct_units)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_reg (i : option io) (sz : nat) : mon reg := + fun s => let r := s.(st_freshreg) in + OK r (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + (st_arrdecls s) + (st_datapath s) + (st_controllogic s) + s.(st_funct_units)) + (create_reg_state_incr s sz i). + Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) @@ -355,7 +392,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) end. (** Translate an instruction to a statement. FIX mulhs mulhu *) -Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := +Definition translate_instr (op : Op.operation) (args : list reg) : mon stmnt := match op, args with | Op.Omove, r::nil => ret (Vvar r) | Op.Ointconst n, _ => ret (Vlit (intToValue n)) @@ -365,7 +402,19 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Omulimm n, r::nil => ret (boplit Vmul r n) | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs") | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu") - | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2) + | Op.Odiv, r1::r2::nil => + do s <- get; + match sdiv_present s.(st_funct_units) 32%positive with + | SignedDiv s n d q r :: _ => + ret (Vseq (Vnonblock (Vvar n) (Vvar r1)) (Vnonblock (Vvar d) (Vvar r2))) + | _ => + do n <- create_reg None 32; + do d <- create_reg None 32; + do q <- create_reg None 32; + do r <- create_reg None 32; + do _ <- add_funct_unit (SignedDiv 32%positive n d q r); + ret (Vseq (Vnonblock (Vvar n) (Vvar r1)) (Vnonblock (Vvar d) (Vvar r2))) + end | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2) | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2) | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2) @@ -408,7 +457,8 @@ Lemma add_branch_instr_state_incr: s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n Vskip (st_datapath s)) - (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)) + s.(st_funct_units)). Proof. intros. apply state_incr_intro; simpl; try (intros; destruct (peq n0 n); subst); @@ -426,7 +476,8 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n Vskip (st_datapath s)) - (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)) + s.(st_funct_units)) (add_branch_instr_state_incr s e n n1 n2 NTRANS) | _ => Error (Errors.msg "Htlgen: add_branch_instr") end. @@ -468,30 +519,6 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). -Lemma create_reg_state_incr: - forall s sz i, - st_incr s (mkstate - s.(st_st) - (Pos.succ (st_freshreg s)) - (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) - s.(st_arrdecls) - (st_datapath s) - (st_controllogic s)). -Proof. constructor; simpl; auto with htlh. Qed. - -Definition create_reg (i : option io) (sz : nat) : mon reg := - fun s => let r := s.(st_freshreg) in - OK r (mkstate - s.(st_st) - (Pos.succ r) - (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) - (st_arrdecls s) - (st_datapath s) - (st_controllogic s)) - (create_reg_state_incr s sz i). - Lemma create_arr_state_incr: forall s sz ln i, st_incr s (mkstate @@ -501,7 +528,8 @@ Lemma create_arr_state_incr: s.(st_scldecls) (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) (st_datapath s) - (st_controllogic s)). + (st_controllogic s) + s.(st_funct_units)). Proof. constructor; simpl; auto with htlh. Qed. Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := @@ -513,7 +541,8 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := s.(st_scldecls) (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) (st_datapath s) - (st_controllogic s)) + (st_controllogic s) + s.(st_funct_units)) (create_arr_state_incr s sz ln i). Definition max_pc_map (m : Maps.PTree.t stmnt) := @@ -576,7 +605,8 @@ Lemma add_data_instr_state_incr : s.(st_arrdecls) (AssocMap.set n (Vseq (AssocMapExt.get_default _ Vskip n s.(st_datapath)) st) s.(st_datapath)) - s.(st_controllogic)). + s.(st_controllogic) + s.(st_funct_units)). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -592,7 +622,8 @@ Definition add_data_instr (n : node) (st : stmnt) : mon unit := s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n (Vseq (AssocMapExt.get_default _ Vskip n s.(st_datapath)) st) s.(st_datapath)) - s.(st_controllogic)) + s.(st_controllogic) + s.(st_funct_units)) (add_data_instr_state_incr s n st). Lemma add_control_instr_state_incr : @@ -606,7 +637,8 @@ Lemma add_control_instr_state_incr : s.(st_scldecls) s.(st_arrdecls) s.(st_datapath) - (AssocMap.set n st s.(st_controllogic))). + (AssocMap.set n st s.(st_controllogic)) + s.(st_funct_units)). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -624,38 +656,13 @@ Definition add_control_instr (n : node) (st : stmnt) : mon unit := s.(st_scldecls) s.(st_arrdecls) s.(st_datapath) - (AssocMap.set n st s.(st_controllogic))) + (AssocMap.set n st s.(st_controllogic)) + s.(st_funct_units)) (add_control_instr_state_incr s n st CTRL) | _ => Error (Errors.msg "HTLPargen.add_control_instr: control logic is not empty") end. -Definition add_control_instr_force_state_incr : - forall s n st, - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - s.(st_datapath) - (AssocMap.set n st s.(st_controllogic))). -Admitted. - -Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := - fun s => - OK tt (mkstate - s.(st_st) - s.(st_freshreg) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - s.(st_datapath) - (AssocMap.set n st s.(st_controllogic))) - (add_control_instr_force_state_incr s n st). - - Fixpoint pred_expr (preg: reg) (p: pred_op) := match p with | Pvar pred => @@ -707,7 +714,8 @@ Lemma create_new_state_state_incr: s.(st_scldecls) s.(st_arrdecls) s.(st_datapath) - s.(st_controllogic)). + s.(st_controllogic) + s.(st_funct_units)). Admitted. Definition create_new_state (p: node): mon node := @@ -719,7 +727,8 @@ Definition create_new_state (p: node): mon node := s.(st_scldecls) s.(st_arrdecls) s.(st_datapath) - s.(st_controllogic)) + s.(st_controllogic) + s.(st_funct_units)) (create_new_state_state_incr s p). Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list (list instr)) := @@ -819,6 +828,7 @@ Definition transf_module (f: function) : mon HTL.module := start rst clk + nil current_state.(st_scldecls) current_state.(st_arrdecls) (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) @@ -834,7 +844,8 @@ Definition max_state (f: function) : state := (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st))) (st_arrdecls (init_state st)) (st_datapath (init_state st)) - (st_controllogic (init_state st)). + (st_controllogic (init_state st)) + (st_funct_units (init_state st)). Definition transl_module (f : function) : Errors.res HTL.module := run_mon (max_state f) (transf_module f). |