From 171b326ade18ab77eb155a9d203f2f523708b29b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 15 Feb 2021 00:06:29 +0000 Subject: Add beginning to scheduling division --- src/hls/HTL.v | 12 +- src/hls/HTLPargen.v | 155 +++++++++++++------------ src/hls/HTLgen.v | 1 + src/hls/HTLgenspec.v | 2 +- src/hls/PrintVerilog.ml | 20 +++- src/hls/Verilog.v | 300 ++++++++++++------------------------------------ src/hls/Veriloggen.v | 1 + 7 files changed, 181 insertions(+), 310 deletions(-) diff --git a/src/hls/HTL.v b/src/hls/HTL.v index c8a0041..d91a340 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -27,16 +27,19 @@ Require compcert.lib.Integers. Require Import compcert.lib.Maps. Require Import vericert.common.Vericertlib. -Require Import vericert.hls.ValueInt. -Require Import vericert.hls.AssocMap. Require Import vericert.hls.Array. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.FunctionalUnits. +Require Import vericert.hls.ValueInt. Require vericert.hls.Verilog. -(** The purpose of the hardware transfer language (HTL) is to create a more +(*| +The purpose of the hardware transfer language (HTL) is to create a more hardware-like layout that is still similar to the register transfer language (RTL) that it came from. The main change is that function calls become module instantiations and that we now describe a state machine instead of a -control-flow graph. *) +control-flow graph. +|*) Local Open Scope assocmap. @@ -65,6 +68,7 @@ Record module: Type := mod_start : reg; mod_reset : reg; mod_clk : reg; + mod_funct_units: funct_units; mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index fcd4441..88fb9b4 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. @@ -47,6 +48,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 := @@ -56,7 +58,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. @@ -126,7 +129,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 := @@ -137,7 +141,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 : @@ -151,7 +156,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); @@ -169,7 +175,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. @@ -185,7 +192,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); @@ -203,7 +211,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. @@ -219,7 +228,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); @@ -237,7 +247,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. @@ -325,6 +336,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?*) @@ -353,7 +390,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)) @@ -363,7 +400,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) @@ -406,7 +455,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); @@ -424,7 +474,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. @@ -466,30 +517,6 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz 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 @@ -499,7 +526,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) := @@ -511,7 +539,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) := @@ -574,7 +603,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); @@ -590,7 +620,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 : @@ -604,7 +635,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); @@ -622,38 +654,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 instr) := @@ -816,6 +825,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))) @@ -831,7 +841,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). diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index f1e6b2a..b323a65 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -610,6 +610,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))) diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 845b1d5..ae7917f 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -183,7 +183,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> + st stk stk_len fin rtrn start rst clk nil 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/PrintVerilog.ml b/src/hls/PrintVerilog.ml index e67b567..e9020ac 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -28,6 +28,7 @@ open Clflags open Printf open VericertClflags +open FunctionalUnits module PMap = Map.Make (struct type t = P.t @@ -149,10 +150,10 @@ let declarearr t = " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ] let print_io = function - | Some Vinput -> "input" - | Some Voutput -> "output reg" - | Some Vinout -> "inout" - | None -> "reg" + | Some Vinput -> "input logic" + | Some Voutput -> "output logic" + | Some Vinout -> "inout logic" + | None -> "logic" let decl i = function | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)] @@ -175,6 +176,16 @@ let rec intersperse c = function let make_io i io r = concat [indent i; io; " "; register r; ";\n"] +let print_funct_units clk = function + | SignedDiv (stages, numer, denom, quot, rem) -> + sprintf "div_signed #(.stages(%d)) divs(.clk(%s), .clken(1'b1), .numer(%s), .denom(%s), .quotient(%s), .remain(%s))\n" + (P.to_int stages) + (register clk) (register numer) (register denom) (register quot) (register rem) + | UnsignedDiv (stages, numer, denom, quot, rem) -> + sprintf "div_unsigned #(.stages(%d)) divs(.clk(%s), .clken(1'b1), .numer(%s), .denom(%s), .quotient(%s), .remain(%s))\n" + (P.to_int stages) + (register clk) (register numer) (register denom) (register quot) (register rem) + let compose f g x = g x |> f let testbench = "module testbench; @@ -233,6 +244,7 @@ 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); if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else ""; if debug then debug_always i m.mod_clk m.mod_st else ""; indent i; "endmodule\n\n" diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index a7db3ba..779b05c 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -17,27 +17,32 @@ * along with this program. If not, see . *) -From Coq Require Import - Structures.OrderedTypeEx - FSets.FMapPositive - Program.Basics - PeanoNat - ZArith - Lists.List - Program. +Set Implicit Arguments. -Require Import Lia. +Require Import Coq.Structures.OrderedTypeEx. +Require Import Coq.FSets.FMapPositive. +Require Import Coq.Arith.PeanoNat. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coq.micromega.Lia. + +Require Import compcert.common.Errors. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Smallstep. +Require Import compcert.lib.Integers. +Require compcert.common.Events. + +Require Import vericert.common.Show. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.Array. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.FunctionalUnits. +Require Import vericert.hls.ValueInt. Import ListNotations. -From vericert Require Import Vericertlib Show ValueInt AssocMap Array. -From compcert Require Events. -From compcert Require Import Integers Errors Smallstep Globalenvs. - Local Open Scope assocmap. -Set Implicit Arguments. - Definition reg : Type := positive. Definition node : Type := positive. Definition szreg : Type := reg * nat. @@ -103,23 +108,30 @@ Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) := Inductive scl_decl : Type := VScalar (sz : nat). Inductive arr_decl : Type := VArray (sz : nat) (ln : nat). -(** * Verilog AST +(*| +Verilog AST +=========== The Verilog AST is defined here, which is the target language of the compilation. -** Value +Value +----- The Verilog [value] is a bitvector containg a size and the actual bitvector. In this case, the [Word.word] type is used as many theorems about that bitvector -have already been proven. *) +have already been proven. +|*) -(** ** Binary Operators +(*| +Binary Operators +---------------- These are the binary operations that can be represented in Verilog. Ideally, multiplication and division would be done by custom modules which could al so be scheduled properly. However, for now every Verilog operator is assumed to take -one clock cycle. *) +one clock cycle. +|*) Inductive binop : Type := | Vadd : binop (** addition (binary [+]) *) @@ -147,13 +159,19 @@ Inductive binop : Type := | Vshru : binop. (** shift right unsigned ([>>]) *) (*| Vror : binop (** shift right unsigned ([>>]) *)*) -(** ** Unary Operators *) +(*| +Unary Operators +--------------- +|*) Inductive unop : Type := | Vneg (** negation ([-]) *) | Vnot. (** not operation [!] *) -(** ** Expressions *) +(*| +Expressions +----------- +|*) Inductive expr : Type := | Vlit : value -> expr @@ -168,7 +186,10 @@ Inductive expr : Type := Definition posToExpr (p : positive) : expr := Vlit (posToValue p). -(** ** Statements *) +(*| +Statements +---------- +|*) Inductive stmnt : Type := | Vskip : stmnt @@ -178,14 +199,17 @@ Inductive stmnt : Type := | Vblock : expr -> expr -> stmnt | Vnonblock : expr -> expr -> stmnt. -(** ** Edges +(*| +Edges +----- These define when an always block should be triggered, for example if the always block should be triggered synchronously at the clock edge, or asynchronously for combinational logic. [edge] is not part of [stmnt] in this formalisation because is closer to the -semantics that are used. *) +semantics that are used. +|*) Inductive edge : Type := | Vposedge : reg -> edge @@ -193,11 +217,14 @@ Inductive edge : Type := | Valledge : edge | Voredge : edge -> edge -> edge. -(** ** Module Items +(*| +Module Items +------------ Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). The declarations are always register declarations as combinational logic can be -done using combinational always block instead of continuous assignments. *) +done using combinational always block instead of continuous assignments. +|*) Inductive io : Type := | Vinput : io @@ -214,7 +241,8 @@ Inductive module_item : Type := | Valways_ff : edge -> stmnt -> module_item | Valways_comb : edge -> stmnt -> module_item. -(** The main module type containing all the important control signals +(*| +The main module type containing all the important control signals - [mod_start] If set, starts the computations in the module. - [mod_reset] If set, reset the state in the module. @@ -223,7 +251,7 @@ Inductive module_item : Type := - [mod_finish] Bit that is set if the result is ready. - [mod_return] The return value that was computed. - [mod_body] The body of the module, including the state machine. -*) +|*) Record module : Type := mkmodule { mod_start : reg; @@ -235,6 +263,7 @@ Record module : Type := mkmodule { mod_stk : reg; mod_stk_len : nat; mod_args : list reg; + mod_funct_units: funct_units; mod_body : list module_item; mod_entrypoint : node; }. @@ -243,15 +272,18 @@ Definition fundef := AST.fundef module. Definition program := AST.program fundef unit. -(** Convert a [positive] to an expression directly, setting it to the right - size. *) +(*| +Convert a [positive] to an expression directly, setting it to the right size. +|*) Definition posToLit (p : positive) : expr := Vlit (posToValue p). Definition fext := unit. Definition fextclk := nat -> fext. -(** ** State +(*| +State +----- The [state] contains the following items: n @@ -270,7 +302,8 @@ retrieved and set appropriately. Verilog, as the Verilog was generated by the RTL, which means that we have to make an assumption about how it looks. In this case, that it contains state which determines which part of the Verilog is executed. This is then the part - of the Verilog that should match with the RTL. *) + of the Verilog that should match with the RTL. +|*) Inductive stackframe : Type := Stackframe : @@ -390,41 +423,9 @@ Definition handle_def {A : Type} (a : A) (val : option A) Local Open Scope error_monad_scope. -(*Definition access_fext (f : fext) (r : reg) : res value := - match AssocMap.get r f with - | Some v => OK v - | _ => OK (ZToValue 0) - end.*) - -(* TODO FIX Vvar case without default *) -(*Fixpoint expr_run (assoc : assocmap) (e : expr) - {struct e} : res value := - match e with - | Vlit v => OK v - | Vvar r => match s with - | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r - | _ => Error (msg "Verilog: Wrong state") - end - | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled") - | Vinputvar r => access_fext s r - | Vbinop op l r => - let lv := expr_run s l in - let rv := expr_run s r in - let oper := binop_run op in - do lv' <- lv; - do rv' <- rv; - handle_opt (msg "Verilog: sizes are not equal") - (eq_to_opt lv' rv' (oper lv' rv')) - | Vunop op e => - let oper := unop_run op in - do ev <- expr_run s e; - OK (oper ev) - | Vternary c te fe => - do cv <- expr_run s c; - if valueToBool cv then expr_run s te else expr_run s fe - end.*) - -(** Return the location of the lhs of an assignment. *) +(*| +Return the location of the lhs of an assignment. +|*) Inductive location : Type := | LocReg (_ : reg) @@ -436,80 +437,6 @@ Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> expr_runp f asr asa iexp iv -> location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)). -(* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l) (e : expr) : res reg := *) -(* match e with *) -(* | Vvar r => OK r *) -(* | _ => Error (msg "Verilog: expression not supported on lhs of assignment") *) -(* end. *) - -(*Fixpoint stmnt_height (st : stmnt) {struct st} : nat := - match st with - | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2) - | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2)) - | Vcase _ ls (Some st) => - S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls) - | _ => 1 - end. - -Fixpoint find_case_stmnt (s : state) (v : value) (cl : list (expr * stmnt)) - {struct cl} : option (res stmnt) := - match cl with - | (e, st)::xs => - match expr_run s e with - | OK v' => - match eq_to_opt v v' (veq v v') with - | Some eq => if valueToBool eq then Some (OK st) else find_case_stmnt s v xs - | None => Some (Error (msg "Verilog: equality check sizes not equal")) - end - | Error msg => Some (Error msg) - end - | _ => None - end. - -Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state := - match n with - | S n' => - match st with - | Vskip => OK s - | Vseq s1 s2 => - do s' <- stmnt_run' n' s s1; - stmnt_run' n' s' s2 - | Vcond c st sf => - do cv <- expr_run s c; - if valueToBool cv - then stmnt_run' n' s st - else stmnt_run' n' s sf - | Vcase e cl defst => - do v <- expr_run s e; - match find_case_stmnt s v cl with - | Some (OK st') => stmnt_run' n' s st' - | Some (Error msg) => Error msg - | None => do s' <- handle_opt (msg "Verilog: no case was matched") - (option_map (stmnt_run' n' s) defst); s' - end - | Vblock lhs rhs => - match s with - | State m assoc nbassoc f c => - do name <- assign_name lhs; - do rhse <- expr_run s rhs; - OK (State m (PositiveMap.add name rhse assoc) nbassoc f c) - | _ => Error (msg "Verilog: Wrong state") - end - | Vnonblock lhs rhs => - match s with - | State m assoc nbassoc f c => - do name <- assign_name lhs; - do rhse <- expr_run s rhs; - OK (State m assoc (PositiveMap.add name rhse nbassoc) f c) - | _ => Error (msg "Verilog: Wrong state") - end - end - | _ => OK s - end. - -Definition stmnt_run (s : state) (st : stmnt) : res state := - stmnt_run' (stmnt_height st) s st. *) - Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> stmnt -> reg_associations -> arr_associations -> Prop := | stmnt_runp_Vskip: @@ -580,20 +507,6 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> asr (nonblock_arr r i asa rhsval). Hint Constructors stmnt_runp : verilog. -(*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := - let run := fun st ls => - do s' <- stmnt_run s st; - mi_step s' ls - in - match m with - | (Valways _ st)::ls => run st ls - | (Valways_ff _ st)::ls => run st ls - | (Valways_comb _ st)::ls => run st ls - | (Vdecl _ _)::ls => mi_step s ls - | (Vdeclarr _ _ _)::ls => mi_step s ls - | nil => OK s - end.*) - Inductive mi_stepp : fext -> reg_associations -> arr_associations -> module_item -> reg_associations -> arr_associations -> Prop := | mi_stepp_Valways : @@ -625,80 +538,8 @@ Inductive mis_stepp : fext -> reg_associations -> arr_associations -> mis_stepp f sr sa nil sr sa. Hint Constructors mis_stepp : verilog. -(*Definition mi_step_commit (s : state) (m : list module_item) : res state := - match mi_step s m with - | OK (State m assoc nbassoc f c) => - OK (State m (merge_assocmap nbassoc assoc) empty_assocmap f c) - | Error msg => Error msg - | _ => Error (msg "Verilog: Wrong state") - end. - -Fixpoint mi_run (f : fextclk) (assoc : assocmap) (m : list module_item) (n : nat) - {struct n} : res assocmap := - match n with - | S n' => - do assoc' <- mi_run f assoc m n'; - match mi_step_commit (State assoc' empty_assocmap f (Pos.of_nat n')) m with - | OK (State assoc _ _ _) => OK assoc - | Error m => Error m - end - | O => OK assoc - end.*) - -(** Resets the module into a known state, so that it can be executed. This is -assumed to be the starting state of the module, and may have to be changed if -other arguments to the module are also to be supported. *) - -(*Definition initial_fextclk (m : module) : fextclk := - fun x => match x with - | S O => (AssocMap.set (mod_reset m) (ZToValue 1) empty_assocmap) - | _ => (AssocMap.set (mod_reset m) (ZToValue 0) empty_assocmap) - end.*) - -(*Definition module_run (n : nat) (m : module) : res assocmap := - mi_run (initial_fextclk m) empty_assocmap (mod_body m) n.*) - Local Close Scope error_monad_scope. -(*Theorem value_eq_size_if_eq: - forall lv rv EQ, - vsize lv = vsize rv -> value_eq_size lv rv = left EQ. -Proof. intros. unfold value_eq_size. - -Theorem expr_run_same: - forall assoc e v, expr_run assoc e = OK v <-> expr_runp assoc e v. -Proof. - split; generalize dependent v; generalize dependent assoc. - - induction e. - + intros. inversion H. constructor. - + intros. inversion H. constructor. assumption. - + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (expr_run assoc e2) eqn:?. - unfold eq_to_opt in H1. destruct (value_eq_size v0 v1) eqn:?. inversion H1. - constructor. apply IHe1. assumption. apply IHe2. assumption. reflexivity. discriminate. discriminate. - discriminate. - + intros. inversion H. destruct (expr_run assoc e) eqn:?. unfold option_map in H1. - inversion H1. constructor. apply IHe. assumption. reflexivity. discriminate. - + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (valueToBool v0) eqn:?. - eapply erun_Vternary_true. apply IHe1. eassumption. apply IHe2. eassumption. assumption. - eapply erun_Vternary_false. apply IHe1. eassumption. apply IHe3. eassumption. assumption. - discriminate. - - induction e. - + intros. inversion H. reflexivity. - + intros. inversion H. subst. simpl. assumption. - + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. - apply IHe2 in H6. rewrite H6. unfold eq_to_opt. assert (vsize lv = vsize rv). - apply EQ. apply (value_eq_size_if_eq lv rv EQ) in H0. rewrite H0. reflexivity. - + intros. inversion H. subst. simpl. destruct (expr_run assoc e) eqn:?. simpl. - apply IHe in H3. rewrite Heqo in H3. - inversion H3. subst. reflexivity. apply IHe in H3. rewrite Heqo in H3. discriminate. - + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. - apply IHe2 in H6. rewrite H6. reflexivity. - subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. apply IHe3. - assumption. -Qed. - - *) - Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := match rl, vl with | r :: rl', v :: vl' => AssocMap.set r v (init_params vl' rl') @@ -886,7 +727,8 @@ Lemma semantics_determinate : Proof. intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. - invert H; invert H0; constructor. (* Traces are always empty *) - - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst. + - invert H; invert H0; crush. + assert (f = f0) by (destruct f; destruct f0; auto); subst. pose proof (mis_stepp_determinate H5 H15). crush. - constructor. invert H; crush. diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index 80c0669..6ea00e0 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -61,6 +61,7 @@ Definition transl_module (m : HTL.module) : Verilog.module := m.(HTL.mod_stk) m.(HTL.mod_stk_len) m.(HTL.mod_params) + m.(HTL.mod_funct_units) body m.(HTL.mod_entrypoint). -- cgit From a47cfd17f0e1fc6aca5e10de9362a4be2d4af468 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 21 Feb 2021 21:35:11 +0000 Subject: Correctly add initial scheduling variables --- src/hls/Schedule.ml | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index c6c8bf4..9adf17c 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -556,6 +556,18 @@ let gather_bb_constraints debug bb = let encode_var bbn n i = { sv_type = VarType (bbn, n); sv_num = i } let encode_bb bbn i = { sv_type = BBType bbn; sv_num = i } +let add_initial_sv n dfg constr = + let add_initial_sv' (i, instr) g = + let pipes = pipeline_stages instr in + if pipes > 0 then + List.init pipes (fun i' -> i') + |> List.fold_left (fun g i' -> + G.add_edge_e g (encode_var n i i', -1, encode_var n i (i'+1)) + ) g + else g + in + DFG.fold_vertex add_initial_sv' dfg constr + let add_super_nodes n dfg = DFG.fold_vertex (function v1 -> fun g -> (if DFG.in_degree dfg v1 = 0 @@ -563,12 +575,14 @@ let add_super_nodes n dfg = else g) |> (fun g' -> if DFG.out_degree dfg v1 = 0 - then G.add_edge_e g' (encode_var n (fst v1) 0, 0, encode_bb n 1) + then G.add_edge_e g' (encode_var n (fst v1) (pipeline_stages (snd v1)), + 0, encode_bb n 1) else g')) dfg let add_data_deps n = - DFG.fold_edges_e (function ((i1, _), l, (i2, _)) -> fun g -> - G.add_edge_e g (encode_var n i1 0, 0, encode_var n i2 0) + DFG.fold_edges_e (function ((i1, instr1), _, (i2, _)) -> fun g -> + let end_sv = pipeline_stages instr1 in + G.add_edge_e g (encode_var n i1 end_sv, 0, encode_var n i2 0) ) let add_ctrl_deps n succs constr = @@ -596,7 +610,7 @@ let add_cycle_constr max n dfg constr = let negated_dfg = negate_graph dfg in let longest_path v = BFDFG.all_shortest_paths negated_dfg v |> BFDFG.H.to_seq |> List.of_seq in - let constrained_paths = List.filter (function (v, m) -> - m > max) in + let constrained_paths = List.filter (function (_, m) -> - m > max) in List.fold_left (fun g -> function (v, v', w) -> G.add_edge_e g (encode_var n (fst v) 0, - (int_of_float (Float.ceil (Float.div (float_of_int w) (float_of_int max))) - 1), @@ -656,6 +670,7 @@ let gather_cfg_constraints c constr curr = | None -> assert false | Some { bb_exit = ctrl; _ } -> add_super_nodes n dfg constr + |> add_initial_sv n dfg |> add_data_deps n dfg |> add_ctrl_deps n (successors_instr ctrl |> List.map P.to_int @@ -797,5 +812,6 @@ let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function = fn_params = f.fn_params; fn_stacksize = f.fn_stacksize; fn_code = List.fold_left (add_to_tree scheduled) PTree.empty reachable; + fn_funct_units = f.fn_funct_units; fn_entrypoint = f.fn_entrypoint } -- cgit 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 From a5ae227155f09822207c49d75fdbb6e4b7652936 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 21 Feb 2021 21:35:52 +0000 Subject: Add operator pipelining pass --- src/hls/PipelineOp.v | 67 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 src/hls/PipelineOp.v diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v new file mode 100644 index 0000000..0783e4e --- /dev/null +++ b/src/hls/PipelineOp.v @@ -0,0 +1,67 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2021 Yann Herklotz + * + * 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 + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +Require Import compcert.common.AST. +Require Import compcert.common.Errors. +Require Import compcert.common.Globalenvs. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require Import compcert.verilog.Op. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.RTLBlockInstr. +Require Import vericert.hls.RTLPar. +Require Import vericert.hls.FunctionalUnits. + +Definition state : Type := code * funct_units. + +Definition div_pos (il: nat * list nat) x := + let (i, l) := il in + match x with + | RBop _ Odiv _ _ => (S i, i :: l) + | RBop _ Odivu _ _ => (S i, i :: l) + | RBop _ Omod _ _ => (S i, i :: l) + | RBop _ Omodu _ _ => (S i, i :: l) + | _ => (S i, l) + end. + +Definition find_divs (bb: bblock) : list nat := + snd (List.fold_left div_pos bb.(bb_body) (1%nat, nil)). + +Definition transf_code (i: state) (bbn: node * bblock) : state := + let (c, fu) := i in + let (n, bb) := bbn in + (PTree.set n bb c, fu). + +Definition transf_function (f: function) : function := + let (c, fu) := List.fold_left transf_code + (PTree.elements f.(fn_code)) + (PTree.empty bblock, f.(fn_funct_units)) in + mkfunction + f.(fn_sig) + f.(fn_params) + f.(fn_stacksize) + c + fu + f.(fn_entrypoint). + +Definition transf_fundef (fd: fundef) : fundef := + transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. -- cgit From 91b62a7100ccb1f8910422bc4566bc57ade8f7e7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Feb 2021 18:41:33 +0000 Subject: Add RTLPar printing --- driver/VericertDriver.ml | 11 ++++--- src/Compiler.v | 1 + src/VericertClflags.ml | 1 + src/extraction/Extraction.v | 1 + src/hls/printRTLPar.ml | 74 +++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 84 insertions(+), 4 deletions(-) create mode 100644 src/hls/printRTLPar.ml diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index d2c301f..4c1e2f9 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -66,6 +66,7 @@ let compile_c_file sourcename ifile ofile = set_dest Vericert.PrintCminor.destination option_dcminor ".cm"; set_dest Vericert.PrintRTL.destination option_drtl ".rtl"; set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock"; + set_dest Vericert.PrintRTLPar.destination option_drtlpar ".rtlpar"; set_dest Vericert.PrintHTL.destination option_dhtl ".htl"; set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest Vericert.PrintLTL.destination option_dltl ".ltl"; @@ -390,6 +391,7 @@ let cmdline_actions = Exact "-dcminor", Set option_dcminor; Exact "-drtl", Set option_drtl; Exact "-drtlblock", Set option_drtlblock; + Exact "-drtlpar", Set option_drtlpar; Exact "-dhtl", Set option_dhtl; Exact "-dltl", Set option_dltl; Exact "-dalloctrace", Set option_dalloctrace; @@ -403,6 +405,7 @@ let cmdline_actions = option_dcminor := true; option_drtl := true; option_drtlblock := true; + option_drtlpar := true; option_dhtl := true; option_dltl := true; option_dalloctrace := true; @@ -417,10 +420,10 @@ let cmdline_actions = warning_options @ (* Vericert.Interpreter mode *) [ Exact "-interp", Set option_interp; - Exact "-quiet", Unit (fun () -> Vericert.Interp.trace := 0); - Exact "-trace", Unit (fun () -> Vericert.Interp.trace := 2); - Exact "-random", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.Random); - Exact "-all", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.All) + Exact "-quiet", Unit (fun () -> Vericert.Interp.trace := 0); + Exact "-trace", Unit (fun () -> Vericert.Interp.trace := 2); + Exact "-random", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.Random); + Exact "-all", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.All) ] (* Optimization options *) (* -f options: come in -f and -fno- variants *) diff --git a/src/Compiler.v b/src/Compiler.v index d99ce56..e837e9d 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -82,6 +82,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: Z -> RTLBlock.program -> unit. +Parameter print_RTLPar: Z -> RTLPar.program -> unit. Definition print {A: Type} (printer: A -> unit) (prog: A) : A := let unused := printer prog in prog. diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml index 534962b..930b613 100644 --- a/src/VericertClflags.ml +++ b/src/VericertClflags.ml @@ -5,5 +5,6 @@ let option_debug_hls = ref false let option_initial = ref false let option_dhtl = ref false let option_drtlblock = ref false +let option_drtlpar = ref false let option_hls_schedule = ref false let option_fif_conv = ref false diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 8aec96e..5c1dac5 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -141,6 +141,7 @@ Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if". +Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if". Extract Constant Compiler.print_HTL => "PrintHTL.print_if". Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". diff --git a/src/hls/printRTLPar.ml b/src/hls/printRTLPar.ml new file mode 100644 index 0000000..7fac0de --- /dev/null +++ b/src/hls/printRTLPar.ml @@ -0,0 +1,74 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Pretty-printers for RTL code *) + +open Printf +open Camlcoq +open Datatypes +open Maps +open AST +open RTLBlockInstr +open RTLPar +open PrintAST +open PrintRTLBlockInstr + +(* Printing of RTL code *) + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let rec regs pp = function + | [] -> () + | [r] -> reg pp r + | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let print_bblock pp (pc, i) = + fprintf pp "%5d:{\n" pc; + List.iter (fun x -> fprintf pp "["; + List.iter (fun x' -> fprintf pp "["; List.iter (print_bblock_body pp) x'; fprintf pp "]\n") x; + fprintf pp "]\n") i.bb_body; + print_bblock_exit pp i.bb_exit; + fprintf pp "\t}\n\n" + +let print_function pp id f = + fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements f.fn_code)) in + List.iter (print_bblock pp) instrs; + fprintf pp "}\n\n" + +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_function pp id f + | _ -> () + +let print_program pp (prog: program) = + List.iter (print_globdef pp) prog.prog_defs + +let destination : string option ref = ref None + +let print_if passno prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out (f ^ "." ^ Z.to_string passno) in + print_program oc prog; + close_out oc -- cgit From 1a7f581dc4b67cbfe17936697aec8f85786c844d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Feb 2021 18:41:47 +0000 Subject: Add operation pipelining --- src/Compiler.v | 4 ++ src/hls/PipelineOp.v | 141 ++++++++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 137 insertions(+), 8 deletions(-) diff --git a/src/Compiler.v b/src/Compiler.v index e837e9d..e9d76dc 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -68,6 +68,7 @@ Require vericert.hls.RTLPargen. Require vericert.hls.HTLPargen. Require vericert.hls.Pipeline. Require vericert.hls.IfConversion. +Require vericert.hls.PipelineOp. Require vericert.HLSOpts. Require Import vericert.hls.HTLgenproof. @@ -240,6 +241,9 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program @@ print (print_RTLBlock 2) @@@ RTLPargen.transl_program + @@ print (print_RTLPar 1) + @@ PipelineOp.transf_program + @@ print (print_RTLPar 2) @@@ HTLPargen.transl_program @@ print print_HTL @@ Veriloggen.transl_program. diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v index 0783e4e..793b752 100644 --- a/src/hls/PipelineOp.v +++ b/src/hls/PipelineOp.v @@ -16,6 +16,9 @@ * along with this program. If not, see . *) +Require Import Coq.Lists.List. + +Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Errors. Require Import compcert.common.Globalenvs. @@ -23,12 +26,15 @@ Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. Require Import compcert.verilog.Op. + Require Import vericert.common.Vericertlib. Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLPar. Require Import vericert.hls.FunctionalUnits. -Definition state : Type := code * funct_units. +Import Option.Notation. + +Local Open Scope positive. Definition div_pos (il: nat * list nat) x := let (i, l) := il in @@ -40,24 +46,143 @@ Definition div_pos (il: nat * list nat) x := | _ => (S i, l) end. -Definition find_divs (bb: bblock) : list nat := - snd (List.fold_left div_pos bb.(bb_body) (1%nat, nil)). +Definition div_pos_in_list (il: nat * list (nat * nat)) bb := + let (i, l) := il in + let dp := snd (List.fold_left div_pos bb (0%nat, nil)) in + (S i, (List.map (fun x => (i, x)) dp) ++ l). + +Definition div_pos_in_block (il: nat * list (nat * nat * nat)) bb := + let (i, l) := il in + let dp := snd (List.fold_left div_pos_in_list bb (0%nat, nil)) in + (S i, (List.map (fun (yx : nat * nat) => let (y, x) := yx in (i, y, x)) dp) ++ l). + +Definition find_divs (bb: bblock) := + snd (List.fold_left div_pos_in_block bb.(bb_body) (0%nat, nil)). + +Fixpoint mapi' {A B: Type} (n: nat) (f: nat -> A -> B) (l: list A): list B := + match l with + | nil => nil + | a :: b => f n a :: mapi' (S n) f b + end. + +Definition mapi {A B: Type} := @mapi' A B 0. + +Definition map_at {A: Type} (n: nat) (f: A -> A) (l: list A): list A := + mapi (fun i il => + if Nat.eqb n i + then f il + else il + ) l. + +Definition map_at_err {A: Type} (n: nat) (f: A -> A) (l: list A): option (list A) := + if (Datatypes.length l <=? n)%nat + then None + else Some (map_at n f l). + +Definition replace_div' sdiv udiv (d: instr) := + match d with + | RBop op Odiv args dst => RBpiped op sdiv args + | RBop op Odivu args dst => RBpiped op udiv args + | RBop op Omod args dst => RBpiped op sdiv args + | RBop op Omodu args dst => RBpiped op udiv args + | _ => d + end. + +Definition get_sdiv (fu: funct_unit) : option (reg * reg * reg) := + match fu with + | SignedDiv s a b d _ => Some (a, b, d) + | _ => None + end. -Definition transf_code (i: state) (bbn: node * bblock) : state := +Definition get_udiv (fu: funct_unit) : option (reg * reg * reg) := + match fu with + | UnsignedDiv s a b d _ => Some (a, b, d) + | _ => None + end. + +Definition get_smod (fu: funct_unit) : option (reg * reg * reg) := + match fu with + | SignedDiv s a b _ d => Some (a, b, d) + | _ => None + end. + +Definition get_umod (fu: funct_unit) : option (reg * reg * reg) := + match fu with + | UnsignedDiv s a b _ d => Some (a, b, d) + | _ => None + end. + +Definition bind3 {A B C D: Type} + (f: option (A * B * C)) + (g: A -> B -> C -> option D) : option D := + match f with + | Some (a, b, c) => g a b c + | None => None + end. + +Notation "'do' ( X , Y , Z ) <- A ; B" := (bind3 A (fun X Y Z => B)) + (at level 200, X ident, Y ident, Z ident, A at level 100, B at level 200). + +Definition replace_div_error (fu: funct_units) (bb: bb) (loc: nat * nat * nat) := + match loc with + | (z, y, x) => + do sdiv <- fu.(avail_sdiv); + do udiv <- fu.(avail_udiv); + do sfu <- PTree.get sdiv fu.(avail_units); + do ufu <- PTree.get udiv fu.(avail_units); + do z' <- List.nth_error bb z; + do y' <- List.nth_error z' y; + do x' <- List.nth_error y' x; + let transf := map_at z (map_at y (map_at x (replace_div' sdiv udiv))) bb in + match x' with + | RBop op Odiv args dst => + do (s1, s2, src) <- get_sdiv sfu; + map_at_err (z + 32)%nat (fun x => (RBassign op sdiv src dst :: nil) :: x) transf + | RBop op Odivu args dst => + do (s1, s2, src) <- get_udiv ufu; + map_at_err (z + 32)%nat (fun x => (RBassign op sdiv src dst :: nil) :: x) transf + | RBop op Omod args dst => + do (s1, s2, src) <- get_smod sfu; + map_at_err (z + 32)%nat (fun x => (RBassign op sdiv src dst :: nil) :: x) transf + | RBop op Omodu args dst => + do (s1, s2, src) <- get_umod ufu; + map_at_err (z + 32)%nat (fun x => (RBassign op sdiv src dst :: nil) :: x) transf + | _ => None + end + end. + +Definition replace_div (fu: funct_units) (bb: bb) loc := + match replace_div_error fu bb loc with + | Some bb' => bb' + | _ => bb + end. + +Definition transf_code (i: code * funct_units) (bbn: node * bblock) := let (c, fu) := i in let (n, bb) := bbn in - (PTree.set n bb c, fu). + let divs := find_divs bb in + match divs with + | nil => (PTree.set n bb c, fu) + | _ => + (PTree.set n (mk_bblock (List.fold_left (replace_div fu) divs bb.(bb_body)) bb.(bb_exit)) c, fu) + end. + +Definition create_fu (r: reg) := + let fu := PTree.set 2 (UnsignedDiv 32 (r+5) (r+6) (r+7) (r+8)) + (PTree.set 1 (SignedDiv 32 (r+1) (r+2) (r+3) (r+4)) (PTree.empty _)) in + mk_avail_funct_units (Some 1) (Some 2) fu. Definition transf_function (f: function) : function := - let (c, fu) := List.fold_left transf_code + let fu := create_fu (max_reg_function f) in + let (c, fu') := List.fold_left transf_code (PTree.elements f.(fn_code)) - (PTree.empty bblock, f.(fn_funct_units)) in + (PTree.empty bblock, fu) in mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c - fu + fu' f.(fn_entrypoint). Definition transf_fundef (fd: fundef) : fundef := -- cgit From 2243443c407a1e951265a9252bac3d3b9b830cbb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Feb 2021 18:42:11 +0000 Subject: Fix arguments to RBassign and piped --- src/hls/HTLPargen.v | 2 +- src/hls/PrintRTLBlockInstr.ml | 5 +++++ src/hls/RTLBlockInstr.v | 6 +++--- src/hls/RTLPargen.v | 2 +- 4 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index a5b5f41..e1c7ec8 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -691,7 +691,7 @@ Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr) 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") + | RBassign p f src dst => error (Errors.msg "HTLPargen.translate_inst: assign") end. Lemma create_new_state_state_incr: diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml index ba7241b..808d342 100644 --- a/src/hls/PrintRTLBlockInstr.ml +++ b/src/hls/PrintRTLBlockInstr.ml @@ -52,6 +52,11 @@ let print_bblock_body pp i = fprintf pp "%a = %a\n" pred p (PrintOp.print_condition reg) (c, args) + | RBpiped (p, fu, args) -> + fprintf pp "%a piped\n" print_pred_option p + | RBassign (p, fu, src, dst) -> + fprintf pp "%a %a = %a" print_pred_option p + reg src reg dst let rec print_bblock_exit pp i = fprintf pp "\t\t"; diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 5ee9702..69cc709 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -252,7 +252,7 @@ Inductive instr : Type := | 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 +| RBassign : option pred_op -> funct_node -> reg -> reg -> instr | RBsetpred : condition -> list reg -> predicate -> instr. Inductive cf_instr : Type := @@ -289,8 +289,8 @@ Definition max_reg_instr (m: positive) (i: instr) := 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 + | RBassign p f src dst => + Pos.max src (Pos.max dst m) | RBsetpred c args p => fold_left Pos.max args m end. diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 97ec9aa..aaabe5d 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -577,7 +577,7 @@ Definition update (f : forest) (i : instr) : forest := 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 + | RBassign p fu src dst => f end. (*| -- cgit From b34a08dd656664352e400379d2e890ad95e3afc2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Feb 2021 18:42:31 +0000 Subject: Fix Scheduling to add missing states --- src/hls/Schedule.ml | 48 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 34 insertions(+), 14 deletions(-) diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 9adf17c..613236f 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -703,16 +703,21 @@ let print_lp constr = let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ] -let parse_soln tree s = +let parse_soln (tree, bbtree) s = let r = Str.regexp "var\\([0-9]+\\)n\\([0-9]+\\)_0[ ]+\\([0-9]+\\)" in - if Str.string_match r s 0 then - IMap.update - (Str.matched_group 1 s |> int_of_string) - (update_schedule - ( Str.matched_group 2 s |> int_of_string, - Str.matched_group 3 s |> int_of_string )) - tree - else tree + let bb = Str.regexp "bb\\([0-9]+\\)_\\([0-9]+\\)[ ]+\\([0-9]+\\)" in + let upd s = IMap.update + (Str.matched_group 1 s |> int_of_string) + (update_schedule + ( Str.matched_group 2 s |> int_of_string, + Str.matched_group 3 s |> int_of_string )) + in + if Str.string_match r s 0 + then (upd s tree, bbtree) + else + (if Str.string_match bb s 0 + then (tree, upd s bbtree) + else (tree, bbtree)) let solve_constraints constr = let oc = open_out "lpsolve.txt" in @@ -721,7 +726,7 @@ let solve_constraints constr = Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt") |> drop 3 - |> List.fold_left parse_soln IMap.empty + |> List.fold_left parse_soln (IMap.empty, IMap.empty) let subgraph dfg l = let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in @@ -750,24 +755,39 @@ let combine_bb_schedule schedule s = let i, st = s in IMap.update st (update_schedule i) schedule +let range s e = + List.init (e - s) (fun i -> i) + |> List.map (fun x -> x + s) + (** Should generate the [RTLPar] code based on the input [RTLBlock] description. *) -let transf_rtlpar c c' (schedule : (int * int) list IMap.t) = +let transf_rtlpar c c' schedule = let f i bb : RTLPar.bblock = match bb with | { bb_body = []; bb_exit = c } -> { bb_body = []; bb_exit = c } | { bb_body = bb_body'; bb_exit = ctrl_flow } -> let dfg = match PTree.get i c' with None -> assert false | Some x -> x in - let i_sched = IMap.find (P.to_int i) schedule in + let bb_st_e = + let m = IMap.find (P.to_int i) (snd schedule) in + (List.assq 0 m, List.assq 1 m) in + let i_sched = IMap.find (P.to_int i) (fst schedule) in let i_sched_tree = List.fold_left combine_bb_schedule IMap.empty i_sched in - let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd + (*let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) + in*) + let body2 = List.fold_left (fun x b -> + match IMap.find_opt b i_sched_tree with + | Some i -> i :: x + | None -> [] :: x + ) [] (range (fst bb_st_e) (snd bb_st_e + 1)) + |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) + |> List.rev in (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*) let final_body2 = List.map (fun x -> subgraph dfg x |> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x []) - |> List.rev) body + |> List.rev) body2 in { bb_body = List.map (fun x -> [x]) final_body2; bb_exit = ctrl_flow -- cgit From 75641815724c68791cc2754e850b35700e07e586 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Feb 2021 19:04:52 +0000 Subject: Get some Verilog output with dividers --- src/hls/HTLPargen.v | 25 ++++++++++++++++--------- src/hls/PrintVerilog.ml | 8 ++++++-- 2 files changed, 22 insertions(+), 11 deletions(-) diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index e1c7ec8..629f53e 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -671,7 +671,7 @@ Definition translate_predicate (a : assignment) ret (a dst (Vternary (pred_expr preg pos) e dst)) end. -Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr) +Definition translate_inst a (fu : funct_units) (fin rtrn stack preg : reg) (n : node) (i : instr) : mon stmnt := match i with | RBnop => @@ -690,8 +690,14 @@ 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 src dst => error (Errors.msg "HTLPargen.translate_inst: assign") + | 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)) end. Lemma create_new_state_state_incr: @@ -721,12 +727,13 @@ Definition create_new_state (p: node): mon node := 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)) := +Definition translate_inst_list (fu: funct_units) + (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 fin rtrn stack preg n l; + do stmnt <- translate_inst Vblock fu 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) @@ -773,11 +780,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 (fin rtrn stack preg: reg) (ni : node * bblock) +Definition transf_bblock (fu: funct_units) (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 fin rtrn stack preg) + do _ <- collectlist (translate_inst_list fu fin rtrn stack preg) (prange n (nstate + poslength bb.(bb_body) - 1)%positive bb.(bb_body)); match bb.(bb_body) with @@ -792,7 +799,7 @@ Definition transf_module (f: function) : mon HTL.module := 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 fin rtrn stack preg) + do _ <- collectlist (transf_bblock f.(fn_funct_units) fin rtrn stack preg) (Maps.PTree.elements f.(fn_code)); do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(fn_params); @@ -818,7 +825,7 @@ Definition transf_module (f: function) : mon HTL.module := start rst clk - initial_funct_units + f.(fn_funct_units) current_state.(st_scldecls) current_state.(st_arrdecls) (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index 824623e..da3bd6e 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -178,11 +178,15 @@ let make_io i io r = concat [indent i; io; " "; register r; ";\n"] let print_funct_units clk = function | SignedDiv (stages, numer, denom, quot, rem) -> - sprintf "div_signed #(.stages(%d)) divs(.clk(%s), .clken(1'b1), .numer(%s), .denom(%s), .quotient(%s), .remain(%s))\n" + sprintf ("div_signed #(.stages(%d)) divs(.clk(%s), " ^^ + ".clken(1'b1), .numer(%s), .denom(%s), " ^^ + ".quotient(%s), .remain(%s))\n") (P.to_int stages) (register clk) (register numer) (register denom) (register quot) (register rem) | UnsignedDiv (stages, numer, denom, quot, rem) -> - sprintf "div_unsigned #(.stages(%d)) divs(.clk(%s), .clken(1'b1), .numer(%s), .denom(%s), .quotient(%s), .remain(%s))\n" + sprintf ("div_unsigned #(.stages(%d)) divs(.clk(%s), " ^^ + ".clken(1'b1), .numer(%s), .denom(%s), " ^^ + ".quotient(%s), .remain(%s))\n") (P.to_int stages) (register clk) (register numer) (register denom) (register quot) (register rem) -- cgit