From d20d765dd0215a866ca7c6335870b190b96b51d1 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Thu, 9 Apr 2026 17:42:43 +0200 Subject: [PATCH] Support first_match sequence operator (#7392) --- src/verilog.y | 4 +- test_regress/t/t_sequence_first_match.py | 18 ++++ test_regress/t/t_sequence_first_match.v | 83 +++++++++++++++++++ .../t/t_sequence_first_match_unsup.out | 52 ++++++++++-- test_regress/t/t_sequence_sexpr_unsup.out | 7 +- 5 files changed, 152 insertions(+), 12 deletions(-) create mode 100755 test_regress/t/t_sequence_first_match.py create mode 100644 test_regress/t/t_sequence_first_match.v diff --git a/src/verilog.y b/src/verilog.y index dc5a80c88..5d5cb252a 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6863,9 +6863,9 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg { $$ = new AstSIntersect{$2, $1, $3}; } // | yFIRST_MATCH '(' sexpr ')' - { $$ = $3; BBUNSUP($1, "Unsupported: first_match (in sequence expression)"); } + { $$ = $3; } // IEEE 16.9.8: no-op in deterministic DFA model | yFIRST_MATCH '(' sexpr ',' sequence_match_itemList ')' - { $$ = $3; BBUNSUP($1, "Unsupported: first_match (in sequence expression)"); DEL($5); } + { $$ = $3; BBUNSUP($1, "Unsupported: first_match with sequence_match_items"); DEL($5); } | ~p~sexpr/*sexpression_or_dist*/ yTHROUGHOUT sexpr { $$ = new AstSThroughout{$2, $1, $3}; } // // Below pexpr's are really sequence_expr, but avoid conflict diff --git a/test_regress/t/t_sequence_first_match.py b/test_regress/t/t_sequence_first_match.py new file mode 100755 index 000000000..d93b04ea1 --- /dev/null +++ b/test_regress/t/t_sequence_first_match.py @@ -0,0 +1,18 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# This program is free software; you can redistribute it and/or modify it +# under the terms of either the GNU Lesser General Public License Version 3 +# or the Perl Artistic License Version 2.0. +# SPDX-FileCopyrightText: 2026 Wilson Snyder +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +import vltest_bootstrap + +test.scenarios('simulator') + +test.compile(verilator_flags2=['--assert']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_sequence_first_match.v b/test_regress/t/t_sequence_first_match.v new file mode 100644 index 000000000..95290de21 --- /dev/null +++ b/test_regress/t/t_sequence_first_match.v @@ -0,0 +1,83 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`define stop $stop +`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0x exp=%0x (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0); +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + + int cyc; + reg [63:0] crc; + + // Derive signals from non-adjacent CRC bits (avoid shift correlation) + wire a = crc[0]; + wire b = crc[4]; + wire c = crc[8]; + wire d = crc[12]; + + int count_fail1 = 0; + int count_fail2 = 0; + int count_fail3 = 0; + int count_fail4 = 0; + int count_fail5 = 0; + int count_fail6 = 0; + + // Test 1: first_match with simple boolean + assert property (@(posedge clk) first_match(a) |-> a) + else count_fail1 <= count_fail1 + 1; + + // Test 2: first_match with boolean OR + assert property (@(posedge clk) first_match(a or b) |-> (a | b)) + else count_fail2 <= count_fail2 + 1; + + // Test 3: first_match with boolean AND + assert property (@(posedge clk) first_match(a and b) |-> (a & b)) + else count_fail3 <= count_fail3 + 1; + + // Test 4: nested first_match + assert property (@(posedge clk) first_match(first_match(a)) |-> a) + else count_fail4 <= count_fail4 + 1; + + // Test 5: first_match with boolean intersect + assert property (@(posedge clk) first_match(a intersect b) |-> (a & b)) + else count_fail5 <= count_fail5 + 1; + + // Test 6: first_match in named sequence + sequence s_fm; + first_match(a and c); + endsequence + assert property (@(posedge clk) s_fm |-> (a & c)) + else count_fail6 <= count_fail6 + 1; + + always @(posedge clk) begin +`ifdef TEST_VERBOSE + $write("[%0t] cyc==%0d crc=%x a=%b b=%b c=%b d=%b\n", + $time, cyc, crc, a, b, c, d); +`endif + cyc <= cyc + 1; + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + if (cyc == 0) begin + crc <= 64'h5aef0c8d_d70a4497; + end + else if (cyc == 99) begin + `checkh(crc, 64'hc77bb9b3784ea091); + // All assertions are true by construction: antecedent implies consequent + `checkd(count_fail1, 0); + `checkd(count_fail2, 0); + `checkd(count_fail3, 0); + `checkd(count_fail4, 0); + `checkd(count_fail5, 0); + `checkd(count_fail6, 0); + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule diff --git a/test_regress/t/t_sequence_first_match_unsup.out b/test_regress/t/t_sequence_first_match_unsup.out index a7541ad3a..48de1e1fb 100644 --- a/test_regress/t/t_sequence_first_match_unsup.out +++ b/test_regress/t/t_sequence_first_match_unsup.out @@ -1,8 +1,50 @@ -%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:54:33: Unsupported: first_match (in sequence expression) - 54 | initial p1 : assert property (first_match ((##1 1) or(##2 1)) |-> x == 1); - | ^~~~~~~~~~~ +%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:51:51: Unsupported: Implication with sequence expression as antecedent + : ... note: In instance 'main' + 51 | initial p0 : assert property ((##1 1) or(##2 1) |-> x == 1); + | ^~~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:60:33: Unsupported: first_match (in sequence expression) +%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:51:16: Unsupported: Unclocked assertion + : ... note: In instance 'main' + 51 | initial p0 : assert property ((##1 1) or(##2 1) |-> x == 1); + | ^~~~~~ +%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:54:65: Unsupported: Implication with sequence expression as antecedent + : ... note: In instance 'main' + 54 | initial p1 : assert property (first_match ((##1 1) or(##2 1)) |-> x == 1); + | ^~~ +%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:54:16: Unsupported: Unclocked assertion + : ... note: In instance 'main' + 54 | initial p1 : assert property (first_match ((##1 1) or(##2 1)) |-> x == 1); + | ^~~~~~ +%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:57:44: Unsupported: Implication with sequence expression as antecedent + : ... note: In instance 'main' + 57 | initial p2 : assert property (1 or ##1 1 |-> x == 0); + | ^~~ +%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:57:16: Unsupported: Unclocked assertion + : ... note: In instance 'main' + 57 | initial p2 : assert property (1 or ##1 1 |-> x == 0); + | ^~~~~~ +%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:60:58: Unsupported: Implication with sequence expression as antecedent + : ... note: In instance 'main' 60 | initial p3 : assert property (first_match (1 or ##1 1) |-> x == 0); - | ^~~~~~~~~~~ + | ^~~ +%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:60:16: Unsupported: Unclocked assertion + : ... note: In instance 'main' + 60 | initial p3 : assert property (first_match (1 or ##1 1) |-> x == 0); + | ^~~~~~ +%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:51:16: Unsupported: Procedural concurrent assertion with clocking event inside always (IEEE 1800-2023 16.14.6) + : ... note: In instance 'main' + 51 | initial p0 : assert property ((##1 1) or(##2 1) |-> x == 1); + | ^~~~~~ +%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:54:16: Unsupported: Procedural concurrent assertion with clocking event inside always (IEEE 1800-2023 16.14.6) + : ... note: In instance 'main' + 54 | initial p1 : assert property (first_match ((##1 1) or(##2 1)) |-> x == 1); + | ^~~~~~ +%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:57:16: Unsupported: Procedural concurrent assertion with clocking event inside always (IEEE 1800-2023 16.14.6) + : ... note: In instance 'main' + 57 | initial p2 : assert property (1 or ##1 1 |-> x == 0); + | ^~~~~~ +%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:60:16: Unsupported: Procedural concurrent assertion with clocking event inside always (IEEE 1800-2023 16.14.6) + : ... note: In instance 'main' + 60 | initial p3 : assert property (first_match (1 or ##1 1) |-> x == 0); + | ^~~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index df6947bb9..8ff412c30 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -20,13 +20,10 @@ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:107:26: Unsupported: sequence argument data type 107 | sequence p_arg_seqence(sequence inseq); | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:112:5: Unsupported: first_match (in sequence expression) - 112 | first_match (a); - | ^~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:115:5: Unsupported: first_match (in sequence expression) +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:115:5: Unsupported: first_match with sequence_match_items 115 | first_match (a, res0 = 1); | ^~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:118:5: Unsupported: first_match (in sequence expression) +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:118:5: Unsupported: first_match with sequence_match_items 118 | first_match (a, res0 = 1, res1 = 2); | ^~~~~~~~~~~ %Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:121:9: Ignoring unsupported: cover sequence