diff --git a/regression/verilog/arrays/packed_real1.desc b/regression/verilog/arrays/packed_real1.desc
new file mode 100644
index 000000000..7a513846c
--- /dev/null
+++ b/regression/verilog/arrays/packed_real1.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+packed_real1.sv
+--module main --bound 0
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+A packed array of reals must be rejected.
diff --git a/regression/verilog/arrays/packed_real1.sv b/regression/verilog/arrays/packed_real1.sv
new file mode 100644
index 000000000..6d261906f
--- /dev/null
+++ b/regression/verilog/arrays/packed_real1.sv
@@ -0,0 +1,9 @@
+module main;
+
+  // Packed arrays can be made of single bit data types
+  // or other packed types.
+  typedef real my_real;
+  my_real [7:0] my_array;
+
+endmodule
+
diff --git a/regression/verilog/arrays/packed_typedef1.desc b/regression/verilog/arrays/packed_typedef1.desc
new file mode 100644
index 000000000..4ad097bdc
--- /dev/null
+++ b/regression/verilog/arrays/packed_typedef1.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+packed_typedef1.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The packed array type must not be dropped.
diff --git a/regression/verilog/arrays/packed_typedef1.sv b/regression/verilog/arrays/packed_typedef1.sv
new file mode 100644
index 000000000..e27e179c1
--- /dev/null
+++ b/regression/verilog/arrays/packed_typedef1.sv
@@ -0,0 +1,8 @@
+module main;
+
+  typedef bit my_bit;
+  my_bit [7:0] my_vector;
+
+  always assert p0: ($bits(my_vector) == 8);
+
+endmodule
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index d5d6d0119..b1eef9284 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -110,9 +110,11 @@ IREP_ID_ONE(wire)
 IREP_ID_ONE(uwire)
 IREP_ID_ONE(wand)
 IREP_ID_ONE(automatic)
