SVA: allow parentheses around sequences

This allows the use of parentheses ( ... ) in sequences.

Raised in #931.

Author: kroening

regression/verilog/SVA/sequence6.desc

@@ -0,0 +1,10 @@
+CORE
+sequence6.sv
+
+^\[main\.p0\] \(1 ##1 1\) \|-> main\.x == 1: PROVED up to bound 5$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+

regression/verilog/SVA/sequence6.sv

@@ -0,0 +1,14 @@
+module main;
+
+  reg [31:0] x;
+  wire clk;
+
+  initial x=0;
+
+  always @(posedge clk)
+    x<=x+1;
+
+  // passes
+  initial p0: assert property ((1 ##1 1) |-> x==1);
+
+endmodule

src/verilog/parser.y

@@ -2555,12 +2555,23 @@ expression_or_dist_brace:
 		{ $$ = $1; mto($1, $3); }
 	;
 
+// The 1800-2017 grammar has an ambiguity where
+// '(' expression ')' can either be an expression or a sequence_expr,
+// which yields a reduce/reduce conflict. Hence, we split the rules
+// for sequence_expr into sequence_expr and sequence_expr_proper.
+
 sequence_expr:
+	  expression_or_dist
+	| sequence_expr_proper
+	;
+
+sequence_expr_proper:
 	  cycle_delay_range sequence_expr %prec "##"
 		{ $$=$1; mto($$, $2); }
         | sequence_expr cycle_delay_range sequence_expr %prec "##"
                 { init($$, ID_sva_sequence_concatenation); mto($$, $1); mto($2, $3); mto($$, $2); }
-	| expression_or_dist
+	| '(' sequence_expr_proper ')'
+		{ $$ = $2; }
 	| expression_or_dist boolean_abbrev
 		{ $$ = $2;
 		  // preserve the operand ordering as in the source code