From 7bb9139abe3a1a54ddb84e0ebc181f4d5d6d6260 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 13 Oct 2024 11:07:22 -0700 Subject: [PATCH] SVA: add grammar for sequence_match_item This adds the grammar rules for the first_match operator with sequence match items. The operator is still unsupported. --- regression/verilog/SVA/sequence_first_match1.sv | 3 +++ src/verilog/parser.y | 13 +++++++++++++ 2 files changed, 16 insertions(+) diff --git a/regression/verilog/SVA/sequence_first_match1.sv b/regression/verilog/SVA/sequence_first_match1.sv index 521c61465..21b3d2ab3 100644 --- a/regression/verilog/SVA/sequence_first_match1.sv +++ b/regression/verilog/SVA/sequence_first_match1.sv @@ -7,4 +7,7 @@ module main(input clk); initial p0: assert property (first_match(x == 0)); + // can come with sequence_match_items + initial p1: assert property (first_match(x == 0, x++)); + endmodule diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 3954fa089..45adcd7f4 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2271,12 +2271,25 @@ sequence_expr: { init($$, ID_sva_sequence_intersect); mto($$, $1); mto($$, $3); } | "first_match" '(' sequence_expr ')' { init($$, ID_sva_sequence_first_match); mto($$, $3); } + | "first_match" '(' sequence_expr ',' sequence_match_item_brace ')' + { init($$, ID_sva_sequence_first_match); mto($$, $3); mto($$, $5); } | expression "throughout" sequence_expr { init($$, ID_sva_sequence_throughout); mto($$, $1); mto($$, $3); } | expression "within" sequence_expr { init($$, ID_sva_sequence_within); mto($$, $1); mto($$, $3); } ; +sequence_match_item_brace: + sequence_match_item + | sequence_match_item_brace ',' sequence_match_item + ; + +sequence_match_item: + operator_assignment + | inc_or_dec_expression + | subroutine_call + ; + boolean_abbrev: consecutive_repetition | non_consecutive_repetition