Merge pull request #534 from diffblue/assertion-statement-label

Verilog: stick statement label onto `assert`/`assume`/`cover`

Author: tautschnig

regression/verilog/SVA/always_with_range1.desc

@@ -1,9 +1,9 @@
 CORE
 always_with_range1.sv
 --bound 20
-^\[main\.property\.1\] always \[0:9\] main\.x < 10: PROVED up to bound 20$
-^\[main\.property\.2\] always \[0:\$\] main\.x < 10: REFUTED$
-^\[main\.property\.3\] s_always \[0:9\] main\.x < 10: PROVED up to 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$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/cover2.desc

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

regression/verilog/SVA/initial1.desc

@@ -1,11 +1,11 @@
 CORE
 initial1.sv
 --module main --bound 1
-^\[main\.property\.1\] main\.counter == 0: PROVED up to bound 1$
-^\[main\.property\.2\] main\.counter == 100: REFUTED$
-^\[main\.property\.3\] ##1 main\.counter == 1: PROVED up to bound 1$
-^\[main\.property\.4\] ##1 main\.counter == 100: REFUTED$
-^\[main\.property\.5\] s_nexttime main\.counter == 1: PROVED up to 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$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/initial1.sv

@@ -21,9 +21,9 @@ module main(input clk);
   initial p2: assert property (##1 counter == 1);
 
   // expected to fail
-  initial p2: assert property (##1 counter == 100);
+  initial p3: assert property (##1 counter == 100);
 
   // expected to pass if there are timeframes 0 and 1
-  initial p3: assert property (s_nexttime counter == 1);
+  initial p4: assert property (s_nexttime counter == 1);
 
 endmodule

regression/verilog/SVA/sequence1.desc

@@ -1,7 +1,7 @@
 CORE
 sequence1.sv
 --bound 20 --numbered-trace
-^\[main\.property\.1\] ##\[0:9\] main\.x == 100: REFUTED$
+^\[main\.property\.p0\] ##\[0:9\] main\.x == 100: REFUTED$
 ^Counterexample with 10 states:$
 ^main\.x@0 = 0$
 ^main\.x@9 = 9$

regression/verilog/SVA/sequence2.desc

@@ -1,7 +1,7 @@
 CORE
 sequence2.sv
 --bound 10 --numbered-trace
-^\[main\.property\.1] ##\[0:\$\] main\.x == 10: REFUTED$
+^\[main\.property\.p0] ##\[0:\$\] main\.x == 10: REFUTED$
 ^Counterexample with 7 states:$
 ^main\.x@0 = 0$
 ^main\.x@1 = 1$

regression/verilog/SVA/sequence3.desc

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

src/verilog/verilog_typecheck.cpp

@@ -1481,7 +1481,21 @@ void verilog_typecheckt::convert_statement(
   else if(statement.id()==ID_force)
     convert_force(to_verilog_force(statement));
   else if(statement.id() == ID_verilog_label_statement)
-    convert_statement(to_verilog_label_statement(statement).statement());
+  {
+    // We stick the label on any assert/assume/conver statement
+    auto &label_statement = to_verilog_label_statement(statement);
+    auto &sub_statement = label_statement.statement();
+
+    if(
+      sub_statement.id() == ID_verilog_assert_property ||
+      sub_statement.id() == ID_verilog_assume_property ||
+      sub_statement.id() == ID_verilog_cover_property)
+    {
+      sub_statement.set(ID_identifier, label_statement.label());
+    }
+
+    convert_statement(sub_statement);
+  }
   else if(statement.id() == ID_wait)
   {
   }