From abbf45049e32f5a5eb80af8eefd4828aee1d75f3 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 16 Mar 2024 08:13:59 -0700 Subject: [PATCH] Verilog: package imports This adds the grammar rules for package imports, both in the header, and as an item. --- .../{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 f7a3ff5a6..df32e8279 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/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) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index cced4ddb1..762f230c9 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -606,6 +606,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 ';' { @@ -613,8 +614,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)); } ; @@ -622,6 +623,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 ';' { @@ -629,8 +631,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)); } ; @@ -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: diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index 070f9f342..8882163fc 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/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()); } diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index b4e2f3fe5..c7afac3e0 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/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()); diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 0b2b9fe2c..4e23b5e89 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/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()) diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 6d6702f68..b987503e0 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/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())