diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-20 21:02:24 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-20 21:02:24 +0100 |
commit | 7a05aa21b3a94842ceaf103a53209d87d7f095d5 (patch) | |
tree | 31ab96aa633b0a972fb719ab3318e24654e464b2 /src/hls/Veriloggen.v | |
parent | 7183a0a0a037026a0d03e4df6153ca2d5879af49 (diff) | |
download | vericert-7a05aa21b3a94842ceaf103a53209d87d7f095d5.tar.gz vericert-7a05aa21b3a94842ceaf103a53209d87d7f095d5.zip |
Move renumbering to be HTL->HTL
Diffstat (limited to 'src/hls/Veriloggen.v')
-rw-r--r-- | src/hls/Veriloggen.v | 242 |
1 files changed, 12 insertions, 230 deletions
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))) |