diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-03 13:58:13 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-03 14:05:17 +0100 |
commit | ea78a7613a5a8a3ef21abe7a622e9073efbd1fc2 (patch) | |
tree | e17fdb1a08d160e2c867534047b564052170d19c /src | |
parent | 5c7c33f6651114ffc2904b242d78bb892f644e41 (diff) | |
download | vericert-ea78a7613a5a8a3ef21abe7a622e9073efbd1fc2.tar.gz vericert-ea78a7613a5a8a3ef21abe7a622e9073efbd1fc2.zip |
Print RAM in HTL output
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/PrintHTL.ml | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml index 8608784..2bee487 100644 --- a/src/hls/PrintHTL.ml +++ b/src/hls/PrintHTL.ml @@ -61,6 +61,21 @@ let ptree_to_list ptree = (fun (pc, i) -> (P.to_int pc, i)) (PTree.elements ptree)) +let print_ram pp opt_ram = + match opt_ram with + | Some ram -> + fprintf pp "ram {\n"; + fprintf pp " size: %d\n" (Nat.to_int ram.ram_size); + fprintf pp " mem: %s\n" (register ram.ram_mem); + fprintf pp " en: %s\n" (register ram.ram_en); + fprintf pp " u_en: %s\n" (register ram.ram_u_en); + fprintf pp " addr: %s\n" (register ram.ram_addr); + fprintf pp " wr_en: %s\n" (register ram.ram_wr_en); + fprintf pp " d_in: %s\n" (register ram.ram_d_in); + fprintf pp " d_out: %s\n" (register ram.ram_d_out); + fprintf pp "}\n\n" + | None -> () + let print_module pp id f = fprintf pp "%s(%s) {\n" (extern_atom id) (registers f.mod_params); @@ -68,6 +83,8 @@ let print_module pp id f = let datapath = ptree_to_list f.mod_datapath in let controllogic = ptree_to_list f.mod_controllogic in + print_ram pp f.mod_ram; + fprintf pp "externctrl {\n"; List.iter (print_externctrl pp) externctrl; fprintf pp " }\n\n"; |