Merge pull request #768 from diffblue/grammar-sva-implication

SVA: fix grammar for overlapped and nonoverlapped implications

Author: tautschnig

regression/verilog/SVA/system_verilog_assertion4.sv

@@ -20,6 +20,6 @@ module main(input clk);
   p10: assert property (x==0 |-> ##1 x==1 and ##2 x==2);
   p11: assert property (x==0 |-> ##1 x==1 and not ##2 x==3);
   p12: assert property (x==0 |-> ##1 x==1 && y==2);
-  p13: assert property ((x==0 |-> y==0) |=> y != 0);
+  p13: assert property ((x==0 -> y==0) |=> y != 0);
 
 endmodule

src/verilog/parser.y

@@ -2181,9 +2181,9 @@ property_expr_proper:
 		{ init($$, ID_sva_or); mto($$, $1); mto($$, $3); }
 	| property_expr "and" property_expr
 		{ init($$, ID_sva_and); mto($$, $1); mto($$, $3); }
-	| property_expr "|->" property_expr
+	| sequence_expr "|->" property_expr
 		{ init($$, ID_sva_overlapped_implication); mto($$, $1); mto($$, $3); }
-	| property_expr "|=>" property_expr
+	| sequence_expr "|=>" property_expr
 		{ init($$, ID_sva_non_overlapped_implication); mto($$, $1); mto($$, $3); }
 	| "if" '(' expression_or_dist ')' property_expr %prec LT_TOK_ELSE
 		{ init($$, ID_sva_if); mto($$, $3); mto($$, $5); stack_expr($$).add_to_operands(nil_exprt()); }