From b86042bab8e03091204ff877fe69b05777c34176 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 1 Dec 2025 19:31:09 -0800 Subject: [PATCH] SystemVerilog: use base_name instead of identifier for assert/assume/cover Assert/assume/cover statements and module items can have an optional label. The label is now stored as base_name, and not identifier, since it is not qualified. --- src/verilog/parser.y | 14 +++++++------- src/verilog/verilog_expr.h | 16 ++++++++++++++++ src/verilog/verilog_typecheck.cpp | 22 +++++++--------------- 3 files changed, 30 insertions(+), 22 deletions(-) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index fa856ce8d..faf14d36b 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -1505,11 +1505,11 @@ package_import_item: package_identifier "::" identifier { init($$, ID_verilog_import_item); stack_expr($$).set(ID_verilog_package, stack_expr($1).id()); - stack_expr($$).set(ID_identifier, stack_expr($3).id()); } + stack_expr($$).set(ID_base_name, stack_expr($3).id()); } | package_identifier "::" "*" { init($$, ID_verilog_import_item); stack_expr($$).set(ID_verilog_package, stack_expr($1).id()); - stack_expr($$).set(ID_identifier, "*"); } + stack_expr($$).set(ID_base_name, "*"); } ; genvar_declaration: @@ -2417,7 +2417,7 @@ concurrent_assertion_item: | block_identifier TOK_COLON concurrent_assertion_statement { $$=$3; - stack_expr($$).set(ID_identifier, stack_expr($1).id()); + stack_expr($$).set(ID_base_name, stack_expr($1).id()); } ; @@ -2435,13 +2435,13 @@ smv_assertion_statement: { init($$, ID_verilog_smv_assert); stack_expr($$).operands().resize(2); to_binary_expr(stack_expr($$)).op0().swap(stack_expr($4)); to_binary_expr(stack_expr($$)).op1().make_nil(); - stack_expr($$).set(ID_identifier, stack_expr($2).id()); + stack_expr($$).set(ID_base_name, stack_expr($2).id()); } | TOK_ASSUME property_identifier TOK_COLON smv_property ';' { init($$, ID_verilog_smv_assume); stack_expr($$).operands().resize(2); to_binary_expr(stack_expr($$)).op0().swap(stack_expr($4)); to_binary_expr(stack_expr($$)).op1().make_nil(); - stack_expr($$).set(ID_identifier, stack_expr($2).id()); + stack_expr($$).set(ID_base_name, stack_expr($2).id()); } ; @@ -3687,7 +3687,7 @@ statement: statement == ID_verilog_immediate_assume || statement == ID_verilog_immediate_cover) { - stack_expr($5).set(ID_identifier, stack_expr($2).id()); + stack_expr($5).set(ID_base_name, stack_expr($2).id()); } mto($$, $5); @@ -3957,7 +3957,7 @@ deferred_immediate_assertion_item: } | block_identifier TOK_COLON deferred_immediate_assertion_statement { /* wrap the statement into an item */ - stack_expr($3).set(ID_identifier, stack_expr($1).id()); + stack_expr($3).set(ID_base_name, stack_expr($1).id()); init($$, ID_verilog_assertion_item); mto($$, $3); } diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index 558618612..f1b960086 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -2049,6 +2049,7 @@ class verilog_assert_assume_cover_module_itemt : public verilog_module_itemt return op1(); } + // The full identifier created by the type checker const irep_idt &identifier() const { return get(ID_identifier); @@ -2058,6 +2059,11 @@ class verilog_assert_assume_cover_module_itemt : public verilog_module_itemt { set(ID_identifier, identifier); } + + const irep_idt &base_name() const + { + return get(ID_base_name); + } }; inline const verilog_assert_assume_cover_module_itemt & @@ -2119,6 +2125,16 @@ class verilog_assert_assume_cover_statementt : public verilog_statementt { set(ID_identifier, _identifier); } + + const irep_idt &base_name() const + { + return get(ID_base_name); + } + + void base_name(irep_idt _base_name) + { + set(ID_base_name, _base_name); + } }; inline const verilog_assert_assume_cover_statementt & diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 60c74ec5b..cfe6d3880 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1054,12 +1054,10 @@ void verilog_typecheckt::convert_assert_assume_cover( // We create a symbol for the property. // The 'value' of the symbol is set by synthesis. - const irep_idt &identifier = module_item.identifier(); - - irep_idt base_name; + irep_idt base_name = module_item.base_name(); // The label is optional. - if(identifier == irep_idt()) + if(base_name == irep_idt{}) { std::string kind = module_item.id() == ID_verilog_assert_property ? "assert" : module_item.id() == ID_verilog_assume_property @@ -1069,10 +1067,8 @@ void verilog_typecheckt::convert_assert_assume_cover( : ""; assertion_counter++; - base_name = kind + "." + std::to_string(assertion_counter); + base_name = kind + '.' + std::to_string(assertion_counter); } - else - base_name = identifier; // The assert/assume/cover module items use the module name space std::string full_identifier = @@ -1124,11 +1120,9 @@ void verilog_typecheckt::convert_assert_assume_cover( // We create a symbol for the property. // The 'value' is set by synthesis. - const irep_idt &identifier = statement.identifier(); + irep_idt base_name = statement.base_name(); - irep_idt base_name; - - if(identifier == irep_idt()) + if(base_name == irep_idt{}) { std::string kind = statement.id() == ID_verilog_immediate_assert ? "assert" : statement.id() == ID_verilog_assert_property ? "assert" @@ -1142,10 +1136,8 @@ void verilog_typecheckt::convert_assert_assume_cover( : ""; assertion_counter++; - base_name = kind + "." + std::to_string(assertion_counter); + base_name = kind + '.' + std::to_string(assertion_counter); } - else - base_name = identifier; // We produce a full hierarchical identifier for the SystemVerilog immediate // and concurrent assertion statements. @@ -1601,7 +1593,7 @@ void verilog_typecheckt::convert_statement( sub_statement.id() == ID_verilog_cover_sequence || sub_statement.id() == ID_verilog_cover_property) { - sub_statement.set(ID_identifier, label_statement.label()); + sub_statement.set(ID_base_name, label_statement.label()); } convert_statement(sub_statement);