diff --git a/regression/verilog/interface/modport_import1.desc b/regression/verilog/interface/modport_import1.desc index 0b09f56d2..9a545b51c 100644 --- a/regression/verilog/interface/modport_import1.desc +++ b/regression/verilog/interface/modport_import1.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE modport_import1.sv ^no properties$ diff --git a/regression/verilog/interface/package_import1.desc b/regression/verilog/interface/package_import1.desc index 22711c85b..ad6ab04d9 100644 --- a/regression/verilog/interface/package_import1.desc +++ b/regression/verilog/interface/package_import1.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE package_import1.sv ^no properties$ diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 9e43a321c..daef410b6 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/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) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index a84767aa8..319f61124 100644 --- a/src/verilog/parser.y +++ b/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 diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 878354c38..b029c0292 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -949,16 +949,16 @@ 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)) { @@ -966,6 +966,32 @@ exprt verilog_typecheck_exprt::convert_expr_function_call( << "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 {