From f3a0c5c0095258159c495d70fda6749bbf89de70 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 2 Feb 2021 20:34:20 +0000 Subject: Add predicated values and instructions --- src/Compiler.v | 7 +++++-- src/hls/HTLPargen.v | 48 ++++++++++++++++++++++++++++++------------- src/hls/PrintRTLBlock.ml | 4 ++-- src/hls/PrintRTLBlockInstr.ml | 38 ++++++++++++++++++++++++++-------- src/hls/PrintVerilog.ml | 1 + src/hls/RTLBlockInstr.v | 21 +++++++++++++------ src/hls/Schedule.ml | 14 ++++++------- 7 files changed, 92 insertions(+), 41 deletions(-) (limited to 'src') diff --git a/src/Compiler.v b/src/Compiler.v index 2406dad..27cb80c 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -67,6 +67,7 @@ Require vericert.hls.RTLBlockgen. Require vericert.hls.RTLPargen. Require vericert.hls.HTLPargen. Require vericert.hls.Pipeline. +Require vericert.hls.IfConversion. Require Import vericert.hls.HTLgenproof. @@ -79,7 +80,7 @@ We then need to declare the external OCaml functions used to print out intermedi Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_HTL: HTL.program -> unit. -Parameter print_RTLBlock: RTLBlock.program -> unit. +Parameter print_RTLBlock: Z -> RTLBlock.program -> unit. Definition print {A: Type} (printer: A -> unit) (prog: A) : A := let unused := printer prog in prog. @@ -233,7 +234,9 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) @@@ RTLBlockgen.transl_program - @@ print print_RTLBlock + @@ print (print_RTLBlock 1) + @@ IfConversion.transf_program + @@ print (print_RTLBlock 2) @@@ RTLPargen.transl_program @@@ HTLPargen.transl_program @@ print print_HTL diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 21f16b9..0508e6f 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -621,10 +621,19 @@ Definition add_control_instr (n : node) (st : stmnt) : mon unit := Error (Errors.msg "HTLPargen.add_control_instr: control logic is not empty") end. -Definition pred_expr (preg: reg) (p: predicate) := - Vrange preg (Vlit (posToValue p)) (Vlit (posToValue p)). +Fixpoint pred_expr (preg: reg) (p: pred_op) := + match p with + | Pvar pred => + Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)) + | Pnot pred => + Vunop Vnot (pred_expr preg pred) + | Pand p1 p2 => + Vbinop Vand (pred_expr preg p1) (pred_expr preg p2) + | Por p1 p2 => + Vbinop Vor (pred_expr preg p1) (pred_expr preg p2) + end. -Definition translate_predicate (preg: reg) (p: option predicate) (dst e: expr) := +Definition translate_predicate (preg: reg) (p: option pred_op) (dst e: expr) := match p with | None => ret (Vnonblock dst e) | Some pos => @@ -652,7 +661,7 @@ Definition translate_inst (fin rtrn stack preg : reg) (n : node) (i : instr) add_data_instr n pred | RBsetpred c args p => do cond <- translate_condition c args; - add_data_instr n (Vnonblock (pred_expr preg p) cond) + add_data_instr n (Vnonblock (pred_expr preg (Pvar p)) cond) end. Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * list instr) @@ -662,25 +671,29 @@ Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * list inst do st <- get; add_control_instr n (state_goto st.(st_st) (Pos.succ n)). -Definition translate_cfi (fin rtrn stack: reg) (ni : node * cf_instr) - : mon unit := - let (n, cfi) := ni in +Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr) + : mon (stmnt * stmnt) := match cfi with | RBgoto n' => do st <- get; - add_node_skip n (state_goto st.(st_st) n') + ret (Vskip, state_goto st.(st_st) n') | RBcond c args n1 n2 => + do st <- get; do e <- translate_condition c args; - add_branch_instr e n n1 n2 + ret (Vskip, state_cond st.(st_st) e n1 n2) | RBreturn r => match r with | Some r' => - add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) - (block rtrn (Vvar r'))) + ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))), + Vskip) | None => - add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) - (block rtrn (Vlit (ZToValue 0%Z)))) + ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))), + Vskip) end + | RBpred_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 ln => error (Errors.msg "HTLPargen: RPjumptable not supported.") | RBcall sig ri rl r n => @@ -691,12 +704,19 @@ Definition translate_cfi (fin rtrn stack: reg) (ni : node * cf_instr) error (Errors.msg "HTLPargen: RPbuildin not supported.") end. +Definition translate_cfi (fin rtrn stack preg: reg) (ni: node * cf_instr) + : mon unit := + let (n, cfi) := ni in + do (s, c) <- translate_cfi' fin rtrn stack preg cfi; + do _ <- add_control_instr n c; + add_data_instr n s. + Definition transf_bblock (fin rtrn stack preg: reg) (ni : node * bblock) : mon unit := let (n, bb) := ni in do _ <- collectlist (translate_inst_list fin rtrn stack preg) (penumerate n bb.(bb_body)); - translate_cfi fin rtrn stack + translate_cfi fin rtrn stack preg ((n + poslength bb.(bb_body))%positive, bb.(bb_exit)). Definition transf_module (f: function) : mon HTL.module := diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml index caf64ff..8fef401 100644 --- a/src/hls/PrintRTLBlock.ml +++ b/src/hls/PrintRTLBlock.ml @@ -63,10 +63,10 @@ let print_program pp (prog: program) = let destination : string option ref = ref None -let print_if prog = +let print_if passno prog = match !destination with | None -> () | Some f -> - let oc = open_out f in + let oc = open_out (f ^ "." ^ Z.to_string passno) in print_program oc prog; close_out oc diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml index a943aab..979ca38 100644 --- a/src/hls/PrintRTLBlockInstr.ml +++ b/src/hls/PrintRTLBlockInstr.ml @@ -9,6 +9,9 @@ open PrintAST let reg pp r = fprintf pp "x%d" (P.to_int r) +let pred pp r = + fprintf pp "p%d" (P.to_int r) + let rec regs pp = function | [] -> () | [r] -> reg pp r @@ -18,24 +21,39 @@ let ros pp = function | Coq_inl r -> reg pp r | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) +let rec print_pred_op pp = function + | Pvar p -> pred pp p + | Pnot p -> fprintf pp "(~ %a)" print_pred_op p + | Pand (p1, p2) -> fprintf pp "(%a & %a)" print_pred_op p1 print_pred_op p2 + | Por (p1, p2) -> fprintf pp "(%a | %a)" print_pred_op p1 print_pred_op p2 + +let print_pred_option pp = function + | Some x -> fprintf pp "(%a)" print_pred_op x + | None -> () + let print_bblock_body pp i = fprintf pp "\t\t"; match i with | RBnop -> fprintf pp "nop\n" - | RBop(_, op, ls, dst) -> - fprintf pp "%a = %a\n" - reg dst (PrintOp.print_operation reg) (op, ls) - | RBload(_, chunk, addr, args, dst) -> - fprintf pp "%a = %s[%a]\n" - reg dst (name_of_chunk chunk) + | RBop(p, op, ls, dst) -> + fprintf pp "%a %a = %a\n" + print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls) + | RBload(p, chunk, addr, args, dst) -> + fprintf pp "%a %a = %s[%a]\n" + print_pred_option p reg dst (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) - | RBstore(_, chunk, addr, args, src) -> - fprintf pp "%s[%a] = %a\n" + | RBstore(p, chunk, addr, args, src) -> + fprintf pp "%a %s[%a] = %a\n" + print_pred_option p (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) reg src + | RBsetpred (c, args, p) -> + fprintf pp "%a = %a\n" + pred p + (PrintOp.print_condition reg) (c, args) -let print_bblock_exit pp i = +let rec print_bblock_exit pp i = fprintf pp "\t\t"; match i with | RBcall(_, fn, args, res, _) -> @@ -65,3 +83,5 @@ let print_bblock_exit pp i = fprintf pp "return %a\n" reg arg | RBgoto n -> fprintf pp "goto %d\n" (P.to_int n) + | RBpred_cf (p, c1, c2) -> + fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2 diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index 4a6c165..b2633ec 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -87,6 +87,7 @@ let rec pprint_expr = function | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] | Vbinop (op, a, b) -> concat [pprint_binop (pprint_expr a) (pprint_expr b) op] | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] + | Vrange (r, e1, e2) -> concat [register r; "["; pprint_expr e1; ":"; pprint_expr e2; "]"] let rec pprint_stmnt i = let pprint_case (e, s) = concat [ indent (i + 1); pprint_expr e; ": begin\n"; pprint_stmnt (i + 2) s; diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index c480d36..4d02998 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -33,11 +33,17 @@ Local Open Scope rtl. Definition node := positive. Definition predicate := positive. +Inductive pred_op : Type := +| Pvar: predicate -> pred_op +| Pnot: pred_op -> pred_op +| Pand: pred_op -> pred_op -> pred_op +| Por: pred_op -> pred_op -> pred_op. + Inductive instr : Type := | RBnop : instr -| RBop : option predicate -> operation -> list reg -> reg -> instr -| RBload : option predicate -> memory_chunk -> addressing -> list reg -> reg -> instr -| RBstore : option predicate -> memory_chunk -> addressing -> list reg -> reg -> instr +| RBop : option pred_op -> operation -> list reg -> reg -> instr +| RBload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr +| RBstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr | RBsetpred : condition -> list reg -> predicate -> instr. Inductive cf_instr : Type := @@ -48,9 +54,10 @@ Inductive cf_instr : Type := | RBcond : condition -> list reg -> node -> node -> cf_instr | RBjumptable : reg -> list node -> cf_instr | RBreturn : option reg -> cf_instr -| RBgoto : node -> cf_instr. +| RBgoto : node -> cf_instr +| RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr. -Definition successors_instr (i : cf_instr) : list node := +Fixpoint successors_instr (i : cf_instr) : list node := match i with | RBcall sig ros args res s => s :: nil | RBtailcall sig ros args => nil @@ -59,6 +66,7 @@ Definition successors_instr (i : cf_instr) : list node := | RBjumptable arg tbl => tbl | RBreturn optarg => nil | RBgoto n => n :: nil + | RBpred_cf p c1 c2 => concat (successors_instr c1 :: successors_instr c2 :: nil) end. Definition max_reg_instr (m: positive) (i: instr) := @@ -74,7 +82,7 @@ Definition max_reg_instr (m: positive) (i: instr) := fold_left Pos.max args 1%positive end. -Definition max_reg_cfi (m : positive) (i : cf_instr) := +Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := match i with | RBcall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m)) @@ -92,6 +100,7 @@ Definition max_reg_cfi (m : positive) (i : cf_instr) := | RBreturn None => m | RBreturn (Some arg) => Pos.max arg m | RBgoto n => m + | RBpred_cf p c1 c2 => Pos.max (max_reg_cfi m c1) (max_reg_cfi m c2) end. Definition regset := Regmap.t val. diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 128f0e1..ec130cb 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -279,8 +279,8 @@ let print_src_type i c = let print_data_dep_order c (i, j) = print_lt0 (gen_var_name_e i c) (gen_var_name_b j c) -let rec gather_cfg_constraints (completed, (bvars, constraints, types)) c curr = - if List.exists (fun x -> P.eq x curr) completed then +let gather_cfg_constraints (completed, (bvars, constraints, types)) c curr = + if List.exists (P.eq curr) completed then (completed, (bvars, constraints, types)) else match PTree.get curr c with @@ -309,11 +309,7 @@ let rec gather_cfg_constraints (completed, (bvars, constraints, types)) c curr = (List.init num_iters (fun x -> x))) bvars in - let next' = List.filter (fun x -> P.lt x curr) next in - List.fold_left - (fun compl curr' -> gather_cfg_constraints compl c curr') - (curr :: completed, (bvars', constraints', types')) - next' + (curr :: completed, (bvars', constraints', types')) let rec intersperse s = function | [] -> [] @@ -415,7 +411,9 @@ let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) = let c' = PTree.map1 (gather_bb_constraints false) c in let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in let _, (vars, constraints, types) = - gather_cfg_constraints ([], ([], "", "")) c' entry + List.map fst (PTree.elements c') |> + List.fold_left (fun compl -> + gather_cfg_constraints compl c') ([], ([], "", "")) in let schedule' = solve_constraints vars constraints types in IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule'; -- cgit