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

Fix not failing assertion when RHS of a range window rejects once (#7773)

This commit is contained in:
Artur Bieniek 2026-06-15 21:32:11 +02:00 committed by GitHub
parent 0233e5044c
commit 7061c1f04d
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 100 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

83
src/V3AssertNfa.cpp
View File

@ -110,6 +110,9 @@ public:
// Reject when source is active and condp is false; set only on
// outermost required-step Link
bool m_rejectOnFail = false;
// Optional dynamic condition vertex for m_rejectOnFail. Used when the
// success condition is another NFA state rather than a static expression.
SvaStateVertex* m_condVtxp = nullptr;
// CONSTRUCTORS
SvaTransEdge(V3Graph* graphp, V3GraphVertex* fromp, V3GraphVertex* top, AstNodeExpr* condp,
@ -208,6 +211,12 @@ class SvaNfaBuilder final {
// topology when true. Default false preserves cover_property semantics.
bool m_isCoverSeq = false;
struct RangeDelayRejectInfo final {
SvaStateVertex* startp = nullptr;
int range = 0;
int rhsLen = 0;
};
AstNodeExpr* throughoutCond(AstNodeExpr* baseCondp, FileLine* flp) {
if (m_throughoutStack.empty()) return baseCondp;
// AND all throughout conditions (supports nesting)
@ -374,7 +383,7 @@ class SvaNfaBuilder final {
// failure, sets outErrorEmitted per semantic-error policy and returns false.
bool applyRangeDelay(AstDelay* delayp, AstNodeExpr* rhsExprp, SvaStateVertex*& currentp,
std::vector<SvaStateVertex*>& midSources, FileLine* flp,
bool& outErrorEmitted) {
bool& outErrorEmitted, RangeDelayRejectInfo* rangeRejectInfop = nullptr) {
const int minDelay = getConstInt(delayp->lhsp());
if (minDelay < 0) {
delayp->v3error("Range delay minimum is not a non-negative elaboration-time constant"
@ -433,8 +442,14 @@ class SvaNfaBuilder final {
guardedEdge(currentp, counterVtxp, flp);
currentp = counterVtxp;
} else if (VN_IS(rhsExprp, SExpr)) {
// Nested-SExpr RHS: merge all [M,N] positions; continuation is per-attempt.
// Nested-SExpr RHS: merge all [M,N] positions. Candidate-local misses
// are not assertion rejects while a later position can still match.
if (rangeRejectInfop) {
const int rhsLen = fixedLength(rhsExprp);
if (rhsLen >= 0) *rangeRejectInfop = {currentp, range, rhsLen};
}
SvaStateVertex* const mergeVtxp = scopedCreateVertex();
mergeVtxp->m_isUnbounded = true;
guardedLink(currentp, mergeVtxp, flp);
for (int i = 0; i < range; ++i) {
SvaStateVertex* const nextVtxp = scopedCreateVertex();
@ -443,6 +458,7 @@ class SvaNfaBuilder final {
currentp = nextVtxp;
}
currentp = mergeVtxp;
m_inUnboundedScope = true;
} else {
// Pure boolean RHS: register chain. Each mid-position links to
// match (match-only); last position is the reject source.
@ -468,12 +484,44 @@ class SvaNfaBuilder final {
return true;
}
void addFiniteRangeReject(const RangeDelayRejectInfo& info, const BuildResult& result,
FileLine* flp) {
if (!info.startp) return;
SvaStateVertex* const expiryVtxp
= addDelayChain(info.startp, info.range + info.rhsLen, flp);
SvaStateVertex* const expiryMatchp = scopedCreateVertex();
std::vector<SvaStateVertex*> sources = result.midSources;
sources.push_back(result.termVertexp);
for (SvaStateVertex* const srcp : sources) {
AstNodeExpr* const condp
= result.finalCondp ? sampled(result.finalCondp->cloneTreePure(false)) : nullptr;
SvaStateVertex* const successNowp = scopedCreateVertex();
guardedLink(srcp, successNowp, condp, flp);
SvaStateVertex* stagep = successNowp;
guardedLink(stagep, expiryMatchp, flp);
for (int i = 0; i < info.range; ++i) {
SvaStateVertex* const nextp = scopedCreateVertex();
guardedEdge(stagep, nextp, flp);
stagep = nextp;
guardedLink(stagep, expiryMatchp, flp);
}
}
SvaStateVertex* const sinkVtxp = m_graph.createStateVertex();
sinkVtxp->m_isRejectSink = true;
SvaTransEdge* const rejectp = m_graph.addLink(expiryVtxp, sinkVtxp);
rejectp->m_rejectOnFail = true;
rejectp->m_condVtxp = expiryMatchp;
}
BuildResult buildSExpr(AstSExpr* sexprp, SvaStateVertex* entryVtxp,
bool isTopLevelStep = false) {
AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay);
if (!delayp || !delayp->isCycleDelay()) return BuildResult::fail();
FileLine* const flp = sexprp->fileline();
AstNodeExpr* const exprp = sexprp->exprp();
// Handle LHS (preExpr)
SvaStateVertex* currentp = entryVtxp;
@ -496,10 +544,12 @@ class SvaNfaBuilder final {
// Handle delay
std::vector<SvaStateVertex*> rangeMidSources;
RangeDelayRejectInfo rangeRejectInfo;
const bool addRangeReject = isTopLevelStep && !m_inUnboundedScope;
if (delayp->isRangeDelay()) {
bool errorEmitted = false;
if (!applyRangeDelay(delayp, sexprp->exprp(), currentp, rangeMidSources, flp,
errorEmitted)) {
errorEmitted, addRangeReject ? &rangeRejectInfo : nullptr)) {
return BuildResult::fail(errorEmitted);
}
} else {
@ -514,8 +564,11 @@ class SvaNfaBuilder final {
}
// Multi-cycle RHS: recurse (only plain boolean is returned as finalCondp).
AstNodeExpr* const exprp = sexprp->exprp();
if (exprp->isMultiCycleSva()) return buildExpr(exprp, currentp, isTopLevelStep);
if (exprp->isMultiCycleSva()) {
const BuildResult result = buildExpr(exprp, currentp, isTopLevelStep);
if (result.valid()) addFiniteRangeReject(rangeRejectInfo, result, flp);
return result;
}
return {currentp, exprp, std::move(rangeMidSources)};
}
@ -1505,15 +1558,25 @@ class SvaNfaLowering final {
computeTerminalMatchAndReject(c, snapshotOkp, sigs, outPerMidSrcsp);
// Phase 3a: required-step rejection.
// Builder only sets m_rejectOnFail on non-clocked Links with m_condp,
// and the source always has a resolved stateSig.
// Builder only sets m_rejectOnFail on non-clocked Links with m_condp
// or m_condVtxp, and the source always has a resolved stateSig.
for (const SvaTransEdge* const tep : c.edges) {
if (!tep->m_rejectOnFail) continue;
const int fi = tep->fromVtxp()->color();
UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp && tep->m_condp, tep->fromVtxp(),
"rejectOnFail Link must have condp and source stateSig");
UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp && (tep->m_condp || tep->m_condVtxp),
tep->fromVtxp(),
"rejectOnFail Link must have condp/condVtxp and source stateSig");
AstNodeExpr* const srcSigp = c.vtx[fi]->datap()->stateSigp->cloneTreePure(false);
AstNodeExpr* const notCondp = new AstLogNot{c.flp, tep->m_condp->cloneTreePure(false)};
AstNodeExpr* condp = nullptr;
if (tep->m_condVtxp) {
const int ci = tep->m_condVtxp->color();
UASSERT_OBJ(c.vtx[ci]->datap()->stateSigp, tep->m_condVtxp,
"rejectOnFail condVtxp missing stateSig");
condp = c.vtx[ci]->datap()->stateSigp->cloneTreePure(false);
} else {
condp = tep->m_condp->cloneTreePure(false);
}
AstNodeExpr* const notCondp = new AstLogNot{c.flp, condp};
AstNodeExpr* const failp = new AstLogAnd{c.flp, srcSigp, notCondp};
if (outRequiredStepSrcsp) {
outRequiredStepSrcsp->push_back(failp->cloneTreePure(false));

34
test_regress/t/t_property_sexpr_range_delay.v
View File

@ -30,6 +30,7 @@ module t (
int count_fail2 = 0;
int count_fail3 = 0;
int count_fail4 = 0;
int count_fail5 = 0;
always_ff @(posedge clk) begin
`ifdef TEST_VERBOSE
@ -49,13 +50,11 @@ module t (
else if (cyc == 99) begin
`checkh(crc, 64'hc77bb9b3784ea091);
`checkh(sum, 64'h38c614665c6b71ad);
// count_fail1 overcounts Questa by 1: NFA per-cycle reject merging
// OR's requiredStep-fail and terminal-fail into one signal; Questa
// resolves the same overlap as a single per-attempt miss.
`checkd(count_fail1, 25); // Questa: 24
`checkd(count_fail2, 50); // Questa: 50
`checkd(count_fail3, 24); // Questa: 24
`checkd(count_fail4, 1); // Questa: 1
`checkd(count_fail1, 24);
`checkd(count_fail2, 50);
`checkd(count_fail3, 24);
`checkd(count_fail4, 1);
`checkd(count_fail5, 1);
$write("*-* All Finished *-*\n");
$finish;
end
@ -131,4 +130,25 @@ module t (
assert property (@(posedge clk) disable iff (cyc < 2)
a |-> ##[+] b ##1 (a | b | c | d | e));
// Finite range delay with a multi-cycle RHS must not reject on an earlier
// candidate when a later candidate in the same window matches.
assert property (@(posedge clk)
cyc == 10 |-> ##[2:4] ((cyc == 12 || cyc == 13) ##1 cyc == 14));
// Same shape, but every RHS candidate in the range window rejects, so the
// assertion attempt itself must reject once.
assert property (@(posedge clk)
cyc == 20 |-> ##[2:4] ((cyc == 22 || cyc == 23) ##1 cyc == 25))
else count_fail5 <= count_fail5 + 1;
// Variable-length nested RHS, then another finite range below
// the liveness scope.
assert property (@(posedge clk)
cyc == 30 |-> ##[1:2] ((cyc == 31) ##[1:2] ((cyc == 32) ##1 1'b1)));
// Finite range whose RHS ends in an NFA state, not a final
// boolean condition.
assert property (@(posedge clk)
cyc == 40 |-> ##[1:2] (##1 (((cyc == 43) ##1 1'b1) or ((cyc == 43) ##1 1'b1))));
endmodule