From 7a05aa21b3a94842ceaf103a53209d87d7f095d5 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Tue, 20 Apr 2021 21:02:24 +0100 Subject: Move renumbering to be HTL->HTL --- src/Compiler.v | 8 +- src/hls/HTLgen.v | 213 +++++++++++++++++++++++++++++++++++++++++++++ src/hls/PrintHTL.ml | 8 +- src/hls/Veriloggen.v | 242 +++------------------------------------------------ 4 files changed, 234 insertions(+), 237 deletions(-) diff --git a/src/Compiler.v b/src/Compiler.v index a87dacf..b5b33e7 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -80,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_HTL: Z -> HTL.program -> unit. Parameter print_RTLBlock: Z -> RTLBlock.program -> unit. Definition print {A: Type} (printer: A -> unit) (prog: A) : A := @@ -190,7 +190,9 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) @@@ HTLgen.transl_program - @@ print print_HTL + @@ print (print_HTL 1) + @@@ HTLgen.renumber_program + @@ print (print_HTL 2) @@@ Veriloggen.transl_program. Definition transf_hls (p : Csyntax.program) : res Verilog.program := @@ -236,7 +238,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@ print (print_RTLBlock 2) @@@ RTLPargen.transl_program @@@ HTLPargen.transl_program - @@ print print_HTL + @@ print (print_HTL 1) @@@ Veriloggen.transl_program. (*| diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index a12b7f9..9347f39 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -28,6 +28,7 @@ Require Import compcert.backend.RTL. Require Import vericert.common.Statemonad. Require Import vericert.common.Vericertlib. +Require Import vericert.common.Maps. Require Import vericert.hls.AssocMap. Require Import vericert.hls.HTL. Require Import vericert.hls.ValueInt. @@ -652,6 +653,218 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program := (fun i v => Errors.OK v) p. *) +Record renumber_state: Type := + mk_renumber_state { + renumber_freshreg : reg; + renumber_regmap : PTree.t reg; + renumber_clk : reg; + }. + +Module RenumberState <: State. + Definition st := renumber_state. + + Definition st_prop (st1 st2 : st) := renumber_clk st1 = renumber_clk st2. + + Lemma st_refl : forall (s : st), st_prop s s. + Proof. constructor. Qed. + + Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. + Proof. congruence. Qed. +End RenumberState. + +Module RenumberMonad := Statemonad(RenumberState). +Module RenumberMonadExtra := Monad.MonadExtra(RenumberMonad). + +Section RENUMBER. + Import RenumberMonad. + Import RenumberState. + Import RenumberMonadExtra. + Import MonadNotation. + + Program Definition map_reg (r: reg) : mon reg := + fun st => OK + (renumber_freshreg st) + (mk_renumber_state (Pos.succ (renumber_freshreg st)) + (PTree.set r (renumber_freshreg st) (renumber_regmap st)) + (renumber_clk st)) + _. + Next Obligation. unfold st_prop; auto. Qed. + + Program Definition clear_mapping : mon unit := + fun st => OK + tt + (mk_renumber_state (renumber_freshreg st) + (PTree.empty reg) + (renumber_clk st)) + _. + Next Obligation. unfold st_prop; auto. Qed. + + Definition renumber_reg (r : reg) : mon reg := + do st <- get; + match PTree.get r (renumber_regmap st) with + | Some reg' => ret reg' + | None => map_reg r + end. + + Definition get_clk : mon reg := do st <- get; ret (renumber_clk st). + + Fixpoint renumber_expr (expr : Verilog.expr) := + match expr with + | Vlit val => ret (Vlit val) + | Vvar reg => + do reg' <- renumber_reg reg; + ret (Vvar reg') + | Vvari reg e => + do reg' <- renumber_reg reg; + do e' <- renumber_expr e; + ret (Vvari reg' e') + | Vinputvar reg => + do reg' <- renumber_reg reg; + ret (Vvar reg') + | Vbinop op e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + ret (Vbinop op e1' e2') + | Vunop op e => + do e' <- renumber_expr e; + ret (Vunop op e') + | Vternary e1 e2 e3 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + do e3' <- renumber_expr e3; + ret (Vternary e1' e2' e3') + | Vrange r e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + do r' <- renumber_reg r; + ret (Vrange r e1' e2') + end. + + Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) := + match stmnt with + | Vskip => ret Vskip + | Vseq s1 s2 => + do s1' <- renumber_stmnt s1; + do s2' <- renumber_stmnt s2; + ret (Vseq s1' s2') + | Vcond e s1 s2 => + do e' <- renumber_expr e; + do s1' <- renumber_stmnt s1; + do s2' <- renumber_stmnt s2; + ret (Vcond e' s1' s2') + | Vcase e cs def => + do e' <- renumber_expr e; + do cs' <- sequence (map + (fun (c : (Verilog.expr * Verilog.stmnt)) => + let (c_expr, c_stmnt) := c in + do expr' <- renumber_expr c_expr; + do stmnt' <- renumber_stmnt c_stmnt; + ret (expr', stmnt')) cs); + do def' <- match def with + | None => ret None + | Some d => do def' <- renumber_stmnt d; ret (Some def') + end; + ret (Vcase e' cs' def') + | Vblock e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + ret (Vblock e1' e2') + | Vnonblock e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + ret (Vnonblock e1' e2') + end. + + Definition renumber_module (m : HTL.module) : mon HTL.module := + do mod_start' <- renumber_reg (HTL.mod_start m); + do mod_reset' <- renumber_reg (HTL.mod_reset m); + do mod_clk' <- get_clk; + do mod_finish' <- renumber_reg (HTL.mod_finish m); + do mod_return' <- renumber_reg (HTL.mod_return m); + do mod_st' <- renumber_reg (HTL.mod_st m); + do mod_stk' <- renumber_reg (HTL.mod_stk m); + do mod_params' <- traverselist renumber_reg (HTL.mod_params m); + do mod_controllogic' <- traverse_ptree1 renumber_stmnt (HTL.mod_controllogic m); + do mod_datapath' <- traverse_ptree1 renumber_stmnt (HTL.mod_datapath m); + + do _ <- clear_mapping; + + match zle (Z.pos (max_pc_map mod_datapath')) Integers.Int.max_unsigned, + zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned with + | left LEDATA, left LECTRL => + ret (HTL.mkmodule + mod_params' + mod_datapath' + mod_controllogic' + (HTL.mod_entrypoint m) + mod_st' + (HTL.mod_stk m) + (HTL.mod_stk_len m) + mod_finish' + mod_return' + mod_start' + mod_reset' + mod_clk' + (HTL.mod_scldecls m) + (HTL.mod_arrdecls m) + (HTL.mod_externctrl m) + (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))) + | _, _ => error (Errors.msg "More than 2^32 states.") + end. + + Definition renumber_fundef (fundef : HTL.fundef) : mon HTL.fundef := + match fundef with + | Internal m => do renumbered <- renumber_module m; ret (Internal renumbered) + | _ => ret fundef + end. + + Section TRANSF_PROGRAM_STATEFUL. + Import RenumberMonad. + Import RenumberState. + Import RenumberMonadExtra. + Import MonadNotation. + + Variables A B V : Type. + Variable transf_fun: ident -> A -> RenumberMonad.mon B. + + Fixpoint transf_globdefs (l: list (ident * globdef A V)) : RenumberMonad.mon (list (ident * globdef B V)) := + match l with + | nil => RenumberMonad.ret nil + | (id, Gfun f) :: l' => + do tf <- transf_fun id f; + do tl' <- transf_globdefs l'; + RenumberMonad.ret ((id, Gfun tf) :: tl') + | (id, Gvar v) :: l' => + do tl' <- transf_globdefs l'; + RenumberMonad.ret ((id, Gvar v) :: tl') + end. + + Definition transform_stateful_program (init_state : RenumberState.st) (p: AST.program A V) : Errors.res (AST.program B V) := + RenumberMonad.run_mon init_state ( + do gl' <- transf_globdefs p.(prog_defs); + RenumberMonad.ret (mkprogram gl' p.(prog_public) p.(prog_main))). + + End TRANSF_PROGRAM_STATEFUL. + + Definition get_main_clk (p : HTL.program) : Errors.res reg := + let ge := Globalenvs.Genv.globalenv p in + match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with + | Some b => + match Globalenvs.Genv.find_funct_ptr ge b with + | Some (AST.Internal m) => Errors.OK (HTL.mod_clk m) + | _ => Errors.Error (Errors.msg "Cannot find internal main for renumbering") + end + | _ => Errors.Error (Errors.msg "Cannot find internal main for renumbering") + end. + + Definition renumber_program (p : HTL.program) : Errors.res HTL.program := + Errors.bind (get_main_clk p) + (fun main_clk => transform_stateful_program _ _ _ + (fun _ => renumber_fundef) + (mk_renumber_state 1%positive (PTree.empty reg) main_clk) + p). +End RENUMBER. + Definition main_is_internal (p : RTL.program) : bool := let ge := Globalenvs.Genv.globalenv p in match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml index 78e422a..65fe1f3 100644 --- a/src/hls/PrintHTL.ml +++ b/src/hls/PrintHTL.ml @@ -70,10 +70,10 @@ let print_program pp prog = 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 - print_program oc prog; - close_out oc + let oc = open_out (f ^ "." ^ Z.to_string passno) in + print_program oc prog; + close_out oc diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index 2ced686..0e359fd 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -31,235 +31,23 @@ Import ListNotations. Local Open Scope error_monad_scope. -Record renumber_state: Type := - mk_renumber_state { - st_freshreg : reg; - st_regmap : PTree.t reg; - }. - -Module RenumberState <: State. - Definition st := renumber_state. - - Definition st_prop (st1 st2 : st) := True. - - Lemma st_refl : forall (s : st), st_prop s s. - Proof. constructor. Qed. - - Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. - Proof. constructor. Qed. -End RenumberState. - -Module VerilogMonad := Statemonad(RenumberState). - -Module VerilogMonadExtra := Monad.MonadExtra(VerilogMonad). - -Section RENUMBER. - Export RenumberState. - Export VerilogMonad. - Import VerilogMonadExtra. - Export MonadNotation. - - Definition renumber_reg (r : reg) : mon reg := - do st <- get; - match PTree.get r st.(st_regmap) with - | Some reg' => ret reg' - | None => - do tt <- set (mk_renumber_state (Pos.succ st.(st_freshreg)) (PTree.set r st.(st_freshreg) st.(st_regmap))) (fun _ => I); - ret st.(st_freshreg) - end. - - Fixpoint renumber_edge (edge : Verilog.edge) := - match edge with - | Vposedge r => - do r' <- renumber_reg r; - ret (Vposedge r') - | Vnegedge r => - do r' <- renumber_reg r; - ret (Vposedge r') - | Valledge => ret Valledge - | Voredge e1 e2 => - do e1' <- renumber_edge e1; - do e2' <- renumber_edge e2; - ret (Voredge e1' e2') - end. - - Definition renumber_declaration (decl : Verilog.declaration) := - match decl with - | Vdecl io reg sz => - do reg' <- renumber_reg reg; - ret (Vdecl io reg' sz) - | Vdeclarr io reg sz len => - do reg' <- renumber_reg reg; - ret (Vdeclarr io reg' sz len) - end. - - Fixpoint renumber_expr (expr : Verilog.expr) := - match expr with - | Vlit val => ret (Vlit val) - | Vvar reg => - do reg' <- renumber_reg reg; - ret (Vvar reg') - | Vvari reg e => - do reg' <- renumber_reg reg; - do e' <- renumber_expr e; - ret (Vvari reg' e') - | Vinputvar reg => - do reg' <- renumber_reg reg; - ret (Vvar reg') - | Vbinop op e1 e2 => - do e1' <- renumber_expr e1; - do e2' <- renumber_expr e2; - ret (Vbinop op e1' e2') - | Vunop op e => - do e' <- renumber_expr e; - ret (Vunop op e') - | Vternary e1 e2 e3 => - do e1' <- renumber_expr e1; - do e2' <- renumber_expr e2; - do e3' <- renumber_expr e3; - ret (Vternary e1' e2' e3') - | Vrange r e1 e2 => - do e1' <- renumber_expr e1; - do e2' <- renumber_expr e2; - do r' <- renumber_reg r; - ret (Vrange r e1' e2') - end. - - Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) := - match stmnt with - | Vskip => ret Vskip - | Vseq s1 s2 => - do s1' <- renumber_stmnt s1; - do s2' <- renumber_stmnt s2; - ret (Vseq s1' s2') - | Vcond e s1 s2 => - do e' <- renumber_expr e; - do s1' <- renumber_stmnt s1; - do s2' <- renumber_stmnt s2; - ret (Vcond e' s1' s2') - | Vcase e cs def => - do e' <- renumber_expr e; - do cs' <- sequence (map - (fun (c : (Verilog.expr * Verilog.stmnt)) => - let (c_expr, c_stmnt) := c in - do expr' <- renumber_expr c_expr; - do stmnt' <- renumber_stmnt c_stmnt; - ret (expr', stmnt')) cs); - do def' <- match def with - | None => ret None - | Some d => do def' <- renumber_stmnt d; ret (Some def') - end; - ret (Vcase e' cs' def') - | Vblock e1 e2 => - do e1' <- renumber_expr e1; - do e2' <- renumber_expr e2; - ret (Vblock e1' e2') - | Vnonblock e1 e2 => - do e1' <- renumber_expr e1; - do e2' <- renumber_expr e2; - ret (Vnonblock e1' e2') - end. - - Definition renumber_module_item (item : Verilog.module_item) := - match item with - | Vdeclaration decl => - do decl' <- renumber_declaration decl; - ret (Vdeclaration decl') - | Valways edge stmnt => - do edge' <- renumber_edge edge; - do stmnt' <- renumber_stmnt stmnt; - ret (Valways edge' stmnt') - | Valways_ff edge stmnt => - do edge' <- renumber_edge edge; - do stmnt' <- renumber_stmnt stmnt; - ret (Valways edge' stmnt') - | Valways_comb edge stmnt => - do edge' <- renumber_edge edge; - do stmnt' <- renumber_stmnt stmnt; - ret (Valways edge' stmnt') - end. - - Definition renumber_module (m : Verilog.module) : mon Verilog.module := - do mod_start' <- renumber_reg (Verilog.mod_start m); - do mod_reset' <- renumber_reg (Verilog.mod_reset m); - do mod_clk' <- renumber_reg (Verilog.mod_clk m); - do mod_finish' <- renumber_reg (Verilog.mod_finish m); - do mod_return' <- renumber_reg (Verilog.mod_return m); - do mod_st' <- renumber_reg (Verilog.mod_st m); - do mod_stk' <- renumber_reg (Verilog.mod_stk m); - do mod_args' <- traverselist renumber_reg (Verilog.mod_args m); - do mod_body' <- traverselist renumber_module_item (Verilog.mod_body m); - - ret (Verilog.mkmodule - mod_start' - mod_reset' - mod_clk' - mod_finish' - mod_return' - mod_st' - mod_stk' - (Verilog.mod_stk_len m) - mod_args' - mod_body' - (Verilog.mod_entrypoint m)). - - Definition renumber_all_modules - (modules : PTree.t Verilog.module) - (start_reg : reg) - (clk : reg) : Errors.res (PTree.t Verilog.module) := - - run_mon (mk_renumber_state start_reg (PTree.empty reg)) - (VerilogMonadExtra.traverse_ptree1 (fun m => - do st <- VerilogMonad.get; - do _ <- VerilogMonad.set - (mk_renumber_state (st_freshreg st) - (PTree.set (mod_clk m) clk - (PTree.empty reg))) - (fun _ => I); - renumber_module m) - modules). -End RENUMBER. - Section TRANSLATE. Local Open Scope error_monad_scope. - Definition transl_datapath_fun (modmap : PTree.t Verilog.module) (a : Verilog.node * HTL.datapath_stmnt) := + Definition transl_datapath_fun (a : Verilog.node * HTL.datapath_stmnt) := let (n, s) := a in let node := Verilog.Vlit (posToValue n) in - match s with - | HTL.HTLfork mod_name args => - do m <- handle_opt (Errors.msg "module does not exist") (modmap ! mod_name); - let reset_mod := Vnonblock (Vvar (Verilog.mod_reset m)) (posToLit 1) in - let zipped_args := List.combine (Verilog.mod_args m) args in - let assign_args := - List.fold_left (fun (acc : stmnt) (a : reg * reg) => let (to, from) := a in - Vseq acc (Vnonblock (Vvar to) (Vvar from))) - zipped_args Vskip in - OK (node, Vseq reset_mod assign_args) - | HTL.HTLjoin mod_name dst => - do m <- handle_opt (Errors.msg "module does not exist") (modmap ! mod_name); - let set_result := Vnonblock (Vvar dst) (Vvar (Verilog.mod_return m)) in - let stop_reset := Vnonblock (Vvar (Verilog.mod_reset m)) (Vlit (ZToValue 0)) in - OK (node, Vseq stop_reset set_result) - | HTL.HTLDataVstmnt s => OK (node, s) - end. + OK (node, s). - Definition transl_datapath modmap st := Errors.mmap (transl_datapath_fun modmap) st. + Definition transl_datapath st := Errors.mmap transl_datapath_fun st. - Definition transl_ctrl_fun (modmap : PTree.t Verilog.module) (a : Verilog.node * HTL.control_stmnt) : Errors.res (Verilog.expr * Verilog.stmnt):= + Definition transl_ctrl_fun (a : Verilog.node * HTL.control_stmnt) : Errors.res (Verilog.expr * Verilog.stmnt):= let (n, s) := a in let node := Verilog.Vlit (posToValue n) in - match s with - | HTL.HTLwait mod_name status expr => - do mod_body <- handle_opt (Errors.msg "module does not exist") (PTree.get mod_name modmap); - let is_done := Vbinop Veq (Vvar (Verilog.mod_finish mod_body)) (Vlit (posToValue 1)) in - let continue := Vnonblock (Vvar status) expr in - Errors.OK (node, Verilog.Vcond is_done continue Vskip) - | HTL.HTLCtrlVstmnt s => Errors.OK (node, s) - end. + Errors.OK (node, s). - Definition transl_ctrl modmap st := Errors.mmap (transl_ctrl_fun modmap) st. + Definition transl_ctrl st := Errors.mmap transl_ctrl_fun st. Definition scl_to_Vdecl_fun (a : reg * (option Verilog.io * Verilog.scl_decl)) := match a with (r, (io, Verilog.VScalar sz)) => (Verilog.Vdecl io r sz) end. @@ -271,13 +59,8 @@ Section TRANSLATE. Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. - Definition called_functions (stmnts : list (Verilog.node * HTL.datapath_stmnt)) : list ident := - List.nodup Pos.eq_dec (Option.map_option (fun (a : (positive * HTL.datapath_stmnt)) => - let (n, stmt) := a in - match stmt with - | HTL.HTLfork fn _ => Some fn - | _ => None - end) stmnts). + Definition called_functions (m : HTL.module) : list ident := + List.nodup Pos.eq_dec (List.map (Basics.compose fst snd) (PTree.elements (HTL.mod_externctrl m))). Definition find_module (program : HTL.program) (name : ident) : Errors.res HTL.module := match option_map snd (find (fun named_module => Pos.eqb (fst named_module) name) program.(prog_defs)) with @@ -323,17 +106,16 @@ Section TRANSLATE. | S fuel' => let inline_start_reg := max_reg_module m in - let inline_names := called_functions (PTree.elements (HTL.mod_datapath m)) in + let inline_names := called_functions m in let htl_modules := PTree.filter (fun m _ => List.existsb (Pos.eqb m) inline_names) (prog_modmap program) in do translated_modules <- PTree.traverse (fun _ => transf_module fuel' program) htl_modules; - do renumbered_modules <- renumber_all_modules translated_modules (max_reg_module m) (HTL.mod_clk m); let cleaned_modules := PTree.map1 (map_body (Option.map_option (clean_up_decl (HTL.mod_clk m)))) - renumbered_modules in + translated_modules in - do case_el_ctrl <- transl_ctrl renumbered_modules (PTree.elements (HTL.mod_controllogic m)); - do case_el_data <- transl_datapath renumbered_modules (PTree.elements (HTL.mod_datapath m)); + do case_el_ctrl <- transl_ctrl (PTree.elements (HTL.mod_controllogic m)); + do case_el_data <- transl_datapath (PTree.elements (HTL.mod_datapath m)); let body : list Verilog.module_item:= Valways (Vposedge (HTL.mod_clk m)) (Vcond (Vbinop Veq (Vvar (HTL.mod_reset m)) (Vlit (ZToValue 1))) -- cgit