luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fix COVERIGN on SVA goto repetition (#8118) 

Signed-off-by: Artur Bieniek <abieniek@antmicro.com>
This commit is contained in:
Artur Bieniek 2026-08-14 19:52:10 +02:00 committed by GitHub
parent 621a67e819
commit 0b50390359
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
3 changed files with 11 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/V3AssertNfa.cpp
View File

@ -912,12 +912,10 @@ class SvaNfaBuilder final {
UASSERT_OBJ(maxN >= minN, repp, "GotoRep range max < min (V3Width invariant)"); UASSERT_OBJ(maxN >= minN, repp, "GotoRep range max < min (V3Width invariant)");
if (exceedsAssertUnrollLimit(repp, maxN)) return BuildResult::failWithError(); if (exceedsAssertUnrollLimit(repp, maxN)) return BuildResult::failWithError();
// IEEE 1800-2023 16.14.3: a ranged goto repetition b[->M:N] ends at every if (m_isCoverSeq) {
// M..N-th match, but only the shared merge vertex below reaches the // Several matches may wait across false cycles, but the NFA stores only one bit for
// terminal, so a cover sequence would under-count. Reject the ranged form // them, so a cover sequence action block could run too few times.
// (the single-count b[->N] has one end and is enumerated correctly). warnEndpointUnsupported(flp, "a goto repetition");
if (m_isCoverSeq && hasMax && maxN > minN) {
warnEndpointUnsupported(flp, "a ranged goto repetition");
return BuildResult::failWithError(); return BuildResult::failWithError();
} }

7
test_regress/t/t_cover_sequence_unsup.out
View File

@ -12,7 +12,10 @@
%Warning-COVERIGN: t/t_cover_sequence_unsup.v:30:21: Ignoring unsupported: cover sequence with this ranged cycle delay %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); 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 %Warning-COVERIGN: t/t_cover_sequence_unsup.v:33:21: Ignoring unsupported: cover sequence with a goto repetition
33 | cover sequence (a [-> 2: 3]); 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 %Error: Exiting due to

3
test_regress/t/t_cover_sequence_unsup.v
View File

@ -29,7 +29,8 @@ module t (
// Ranged cycle delay wide enough to use the counter FSM. // Ranged cycle delay wide enough to use the counter FSM.
cover sequence (a ##[1:300] b); 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]); cover sequence (a [-> 2: 3]);
endmodule endmodule