SystemVerilog: assertion statements use hierarchical identifiers

Assertion statements with a block label have regular hierarchical identifiers, and do not use a separate "property" name space. The behavior for SMV-style assertion statements is unchanged. Assertion statements without block item now get a label based on the kind of the assertion item (assert/assume/cover).
diffblue · Jun 23, 2024 · 840b233 · 840b233
1 parent 459b5f8
commit 840b233
Show file tree

Hide file tree

Showing 13 changed files with 43 additions and 27 deletions.
diff --git a/regression/verilog/Memory2/test.desc b/regression/verilog/Memory2/test.desc
@@ -3,6 +3,6 @@ main.v
 --module main --bound 1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.property.property1\] .* PROVED up to bound 1$
+^\[main\.property\.property1\] .* PROVED up to bound 1$
 --
 ^warning: ignoring
diff --git a/regression/verilog/SVA/always_with_range1.desc b/regression/verilog/SVA/always_with_range1.desc
@@ -1,9 +1,9 @@
 CORE
 always_with_range1.sv
 --bound 20
-^\[main\.property\.p0\] always \[0:9\] main\.x < 10: PROVED up to bound 20$
-^\[main\.property\.p1\] always \[0:\$\] main\.x < 10: REFUTED$
-^\[main\.property\.p2\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$
+^\[main\.p0\] always \[0:9\] main\.x < 10: PROVED up to bound 20$
+^\[main\.p1\] always \[0:\$\] main\.x < 10: REFUTED$
+^\[main\.p2\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$
 ^EXIT=10$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/SVA/cover2.desc b/regression/verilog/SVA/cover2.desc
@@ -1,11 +1,11 @@
 CORE
 cover2.sv
 --bound 10 --numbered-trace
-^\[main\.property\.p0\] cover main\.counter == 1: PROVED$
+^\[main\.p0\] cover main\.counter == 1: PROVED$
 ^Trace with 2 states:$
 ^main\.counter@0 = 0$
 ^main\.counter@1 = 1$
-^\[main\.property\.p1\] cover main\.counter == 100: REFUTED up to bound 10$
+^\[main\.p1\] cover main\.counter == 100: REFUTED up to bound 10$
 ^EXIT=10$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/SVA/immediate2.desc b/regression/verilog/SVA/immediate2.desc
@@ -1,9 +1,9 @@
 CORE broken-smt-backend
 immediate2.sv
 --bound 0
-^\[main\.property\.1\] assume always \(main\.index >= 10 |-> 0\): ASSUMED$
-^\[main\.property\.2\] always main\.index < 10: PROVED up to bound 0$
-^\[main\.property\.3\] always 0: REFUTED$
+^\[main\.assert\.1\] assume always \(main\.index >= 10 |-> 0\): ASSUMED$
+^\[main\.assert\.2\] always main\.index < 10: PROVED up to bound 0$
+^\[main\.assert\.3\] always 0: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/SVA/initial1.desc b/regression/verilog/SVA/initial1.desc
@@ -1,11 +1,11 @@
 CORE
 initial1.sv
 --module main --bound 1
-^\[main\.property\.p0\] main\.counter == 0: PROVED up to bound 1$
-^\[main\.property\.p1\] main\.counter == 100: REFUTED$
-^\[main\.property\.p2\] ##1 main\.counter == 1: PROVED up to bound 1$
-^\[main\.property\.p3\] ##1 main\.counter == 100: REFUTED$
-^\[main\.property\.p4\] s_nexttime main\.counter == 1: PROVED up to bound 1$
+^\[main\.p0\] main\.counter == 0: PROVED up to bound 1$
+^\[main\.p1\] main\.counter == 100: REFUTED$
+^\[main\.p2\] ##1 main\.counter == 1: PROVED up to bound 1$
+^\[main\.p3\] ##1 main\.counter == 100: REFUTED$
+^\[main\.p4\] s_nexttime main\.counter == 1: PROVED up to bound 1$
 ^EXIT=10$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/SVA/initial2.desc b/regression/verilog/SVA/initial2.desc
@@ -1,8 +1,8 @@
 CORE
 initial2.sv
 --module main --bound 1
-^\[main\.property\.1\] 1 == 1: PROVED up to bound 1
-^\[main\.property\.2\] main\.counter == 2: PROVED up to bound 1
+^\[main\.assert\.1\] 1 == 1: PROVED up to bound 1
+^\[main\.assert\.2\] main\.counter == 2: PROVED up to bound 1
 ^EXIT=0$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/SVA/sequence1.desc b/regression/verilog/SVA/sequence1.desc
@@ -1,7 +1,7 @@
 CORE
 sequence1.sv
 --bound 20 --numbered-trace
-^\[main\.property\.p0\] ##\[0:9\] main\.x == 100: REFUTED$
+^\[main\.p0\] ##\[0:9\] main\.x == 100: REFUTED$
 ^Counterexample with 10 states:$
 ^main\.x@0 = 0$
 ^main\.x@9 = 9$

diff --git a/regression/verilog/SVA/sequence2.desc b/regression/verilog/SVA/sequence2.desc
@@ -1,7 +1,7 @@
 CORE
 sequence2.sv
 --bound 10 --numbered-trace
-^\[main\.property\.p0] ##\[0:\$\] main\.x == 10: REFUTED$
+^\[main\.p0] ##\[0:\$\] main\.x == 10: REFUTED$
 ^Counterexample with 7 states:$
 ^main\.x@0 = 0$
 ^main\.x@1 = 1$

diff --git a/regression/verilog/SVA/sequence3.desc b/regression/verilog/SVA/sequence3.desc
@@ -1,9 +1,9 @@
 CORE
 sequence3.sv
 --bound 20 --numbered-trace
-^\[main\.property\.p0\] ##\[\*\] main\.x == 6: REFUTED$
+^\[main\.p0\] ##\[\*\] main\.x == 6: REFUTED$
 ^Counterexample with 2 states:$
-^\[main\.property\.p1\] ##\[\+\] main\.x == 0: REFUTED$
+^\[main\.p1\] ##\[\+\] main\.x == 0: REFUTED$
 ^Counterexample with 7 states:$
 ^EXIT=10$
 ^SIGNAL=0$

diff --git a/regression/verilog/SVA/sequence_followed_by1.desc b/regression/verilog/SVA/sequence_followed_by1.desc
@@ -1,8 +1,8 @@
 CORE
 sequence_followed_by1.sv
 --bound 20 --numbered-trace
-^\[main\.property\.p0\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): FAILURE: property not supported by BMC engine$
-^\[main\.property\.p1\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): FAILURE: property not supported by BMC engine$
+^\[main\.p0\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): FAILURE: property not supported by BMC engine$
+^\[main\.p1\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): FAILURE: property not supported by BMC engine$
 ^EXIT=10$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/SVA/strong1.desc b/regression/verilog/SVA/strong1.desc
@@ -1,7 +1,7 @@
 CORE
 strong1.sv
 --bound 20
-^\[main\.property\.p0\] strong\(##\[0:9\] main\.x == 100\): REFUTED$
+^\[main\.p0\] strong\(##\[0:9\] main\.x == 100\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/SVA/weak1.desc b/regression/verilog/SVA/weak1.desc
@@ -1,7 +1,7 @@
 CORE
 weak1.sv
 --bound 20
-^\[main\.property\.p0\] weak\(##\[0:9\] main\.x == 100\): REFUTED$
+^\[main\.p0\] weak\(##\[0:9\] main\.x == 100\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp
@@ -1082,14 +1082,30 @@ void verilog_typecheckt::convert_assert_assume_cover(
 
   if(identifier == irep_idt())
   {
+    std::string kind = statement.id() == ID_verilog_immediate_assert  ? "assert"
+                       : statement.id() == ID_verilog_assert_property ? "assert"
+                       : statement.id() == ID_verilog_smv_assert      ? "assert"
+                       : statement.id() == ID_verilog_cover_property  ? "cover"
+                       : statement.id() == ID_verilog_immediate_assume
+                         ? "assume"
+                       : statement.id() == ID_verilog_assume_property ? "assume"
+                       : statement.id() == ID_verilog_smv_assume      ? "assume"
+                                                                      : "";
+
     assertion_counter++;
-    base_name = std::to_string(assertion_counter);
+    base_name = kind + "." + std::to_string(assertion_counter);
   }
   else
     base_name = identifier;
 
-  std::string full_identifier =
-    id2string(module_identifier) + ".property." + id2string(base_name);
+  // We produce a full hierarchical identifier for the SystemVerilog immediate
+  // and concurrent assertion statements.
+  // We produce a separate name space for the SMV assertions/assumptions.
+  auto full_identifier =
+    statement.id() == ID_verilog_smv_assert ||
+        statement.id() == ID_verilog_smv_assume
+      ? id2string(module_identifier) + ".property." + id2string(base_name)
+      : hierarchical_identifier(base_name);
 
   if(symbol_table.symbols.find(full_identifier) != symbol_table.symbols.end())
   {