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