From 359194617de51adcc451b45b6c1b0a9332820906 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 21 Feb 2021 21:35:34 +0000 Subject: Add new instructions for pipelines --- src/hls/FunctionalUnits.v | 6 ++++-- src/hls/HTLPargen.v | 26 ++++++++------------------ src/hls/HTLgen.v | 3 ++- src/hls/HTLgenspec.v | 3 ++- src/hls/IfConversion.v | 2 +- src/hls/Partition.ml | 1 + src/hls/PrintVerilog.ml | 4 +++- src/hls/RTLBlockInstr.v | 8 ++++++++ src/hls/RTLPargen.v | 4 ++++ 9 files changed, 33 insertions(+), 24 deletions(-) diff --git a/src/hls/FunctionalUnits.v b/src/hls/FunctionalUnits.v index 019cf15..392b1ae 100644 --- a/src/hls/FunctionalUnits.v +++ b/src/hls/FunctionalUnits.v @@ -21,13 +21,15 @@ Require Import compcert.lib.Maps. Require Import vericert.common.Vericertlib. +Definition funct_node := positive. + Inductive funct_unit: Type := | SignedDiv (size: positive) (numer denom quot rem: reg): funct_unit | UnsignedDiv (size: positive) (numer denom quot rem: reg): funct_unit. Record funct_units := mk_avail_funct_units { - avail_sdiv: option positive; - avail_udiv: option positive; + avail_sdiv: option funct_node; + avail_udiv: option funct_node; avail_units: PTree.t funct_unit; }. diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 01588f6..a5b5f41 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -392,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 stmnt := +Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := match op, args with | Op.Omove, r::nil => ret (Vvar r) | Op.Ointconst n, _ => ret (Vlit (intToValue n)) @@ -402,22 +402,10 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon stmnt := | 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 => - 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) + | Op.Odiv, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: div") + | Op.Odivu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: divu") + | Op.Omod, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mod") + | Op.Omodu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: modu") | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2) | Op.Oandimm n, r::nil => ret (boplit Vand r n) | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2) @@ -702,6 +690,8 @@ Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr) | RBsetpred c args p => do cond <- translate_condition c args; ret (a (pred_expr preg (Pvar p)) cond) + | RBpiped p f args => error (Errors.msg "HTLPargen.translate_inst: piped") + | RBassign p f dst => error (Errors.msg "HTLPargen.translate_inst: assign") end. Lemma create_new_state_state_incr: @@ -828,7 +818,7 @@ Definition transf_module (f: function) : mon HTL.module := start rst clk - nil + initial_funct_units current_state.(st_scldecls) current_state.(st_arrdecls) (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index b323a65..76616fb 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -32,6 +32,7 @@ Require Import vericert.hls.AssocMap. Require Import vericert.hls.HTL. Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. +Require Import vericert.hls.FunctionalUnits. Hint Resolve AssocMap.gempty : htlh. Hint Resolve AssocMap.gso : htlh. @@ -610,7 +611,7 @@ Definition transf_module (f: function) : mon HTL.module := start rst clk - nil + initial_funct_units current_state.(st_scldecls) current_state.(st_arrdecls) (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index ae7917f..556e3cc 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -31,6 +31,7 @@ Require Import vericert.hls.ValueInt. Require Import vericert.hls.HTL. Require Import vericert.hls.HTLgen. Require Import vericert.hls.AssocMap. +Require Import vericert.hls.FunctionalUnits. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. Hint Resolve Maps.PTree.elements_correct : htlspec. @@ -183,7 +184,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk nil scldecls arrdecls wf) -> + st stk stk_len fin rtrn start rst clk initial_funct_units scldecls arrdecls wf) -> (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 39d9fd2..e893578 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -113,7 +113,7 @@ Definition transf_function (f: function) : function := let (_, c) := List.fold_left if_convert_code (find_blocks_with_cond f.(fn_code)) (1%nat, f.(fn_code)) in - mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c f.(fn_entrypoint). + mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c f.(fn_funct_units) f.(fn_entrypoint). Definition transf_fundef (fd: fundef) : fundef := transf_fundef transf_function fd. diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml index 19c6048..270db14 100644 --- a/src/hls/Partition.ml +++ b/src/hls/Partition.ml @@ -118,6 +118,7 @@ let function_from_RTL f = fn_stacksize = f.RTL.fn_stacksize; fn_params = f.RTL.fn_params; fn_entrypoint = f.RTL.fn_entrypoint; + fn_funct_units = FunctionalUnits.initial_funct_units; fn_code = c } diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index 8c9f20e..824623e 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -257,7 +257,9 @@ let pprint_module debug 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; - concat (List.map (print_funct_units m.mod_clk) m.mod_funct_units); + concat (List.map (print_funct_units m.mod_clk) + (Maps.PTree.elements m.mod_funct_units.avail_units + |> List.map snd)); if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else ""; if debug then debug_always_verbose i m.mod_clk m.mod_st else ""; indent i; "endmodule\n\n" diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 86f8eba..5ee9702 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -30,6 +30,7 @@ Require Import compcert.verilog.Op. Require Import vericert.common.Vericertlib. Require Import vericert.hls.Sat. +Require Import vericert.hls.FunctionalUnits. Local Open Scope rtl. @@ -250,6 +251,8 @@ Inductive instr : Type := | 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 +| RBpiped : option pred_op -> funct_node -> list reg -> instr +| RBassign : option pred_op -> funct_node -> reg -> instr | RBsetpred : condition -> list reg -> predicate -> instr. Inductive cf_instr : Type := @@ -284,6 +287,10 @@ Definition max_reg_instr (m: positive) (i: instr) := fold_left Pos.max args (Pos.max dst m) | RBstore p chunk addr args src => fold_left Pos.max args (Pos.max src m) + | RBpiped p f args => + fold_left Pos.max args m + | RBassign p f dst => + Pos.max dst m | RBsetpred c args p => fold_left Pos.max args m end. @@ -339,6 +346,7 @@ Section DEFINITION. fn_params: list reg; fn_stacksize: Z; fn_code: code; + fn_funct_units: funct_units; fn_entrypoint: node }. diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index e2e9a90..97ec9aa 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -576,6 +576,8 @@ Definition update (f : forest) (i : instr) : forest := | RBstore p chunk addr rl r => f # Mem <- (Estore (f # Mem) chunk addr (list_translation rl f) (f # (Reg r))) | RBsetpred c addr p => f + | RBpiped p fu args => f + | RBassign p fu dst => f end. (*| @@ -673,6 +675,7 @@ Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function : f.(fn_params) f.(fn_stacksize) tfcode + f.(fn_funct_units) f.(fn_entrypoint)) else Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent."). @@ -683,6 +686,7 @@ Definition transl_function_temp (f: RTLBlock.function) : Errors.res RTLPar.funct f.(fn_params) f.(fn_stacksize) tfcode + f.(fn_funct_units) f.(fn_entrypoint)). Definition transl_fundef := transf_partial_fundef transl_function_temp. -- cgit