Fix mid-range consecutive repetition rejects (#8041)

Signed-off-by: Artur Bieniek <abieniek@antmicro.com>
This commit is contained in:
Artur Bieniek 2026-08-04 18:50:33 +02:00 committed by GitHub
parent 3c4ea47e02
commit e4b6bac50a
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
3 changed files with 15 additions and 5 deletions

View File

@ -783,12 +783,11 @@ class SvaNfaBuilder final {
guardedEdge(currentp, nextp, flp);
currentp = nextp;
}
// Mark first and last boolean Links as rejectOnFail for correct
// reject on standalone ConsRep.
// Every repetition in the minimum prefix is required.
SvaStateVertex* const condVtxp = scopedCreateVertex();
SvaTransEdge* const linkp
= guardedLink(currentp, condVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
if (isTopLevelStep && (i == 0 || i == minN - 1)) { linkp->m_rejectOnFail = true; }
if (isTopLevelStep) linkp->m_rejectOnFail = true;
currentp = condVtxp;
}
// After minN: currentp is the first valid end-of-match position for [*m:n].

View File

@ -46,6 +46,8 @@ module t (
int count_fail19 = 0;
int count_fail20 = 0;
int count_fail21 = 0;
int count_fail22 = 0;
int count_fail23 = 0;
// Test 1: a[*3] |-> b
assert property (@(posedge clk) a [* 3] |-> b)
@ -126,6 +128,14 @@ module t (
assert property (@(posedge clk) c |-> (a ##1 a [+]))
else count_fail21 <= count_fail21 + 1;
// Test 22: Fail the middle required check of an exact repetition.
assert property (@(posedge clk) cyc == 1 |-> ##1 (cyc != 3) [*3])
else count_fail22 <= count_fail22 + 1;
// Test 23: A bounded range succeeds at its minimum, later repetitions are optional.
assert property (@(posedge clk) cyc == 1 |-> ##1 (cyc != 5) [*3:5])
else count_fail23 <= count_fail23 + 1;
// Counter FSM with M>0: range > kChainLimit (256) forces counter vertex
// creation; min>0 exercises the Gte/active gating path in resolveLinks and
// emitNbaLogic. Cover-only so count_fail values above are undisturbed.
@ -165,6 +175,8 @@ module t (
`checkd(count_fail16, count_fail17);
`checkd(count_fail18, count_fail19);
`checkd(count_fail20, count_fail21);
`checkd(count_fail22, 1);
`checkd(count_fail23, 0);
$write("*-* All Finished *-*\n");
$finish;
end

View File

@ -40,8 +40,7 @@ module t (
else if (cyc == 99) begin
`checkh(crc, 64'hc77bb9b3784ea091);
`checkd(count_fail_257, 0);
// Mismatch due to pre-existing ~26.5% NFA reject gap on |-> ##1 [*N]
`checkd(count_fail_513, 23); // All other sims: 31
`checkd(count_fail_513, 31);
$write("*-* All Finished *-*\n");
$finish;
end