Merge pull request #238 from diffblue/concurrent-assertion-statement

Concurrent assertion statements

Author: tautschnig

regression/verilog/system_verilog_assertion/initial1.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+initial1.sv
+--module main --bound 1
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Syntax is missing for initial label: assert property (...);

regression/verilog/system_verilog_assertion/initial1.sv

@@ -0,0 +1,20 @@
+module main(input clk);
+
+  // count up from 0 to 10
+  reg [7:0] counter;
+
+  initial counter = 0;
+
+  always @(posedge clk)
+    if(counter == 10)
+      counter = 0;
+    else
+      counter = counter + 1;
+
+  // expected to pass
+  initial p0: assert property (counter == 0);
+
+  // expected to pass if there are timeframes 0 and 1
+  initial p1: assert property (s_nexttime counter == 1);
+
+endmodule

src/verilog/parser.y

@@ -803,10 +803,8 @@ module_or_generate_item:
 	| attribute_instance_brace gate_instantiation { $$=$2; }
 	// | attribute_instance_brace udp_instantiation { $$=$2; }
 	| attribute_instance_brace module_instantiation { $$=$2; }
-	| attribute_instance_brace concurrent_assert_statement { $$=$2; }
-	| attribute_instance_brace concurrent_assume_statement { $$=$2; }
-	| attribute_instance_brace concurrent_cover_statement { $$=$2; }
-	| attribute_instance_brace concurrent_assertion_item_declaration { $$=$2; }
+	| attribute_instance_brace concurrent_assertion_item { $$=$2; }
+	| attribute_instance_brace assertion_item_declaration { $$=$2; }
 	| attribute_instance_brace module_common_item { $$=$2; }
 	;
 
@@ -1535,8 +1533,19 @@ block_item_declaration:
 // System Verilog standard 1800-2017
 // A.2.10 Assertion declarations
 
-concurrent_assertion_item_declaration:
-	  property_declaration
+concurrent_assertion_item:
+          concurrent_assertion_statement
+        | block_identifier TOK_COLON concurrent_assertion_statement
+		{
+		  $$=$3;
+		  stack_expr($$).set(ID_identifier, stack_expr($1).id());
+		}
+	;
+
+concurrent_assertion_statement:
+	  assert_property_statement
+	| assume_property_statement
+	| cover_property_statement
 	;
 
 assert_property_statement:
@@ -1567,6 +1576,10 @@ cover_property_statement: TOK_COVER TOK_PROPERTY '(' expression ')' action_block
 		{ init($$, ID_cover); mto($$, $4); mto($$, $6); }
 	;
 
+assertion_item_declaration:
+	  property_declaration
+	;
+
 property_declaration:
           TOK_PROPERTY property_identifier TOK_ENDPROPERTY
         ;
@@ -2074,6 +2087,40 @@ always_construct: TOK_ALWAYS statement
 		{ init($$, ID_always); mto($$, $2); }
 	;
 
+blocking_assignment:
+	  variable_lvalue '=' delay_or_event_control expression
+		{ init($$, ID_blocking_assign); mto($$, $1); mto($$, $4); }
+        | operator_assignment
+	;
+
+operator_assignment:
+          variable_lvalue assignment_operator expression
+		{ init($$, ID_blocking_assign); mto($$, $1); mto($$, $3); }
+        ;
+
+assignment_operator:
+          '='
+        | TOK_PLUSEQUAL
+        | TOK_MINUSEQUAL
+        | TOK_ASTERICEQUAL
+        | TOK_SLASHEQUAL
+        | TOK_PERCENTEQUAL
+        | TOK_AMPEREQUAL
+        | TOK_VERTBAREQUAL
+        | TOK_CARETEQUAL
+        | TOK_LESSLESSEQUAL
+        | TOK_GREATERGREATEREQUAL
+        | TOK_LESSLESSLESSEQUAL
+        | TOK_GREATERGREATERGREATEREQUAL
+        ;
+
+nonblocking_assignment:
+	  variable_lvalue TOK_LESSEQUAL expression
+		{ init($$, ID_non_blocking_assign); mto($$, $1); mto($$, $3); }
+	| variable_lvalue TOK_LESSEQUAL delay_or_event_control expression
+		{ init($$, ID_non_blocking_assign); mto($$, $1); mto($$, $4); }
+	;
+
 // The extra rule to allow block_item_declaration is to avoid an ambiguity
 // caused by the attribute_instance_brace.
 statement: 
@@ -2086,12 +2133,10 @@ statement:
         ;
 
 statement_item:
-          assert_property_statement
-        | assume_property_statement
-        | blocking_assignment ';' { $$ = $1; }
+          blocking_assignment ';' { $$ = $1; }
 	| nonblocking_assignment ';' { $$ = $1; }
 	| case_statement
-	| cover_property_statement
+	| concurrent_assertion_statement
 	| conditional_statement
 	| inc_or_dec_expression ';'
 	| subroutine_call_statement
@@ -2103,7 +2148,7 @@ statement_item:
 	| procedural_continuous_assignments ';'
 	| seq_block
 	| wait_statement
-	| immediate_assert_statement
+	| procedural_assertion_statement
 	;
 
 subroutine_call_statement:
@@ -2333,7 +2378,19 @@ statement_brace:
 // System Verilog standard 1800-2017
 // A.6.10 Assertion statements
 
-immediate_assert_statement: TOK_ASSERT '(' expression ')' action_block
+procedural_assertion_statement:
+	  immediate_assertion_statement
+	;
+
+immediate_assertion_statement:
+	  simple_immediate_assertion_statement
+	;
+
+simple_immediate_assertion_statement:
+	  simple_immediate_assert_statement
+	;
+
+simple_immediate_assert_statement: TOK_ASSERT '(' expression ')' action_block
 		{ init($$, ID_assert); mto($$, $3); mto($$, $5); }
 	;
 
@@ -2354,40 +2411,6 @@ procedural_continuous_assignments:
 	/* | TOK_RELEASE net_lvalue */
 	;
 
-blocking_assignment:
-	  variable_lvalue '=' delay_or_event_control expression
-		{ init($$, ID_blocking_assign); mto($$, $1); mto($$, $4); }
-        | operator_assignment
-	;
-	
-operator_assignment:
-          variable_lvalue assignment_operator expression
-		{ init($$, ID_blocking_assign); mto($$, $1); mto($$, $3); }
-        ;
-
-assignment_operator:
-          '='
-        | TOK_PLUSEQUAL
-        | TOK_MINUSEQUAL
-        | TOK_ASTERICEQUAL
-        | TOK_SLASHEQUAL
-        | TOK_PERCENTEQUAL
-        | TOK_AMPEREQUAL
-        | TOK_VERTBAREQUAL
-        | TOK_CARETEQUAL
-        | TOK_LESSLESSEQUAL
-        | TOK_GREATERGREATEREQUAL
-        | TOK_LESSLESSLESSEQUAL
-        | TOK_GREATERGREATERGREATEREQUAL
-        ;
-
-nonblocking_assignment:
-	  variable_lvalue TOK_LESSEQUAL expression
-		{ init($$, ID_non_blocking_assign); mto($$, $1); mto($$, $3); }
-	| variable_lvalue TOK_LESSEQUAL delay_or_event_control expression
-		{ init($$, ID_non_blocking_assign); mto($$, $1); mto($$, $4); }
-	;
-
 procedural_timing_control_statement:
           procedural_timing_control statement_or_null
 		{ $$=$1; mto($$, $2); }