Verilog: import of tasks/functions in interfaces and modports

regression/verilog/interface/modport_import1.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 modport_import1.sv
 
 ^no properties$

regression/verilog/interface/package_import1.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 package_import1.sv
 
 ^no properties$

src/hw_cbmc_irep_ids.h

@@ -340,6 +340,8 @@ IREP_ID_ONE(verilog_import_item)
 IREP_ID_ONE(verilog_interface)
 IREP_ID_ONE(verilog_modport_declaration)
 IREP_ID_ONE(verilog_modport_item)
+IREP_ID_ONE(verilog_modport_import)
+IREP_ID_ONE(verilog_modport_export)
 IREP_ID_ONE(verilog_modport)
 IREP_ID_ONE(verilog_class)
 IREP_ID_ONE(verilog_class_type)

src/verilog/parser.y

@@ -2948,6 +2948,19 @@ modport_ports_declaration:
         | non_type_identifier
                 { init($$, ID_nil);
                   mto($$, $1); }
+        | TOK_IMPORT modport_tf_port
+                { init($$, ID_verilog_modport_import);
+                  mto($$, $2); }
+        | TOK_EXPORT modport_tf_port
+                { init($$, ID_verilog_modport_export);
+                  mto($$, $2); }
+        ;
+
+// System Verilog standard 1800-2017
+// A.2.9: modport_tf_port ::= method_prototype | tf_identifier
+modport_tf_port:
+          method_prototype
+        | non_type_identifier
         ;
 
 // System Verilog standard 1800-2017

src/verilog/verilog_typecheck_expr.cpp

@@ -949,23 +949,49 @@ exprt verilog_typecheck_exprt::convert_expr_function_call(
   }
   else if(f_op.id() == ID_verilog_identifier)
   {
-    base_name = to_verilog_identifier_expr(f_op).base_name();
+    auto &identifier_expr = to_verilog_identifier_expr(f_op);
+    base_name = identifier_expr.base_name();
+    const auto import = identifier_expr.import();
+    const auto preresolved = identifier_expr.preresolved();
 
-    // first look in the current module
-    irep_idt full_identifier =
-      id2string(module_instance) + "." + id2string(base_name);
-
-    if(ns.lookup(full_identifier, symbol))
+    if(import != irep_idt{})
     {
-      // not there? Try compilation-unit scope.
-      full_identifier = verilog_unit_scope_identifier(base_name);
+      // A function/task made visible via a package import
+      // (IEEE 1800-2017 26.3), e.g. 'import pkg::*;' followed by a call.
+      irep_idt full_identifier = "Verilog::" + id2string(import);
 
       if(ns.lookup(full_identifier, symbol))
       {
         throw errort().with_location(f_op.source_location())
           << "unknown function `" << base_name << "'";
       }
     }
+    else if(preresolved != irep_idt{})
+    {
+      if(ns.lookup(preresolved, symbol))
+      {
+        throw errort().with_location(f_op.source_location())
+          << "unknown function `" << base_name << "'";
+      }
+    }
+    else
+    {
+      // first look in the current module
+      irep_idt full_identifier =
+        id2string(module_instance) + "." + id2string(base_name);
+
+      if(ns.lookup(full_identifier, symbol))
+      {
+        // not there? Try compilation-unit scope.
+        full_identifier = verilog_unit_scope_identifier(base_name);
+
+        if(ns.lookup(full_identifier, symbol))
+        {
+          throw errort().with_location(f_op.source_location())
+            << "unknown function `" << base_name << "'";
+        }
+      }
+    }
   }
   else
   {