diff --git a/regression/verilog/SVA/sequence_repetition4.desc b/regression/verilog/SVA/sequence_repetition4.desc new file mode 100644 index 00000000..dc95666f --- /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: PROVED up to bound 5 +^\[main\.p1\] main\.x == 0 ##1 main\.x == 1 ##1 0: 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