Verilog: module ports may be arrays

This adds support for ANSI-style declarations of module ports with array
type.

Author: kroening

regression/verilog/modules/ports7.desc

@@ -0,0 +1,7 @@
+CORE
+ports7.v
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/modules/ports7.v

@@ -0,0 +1,20 @@
+// Ports can be arrays.
+module sub(input [31:0] array [9:0]);
+
+  always assert p0: array[0] == 0;
+  always assert p9: array[9] == 9;
+
+endmodule
+
+module main;
+  reg [31:0] array [9:0];
+
+  initial begin
+    integer i;
+    for(i=0; i<10; i=i+1)
+      array[i] = i;
+  end
+
+  sub s(array);
+
+endmodule

regression/verilog/modules/ports8.desc

@@ -0,0 +1,7 @@
+CORE
+ports8.v
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/modules/ports8.v

@@ -0,0 +1,22 @@
+// Ports can be arrays.
+module sub(output reg [31:0] array [9:0]);
+
+  wire some_floating_wire;
+
+  always @some_floating_wire begin
+    integer i;
+    for(i=0; i<10; i=i+1)
+      array[i] = i;
+  end
+
+endmodule
+
+module main;
+  wire [31:0] array [9:0];
+
+  sub s(array);
+
+  always assert p0: array[0] == 0;
+  always assert p9: array[9] == 9;
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -27,8 +27,8 @@ IREP_ID_ONE(sva_s_until_with)
 IREP_ID_ONE(sva_overlapped_implication)
 IREP_ID_ONE(sva_non_overlapped_implication)
 IREP_ID_ONE(module_instance)
-IREP_ID_ONE(C_offset)
-IREP_ID_ONE(C_little_endian)
+IREP_ID_TWO(C_offset, #offset)
+IREP_ID_TWO(C_little_endian, #little_endian)
 IREP_ID_ONE(ports)
 IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)

src/verilog/parser.y

@@ -822,23 +822,26 @@ ansi_port_declaration:
 	;
 
 module_port_input_declaration:
-	  TOK_INPUT net_port_type port_identifier
+	  TOK_INPUT net_port_type port_identifier unpacked_dimension_brace
 		{ init($$, ID_decl);
                   stack_expr($$).set(ID_class, ID_input);
-                  addswap($$, ID_type, $2);
+                  add_as_subtype(stack_type($4), stack_type($2));
+                  addswap($$, ID_type, $4);
                   mto($$, $3); }
 	;
 
 module_port_output_declaration:
-	  TOK_OUTPUT net_port_type port_identifier
+	  TOK_OUTPUT net_port_type port_identifier unpacked_dimension_brace
 		{ init($$, ID_decl);
                   stack_expr($$).set(ID_class, ID_output);
-                  addswap($$, ID_type, $2);
+                  add_as_subtype(stack_type($4), stack_type($2));
+                  addswap($$, ID_type, $4);
                   mto($$, $3); }
-	| TOK_OUTPUT data_type port_identifier
+	| TOK_OUTPUT data_type port_identifier unpacked_dimension_brace
 		{ init($$, ID_decl);
                   stack_expr($$).set(ID_class, ID_output_register);
-                  addswap($$, ID_type, $2);
+                  add_as_subtype(stack_type($4), stack_type($2));
+                  addswap($$, ID_type, $4);
                   mto($$, $3); }
 	;
 
@@ -1089,10 +1092,11 @@ specparam_declaration:
 // A.2.1.2 Port declarations
 
 module_port_inout_declaration:
-	  TOK_INOUT net_port_type port_identifier
+	  TOK_INOUT net_port_type port_identifier unpacked_dimension_brace
 		{ init($$, ID_decl);
                   stack_expr($$).set(ID_class, ID_inout);
-                  addswap($$, ID_type, $2);
+                  add_as_subtype(stack_type($4), stack_type($2));
+                  addswap($$, ID_type, $4);
                   mto($$, $3); }
 	;
 

src/verilog/verilog_typecheck.cpp

@@ -92,7 +92,7 @@ array_typet verilog_typecheckt::array_type(
   else
     array_subtype=array_type(src_subtype, element_type);
 
-  const exprt final_size_expr = from_integer(size, natural_typet());
+  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);