Merge pull request #1353 from diffblue/label-immediate-assertions

SystemVerilog: labeled immediate assert/assume/cover statements

Author: tautschnig

CHANGELOG

@@ -2,6 +2,7 @@
 
 * Verilog: semantic fix for output register ports
 * SystemVerilog: cover sequence
+* SystemVerilog: labeled immediate assert/assume/cover statements
 * SystemVerilog: semantics fix for explicit casts
 
 # EBMC 5.7

regression/ebmc-spot/sva-buechi/initial2.bmc.desc

@@ -1,8 +1,8 @@
 CORE
 ../../verilog/SVA/initial2.sv
 --buechi --module main
-^\[main\.assert\.1\] main\.counter == 1: PROVED \(1-induction\)$
-^\[main\.assert\.2\] main\.counter == 2: PROVED \(1-induction\)$
+^\[main\.p0\] main\.counter == 1: PROVED \(1-induction\)$
+^\[main\.p1\] main\.counter == 2: PROVED \(1-induction\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc-spot/sva-buechi/initial2.k.desc

@@ -1,8 +1,8 @@
 CORE
 ../../verilog/SVA/initial2.sv
 --buechi --k-induction --bound 1 --module main
-^\[main\.assert\.1\] main\.counter == 1: PROVED$
-^\[main\.assert\.2\] main\.counter == 2: PROVED$
+^\[main\.p0\] main\.counter == 1: PROVED$
+^\[main\.p1\] main\.counter == 2: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/initial2.desc

@@ -1,8 +1,8 @@
 CORE
 initial2.sv
 --module main
-^\[main\.assert\.1\] main\.counter == 1: PROVED .*$
-^\[main\.assert\.2\] main\.counter == 2: PROVED .*$
+^\[main\.p0\] main\.counter == 1: PROVED .*$
+^\[main\.p1\] main\.counter == 2: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/initial2.sv

@@ -6,12 +6,12 @@ module main(input clk);
   initial begin
     counter = 1;
     // expected to pass
-    assert(counter == 1);
+    p0: assert(counter == 1);
     counter = 2;
   end
 
   // expected to pass
-  initial assert property (counter == 2);
+  initial p1: assert property (counter == 2);
 
   always_ff @(posedge clk)
     counter = counter + 1;

src/verilog/parser.y

@@ -3661,7 +3661,18 @@ statement:
           attribute_instance_brace block_identifier TOK_COLON attribute_instance_brace statement_item
                 { init($$, ID_verilog_label_statement);
                   stack_expr($$).set(ID_base_name, stack_expr($2).id());
-                  mto($$, $5); }
+
+                  // We'll stick the label onto any assertion
+                  auto statement = stack_expr($5).id();
+                  if(statement == ID_verilog_immediate_assert ||
+                     statement == ID_verilog_immediate_assume ||
+                     statement == ID_verilog_immediate_cover)
+                  {
+		    stack_expr($5).set(ID_identifier, stack_expr($2).id());
+		  }
+
+                  mto($$, $5);
+                }
         | attribute_instance_brace statement_item
                 { $$=$2; }
         ;