From 38a788067c979acdf10e41a5a145700c2f38cc48 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 21 Jan 2025 13:59:25 -0800
Subject: [PATCH] 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.

This also fixes a bug in the lowering of the consecutive sequence repetition
operator, exposed by the change above.
---
 regression/verilog/SVA/sequence_repetition4.desc | 10 ++++++++++
 regression/verilog/SVA/sequence_repetition4.sv   | 15 +++++++++++++++
 src/verilog/parser.y                             |  5 +++++
 src/verilog/sva_expr.cpp                         |  2 +-
 4 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 regression/verilog/SVA/sequence_repetition4.desc
 create mode 100644 regression/verilog/SVA/sequence_repetition4.sv

diff --git a/regression/verilog/SVA/sequence_repetition4.desc b/regression/verilog/SVA/sequence_repetition4.desc
new file mode 100644
index 00000000..1fde9112
--- /dev/null
+++ b/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
+--
diff --git a/regression/verilog/SVA/sequence_repetition4.sv b/regression/verilog/SVA/sequence_repetition4.sv
new file mode 100644
index 00000000..47cb98ff
--- /dev/null
+++ b/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
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index a898a424..e2c256e0 100644
--- a/src/verilog/parser.y
+++ b/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
diff --git a/src/verilog/sva_expr.cpp b/src/verilog/sva_expr.cpp
index 5911c55c..b1aad1d8 100644
--- a/src/verilog/sva_expr.cpp
+++ b/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;