SVA: sequence repetition for proper sequences

The sequence abbreviation operator can be applied to a full sequence, not
just state formulas.  This adds the grammar for this case.

Author: kroening

regression/verilog/SVA/sequence_repetition4.desc

@@ -0,0 +1,10 @@
+CORE
+sequence_repetition4.sv
+
+^\[main\.p0\] main\.x == 0 ##1 main\.x == 1: PROVED up to bound 5
+^\[main\.p1\] main\.x == 0 ##1 main\.x == 1 ##1 0: REFUTED
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sequence_repetition4.sv

@@ -0,0 +1,15 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  // 0 1 0 1 0 1 ...
+  always_ff @(posedge clk)
+    x = x == 0 ? 1 : 0;
+
+  // should pass
+  initial p0: assert property ((x == 0 ##1 x == 1)[*2]);
+
+  // should fail
+  initial p1: assert property ((x == 0 ##1 x == 1 ##1 x == 0)[*2]);
+
+endmodule

src/verilog/parser.y

@@ -2572,6 +2572,11 @@ sequence_expr_proper:
                 { init($$, ID_sva_sequence_concatenation); mto($$, $1); mto($2, $3); mto($$, $2); }
 	| '(' sequence_expr_proper ')'
 		{ $$ = $2; }
+	| '(' sequence_expr_proper ')' sequence_abbrev
+		{ $$ = $4;
+		  // preserve the operand ordering as in the source code
+		  stack_expr($$).operands().insert(stack_expr($$).operands().begin(), stack_expr($2));
+		}
 	| expression_or_dist boolean_abbrev
 		{ $$ = $2;
 		  // preserve the operand ordering as in the source code