diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 397874dfc..88103937c 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -912,12 +912,10 @@ class SvaNfaBuilder final { UASSERT_OBJ(maxN >= minN, repp, "GotoRep range max < min (V3Width invariant)"); if (exceedsAssertUnrollLimit(repp, maxN)) return BuildResult::failWithError(); - // IEEE 1800-2023 16.14.3: a ranged goto repetition b[->M:N] ends at every - // M..N-th match, but only the shared merge vertex below reaches the - // terminal, so a cover sequence would under-count. Reject the ranged form - // (the single-count b[->N] has one end and is enumerated correctly). - if (m_isCoverSeq && hasMax && maxN > minN) { - warnEndpointUnsupported(flp, "a ranged goto repetition"); + if (m_isCoverSeq) { + // Several matches may wait across false cycles, but the NFA stores only one bit for + // them, so a cover sequence action block could run too few times. + warnEndpointUnsupported(flp, "a goto repetition"); return BuildResult::failWithError(); } diff --git a/test_regress/t/t_cover_sequence_unsup.out b/test_regress/t/t_cover_sequence_unsup.out index 47af703cb..7850b7d99 100644 --- a/test_regress/t/t_cover_sequence_unsup.out +++ b/test_regress/t/t_cover_sequence_unsup.out @@ -12,7 +12,10 @@ %Warning-COVERIGN: t/t_cover_sequence_unsup.v:30:21: Ignoring unsupported: cover sequence with this ranged cycle delay 30 | cover sequence (a ##[1:300] b); | ^~ -%Warning-COVERIGN: t/t_cover_sequence_unsup.v:33:21: Ignoring unsupported: cover sequence with a ranged goto repetition - 33 | cover sequence (a [-> 2: 3]); +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:33:21: Ignoring unsupported: cover sequence with a goto repetition + 33 | cover sequence (a [-> 2]); + | ^~~ +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:34:21: Ignoring unsupported: cover sequence with a goto repetition + 34 | cover sequence (a [-> 2: 3]); | ^~~ %Error: Exiting due to diff --git a/test_regress/t/t_cover_sequence_unsup.v b/test_regress/t/t_cover_sequence_unsup.v index b2770a2fa..660d0409b 100644 --- a/test_regress/t/t_cover_sequence_unsup.v +++ b/test_regress/t/t_cover_sequence_unsup.v @@ -29,7 +29,8 @@ module t ( // Ranged cycle delay wide enough to use the counter FSM. cover sequence (a ##[1:300] b); - // Ranged goto repetition (every M..N-th match is a separate end). + // Goto repetition coalesces multiple live attempts into one NFA state. + cover sequence (a [-> 2]); cover sequence (a [-> 2: 3]); endmodule