diff options
Diffstat (limited to 'src/hls/HTLPargen.v')
| -rw-r--r-- | src/hls/HTLPargen.v | 246 |
1 files changed, 143 insertions, 103 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 629f53e..b66a704 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -29,16 +29,18 @@ Require Import vericert.common.Vericertlib. Require Import vericert.hls.AssocMap. Require Import vericert.hls.FunctionalUnits. Require Import vericert.hls.HTL. +Require Import vericert.hls.Predicate. Require Import vericert.hls.RTLBlockInstr. -Require Import vericert.hls.RTLPar. +Require Import vericert.hls.RTLParFU. +Require Import vericert.hls.FunctionalUnits. Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. -Hint Resolve AssocMap.gempty : htlh. -Hint Resolve AssocMap.gso : htlh. -Hint Resolve AssocMap.gss : htlh. -Hint Resolve Ple_refl : htlh. -Hint Resolve Ple_succ : htlh. +#[local] Hint Resolve AssocMap.gempty : htlh. +#[local] Hint Resolve AssocMap.gso : htlh. +#[local] Hint Resolve AssocMap.gss : htlh. +#[local] Hint Resolve Ple_refl : htlh. +#[local] Hint Resolve Ple_succ : htlh. Definition assignment : Type := expr -> expr -> stmnt. @@ -50,7 +52,6 @@ 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 := @@ -60,8 +61,7 @@ Definition init_state (st : reg) : state := (AssocMap.empty (option io * scl_decl)) (AssocMap.empty (option io * arr_decl)) (AssocMap.empty stmnt) - (AssocMap.empty stmnt) - initial_funct_units. + (AssocMap.empty stmnt). Module HTLState <: State. @@ -77,10 +77,10 @@ Module HTLState <: State. s1.(st_controllogic)!n = None \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> st_incr s1 s2. - Hint Constructors st_incr : htlh. + #[local] Hint Constructors st_incr : htlh. Definition st_prop := st_incr. - Hint Unfold st_prop : htlh. + #[local] Hint Unfold st_prop : htlh. Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed. @@ -131,9 +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_funct_units)). -Proof. auto with htlh. Qed. + s.(st_controllogic)). +Proof. Admitted. Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := fun s => OK tt (mkstate @@ -143,8 +142,7 @@ 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_funct_units)) + s.(st_controllogic)) (declare_reg_state_incr i s r sz). Lemma add_instr_state_incr : @@ -158,8 +156,7 @@ 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)) - s.(st_funct_units)). + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -177,8 +174,7 @@ 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)) - s.(st_funct_units)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) (add_instr_state_incr s n n' st TRANS) | _ => Error (Errors.msg "HTL.add_instr") end. @@ -194,8 +190,7 @@ 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)) - s.(st_funct_units)). + (AssocMap.set n Vskip s.(st_controllogic))). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -213,8 +208,7 @@ 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)) - s.(st_funct_units)) + (AssocMap.set n Vskip s.(st_controllogic))) (add_instr_skip_state_incr s n st TRANS) | _ => Error (Errors.msg "HTL.add_instr_skip") end. @@ -230,8 +224,7 @@ 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)) - s.(st_funct_units)). + (AssocMap.set n st s.(st_controllogic))). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -249,8 +242,7 @@ 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)) - s.(st_funct_units)) + (AssocMap.set n st s.(st_controllogic))) (add_node_skip_state_incr s n st TRANS) | _ => Error (Errors.msg "HTL.add_node_skip") end. @@ -347,8 +339,7 @@ Lemma create_reg_state_incr: (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) (st_datapath s) - (st_controllogic s) - s.(st_funct_units)). + (st_controllogic s)). Proof. constructor; simpl; auto with htlh. Qed. Definition create_reg (i : option io) (sz : nat) : mon reg := @@ -360,8 +351,7 @@ Definition create_reg (i : option io) (sz : nat) : mon reg := (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) (st_arrdecls s) (st_datapath s) - (st_controllogic s) - s.(st_funct_units)) + (st_controllogic s)) (create_reg_state_incr s sz i). Definition translate_eff_addressing (a: Op.addressing) (args: list reg) @@ -445,8 +435,7 @@ 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)) - s.(st_funct_units)). + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). Proof. intros. apply state_incr_intro; simpl; try (intros; destruct (peq n0 n); subst); @@ -464,8 +453,7 @@ 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)) - s.(st_funct_units)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) (add_branch_instr_state_incr s e n n1 n2 NTRANS) | _ => Error (Errors.msg "Htlgen: add_branch_instr") end. @@ -516,8 +504,7 @@ 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) - s.(st_funct_units)). + (st_controllogic s)). Proof. constructor; simpl; auto with htlh. Qed. Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := @@ -529,8 +516,7 @@ 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) - s.(st_funct_units)) + (st_controllogic s)) (create_arr_state_incr s sz ln i). Definition max_pc_map (m : Maps.PTree.t stmnt) := @@ -593,8 +579,7 @@ 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_funct_units)). + s.(st_controllogic)). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -610,8 +595,7 @@ 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_funct_units)) + s.(st_controllogic)) (add_data_instr_state_incr s n st). Lemma add_control_instr_state_incr : @@ -625,8 +609,7 @@ Lemma add_control_instr_state_incr : s.(st_scldecls) s.(st_arrdecls) s.(st_datapath) - (AssocMap.set n st s.(st_controllogic)) - s.(st_funct_units)). + (AssocMap.set n st s.(st_controllogic))). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); @@ -644,19 +627,45 @@ 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)) - s.(st_funct_units)) + (AssocMap.set n st s.(st_controllogic))) (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 => - Vrange preg (Vlit (natToValue pred)) (Vlit (natToValue pred)) - | Pnot pred => - Vunop Vnot (pred_expr preg pred) + | Plit (b, pred) => + if b + then Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)) + else Vunop Vnot (Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred))) + | Ptrue => Vlit (ZToValue 1) + | Pfalse => Vlit (ZToValue 0) | Pand p1 p2 => Vbinop Vand (pred_expr preg p1) (pred_expr preg p2) | Por p1 p2 => @@ -671,33 +680,20 @@ Definition translate_predicate (a : assignment) ret (a dst (Vternary (pred_expr preg pos) e dst)) end. -Definition translate_inst a (fu : funct_units) (fin rtrn stack preg : reg) (n : node) (i : instr) +Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr) : mon stmnt := match i with - | RBnop => + | FUnop => ret Vskip - | RBop p op args dst => + | FUop p op args dst => do instr <- translate_instr op args; do _ <- declare_reg None dst 32; translate_predicate a preg p (Vvar dst) instr - | RBload p chunk addr args dst => - do src <- translate_arr_access chunk addr args stack; - do _ <- declare_reg None dst 32; - translate_predicate a preg p (Vvar dst) src - | RBstore p chunk addr args src => - do dst <- translate_arr_access chunk addr args stack; - translate_predicate a preg p dst (Vvar src) - | RBsetpred c args p => + | FUread p1 p2 r => ret Vskip + | FUwrite p1 p2 r => ret Vskip + | FUsetpred _ c args p => do cond <- translate_condition c args; - ret (a (pred_expr preg (Pvar p)) cond) - | RBpiped p f args => - match PTree.get f fu.(avail_units), args with - | Some (SignedDiv s n d q _), r1::r2::nil => - ret (Vseq (a (Vvar n) (Vvar r1)) (a (Vvar d) (Vvar r2))) - | _, _ => error (Errors.msg "HTLPargen.translate_inst: not a signed divide.") - end - | RBassign p f src dst => - ret (a (Vvar dst) (Vvar src)) + ret (a (pred_expr preg (Plit (true, p))) cond) end. Lemma create_new_state_state_incr: @@ -710,8 +706,7 @@ Lemma create_new_state_state_incr: s.(st_scldecls) s.(st_arrdecls) s.(st_datapath) - s.(st_controllogic) - s.(st_funct_units)). + s.(st_controllogic)). Admitted. Definition create_new_state (p: node): mon node := @@ -723,17 +718,15 @@ Definition create_new_state (p: node): mon node := s.(st_scldecls) s.(st_arrdecls) s.(st_datapath) - s.(st_controllogic) - s.(st_funct_units)) + s.(st_controllogic)) (create_new_state_state_incr s p). -Definition translate_inst_list (fu: funct_units) - (fin rtrn stack preg: reg) (ni : node * node * list (list instr)) := +Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list (list instr)) := match ni with | (n, p, li) => do _ <- collectlist (fun l => - do stmnt <- translate_inst Vblock fu fin rtrn stack preg n l; + do stmnt <- translate_inst Vblock fin rtrn stack preg n l; add_data_instr n stmnt) (concat li); do st <- get; add_control_instr n (state_goto st.(st_st) p) @@ -742,14 +735,14 @@ Definition translate_inst_list (fu: funct_units) Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr) : mon (stmnt * stmnt) := match cfi with - | RBgoto n' => + | FUgoto n' => do st <- get; ret (Vskip, state_goto st.(st_st) n') - | RBcond c args n1 n2 => + | FUcond c args n1 n2 => do st <- get; do e <- translate_condition c args; ret (Vskip, state_cond st.(st_st) e n1 n2) - | RBreturn r => + | FUreturn r => match r with | Some r' => ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))), @@ -758,18 +751,18 @@ Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr) ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))), Vskip) end - | RBpred_cf p c1 c2 => + | FUpred_cf p c1 c2 => do (tc1s, tc1c) <- translate_cfi' fin rtrn stack preg c1; do (tc2s, tc2c) <- translate_cfi' fin rtrn stack preg c2; ret ((Vcond (pred_expr preg p) tc1s tc2s), (Vcond (pred_expr preg p) tc1c tc2c)) - | RBjumptable r tbl => + | FUjumptable r tbl => do s <- get; - ret (Vskip, Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip)) - | RBcall sig ri rl r n => + ret (Vskip, Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr s.(st_st) tbl)) (Some Vskip)) + | FUcall sig ri rl r n => error (Errors.msg "HTLPargen: RPcall not supported.") - | RBtailcall sig ri lr => + | FUtailcall sig ri lr => error (Errors.msg "HTLPargen: RPtailcall not supported.") - | RBbuiltin e lb b n => + | FUbuiltin e lb b n => error (Errors.msg "HTLPargen: RPbuildin not supported.") end. @@ -780,11 +773,11 @@ Definition translate_cfi (fin rtrn stack preg: reg) (ni: node * cf_instr) do _ <- add_control_instr n c; add_data_instr n s. -Definition transf_bblock (fu: funct_units) (fin rtrn stack preg: reg) (ni : node * bblock) +Definition transf_bblock (fin rtrn stack preg: reg) (ni : node * bblock) : mon unit := let (n, bb) := ni in do nstate <- create_new_state ((poslength bb.(bb_body)))%positive; - do _ <- collectlist (translate_inst_list fu fin rtrn stack preg) + do _ <- collectlist (translate_inst_list fin rtrn stack preg) (prange n (nstate + poslength bb.(bb_body) - 1)%positive bb.(bb_body)); match bb.(bb_body) with @@ -792,14 +785,31 @@ Definition transf_bblock (fu: funct_units) (fin rtrn stack preg: reg) (ni : node | _ => translate_cfi fin rtrn stack preg (nstate, bb.(bb_exit)) end. -Definition transf_module (f: function) : mon HTL.module := +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 <? b) && (b <? c) && (c <? d) + && (d <? e) && (e <? f) && (f <? g))%positive true with + | left t => left _ + | _ => _ + end); auto. + simplify; repeat match goal with + | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H + end; unfold module_ordering; auto. +Defined. + +Lemma clk_greater : + forall ram clk r', + Some ram = Some r' -> (clk < ram_addr r')%positive. +Proof. Admitted. + +Definition transf_module (f: function) : mon HTL.module. + refine ( if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); do preg <- create_reg None 32; - do _ <- collectlist (transf_bblock f.(fn_funct_units) fin rtrn stack preg) + do _ <- collectlist (transf_bblock fin rtrn stack preg) (Maps.PTree.elements f.(fn_code)); do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(fn_params); @@ -810,8 +820,12 @@ Definition transf_module (f: function) : mon HTL.module := 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 - | left LEDATA, left LECTRL => + Integers.Int.max_unsigned, + decide_order (st_st current_state) fin rtrn stack start rst clk, + max_list_dec (fn_params f) (st_st current_state), + get_ram 0 (fn_funct_units f) + with + | left LEDATA, left LECTRL, left MORD, left WFPARAMS, Some (i, ram) => ret (HTL.mkmodule f.(fn_params) current_state.(st_datapath) @@ -825,13 +839,40 @@ Definition transf_module (f: function) : mon HTL.module := start rst clk - f.(fn_funct_units) current_state.(st_scldecls) current_state.(st_arrdecls) - (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) - | _, _ => error (Errors.msg "More than 2^32 states.") + (Some ram) + (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)) + MORD + _ + WFPARAMS) + | left LEDATA, left LECTRL, left MORD, left WFPARAMS, _ => + ret (HTL.mkmodule + f.(fn_params) + current_state.(st_datapath) + current_state.(st_controllogic) + f.(fn_entrypoint) + current_state.(st_st) + stack + stack_len + fin + rtrn + start + rst + clk + current_state.(st_scldecls) + current_state.(st_arrdecls) + None + (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)) + MORD + _ + WFPARAMS) + | _, _, _, _, _ => error (Errors.msg "More than 2^32 states.") end - else error (Errors.msg "Stack size misalignment."). + else error (Errors.msg "Stack size misalignment.")). + apply clk_greater. + discriminate. +Defined. Definition max_state (f: function) : state := let st := Pos.succ (max_reg_function f) in @@ -841,15 +882,14 @@ 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_funct_units (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_fundef := transf_partial_fundef transl_module. -Definition main_is_internal (p : RTLPar.program) : bool := +Definition main_is_internal (p : RTLParFU.program) : bool := let ge := Globalenvs.Genv.globalenv p in match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with | Some b => @@ -860,7 +900,7 @@ Definition main_is_internal (p : RTLPar.program) : bool := | _ => false end. -Definition transl_program (p : RTLBlockInstr.program) : Errors.res HTL.program := +Definition transl_program (p : RTLParFU.program) : Errors.res HTL.program := if main_is_internal p then transform_partial_program transl_fundef p else Errors.Error (Errors.msg "Main function is not Internal."). |