Skip to content

Commit

Permalink
SVA: add grammar for sequence_match_item
Browse files Browse the repository at this point in the history
This adds the grammar rules for the first_match operator with sequence match
items.  The operator is still unsupported.
  • Loading branch information
kroening committed Oct 13, 2024
1 parent 2399b56 commit 7bb9139
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 0 deletions.
3 changes: 3 additions & 0 deletions regression/verilog/SVA/sequence_first_match1.sv
Original file line number Diff line number Diff line change
Expand Up @@ -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
13 changes: 13 additions & 0 deletions src/verilog/parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 7bb9139

Please sign in to comment.