5 files changed, 20 insertions, 18 deletions

diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 6ab733f..4d0ba42 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -32,6 +32,7 @@ Local Open Scope assocmap.
 
 Definition reg := positive.
 Definition node := positive.
+Definition ident := positive.
 
 Definition datapath := PTree.t Verilog.stmnt.
 Definition controllogic := PTree.t Verilog.stmnt.
@@ -41,6 +42,12 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
     In p0 (map fst (Maps.PTree.elements m)) ->
     Z.pos p0 <= Integers.Int.max_unsigned.
 
+Inductive instantiation : Type :=
+  (** [HTLinstantiation mod_name inst_name args dest fin]. This does not map directly
+      to a verilog instantiation. It omits all control signals (clk, rst, etc.)
+      except the finished signal *)
+  HTLinstantiation : ident -> ident -> list reg -> reg -> reg -> instantiation.
+
 Record module: Type :=
   mkmodule {
     mod_params : list reg;
@@ -55,7 +62,7 @@ Record module: Type :=
     mod_start : reg;
     mod_reset : reg;
     mod_clk : reg;
-    mod_insts : AssocMap.t Verilog.instantiation;
+    mod_insts : AssocMap.t instantiation;
     mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl);
     mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl);
     mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath);
diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml
index f4e3e5c..ffa853f 100644
--- a/src/verilog/PrintHTL.ml
+++ b/src/verilog/PrintHTL.ml
@@ -31,6 +31,7 @@ open VericertClflags
 
 let pstr pp = fprintf pp "%s"
 
+(* TODO import from PrintVerilog.v *)
 let rec intersperse c = function
   | [] -> []
   | [x] -> [x]
@@ -38,12 +39,14 @@ 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_instance pp (pc, i) =
-  fprintf pp "%5d:\t%s" pc (pprint_instantiation 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
@@ -59,7 +62,7 @@ let print_module pp id f =
   let insts = ptree_to_list f.mod_insts in
   if List.length insts > 0 then (
     fprintf pp "  instances {\n";
-    List.iter (print_instance pp) insts;
+    List.iter (print_instantiation pp) insts;
     fprintf pp "  }\n\n";
   ) else fprintf pp "  ";
   fprintf pp "datapath {\n";
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index a2fd78f..6fe2292 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -109,13 +109,6 @@ let rec pprint_stmnt i =
   | Vblock (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"]
   | Vnonblock (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"]
 
-let pprint_instantiation = function
-  | Vinstantiation (m, name, args) -> concat [
-      vmodule m; " ";
-      instance name; "("; concat (intersperse ", " (List.map register args)); ")";
-      ";\n"
-    ]
-
 let rec pprint_edge = function
   | Vposedge r -> concat ["posedge "; register r]
   | Vnegedge r -> concat ["negedge "; register r]
@@ -148,7 +141,11 @@ let print_io = function
 let decl i = function
   | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)]
   | Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)]
-  | Vinstancedecl inst -> concat [indent i; pprint_instantiation inst]
+  | Vinstancedecl (m, name, args) -> concat [
+      indent i; vmodule m; " ";
+      instance name; "("; concat (intersperse ", " (List.map register args)); ")";
+      ";\n"
+    ]
 
 (* TODO Fix always blocks, as they currently always print the same. *)
 let pprint_module_item i = function
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index 1a37126..6a15ee9 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -18,8 +18,6 @@
 
 val pprint_stmnt : int -> Verilog.stmnt -> string
 
-val pprint_instantiation : Verilog.instantiation -> string
-
 val print_value : out_channel -> ValueInt.value -> unit
 
 val print_program : bool -> out_channel -> Verilog.program -> unit
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 4f5c838..6f65fdc 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -177,9 +177,6 @@ Inductive stmnt : Type :=
 | Vblock : expr -> expr -> stmnt
 | Vnonblock : expr -> expr -> stmnt.
 
-Inductive instantiation : Type :=
-  Vinstantiation : ident -> ident -> list reg -> instantiation.
-
 (** ** Edges
 
 These define when an always block should be triggered, for example if the always
@@ -209,7 +206,7 @@ Inductive io : Type :=
 Inductive declaration : Type :=
 | Vdecl : option io -> reg -> nat -> declaration
 | Vdeclarr : option io -> reg -> nat -> nat -> declaration
-| Vinstancedecl : instantiation -> declaration.
+| Vinstancedecl : ident -> ident -> list reg -> declaration.
 
 Inductive module_item : Type :=
 | Vdeclaration : declaration -> module_item