Separate HTL instantiations from Verilog ones

In HTL, they reference their data arguments, destination, and finished
control signal. Meanwhile, in Verilog, they just contain an unstructured
list of parameters.

This is done because when modules are generated in the HTL stage we do
not have access to any of the instantiating module's control
signals (they are declared after the entirety of the module has been
translated). Also, I believe, these signals are not part of the HTL semantics.

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