diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2020-11-20 19:06:57 +0000 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2020-11-20 19:21:43 +0000 |
commit | b32015874cb65630736f7f2d9a42419dff6e528c (patch) | |
tree | dd3a7d013704cdf0900b4219bef17974f334533c | |
parent | 982e6c69a52e8ec4e677147004cc5472f8a80d6d (diff) | |
download | vericert-b32015874cb65630736f7f2d9a42419dff6e528c.tar.gz vericert-b32015874cb65630736f7f2d9a42419dff6e528c.zip |
Print HTL args as reg_{n}, not x{n}
-rw-r--r-- | src/verilog/PrintHTL.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml index 10b35b5..f4e3e5c 100644 --- a/src/verilog/PrintHTL.ml +++ b/src/verilog/PrintHTL.ml @@ -31,13 +31,13 @@ open VericertClflags let pstr pp = fprintf pp "%s" -let reg pp r = - fprintf pp "x%d" (P.to_int r) +let rec intersperse c = function + | [] -> [] + | [x] -> [x] + | x :: xs -> x :: c :: intersperse c xs -let rec regs pp = function - | [] -> () - | [r] -> reg pp r - | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl +let register a = sprintf "reg_%d" (P.to_int a) +let registers a = String.concat "" (intersperse ", " (List.map register a)) let print_instruction pp (pc, i) = fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i) @@ -53,7 +53,7 @@ let ptree_to_list ptree = (PTree.elements ptree)) let print_module pp id f = - fprintf pp "%s(%a) {\n" (extern_atom id) regs f.mod_params; + fprintf pp "%s(%s) {\n" (extern_atom id) (registers f.mod_params); let datapath = ptree_to_list f.mod_datapath in let controllogic = ptree_to_list f.mod_controllogic in let insts = ptree_to_list f.mod_insts in |