From 3a3a57695fa611f044ea99b01810065dc75094d4 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 10 Jan 2025 16:09:18 -0800 Subject: [PATCH] SystemVerilog: package scope operator This adds the SystemVerilog package scope operator ::. --- CHANGELOG | 1 + regression/verilog/packages/package2.desc | 7 ++++ regression/verilog/packages/package2.sv | 15 +++++++ src/hw_cbmc_irep_ids.h | 1 + src/verilog/parser.y | 15 ++++++- src/verilog/verilog_expr.cpp | 8 ++++ src/verilog/verilog_language.cpp | 2 +- src/verilog/verilog_parse_tree.cpp | 7 ++++ src/verilog/verilog_parse_tree.h | 2 +- src/verilog/verilog_typecheck.cpp | 48 ++++++----------------- src/verilog/verilog_typecheck.h | 12 +----- src/verilog/verilog_typecheck_base.cpp | 23 ++++++++++- src/verilog/verilog_typecheck_base.h | 3 +- src/verilog/verilog_typecheck_expr.cpp | 28 +++++++++++++ 14 files changed, 119 insertions(+), 53 deletions(-) create mode 100644 regression/verilog/packages/package2.desc create mode 100644 regression/verilog/packages/package2.sv diff --git a/CHANGELOG b/CHANGELOG index 0f4f3e15..5a57c209 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -9,6 +9,7 @@ * SystemVerilog: $bitstoreal/$bitstoshortreal, $realtobits/$shortrealtobits * SystemVerilog: $itor, $rtoi * SystemVerilog: chandle, event +* SystemVerilog: package scope operator # EBMC 5.4 diff --git a/regression/verilog/packages/package2.desc b/regression/verilog/packages/package2.desc new file mode 100644 index 00000000..e2d2ae35 --- /dev/null +++ b/regression/verilog/packages/package2.desc @@ -0,0 +1,7 @@ +CORE +package2.sv + +^^\[.*\] always main\.Q == 123: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/packages/package2.sv b/regression/verilog/packages/package2.sv new file mode 100644 index 00000000..39a465df --- /dev/null +++ b/regression/verilog/packages/package2.sv @@ -0,0 +1,15 @@ +package moo; + + parameter P = 123; + +endpackage + +module main; + + import moo::*; + + parameter Q = moo::P; + + assert final (Q == 123); + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 5ece86e0..30acfbb4 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -250,6 +250,7 @@ IREP_ID_ONE(verilog_class) IREP_ID_ONE(verilog_module) IREP_ID_ONE(verilog_package) IREP_ID_ONE(verilog_package_import) +IREP_ID_ONE(verilog_package_scope) IREP_ID_ONE(verilog_program) IREP_ID_ONE(verilog_udp) IREP_ID_ONE(module_source) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 7466356b..e1f5d2fc 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -1355,9 +1355,13 @@ package_import_item_brace: package_import_item: package_identifier "::" identifier - { init($$, ID_verilog_import_item); mto($$, $1); mto($$, $3); } + { init($$, ID_verilog_import_item); + stack_expr($$).set(ID_verilog_package, stack_expr($1).id()); + stack_expr($$).set(ID_identifier, stack_expr($3).id()); } | package_identifier "::" "*" - { init($$, ID_verilog_import_item); mto($$, $1); } + { init($$, ID_verilog_import_item); + stack_expr($$).set(ID_verilog_package, stack_expr($1).id()); + stack_expr($$).set(ID_identifier, "*"); } ; genvar_declaration: @@ -4032,6 +4036,10 @@ part_select_range: primary: primary_literal | hierarchical_identifier_select + | package_scope hierarchical_identifier_select + { init($$, ID_verilog_package_scope); + mto($$, $1); + mto($$, $2); } | concatenation | multiple_concatenation | function_subroutine_call @@ -4209,6 +4217,9 @@ net_identifier: identifier; package_identifier: TOK_NON_TYPE_IDENTIFIER; +package_scope: package_identifier "::" + ; + param_identifier: TOK_NON_TYPE_IDENTIFIER; port_identifier: identifier; diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp index 9d3aebbf..56edaa5d 100644 --- a/src/verilog/verilog_expr.cpp +++ b/src/verilog/verilog_expr.cpp @@ -100,6 +100,14 @@ static void dependencies_rec( { dependencies_rec(to_verilog_generate_for(module_item).body(), dest); } + else if(module_item.id() == ID_verilog_package_import) + { + for(auto &import_item : module_item.get_sub()) + { + dest.push_back( + verilog_package_identifier(import_item.get(ID_verilog_package))); + } + } } std::vector verilog_item_containert::dependencies() const diff --git a/src/verilog/verilog_language.cpp b/src/verilog/verilog_language.cpp index 74aa2c8a..fc6b277c 100644 --- a/src/verilog/verilog_language.cpp +++ b/src/verilog/verilog_language.cpp @@ -132,7 +132,7 @@ void verilog_languaget::dependencies( std::set &dependency_set) { verilog_parse_treet::item_mapt::const_iterator it = - parse_tree.item_map.find(id2string(verilog_module_name(module))); + parse_tree.item_map.find(id2string(verilog_item_key(module))); if(it != parse_tree.item_map.end()) { diff --git a/src/verilog/verilog_parse_tree.cpp b/src/verilog/verilog_parse_tree.cpp index d4bcb6d4..93df40db 100644 --- a/src/verilog/verilog_parse_tree.cpp +++ b/src/verilog/verilog_parse_tree.cpp @@ -62,8 +62,15 @@ void verilog_parse_treet::modules_provided( for(auto &item : items) { if(item.id() == ID_verilog_module) + { module_set.insert(id2string( verilog_module_symbol(to_verilog_module_source(item).base_name()))); + } + else if(item.id() == ID_verilog_package) + { + module_set.insert(id2string(verilog_package_identifier( + to_verilog_module_source(item).base_name()))); + } } } diff --git a/src/verilog/verilog_parse_tree.h b/src/verilog/verilog_parse_tree.h index db40d634..298a3920 100644 --- a/src/verilog/verilog_parse_tree.h +++ b/src/verilog/verilog_parse_tree.h @@ -75,7 +75,7 @@ class verilog_parse_treet // An index into the items list. // The key is - // package::name for pagages + // package::name for packages // name for modules, etc. // as packages have a separate name space (1800-2017 3.13). typedef std:: diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index e61b46a4..21495841 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1947,55 +1947,27 @@ Function: verilog_typecheck bool verilog_typecheck( const verilog_parse_treet &parse_tree, symbol_table_baset &symbol_table, - const std::string &module, + const irep_idt &module_identifier, bool warn_implicit_nets, message_handlert &message_handler) { verilog_parse_treet::item_mapt::const_iterator it = - parse_tree.item_map.find(id2string(verilog_module_name(module))); + parse_tree.item_map.find(id2string(verilog_item_key(module_identifier))); if(it == parse_tree.item_map.end()) { messaget message(message_handler); - message.error() << "module `" << module - << "' not found" << messaget::eom; + message.error() << "module `" << module_identifier << "' not found" + << messaget::eom; return true; } - auto &module_source = to_verilog_module_source(*it->second); - - return verilog_typecheck( - symbol_table, - module_source, - parse_tree.standard, - warn_implicit_nets, - message_handler); -} - -/*******************************************************************\ - -Function: verilog_typecheck - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bool verilog_typecheck( - symbol_table_baset &symbol_table, - const verilog_module_sourcet &verilog_module_source, - verilog_standardt standard, - bool warn_implicit_nets, - message_handlert &message_handler) -{ - // create symbol + auto &verilog_module_source = to_verilog_module_source(*it->second); + // create the symbol irep_idt base_name = verilog_module_source.base_name(); - symbolt symbol{verilog_module_symbol(base_name), module_typet{}, ID_Verilog}; + symbolt symbol{module_identifier, module_typet{}, ID_Verilog}; symbol.base_name = base_name; symbol.pretty_name = base_name; @@ -2017,7 +1989,11 @@ bool verilog_typecheck( } verilog_typecheckt verilog_typecheck( - standard, warn_implicit_nets, *new_symbol, symbol_table, message_handler); + parse_tree.standard, + warn_implicit_nets, + *new_symbol, + symbol_table, + message_handler); return verilog_typecheck.typecheck_main(); } diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h index 0edfac7d..007357d3 100644 --- a/src/verilog/verilog_typecheck.h +++ b/src/verilog/verilog_typecheck.h @@ -22,21 +22,13 @@ Author: Daniel Kroening, kroening@kroening.com bool verilog_typecheck( const verilog_parse_treet &parse_tree, symbol_table_baset &, - const std::string &module, + const irep_idt &module_identifier, bool warn_implicit_nets, message_handlert &message_handler); bool verilog_typecheck( symbol_table_baset &, - const verilog_module_sourcet &verilog_module_source, - verilog_standardt, - bool warn_implicit_nets, - message_handlert &message_handler); - -bool verilog_typecheck( - symbol_table_baset &, - const std::string &module_identifier, - verilog_standardt, + const irep_idt &module_identifier, const exprt::operandst ¶meters, message_handlert &message_handler); diff --git a/src/verilog/verilog_typecheck_base.cpp b/src/verilog/verilog_typecheck_base.cpp index 62bf9b98..b8dc7eb9 100644 --- a/src/verilog/verilog_typecheck_base.cpp +++ b/src/verilog/verilog_typecheck_base.cpp @@ -36,6 +36,25 @@ irep_idt verilog_module_symbol(const irep_idt &base_name) /*******************************************************************\ +Function: verilog_package_identifier + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +irep_idt verilog_package_identifier(const irep_idt &base_name) +{ + // Packages and modules have separate name spaces, + // hence the prefix. + return "Verilog::package::" + id2string(base_name); +} + +/*******************************************************************\ + Function: strip_verilog_prefix Inputs: @@ -58,7 +77,7 @@ irep_idt strip_verilog_prefix(const irep_idt &identifier) /*******************************************************************\ -Function: verilog_module_name +Function: verilog_item_key Inputs: @@ -68,7 +87,7 @@ Function: verilog_module_name \*******************************************************************/ -irep_idt verilog_module_name(const irep_idt &identifier) +irep_idt verilog_item_key(const irep_idt &identifier) { return strip_verilog_prefix(identifier); } diff --git a/src/verilog/verilog_typecheck_base.h b/src/verilog/verilog_typecheck_base.h index 91f93c78..dcd93b88 100644 --- a/src/verilog/verilog_typecheck_base.h +++ b/src/verilog/verilog_typecheck_base.h @@ -17,7 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "verilog_standard.h" irep_idt verilog_module_symbol(const irep_idt &base_name); -irep_idt verilog_module_name(const irep_idt &identifier); +irep_idt verilog_package_identifier(const irep_idt &base_name); +irep_idt verilog_item_key(const irep_idt &identifier); irep_idt strip_verilog_prefix(const irep_idt &identifier); class array_typet; diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index c06631f1..8835375b 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2790,6 +2790,34 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) { if(expr.id() == ID_verilog_bit_select) return convert_bit_select_expr(to_binary_expr(expr)); + else if(expr.id() == ID_verilog_package_scope) + { + auto location = expr.source_location(); + + if(expr.rhs().id() != ID_symbol) + throw errort().with_location(location) + << expr.id() << " expects symbol on the rhs"; + + auto package_base = expr.lhs().id(); + auto rhs_base = expr.rhs().get(ID_base_name); + + // stitch together + irep_idt full_identifier = + id2string(verilog_package_identifier(expr.lhs().id())) + '.' + + id2string(rhs_base); + + const symbolt *symbol; + if(ns.lookup(full_identifier, symbol)) + { + throw errort().with_location(location) + << "identifier " << rhs_base << " not found in package " + << package_base; + } + + // found! + return symbol_exprt{full_identifier, symbol->type}.with_source_location( + location); + } else if(expr.id()==ID_replication) return convert_replication_expr(to_replication_expr(expr)); else if(expr.id() == ID_and || expr.id() == ID_or)