From f637736c1ff60ea9189784535e7cedec1d18aae2 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 16 Mar 2024 08:13:59 -0700 Subject: [PATCH] Verilog: package imports --- .../{package => packages}/package1.desc | 0 .../verilog/{package => packages}/package1.sv | 1 + src/hw_cbmc_irep_ids.h | 4 +- src/verilog/parser.y | 37 +++++++++++++++++-- src/verilog/verilog_elaborate.cpp | 3 ++ src/verilog/verilog_interfaces.cpp | 3 ++ src/verilog/verilog_synthesis.cpp | 4 ++ src/verilog/verilog_typecheck.cpp | 3 ++ 8 files changed, 50 insertions(+), 5 deletions(-) rename regression/verilog/{package => packages}/package1.desc (100%) rename regression/verilog/{package => packages}/package1.sv (80%) diff --git a/regression/verilog/package/package1.desc b/regression/verilog/packages/package1.desc similarity index 100% rename from regression/verilog/package/package1.desc rename to regression/verilog/packages/package1.desc diff --git a/regression/verilog/package/package1.sv b/regression/verilog/packages/package1.sv similarity index 80% rename from regression/verilog/package/package1.sv rename to regression/verilog/packages/package1.sv index dc46072e8..370bff3f0 100644 --- a/regression/verilog/package/package1.sv +++ b/regression/verilog/packages/package1.sv @@ -3,4 +3,5 @@ package my_pkg; endpackage module main; + import my_pkg::*; endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 7ca642e29..f1a97058c 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -139,8 +139,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) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 66b19d97b..60e1e83c8 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -662,6 +662,7 @@ module_nonansi_header: attribute_instance_brace module_keyword module_identifier_with_scope + package_import_declaration_brace parameter_port_list_opt list_of_ports_opt ';' { @@ -669,8 +670,8 @@ module_nonansi_header: 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)); } ; @@ -678,6 +679,7 @@ module_ansi_header: attribute_instance_brace module_keyword module_identifier_with_scope + package_import_declaration_brace parameter_port_list_opt list_of_port_declarations ';' { @@ -685,8 +687,8 @@ module_ansi_header: 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)); } ; @@ -1165,6 +1167,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: diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index 6172a73bb..26f185286 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -778,6 +778,9 @@ void verilog_typecheckt::collect_symbols( else if(module_item.id() == ID_verilog_empty_item) { } + else if(module_item.id() == ID_verilog_package_import) + { + } else DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string()); } diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index 7a6c97c26..5a0c52bf7 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/src/verilog/verilog_interfaces.cpp @@ -284,6 +284,9 @@ void verilog_typecheckt::interface_module_item( else if(module_item.id() == ID_verilog_empty_item) { } + else if(module_item.id() == ID_verilog_package_import) + { + } else { DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string()); diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 852310468..0a7ca8ff0 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -2684,6 +2684,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()) diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 4a779cc3d..15245653a 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1642,6 +1642,9 @@ void verilog_typecheckt::convert_module_item( else if(module_item.id() == ID_verilog_empty_item) { } + else if(module_item.id() == ID_verilog_package_import) + { + } else { throw errort().with_location(module_item.source_location())