diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/translation/Veriloggen.v | 87 |
1 files changed, 44 insertions, 43 deletions
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index 137ab08..2e8c4ac 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -25,49 +25,6 @@ Import ListNotations. Local Open Scope error_monad_scope. -Definition transl_datapath_fun (modmap : PTree.t Verilog.module) (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 mod_body <- handle_opt (Errors.msg "module does not exist") (modmap ! mod_name); - let reset_mod := Vnonblock (Vvar (Verilog.mod_reset mod_body)) (posToLit 1) in - let zipped_args := List.combine (Verilog.mod_args mod_body) 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 => OK (node, Verilog.Vskip) (* inline_call m args *) - | HTL.HTLDataVstmnt s => OK (node, s) - end. - -Definition transl_datapath modmap st := Errors.mmap (transl_datapath_fun modmap) st. - -Definition transl_ctrl_fun (modmap : PTree.t Verilog.module) (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. - -Definition transl_ctrl modmap st := Errors.mmap (transl_ctrl_fun modmap) 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. - -Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl. - -Definition arr_to_Vdeclarr_fun (a : reg * (option Verilog.io * Verilog.arr_decl)) := - match a with (r, (io, Verilog.VArray sz l)) => (Verilog.Vdeclarr io r sz l) end. - -Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. - Record renumber_state: Type := mk_renumber_state { st_freshreg : reg; @@ -252,9 +209,53 @@ Section RENUMBER. 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) := + let (n, s) := a in + let node := Verilog.Vlit (posToValue n) in + match s with + | HTL.HTLfork mod_name args => + do mod_body <- handle_opt (Errors.msg "module does not exist") (modmap ! mod_name); + let reset_mod := Vnonblock (Vvar (Verilog.mod_reset mod_body)) (posToLit 1) in + let zipped_args := List.combine (Verilog.mod_args mod_body) 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 => OK (node, Verilog.Vskip) (* inline_call m args *) + | HTL.HTLDataVstmnt s => OK (node, s) + end. + + Definition transl_datapath modmap st := Errors.mmap (transl_datapath_fun modmap) st. + + Definition transl_ctrl_fun (modmap : PTree.t Verilog.module) (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. + + Definition transl_ctrl modmap st := Errors.mmap (transl_ctrl_fun modmap) 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. + + Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl. + + Definition arr_to_Vdeclarr_fun (a : reg * (option Verilog.io * Verilog.arr_decl)) := + match a with (r, (io, Verilog.VArray sz l)) => (Verilog.Vdeclarr io r sz l) end. + + 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 |