Skip to content

Commit

Permalink
SVA: allow parentheses around sequences
Browse files Browse the repository at this point in the history
This allows the use of parentheses ( ... ) in sequences.

Raised in #931.
  • Loading branch information
kroening committed Jan 19, 2025
1 parent f6c38d9 commit 270c867
Show file tree
Hide file tree
Showing 3 changed files with 36 additions and 1 deletion.
10 changes: 10 additions & 0 deletions regression/verilog/SVA/sequence6.desc
Original file line number Diff line number Diff line change
@@ -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
--

14 changes: 14 additions & 0 deletions regression/verilog/SVA/sequence6.sv
Original file line number Diff line number Diff line change
@@ -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
13 changes: 12 additions & 1 deletion src/verilog/parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 270c867

Please sign in to comment.