Merge pull request #1392 from diffblue/verilog-interconnect-grammar

SystemVerilog: grammar for interconnect nets

Author: tautschnig

regression/verilog/modules/interconnect1.desc

@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 interconnect1.sv
 
-^EXIT=0$
+^file .* line 2: no support for interconnect nets$
+^EXIT=2$
 ^SIGNAL=0$
 --
 --
-interconnect is not implemented.

src/hw_cbmc_irep_ids.h

@@ -123,6 +123,7 @@ IREP_ID_ONE(verilog_associative_array)
 IREP_ID_ONE(verilog_declarations)
 IREP_ID_ONE(verilog_default_clocking)
 IREP_ID_ONE(verilog_default_disable)
+IREP_ID_ONE(verilog_interconnect)
 IREP_ID_ONE(verilog_lifetime)
 IREP_ID_ONE(verilog_logical_equality)
 IREP_ID_ONE(verilog_logical_inequality)

src/verilog/parser.y

@@ -1521,6 +1521,10 @@ net_declaration:
                   addswap($$, ID_class, $1);
                   addswap($$, ID_type, $4);
                   swapop($$, $6); }
+        | TOK_INTERCONNECT delay3_opt list_of_net_decl_assignments ';'
+		{ init($$, ID_decl);
+                  stack_expr($$).set(ID_class, ID_verilog_interconnect);
+                  swapop($$, $3); }
 	;
 
 // Note that the identifier that is defined using the typedef may be
@@ -1790,14 +1794,19 @@ net_type_opt:
         | net_type
         ;
 
-net_port_type: net_type_opt signing_opt packed_dimension_brace
-                {
-	          // The net type is a subtype of the signing.
-	          add_as_subtype(stack_type($2), stack_type($1));
-	          // That becomes a subtype of the packed dimension.
-                  add_as_subtype(stack_type($3), stack_type($2));
-                  $$ = $3;
-	        }
+net_port_type:
+	  net_type_opt signing_opt packed_dimension_brace
+	{
+	  // The net type is a subtype of the signing.
+	  add_as_subtype(stack_type($2), stack_type($1));
+	  // That becomes a subtype of the packed dimension.
+	  add_as_subtype(stack_type($3), stack_type($2));
+	  $$ = $3;
+	}
+	| TOK_INTERCONNECT
+	{
+	  init($$, ID_verilog_interconnect);
+	}
         ;
 
 variable_port_type: var_data_type ;

src/verilog/verilog_elaborate.cpp

@@ -492,8 +492,14 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
       symbols_added.push_back(symbol.name);
     }
   }
-  else if(decl_class == ID_reg || decl_class == ID_var)
+  else if(
+    decl_class == ID_reg || decl_class == ID_var ||
+    decl_class == ID_verilog_interconnect)
   {
+    if(decl_class == ID_verilog_interconnect)
+      throw errort().with_location(decl.source_location())
+        << "no support for interconnect nets";
+
     symbolt symbol;
 
     symbol.mode = mode;