SystemVerilog: final immediate assertions

This adds SystemVerilog final immediate assertions.

Author: kroening

regression/verilog/SVA/immediate3.desc

@@ -0,0 +1,9 @@
+CORE
+immediate3.sv
+--bound 0
+^\[full_adder\.assert\.1\] always \(\{ full_adder\.carry, full_adder\.sum \}\) == full_adder\.a \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/immediate3.sv

@@ -0,0 +1,9 @@
+module full_adder(input a, b, c, output sum, carry);
+
+  assign sum = a ^ b ^ c;
+  assign carry = a & b | (a ^ b) & c;
+
+  always @(*)
+    assert final({carry, sum} == a + b + c);
+
+endmodule

src/verilog/parser.y

@@ -3099,6 +3099,13 @@ statement_brace:
 
 assertion_item:
 	  concurrent_assertion_item
+	| deferred_immediate_assertion_item
+	;
+
+deferred_immediate_assertion_item:
+	  deferred_immediate_assertion_statement
+	| block_identifier TOK_COLON deferred_immediate_assertion_statement
+		{ $$ = $3; }
 	;
 
 procedural_assertion_statement:
@@ -3110,6 +3117,7 @@ procedural_assertion_statement:
 
 immediate_assertion_statement:
 	  simple_immediate_assertion_statement
+	| deferred_immediate_assertion_statement
 	;
 
 simple_immediate_assertion_statement:
@@ -3130,6 +3138,27 @@ simple_immediate_cover_statement: TOK_COVER '(' expression ')' action_block
 		{ init($$, ID_verilog_immediate_cover); mto($$, $3); mto($$, $5); }
 	;
 
+deferred_immediate_assertion_statement:
+	  deferred_immediate_assert_statement
+	| deferred_immediate_assume_statement
+	| deferred_immediate_cover_statement
+	;
+
+deferred_immediate_assert_statement:
+	  TOK_ASSERT TOK_FINAL '(' expression ')' action_block
+		{ init($$, ID_verilog_immediate_assert); mto($$, $4); mto($$, $6); }
+	;
+
+deferred_immediate_assume_statement:
+	  TOK_ASSUME TOK_FINAL '(' expression ')' action_block
+		{ init($$, ID_verilog_immediate_assume); mto($$, $4); mto($$, $6); }
+	;
+
+deferred_immediate_cover_statement:
+	  TOK_COVER TOK_FINAL '(' expression ')' statement_or_null
+		{ init($$, ID_verilog_immediate_cover); mto($$, $4); mto($$, $6); }
+	;
+
 wait_statement: TOK_WAIT '(' expression ')' statement_or_null
 		{ init($$, ID_wait); mto($$, $3); mto($$, $5); }
 	;