Verilog: package imports

This adds the grammar rules for package imports, both in the header, and as
an item.

regression/verilog/package/package1.sv → regression/verilog/packages/package1.sv

@@ -3,4 +3,5 @@ package my_pkg;
 endpackage
 
 module main;
+  import my_pkg::*;
 endmodule

src/hw_cbmc_irep_ids.h

@@ -151,8 +151,10 @@ IREP_ID_ONE(iff)
 IREP_ID_ONE(offset)
 IREP_ID_ONE(xnor)
 IREP_ID_ONE(specify)
-IREP_ID_ONE(verilog_module)
 IREP_ID_ONE(verilog_empty_item)
+IREP_ID_ONE(verilog_import_item)
+IREP_ID_ONE(verilog_module)
+IREP_ID_ONE(verilog_package_import)
 IREP_ID_ONE(module_source)
 IREP_ID_ONE(module_items)
 IREP_ID_ONE(parameter_port_list)

src/verilog/parser.y

@@ -606,31 +606,33 @@ module_nonansi_header:
 	  attribute_instance_brace
 	  module_keyword
 	  module_identifier_with_scope
+	  package_import_declaration_brace
 	  parameter_port_list_opt
 	  list_of_ports_opt ';'
           {
             init($$); stack_expr($$).operands().resize(5);
             stack_expr($$).operands()[0].swap(stack_expr($1));
             stack_expr($$).operands()[1].swap(stack_expr($2));
             stack_expr($$).operands()[2].swap(stack_expr($3));
-            stack_expr($$).operands()[3].swap(stack_expr($4));
-            stack_expr($$).operands()[4].swap(stack_expr($5));
+            stack_expr($$).operands()[3].swap(stack_expr($5));
+            stack_expr($$).operands()[4].swap(stack_expr($6));
           }
         ;
 
 module_ansi_header:
           attribute_instance_brace
 	  module_keyword
 	  module_identifier_with_scope
+	  package_import_declaration_brace
 	  parameter_port_list_opt
 	  list_of_port_declarations ';'
           {
             init($$); stack_expr($$).operands().resize(5);
             stack_expr($$).operands()[0].swap(stack_expr($1));
             stack_expr($$).operands()[1].swap(stack_expr($2));
             stack_expr($$).operands()[2].swap(stack_expr($3));
-            stack_expr($$).operands()[3].swap(stack_expr($4));
-            stack_expr($$).operands()[4].swap(stack_expr($5));
+            stack_expr($$).operands()[3].swap(stack_expr($5));
+            stack_expr($$).operands()[4].swap(stack_expr($6));
           }
         ;
 
@@ -1117,6 +1119,33 @@ data_declaration:
 		  addswap($$, ID_type, $2);
 		  swapop($$, $3); }
 	| type_declaration
+	| package_import_declaration
+	;
+
+package_import_declaration_brace:
+	  /* Optional */
+		{ init($$); }
+	| package_import_declaration_brace package_import_declaration
+		{ $$ = $1; mts($$, $2); }
+	;
+
+package_import_declaration:
+	  TOK_IMPORT package_import_item_brace ';'
+		{ init($$, ID_verilog_package_import); swapop($$, $2); }
+	;
+
+package_import_item_brace:
+	  package_import_item
+		{ init($$); mts($$, $1); }
+	| package_import_item_brace ',' package_import_item
+		{ $$ = $1; mts($$, $3); }
+	;
+
+package_import_item:
+	  package_identifier "::" identifier
+		{ init($$, ID_verilog_import_item); mto($$, $1); mto($$, $3); }
+	| package_identifier "::" "*"
+		{ init($$, ID_verilog_import_item); mto($$, $1); }
 	;
 
 genvar_declaration:

src/verilog/verilog_elaborate.cpp

@@ -769,6 +769,9 @@ void verilog_typecheckt::collect_symbols(
   else if(module_item.id() == ID_verilog_smv_assume)
   {
   }
+  else if(module_item.id() == ID_verilog_package_import)
+  {
+  }
   else
     DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());
 }

src/verilog/verilog_interfaces.cpp

@@ -293,6 +293,9 @@ void verilog_typecheckt::interface_module_item(
   else if(module_item.id() == ID_verilog_smv_assume)
   {
   }
+  else if(module_item.id() == ID_verilog_package_import)
+  {
+  }
   else
   {
     DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());

src/verilog/verilog_synthesis.cpp

@@ -2740,6 +2740,10 @@ void verilog_synthesist::synth_module_item(
   else if(module_item.id() == ID_verilog_empty_item)
   {
   }
+  else if(module_item.id() == ID_verilog_package_import)
+  {
+    // done already
+  }
   else
   {
     throw errort().with_location(module_item.source_location())

src/verilog/verilog_typecheck.cpp

@@ -1584,6 +1584,9 @@ void verilog_typecheckt::convert_module_item(
   else if(module_item.id() == ID_verilog_smv_assume)
   {
   }
+  else if(module_item.id() == ID_verilog_package_import)
+  {
+  }
   else
   {
     throw errort().with_location(module_item.source_location())