SystemVerilog .* wildcard port connections

SystemVerilog 1800-2005 has introduced the .* operator, used for

a) wildcard port connections (23.3.2.4), and

b) wildcard patterns (12.6).

This adds support to the scanner, parser, and type checker for wildcard port connections.

Author: kroening

CHANGELOG

@@ -7,6 +7,7 @@
 * Verilog: $isunknown
 * SystemVerilog: fix for #-# and #=# for empty matches
 * SystemVerilog: fix for |-> and |=> for empty matches
+* SystemVerilog: support 1800-2005 .* wildcard port connections
 * LTL/SVA to Buechi with --buechi
 * SMV: abs, bool, count, max, min, toint, word1
 * BMC: new encoding for F, avoiding spurious traces

regression/verilog/modules/wildcard_port_connection1.desc

@@ -0,0 +1,7 @@
+CORE
+wildcard_port_connection1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/modules/wildcard_port_connection1.sv

@@ -0,0 +1,9 @@
+module M(input a, b);
+  assert final (a);
+  assert final (!b);
+endmodule
+
+module main;
+  wire a = 0, b = 1;
+  M m(.*);
+endmodule

src/hw_cbmc_irep_ids.h

@@ -214,7 +214,8 @@ IREP_ID_ONE(verilog_always)
 IREP_ID_ONE(verilog_always_comb)
 IREP_ID_ONE(verilog_always_ff)
 IREP_ID_ONE(verilog_always_latch)
-IREP_ID_ONE(named_port_connection)
+IREP_ID_ONE(verilog_named_port_connection)
+IREP_ID_ONE(verilog_wildcard_port_connection)
 IREP_ID_ONE(verilog_final)
 IREP_ID_ONE(initial)
 IREP_ID_ONE(verilog_label_statement)

src/verilog/parser.y

@@ -405,6 +405,7 @@ int yyverilogerror(const char *error)
 %token TOK_LSQPLUS              "[+"
 %token TOK_LSQEQUAL             "[="
 %token TOK_LSQMINUSGREATER      "[->"
+%token TOK_DOTASTERIC           ".*"
 
 /* System Verilog Keywords */
 %token TOK_ACCEPT_ON        "accept_on"
@@ -3100,9 +3101,10 @@ named_port_connection_brace:
 
 named_port_connection:
 	  '.' port_identifier '(' expression_opt ')'
-		{ init($$, ID_named_port_connection);
+		{ init($$, ID_verilog_named_port_connection);
                   mto($$, $2);
                   mto($$, $4); }
+	| ".*" { init($$, ID_verilog_wildcard_port_connection); }
 	;
 
 // System Verilog standard 1800-2017
@@ -3736,6 +3738,26 @@ open_value_range: value_range;
 // System Verilog standard 1800-2017
 // A.6.7.1 Patterns
 
+pattern:
+	  "." variable_identifier
+	| ".*"
+	| constant_expression
+	| "tagged" member_identifier
+	| "tagged" member_identifier pattern
+	| "'{" pattern_list "}"
+	| "'{" member_pattern_list "}"
+	;
+
+pattern_list:
+	  pattern
+	| pattern_list "," pattern
+	;
+
+member_pattern_list:
+          member_identifier ":" pattern
+        | member_pattern_list "," member_identifier ":" pattern
+        ;
+
 assignment_pattern:
 	  '\'' '{' expression_brace '}'
 		{ init($$, ID_verilog_assignment_pattern); swapop($$, $3); }

src/verilog/scanner.l

@@ -273,6 +273,8 @@ void verilog_scanner_init()
 "[+"            { SYSTEM_VERILOG_OPERATOR(TOK_LSQPLUS, "[+"); }
 "[="            { SYSTEM_VERILOG_OPERATOR(TOK_LSQEQUAL, "[="); }
 "[->"           { SYSTEM_VERILOG_OPERATOR(TOK_LSQMINUSGREATER, "[->"); }
+                /* port connections, patterns */
+".*"            { SYSTEM_VERILOG_OPERATOR(TOK_DOTASTERIC, ".*"); }
 
                 /* Verilog 1364-1995 keywords */
 

src/verilog/verilog_expr.h

@@ -799,7 +799,7 @@ class verilog_inst_baset : public verilog_module_itemt
     named_port_connectiont(exprt _port, exprt _value)
       : binary_exprt(
           std::move(_port),
-          ID_named_port_connection,
+          ID_verilog_named_port_connection,
           std::move(_value),
           typet{})
     {
@@ -863,7 +863,8 @@ class verilog_inst_baset : public verilog_module_itemt
     {
       auto &connections = this->connections();
       return connections.empty() ||
-             connections.front().id() == ID_named_port_connection;
+             (connections.front().id() == ID_verilog_named_port_connection ||
+              connections.front().id() == ID_verilog_wildcard_port_connection);
     }
 
   protected:
@@ -889,15 +890,15 @@ class verilog_inst_baset : public verilog_module_itemt
 inline const verilog_inst_baset::named_port_connectiont &
 to_verilog_named_port_connection(const exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_named_port_connection);
+  PRECONDITION(expr.id() == ID_verilog_named_port_connection);
   verilog_inst_baset::named_port_connectiont::check(expr);
   return static_cast<const verilog_inst_baset::named_port_connectiont &>(expr);
 }
 
 inline verilog_inst_baset::named_port_connectiont &
 to_verilog_named_port_connection(exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_named_port_connection);
+  PRECONDITION(expr.id() == ID_verilog_named_port_connection);
   verilog_inst_baset::named_port_connectiont::check(expr);
   return static_cast<verilog_inst_baset::named_port_connectiont &>(expr);
 }

src/verilog/verilog_typecheck.cpp

@@ -115,10 +115,27 @@ void verilog_typecheckt::typecheck_port_connections(
     // We don't require that all ports are connected.
 
     std::set<irep_idt> assigned_ports;
+    bool wildcard = false;
 
     for(auto &connection : inst.connections())
     {
-      if(connection.id() != ID_named_port_connection)
+      if(connection.id() == ID_verilog_wildcard_port_connection)
+      {
+        // .*
+        if(wildcard)
+        {
+          // .* can only be given once
+          throw errort{}.with_location(connection.source_location())
+            << "wildcard connection given more than once";
+        }
+        else
+        {
+          wildcard = true;
+          continue;
+        }
+      }
+
+      if(connection.id() != ID_verilog_named_port_connection)
       {
         throw errort().with_location(inst.source_location())
           << "expected a named port connection";
@@ -165,7 +182,7 @@ void verilog_typecheckt::typecheck_port_connections(
       assigned_ports.insert(identifier);
     }
   }
-  else // just a list without names
+  else // Positional connections, i.e., just a list without port names
   {
     if(inst.connections().size() != ports.size())
     {