Merge pull request #944 from diffblue/sequence_repetition4

SVA: sequence repetition for proper sequences

Author: tautschnig

regression/verilog/SVA/sequence_repetition4.desc

@@ -0,0 +1,10 @@
+CORE
+sequence_repetition4.sv
+
+^\[main\.p0\] \(main\.x == 0 ##1 main\.x == 1\) \[\*2\]: PROVED up to bound \d+$
+^\[main\.p1\] \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 0\) \[\*2\]: 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

src/verilog/sva_expr.cpp

@@ -51,7 +51,7 @@ exprt sva_sequence_consecutive_repetition_exprt::lower() const
     auto cycle_delay =
       sva_cycle_delay_exprt{from_integer(1, integer_typet{}), lhs()};
     result = sva_sequence_concatenation_exprt{
-      std::move(cycle_delay), std::move(result)};
+      std::move(result), std::move(cycle_delay)};
   }
 
   return result;