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.

Author: kroening

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);
 		}

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 &

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);