From 270c8679c4ba3619c549d3d77a6f6d626220e17b Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 19 Jan 2025 10:03:27 -0800
Subject: [PATCH] SVA: allow parentheses around sequences

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

Raised in #931.
---
 regression/verilog/SVA/sequence6.desc | 10 ++++++++++
 regression/verilog/SVA/sequence6.sv   | 14 ++++++++++++++
 src/verilog/parser.y                  | 13 ++++++++++++-
 3 files changed, 36 insertions(+), 1 deletion(-)
 create mode 100644 regression/verilog/SVA/sequence6.desc
 create mode 100644 regression/verilog/SVA/sequence6.sv

diff --git a/regression/verilog/SVA/sequence6.desc b/regression/verilog/SVA/sequence6.desc
new file mode 100644
index 00000000..4b0237a8
--- /dev/null
+++ b/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
+--
+
diff --git a/regression/verilog/SVA/sequence6.sv b/regression/verilog/SVA/sequence6.sv
new file mode 100644
index 00000000..77b933ca
--- /dev/null
+++ b/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
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index 0c451cec..a898a424 100644
--- a/src/verilog/parser.y
+++ b/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