Revert changes relating to instance generation

Revert "Add todo for missing logic around instantiations"
This reverts commit 303a45374643f75698c61f062899973d2c297831.

Revert "Add wires and use them for output of instances"
This reverts commit a72f26319dabca414a2b576424b9f72afaca161c.

Revert "Separate HTL instantiations from Verilog ones"
This reverts commit 653c8729f4322f538aa7116c5e311c884b3c5047.

Revert "Translate instantiations from HTL to verilog"
This reverts commit 982e6c69a52e8ec4e677147004cc5472f8a80d6d.

Revert "Print instantiations in HTL output"
This reverts commit 9b87637d3e4d6a75dee1221b017e3ccf6632642e.

Revert "Add a field in HTL modules for instances"
This reverts commit d79dae026b150e9671e0aa7262f6aa2d1d302502.

Revert "Generate (invalid) module instantiations for calls"
This reverts commit dfaa3a9cbc07649feea3220693a8a854a32eafb6.

4 files changed, 16 insertions, 48 deletions

diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 2432e7e..620ef14 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -32,7 +32,6 @@ 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.
@@ -42,12 +41,6 @@ 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;
@@ -62,8 +55,7 @@ Record module: Type :=
     mod_start : reg;
     mod_reset : reg;
     mod_clk : reg;
-    mod_insts : AssocMap.t instantiation;
-    mod_scldecls : AssocMap.t Verilog.scl_decl;
+    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 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";
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index a355a17..b3fb6c8 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -36,11 +36,6 @@ let fold_map f s = List.map f s |> concat
 
 let pstr pp = fprintf pp "%s"
 
-let rec intersperse c = function
-  | [] -> []
-  | [x] -> [x]
-  | x :: xs -> x :: c :: intersperse c xs
-
 let pprint_binop l r =
   let unsigned op = sprintf "{%s %s %s}" l op r in
   let signed op = sprintf "{$signed(%s) %s $signed(%s)}" l op r in
@@ -74,8 +69,6 @@ let unop = function
   | Vnot -> " ! "
 
 let register a = sprintf "reg_%d" (P.to_int a)
-let vmodule a = sprintf "%s" (extern_atom a)
-let instance a = sprintf "instance_%d" (P.to_int a)
 
 (*let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*)
 
@@ -141,12 +134,6 @@ 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)]
-  | Vdeclwire (r, sz) -> concat [indent i; declare "wire" (r, sz)]
-  | 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
@@ -158,6 +145,11 @@ let pprint_module_item i = function
   | Valways_comb (e, s) ->
     concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
 
+let rec intersperse c = function
+  | [] -> []
+  | [x] -> [x]
+  | x :: xs -> x :: c :: intersperse c xs
+
 let make_io i io r = concat [indent i; io; " "; register r; ";\n"]
 
 let compose f g x = g x |> f
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 27522b4..3b0dd0a 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -39,7 +39,6 @@ Set Implicit Arguments.
 
 Definition reg : Type := positive.
 Definition node : Type := positive.
-Definition ident : Type := positive.
 Definition szreg : Type := reg * nat.
 
 Record associations (A : Type) : Type :=
@@ -100,15 +99,7 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
 Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
   mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)).
 
-Inductive io : Type :=
-| Vinput : io
-| Voutput : io
-| Vinout : io.
-
-Inductive scl_decl : Type :=
-| VScalar (io: option Verilog.io) (sz : nat)
-| VWire (sz : nat).
-
+Inductive scl_decl : Type := VScalar (sz : nat).
 Inductive arr_decl : Type := VArray (sz : nat) (ln : nat).
 
 (** * Verilog AST
@@ -202,13 +193,18 @@ Inductive edge : Type :=
 
 (** ** Module Items
 
-Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). *)
+Module items can either be declarations ([Vdecl]) or always blocks ([Valways]).
+The declarations are always register declarations as combinational logic can be
+done using combinational always block instead of continuous assignments. *)
+
+Inductive io : Type :=
+| Vinput : io
+| Voutput : io
+| Vinout : io.
 
 Inductive declaration : Type :=
 | Vdecl : option io -> reg -> nat -> declaration
-| Vdeclarr : option io -> reg -> nat -> nat -> declaration
-| Vdeclwire : reg -> nat -> declaration
-| Vinstancedecl : ident -> ident -> list reg -> declaration.
+| Vdeclarr : option io -> reg -> nat -> nat -> declaration.
 
 Inductive module_item : Type :=
 | Vdeclaration : declaration -> module_item