SystemVerilog .*

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.

Author: kroening

CHANGELOG

@@ -5,6 +5,7 @@
 * Verilog: $onehot and $onehot0 are now elaboration-time constant
 * SystemVerilog: fix for #-# and #=# for empty matches
 * SystemVerilog: fix for |-> and |=> for empty matches
+* SystemVerilog: support 1800-2005 .*
 * 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

@@ -212,7 +212,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"
@@ -3101,9 +3102,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
@@ -3737,6 +3739,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{})
     {
@@ -854,6 +854,19 @@ class verilog_inst_baset : public verilog_module_itemt
       return operands();
     }
 
+    bool positional_connections() const
+    {
+      return !named_connections();
+    }
+
+    bool named_connections() const
+    {
+      auto &connections = this->connections();
+      return !connections.empty() &&
+             (connections.front().id() == ID_verilog_named_port_connection ||
+              connections.front().id() == ID_verilog_wildcard_port_connection);
+    }
+
   protected:
     using exprt::operands;
   };
@@ -877,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_synthesis.cpp

@@ -1376,17 +1376,17 @@ Function: verilog_synthesist::instantiate_ports
 
 void verilog_synthesist::instantiate_ports(
   const irep_idt &instance,
-  const exprt &inst,
+  const verilog_instt::instancet &inst,
   const symbolt &symbol,
   const replace_mapt &replace_map,
   transt &trans)
 {
-  if(inst.operands().size()==0)
+  if(inst.connections().size() == 0)
     return;
 
   // named port connection?
 
-  if(to_multi_ary_expr(inst).op0().id() == ID_named_port_connection)
+  if(inst.named_connections())
   {
     const irept::subt &ports = symbol.type.find(ID_ports).get_sub();
 
@@ -1397,7 +1397,7 @@ void verilog_synthesist::instantiate_ports(
           to_symbol_expr((const exprt &)(port)).get_identifier());
 
     // no requirement that all ports are connected
-    for(const auto &o_it : inst.operands())
+    for(const auto &o_it : inst.connections())
     {
       if(o_it.operands().size()==2)
       {
@@ -1418,17 +1418,17 @@ void verilog_synthesist::instantiate_ports(
   {
     const irept::subt &ports = symbol.type.find(ID_ports).get_sub();
 
-    if(inst.operands().size()!=ports.size())
+    if(inst.connections().size() != ports.size())
     {
       throw errort().with_location(inst.source_location())
         << "wrong number of ports: expected " << ports.size() << " but got "
-        << inst.operands().size();
+        << inst.connections().size();
     }
 
     irept::subt::const_iterator p_it=
       ports.begin();
 
-    for(const auto &o_it : inst.operands())
+    for(const auto &o_it : inst.connections())
     {
       DATA_INVARIANT(o_it.is_not_nil(), "all ports must be connected");
 

src/verilog/verilog_synthesis_class.h

@@ -310,7 +310,7 @@ class verilog_synthesist:
 
   void instantiate_ports(
     const irep_idt &instance,
-    const exprt &inst,
+    const verilog_instt::instancet &inst,
     const symbolt &,
     const replace_mapt &,
     transt &);

src/verilog/verilog_typecheck.cpp

@@ -123,16 +123,32 @@ void verilog_typecheckt::typecheck_port_connections(
   }
 
   // named port connection?
-
-  if(inst.connections().front().id() == ID_named_port_connection)
+  if(inst.named_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";
@@ -179,7 +195,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())
     {