-IREP_ID_ONE(verilog_enum)
 IREP_ID_TWO(C_verilog_type, #verilog_type)
+IREP_ID_ONE(verilog_enum)
+IREP_ID_ONE(verilog_packed_array)
 IREP_ID_ONE(verilog_type_reference)
+IREP_ID_ONE(verilog_unpacked_array)
 IREP_ID_ONE(enum_names)
 IREP_ID_ONE(var)
 IREP_ID_ONE(trireg)
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index 60529a7d4..d289b4d48 100644
--- a/src/verilog/parser.y
+++ b/src/verilog/parser.y
@@ -785,8 +785,10 @@ module_port_input_declaration:
 	  TOK_INPUT net_port_type port_identifier unpacked_dimension_brace
 		{ init($$, ID_decl);
                   stack_expr($$).set(ID_class, ID_input);
-                  add_as_subtype(stack_type($4), stack_type($2));
-                  addswap($$, ID_type, $4);
+                  // The net_port_type goes onto the declaration,
+                  // and the unpacked_array_type goes onto the declarator.
+                  addswap($$, ID_type, $2);
+                  addswap($3, ID_type, $4);
                   mto($$, $3); }
 	;
 
@@ -794,14 +796,18 @@ module_port_output_declaration:
 	  TOK_OUTPUT net_port_type port_identifier unpacked_dimension_brace
 		{ init($$, ID_decl);
                   stack_expr($$).set(ID_class, ID_output);
-                  add_as_subtype(stack_type($4), stack_type($2));
-                  addswap($$, ID_type, $4);
+                  // The data_type goes onto the declaration,
+                  // and the unpacked_array_type goes onto the declarator.
+                  addswap($$, ID_type, $2);
+                  addswap($3, ID_type, $4);
                   mto($$, $3); }
 	| TOK_OUTPUT data_type port_identifier unpacked_dimension_brace
 		{ init($$, ID_decl);
                   stack_expr($$).set(ID_class, ID_output_register);
-                  add_as_subtype(stack_type($4), stack_type($2));
-                  addswap($$, ID_type, $4);
+                  // The data_type goes onto the declaration,
+                  // and the unpacked_array_type goes onto the declarator.
+                  addswap($$, ID_type, $2);
+                  addswap($3, ID_type, $4);
                   mto($$, $3); }
 	;
 
@@ -1132,12 +1138,7 @@ genvar_declaration:
 	;
 
 net_declaration:
-          net_type drive_strength_opt vectored_scalared_opt data_type_or_implicit delay3_opt list_of_net_names ';'
-		{ init($$, ID_decl);
-                  addswap($$, ID_class, $1);
-                  addswap($$, ID_type, $4);
-                  swapop($$, $6); }
-        | net_type drive_strength_opt vectored_scalared_opt data_type_or_implicit delay3_opt list_of_net_decl_assignments ';'
+          net_type drive_strength_opt vectored_scalared_opt data_type_or_implicit delay3_opt list_of_net_decl_assignments ';'
 		{ init($$, ID_decl);
                   addswap($$, ID_class, $1);
                   addswap($$, ID_type, $4);
@@ -1167,21 +1168,6 @@ vectored_scalared_opt:
 	| TOK_SCALARED     { init($$, "scalared"); }
 	;
 
-list_of_net_names:
-	  net_name
-		{ init($$); mto($$, $1); }
-	| list_of_net_names ',' net_name
-		{ $$=$1;    mto($$, $3); }
-	;
-
-net_name: net_identifier packed_dimension_brace
-          {
-            $$=$1;
-            stack_expr($$).id(ID_declarator);
-            addswap($$, ID_type, $2);
-          }
-	;
-
 list_of_net_decl_assignments:
 	  net_decl_assignment
 		{ init($$); mto($$, $1); }
@@ -1244,7 +1230,9 @@ data_type:
 	| TOK_VIRTUAL interface_opt interface_identifier
 	        { init($$, "virtual_interface"); }
 	| /*scope_opt*/ type_identifier packed_dimension_brace
-		{ $$ = $1; stack_expr($$).id(ID_typedef_type); }
+		{ stack_expr($1).id(ID_typedef_type);
+                  add_as_subtype(stack_type($2), stack_type($1));
+                  $$ = $2; }
 //	| class_type
 	| TOK_EVENT
 	        { init($$, ID_event); }
@@ -1659,8 +1647,16 @@ range:	part_select;
 // System Verilog standard 1800-2017
 // A.2.4 Declaration assignments
 
-net_decl_assignment: net_identifier '=' expression
-		{ $$ = $1; stack_expr($$).id(ID_declarator); addswap($$, ID_value, $3); }
+net_decl_assignment:
+	  net_identifier unpacked_dimension_brace
+		{ $$ = $1;
+		  stack_expr($$).id(ID_declarator);
+		  addswap($$, ID_type, $2); }
+	| net_identifier unpacked_dimension_brace '=' expression
+		{ $$ = $1;
+		  stack_expr($$).id(ID_declarator);
+		  addswap($$, ID_type, $2);
+		  addswap($$, ID_value, $4); }
 	;
 
 variable_decl_assignment:
@@ -1693,7 +1689,7 @@ packed_dimension_opt:
 
 packed_dimension:
 	  '[' const_expression TOK_COLON const_expression ']'
-		{ init($$, ID_array);
+		{ init($$, ID_verilog_packed_array);
 		  stack_type($$).add_subtype().make_nil();
 		  exprt &range=static_cast<exprt &>(stack_type($$).add(ID_range));
 		  range.add_to_operands(stack_expr($2));
@@ -1703,13 +1699,14 @@ packed_dimension:
 
 unpacked_dimension:
 	  '[' const_expression TOK_COLON const_expression ']'
-		{ init($$, ID_array);
+		{ init($$, ID_verilog_unpacked_array);
 		  stack_type($$).add_subtype().make_nil();
 		  exprt &range=static_cast<exprt &>(stack_type($$).add(ID_range));
 		  range.add_to_operands(stack_expr($2));
 		  range.add_to_operands(stack_expr($4)); }
 	| '[' expression ']'
-		{ init($$, ID_array);
+		{ // starts at index 0
+		  init($$, ID_verilog_unpacked_array);
 		  stack_type($$).add_subtype().make_nil();
 		  stack_type($$).set(ID_size, std::move(stack_expr($2)));
 		}
diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp
index 6172a73bb..9cc0a7f4c 100644
--- a/src/verilog/verilog_elaborate.cpp
+++ b/src/verilog/verilog_elaborate.cpp
@@ -24,7 +24,9 @@ void verilog_typecheckt::collect_port_symbols(const verilog_declt &decl)
 
   const irep_idt &base_name = declarator.base_name();
   const irep_idt &port_class = decl.get_class();
+
   auto type = convert_type(decl.type());
+
   irep_idt identifier = hierarchical_identifier(base_name);
 
   if(port_class.empty())
@@ -34,7 +36,18 @@ void verilog_typecheckt::collect_port_symbols(const verilog_declt &decl)
   else
   {
     // add the symbol
-    symbolt new_symbol(identifier, type, mode);
+    typet final_type;
+    if(declarator.type().is_nil())
+      final_type = type;
+    else if(declarator.type().id() == ID_verilog_unpacked_array)
+      final_type = unpacked_array_type(declarator.type(), type);
+    else
+    {
+      throw errort().with_location(declarator.source_location())
+        << "unexpected type on declarator";
+    }
+
+    symbolt new_symbol(identifier, final_type, mode);
 
     if(port_class == ID_input)
     {
@@ -222,8 +235,8 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
         if(declarator.type().is_nil())
           symbol.type = type;
-        else if(declarator.type().id() == ID_array)
-          symbol.type = array_type(declarator.type(), type);
+        else if(declarator.type().id() == ID_verilog_unpacked_array)
+          symbol.type = unpacked_array_type(declarator.type(), type);
         else
         {
           throw errort().with_location(declarator.source_location())
@@ -315,7 +328,15 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
             << "empty symbol name";
         }
 
-        symbol.type = type;
+        if(declarator.type().is_nil())
+          symbol.type = type;
+        else if(declarator.type().id() == ID_verilog_unpacked_array)
+          symbol.type = unpacked_array_type(declarator.type(), type);
+        else
+        {
+          throw errort().with_location(declarator.source_location())
+            << "unexpected type on declarator";
+        }
 
         symbol.name = hierarchical_identifier(symbol.base_name);
 
@@ -401,8 +422,8 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
       if(declarator.type().is_nil())
         symbol.type = type;
-      else if(declarator.type().id() == ID_array)
-        symbol.type = array_type(declarator.type(), type);
+      else if(declarator.type().id() == ID_verilog_unpacked_array)
+        symbol.type = unpacked_array_type(declarator.type(), type);
       else
       {
         throw errort().with_location(symbol.location)
@@ -468,8 +489,8 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
       if(declarator.type().is_nil())
         symbol.type = type;
-      else if(declarator.type().id() == ID_array)
-        symbol.type = array_type(declarator.type(), type);
+      else if(declarator.type().id() == ID_verilog_unpacked_array)
+        symbol.type = unpacked_array_type(declarator.type(), type);
       else
       {
         throw errort().with_location(symbol.location)
diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp
index 4a779cc3d..c6352a498 100644
--- a/src/verilog/verilog_typecheck.cpp
+++ b/src/verilog/verilog_typecheck.cpp
@@ -28,80 +28,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 /*******************************************************************\
 
-Function: verilog_typecheckt::array_type
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-array_typet verilog_typecheckt::array_type(
-  const irept &src,
-  const typet &element_type)
-{
-  // int whatnot[x:y];
-  // 'src' is yet to be converted, but 'element_type' is already converted.
-  PRECONDITION(src.id() == ID_array);
-
-  // Unpacked arrays may have a range [x:y],
-  // or a size [s], equivalent to [0:s-1]
-  const exprt &range_expr = static_cast<const exprt &>(src.find(ID_range));
-  const exprt &size_expr = static_cast<const exprt &>(src.find(ID_size));
-
-  mp_integer size, offset;
-  bool little_endian;
-
-  if(range_expr.is_not_nil())
-  {
-    // these may be negative
-    mp_integer msb, lsb;
-    convert_range(range_expr, msb, lsb);
-    little_endian = (lsb <= msb);
-    size = (little_endian ? msb - lsb : lsb - msb) + 1;
-    offset = little_endian ? lsb : msb;
-  }
-  else if(size_expr.is_not_nil())
-  {
-    little_endian = true;
-    size = convert_integer_constant_expression(size_expr);
-    offset = 0;
-    if(size < 0)
-    {
-      throw errort().with_location(size_expr.find_source_location())
-        << "array size must be nonnegative";
-    }
-  }
-  else
-  {
-    throw errort() << "array must have range or size";
-  }
-
-  const typet src_subtype =
-    static_cast<const typet &>(src).has_subtype()
-      ? static_cast<const type_with_subtypet &>(src).subtype()
-      : typet(ID_nil);
-
-  typet array_subtype;
-  
-  // may need to go recursive
-  if(src_subtype.is_nil())
-    array_subtype=element_type;
-  else
-    array_subtype=array_type(src_subtype, element_type);
-
-  const exprt final_size_expr = from_integer(size, integer_typet());
-  array_typet result(array_subtype, final_size_expr);
-  result.set(ID_offset, from_integer(offset, integer_typet()));
-  result.set(ID_C_little_endian, little_endian);
-  
-  return result;
-}
-
-/*******************************************************************\
-
 Function: verilog_typecheckt::typecheck_port_connection
 
   Inputs:
diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h
index a4cf42d75..d01b1c63e 100644
--- a/src/verilog/verilog_typecheck.h
+++ b/src/verilog/verilog_typecheck.h
@@ -125,10 +125,6 @@ class verilog_typecheckt:
   void interface_generate_block(const class verilog_generate_blockt &);
   void interface_statement(const class verilog_statementt &);
 
-  array_typet array_type(
-    const irept &src,
-    const typet &element_type);
-
   // type checking
   
   typedef enum { A_CONTINUOUS, A_BLOCKING, A_NON_BLOCKING } vassignt;
diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h
index 3fe66242c..99ba701da 100644
--- a/src/verilog/verilog_typecheck_expr.h
+++ b/src/verilog/verilog_typecheck_expr.h
@@ -64,6 +64,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 
   typet convert_type(const typet &);
   typet convert_enum(const class verilog_enum_typet &);
+  array_typet unpacked_array_type(const typet &src, const typet &element_type);
 
   void convert_range(
     const exprt &range,
diff --git a/src/verilog/verilog_typecheck_type.cpp b/src/verilog/verilog_typecheck_type.cpp
index 0485d99d5..f595bbada 100644
--- a/src/verilog/verilog_typecheck_type.cpp
+++ b/src/verilog/verilog_typecheck_type.cpp
@@ -16,6 +16,81 @@ Author: Daniel Kroening, kroening@kroening.com
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::unpacked_array_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+array_typet verilog_typecheck_exprt::unpacked_array_type(
+  const typet &src,
+  const typet &element_type)
+{
+  // int whatnot[x:y];
+  // 'src' is yet to be converted, but 'element_type' is already converted.
+  PRECONDITION(src.id() == ID_verilog_unpacked_array);
+
+  // Unpacked arrays may have a range [x:y],
+  // or a size [s], equivalent to [0:s-1]
+  const exprt &range_expr = static_cast<const exprt &>(src.find(ID_range));
+  const exprt &size_expr = static_cast<const exprt &>(src.find(ID_size));
+
+  mp_integer size, offset;
+  bool little_endian;
+
+  if(range_expr.is_not_nil())
+  {
+    // these may be negative
+    mp_integer msb, lsb;
+    convert_range(range_expr, msb, lsb);
+    little_endian = (lsb <= msb);
+    size = (little_endian ? msb - lsb : lsb - msb) + 1;
+    offset = little_endian ? lsb : msb;
+  }
+  else if(size_expr.is_not_nil())
+  {
+    little_endian = true;
+    size = convert_integer_constant_expression(size_expr);
+    offset = 0;
+    if(size < 0)
+    {
+      // The size must be positive. 1800-2017 7.4.2
+      throw errort().with_location(size_expr.find_source_location())
+        << "array size must be nonnegative";
+    }
+  }
+  else
+  {
+    throw errort() << "unpacked array must have range or size";
+  }
+
+  const typet src_subtype =
+    static_cast<const typet &>(src).has_subtype()
+      ? static_cast<const type_with_subtypet &>(src).subtype()
+      : typet(ID_nil);
+
+  typet array_subtype;
+
+  // may need to go recursive
+  if(src_subtype.is_nil())
+    array_subtype = element_type;
+  else
+    array_subtype = unpacked_array_type(src_subtype, element_type);
+
+  const exprt final_size_expr = from_integer(size, integer_typet());
+  array_typet result(array_subtype, final_size_expr);
+  result.set(ID_offset, from_integer(offset, integer_typet()));
+  result.set(ID_C_little_endian, little_endian);
+
+  return result;
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::convert_type
 
   Inputs:
@@ -111,7 +186,7 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
     result.set(ID_C_identifier, enum_type.identifier());
     return result.with_source_location(source_location);
   }
-  else if(src.id() == ID_array)
+  else if(src.id() == ID_verilog_packed_array)
   {
     const exprt &range=static_cast<const exprt &>(src.find(ID_range));
 
@@ -147,7 +222,8 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
     }
     else
     {
-      // we have a genuine array, and do a recursive call
+      // We have a multi-dimensional packed array,
+      // and do a recursive call.
       const exprt size=from_integer(width, integer_typet());
       typet s=convert_type(subtype);
 
@@ -158,6 +234,11 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
       return std::move(result).with_source_location(source_location);
     }
   }
+  else if(src.id() == ID_verilog_unpacked_array)
+  {
+    // not expected here -- these stick to the declarators
+    PRECONDITION(false);
+  }
   else if(src.id() == ID_verilog_type_reference)
   {
     auto &type_reference = to_verilog_type_reference(src);