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