Verilog: allow interface, package and class names as named formals

CHANGELOG

@@ -13,6 +13,8 @@
 * SystemVerilog: $typename for logic types
 * Verilog: +incdir+ command-line option
 * Verilog: -l and +libfile+ command-line options
+* SystemVerilog: named port connections and named parameter assignments
+  may name formals that clash with interface, package or class names
 * Refreshed IC3 engine --new-ic3
 
 # EBMC 6.0

regression/verilog/interface/port4.desc

@@ -0,0 +1,8 @@
+CORE
+port4.sv
+--module main --bound 0
+^\[main\.s\.p0\] main\.s\.data_if == 1: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/verilog/interface/port4.sv

@@ -0,0 +1,17 @@
+// The formal name in a named port connection lives in the port name
+// space of the instantiated module, and hence may coincide with the
+// name of an interface.
+module sub(input logic data_if);
+  initial p0: assert(data_if == 1);
+endmodule
+
+interface data_if;
+  logic value;
+  initial value = 1;
+endinterface
+
+module main;
+  data_if shared();
+
+  sub s(.data_if(shared.value));
+endmodule

regression/verilog/modules/named_parameter_assignment1.desc

@@ -0,0 +1,8 @@
+CORE
+named_parameter_assignment1.sv
+--module main --bound 0
+^\[main\.u\.assert\.1\] .*: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/verilog/modules/named_parameter_assignment1.sv

@@ -0,0 +1,32 @@
+// The parameter name in a named parameter assignment is looked up in the
+// parameter name space of the instantiated module, and hence may coincide
+// with a typedef, interface, package or class name that happens to be
+// visible at the point of instantiation.
+module sub #(
+  parameter int some_type = 1,
+  parameter int some_if = 2,
+  parameter int some_pkg = 3,
+  parameter int some_class = 4) ();
+
+  initial assert (some_type == 10 && some_if == 20 &&
+                  some_pkg == 30 && some_class == 40);
+
+endmodule
+
+typedef int some_type;
+
+interface some_if;
+  logic x;
+endinterface
+
+package some_pkg;
+endpackage
+
+class some_class;
+endclass
+
+module main;
+
+  sub #(.some_type(10), .some_if(20), .some_pkg(30), .some_class(40)) u();
+
+endmodule

regression/verilog/modules/named_port_connection2.desc

@@ -0,0 +1,8 @@
+CORE
+named_port_connection2.sv
+--module main --bound 0
+^\[main\.u\.assert\.1\] .*: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/verilog/modules/named_port_connection2.sv

@@ -0,0 +1,31 @@
+// The formal name in a named port connection is looked up in the
+// port name space of the instantiated module, and hence may coincide
+// with a typedef, interface, package or class name that happens to be
+// visible at the point of instantiation.
+module sub(
+  input some_type,
+  input some_if,
+  input some_pkg,
+  input some_class);
+
+  initial assert (some_type && some_if && some_pkg && some_class);
+
+endmodule
+
+typedef int some_type;
+
+interface some_if;
+  logic x;
+endinterface
+
+package some_pkg;
+endpackage
+
+class some_class;
+endclass
+
+module main;
+
+  sub u(.some_type(1), .some_if(1), .some_pkg(1), .some_class(1));
+
+endmodule

src/verilog/parser.y

@@ -3874,8 +3874,10 @@ named_port_connection_brace:
         ;
 
 named_port_connection:
-          // This needs to be 'any_identifier' to allow identifiers that
-          // are typedefs in the local scope.
+          // This needs to be 'any_identifier': the formal name is looked
+          // up in the instantiated module's port name space, and hence may
+          // coincide with a typedef, interface, package or class name that
+          // is visible in the local scope.
           '.' any_identifier '(' expression_opt ')'
                 { init($$, ID_verilog_named_port_connection);
                   mto($$, $2);
@@ -5490,8 +5492,14 @@ attr_name: identifier
 // An extension of the System Verilog grammar to allow defining new identifiers
 // even if they are already used for a different kind of identifier
 // in a higher scope.
+// Note that the scanner gives all identifier tokens the same shape,
+// namely ID_verilog_identifier with ID_base_name set. Hence, no action
+// is required to normalize the alternatives below.
 any_identifier:
           TOK_TYPE_IDENTIFIER
+        | TOK_CLASS_IDENTIFIER
+        | TOK_PACKAGE_IDENTIFIER
+        | TOK_INTERFACE_IDENTIFIER
         | non_type_identifier
         ;
 
@@ -5603,7 +5611,10 @@ type_identifier: TOK_TYPE_IDENTIFIER
 
 ps_type_identifier: type_identifier;
 
-parameter_identifier: non_type_identifier;
+// This needs to be 'any_identifier': the parameter name in a named
+// parameter assignment is looked up in the instantiated module's
+// parameter name space, not in the local scope.
+parameter_identifier: any_identifier;
 
 udp_identifier: non_type_identifier;