SystemVerilog: type parameter ports

This adds support for SystemVerilog type parameter ports (1800-2017 6.20.3).

Author: kroening

CHANGELOG

@@ -1,5 +1,6 @@
 # EBMC 5.9
 
+* SystemVerilog: type parameter ports
 * SystemVerilog: fix for type parameters
 * SMV: word constants
 * SMV: IVAR declarations

regression/verilog/modules/parameter_ports4.desc

@@ -0,0 +1,7 @@
+CORE
+type_parameter_port1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/verilog/modules/type_parameter_port1.desc

@@ -0,0 +1,7 @@
+CORE
+type_parameter_port2.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/verilog/modules/parameter_ports4.sv renamed to regression/verilog/modules/type_parameter_port1.sv

@@ -0,0 +1,13 @@
+module sub #(parameter type T = int)();
+
+  var T my_var;
+
+endmodule
+
+module main;
+
+  sub #(.T(byte)) submodule();
+
+  p1: assert final ($bits(submodule.my_var) == 8);
+
+endmodule // main

regression/verilog/modules/type_parameter_port2.desc

@@ -0,0 +1,7 @@
+CORE
+type_parameter_port3.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/verilog/modules/type_parameter_port2.sv

@@ -0,0 +1,13 @@
+module sub #(type T = int)();
+
+  var T my_var;
+
+endmodule
+
+module main;
+
+  sub #(byte) submodule();
+
+  p1: assert final ($bits(submodule.my_var) == 8);
+
+endmodule // main

regression/verilog/modules/type_parameter_port3.desc

@@ -1985,6 +1985,8 @@ list_of_variable_identifiers:
 parameter_port_declaration:
           TOK_PARAMETER data_type_or_implicit param_assignment
 		{ init($$, ID_decl); stack_expr($$).type() = std::move(stack_type($2)); mto($$, $3); }
+        | TOK_PARAMETER TOK_TYPE type_assignment
+		{ init($$, ID_decl); stack_expr($$).type() = typet{ID_type}; mto($$, $3); }
 	| TOK_LOCALPARAM data_type_or_implicit param_assignment
 		{ init($$, ID_decl); stack_expr($$).type() = std::move(stack_type($2)); mto($$, $3); }
 	| data_type param_assignment
@@ -2028,7 +2030,7 @@ list_of_type_assignments:
 	;
 
 type_assignment: param_identifier '=' data_type
-		{ init($$, ID_parameter);
+		{ init($$, ID_declarator);
 		  auto base_name = stack_expr($1).id();
 		  stack_expr($$).set(ID_identifier, base_name);
 		  stack_expr($$).set(ID_base_name, base_name);
@@ -3161,11 +3163,23 @@ named_parameter_assignment_brace:
 	  	{ $$=$1; mto($$, $3); }
 	;
 
-ordered_parameter_assignment:
-          expression;
+ordered_parameter_assignment: param_expression
+	;
+
+param_expression:
+          expression
+        | data_type
+		{ init($$, ID_type); stack_expr($$).type() = stack_type($1); }
+        ;
+
+param_expression_opt:
+          /* empty */
+		{ init($$, ID_nil); }
+        | param_expression
+        ;
 
 named_parameter_assignment:
-	  '.' parameter_identifier '(' expression_opt ')'
+	  '.' parameter_identifier '(' param_expression_opt ')'
 	  	{ init($$, ID_named_parameter_assignment);
 	  	  stack_expr($$).add(ID_parameter).swap(stack_expr($2));
 	  	  stack_expr($$).add(ID_value).swap(stack_expr($4));

regression/verilog/modules/type_parameter_port3.sv

@@ -245,15 +245,17 @@ irep_idt verilog_typecheckt::parameterize_module(
 
     if(pv.is_not_nil())
     {
-      mp_integer i;
-      if(to_integer_non_constant(pv, i))
+      if(pv.id() == ID_type)
       {
-        throw errort().with_location(pv.source_location())
-          << "parameter value expected to be constant, but got `"
-          << to_string(pv) << "'";
+        suffix += "some_type";
       }
-      else
+      else if(pv.id() == ID_constant)
+      {
+        mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(pv));
         suffix += integer2string(i);
+      }
+      else
+        DATA_INVARIANT(false, "parameter value expected to be type or constant");
     }
   }