aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/PrintHTL.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/verilog/PrintHTL.ml')
-rw-r--r--src/verilog/PrintHTL.ml12
1 files changed, 0 insertions, 12 deletions
diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml
index ffa853f..d87b755 100644
--- a/src/verilog/PrintHTL.ml
+++ b/src/verilog/PrintHTL.ml
@@ -31,7 +31,6 @@ open VericertClflags
let pstr pp = fprintf pp "%s"
-(* TODO import from PrintVerilog.v *)
let rec intersperse c = function
| [] -> []
| [x] -> [x]
@@ -39,15 +38,10 @@ let rec intersperse c = function
let register a = sprintf "reg_%d" (P.to_int a)
let registers a = String.concat "" (intersperse ", " (List.map register a))
-let vmodule a = sprintf "%s" (extern_atom a)
-let instance a = sprintf "instance_%d" (P.to_int a)
let print_instruction pp (pc, i) =
fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i)
-let print_instantiation pp (pc, HTLinstantiation (mod_name, inst_name, args, dst, fin)) =
- fprintf pp "%5d:\t %s %s(%s) -> %s\n" pc (vmodule mod_name) (instance inst_name) (registers args) (register dst)
-
let ptree_to_list ptree =
List.sort
(fun (pc1, _) (pc2, _) -> compare pc2 pc1)
@@ -59,12 +53,6 @@ let print_module pp id f =
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
- if List.length insts > 0 then (
- fprintf pp " instances {\n";
- List.iter (print_instantiation pp) insts;
- fprintf pp " }\n\n";
- ) else fprintf pp " ";
fprintf pp "datapath {\n";
List.iter (print_instruction pp) datapath;
fprintf pp " }\n\n controllogic {\n";