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

Use unsigned in NFA, guard against overflow using V3Width. (#8152) 

Signed-off-by: Artur Bieniek <abieniek@antmicro.com>
This commit is contained in:
Artur Bieniek 2026-08-19 08:05:05 +02:00 committed by GitHub
parent f5ae58ddab
commit 06ee8b7261
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
8 changed files with 150 additions and 97 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

135
src/V3AssertNfa.cpp
View File

@ -72,7 +72,7 @@ public:
std::vector<AstNodeExpr*> m_throughoutConds; std::vector<AstNodeExpr*> m_throughoutConds;
// Nonzero for a bitset ring-buffer vertex for ## delays. // Nonzero for a bitset ring-buffer vertex for ## delays.
bool m_isFixedDelayRing = false; bool m_isFixedDelayRing = false;
int m_delayRingSize = 0; // Fixed delay cycles. Range: max-min+1. unsigned m_delayRingSize = 0; // Fixed delay cycles. Range: max-min+1.
AstNodeExpr* m_delayRingClearCondp = nullptr; // local RHS for pure-boolean range AstNodeExpr* m_delayRingClearCondp = nullptr; // local RHS for pure-boolean range
// OWNED; enclosing-abort fire condition clearing in-flight ring bits // OWNED; enclosing-abort fire condition clearing in-flight ring bits
AstNodeExpr* m_abortClearp = nullptr; AstNodeExpr* m_abortClearp = nullptr;
@ -324,7 +324,7 @@ class SvaNfaBuilder final {
struct RangeDelayRejectInfo final { struct RangeDelayRejectInfo final {
SvaStateVertex* startp = nullptr; SvaStateVertex* startp = nullptr;
int range = 0; unsigned range = 0;
int rhsLen = 0; int rhsLen = 0;
}; };
@ -354,10 +354,10 @@ class SvaNfaBuilder final {
return guardp; return guardp;
} }
static int getConstInt(AstNodeExpr* exprp) { static unsigned getConstUInt(AstNodeExpr* exprp) {
AstNodeExpr* const constp = V3Const::constifyEdit(exprp->cloneTreePure(false)); AstNodeExpr* const constp = V3Const::constifyEdit(exprp->cloneTreePure(false));
const AstConst* const cp = VN_CAST(constp, Const); const AstConst* const cp = VN_CAST(constp, Const);
const int val = cp ? cp->toSInt() : -1; const unsigned val = cp ? cp->toUInt() : 0;
VL_DO_DANGLING(constp->deleteTree(), constp); VL_DO_DANGLING(constp->deleteTree(), constp);
return val; return val;
} }
@ -379,16 +379,15 @@ class SvaNfaBuilder final {
if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) { if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) {
AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay); AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay);
if (!delayp || !delayp->isCycleDelay()) return -1; if (!delayp || !delayp->isCycleDelay()) return -1;
int delayCycles = -1; unsigned delayCycles;
if (delayp->isRangeDelay()) { if (delayp->isRangeDelay()) {
if (delayp->isUnbounded()) return -1; // LCOV_EXCL_LINE if (delayp->isUnbounded()) return -1; // LCOV_EXCL_LINE
const int minD = getConstInt(delayp->lhsp()); const unsigned minD = getConstUInt(delayp->lhsp());
const int maxD = getConstInt(delayp->rhsp()); const unsigned maxD = getConstUInt(delayp->rhsp());
if (minD < 0 || maxD < 0 || minD != maxD) return -1; if (minD != maxD) return -1;
delayCycles = minD; delayCycles = minD;
} else { } else {
delayCycles = getConstInt(delayp->lhsp()); delayCycles = getConstUInt(delayp->lhsp());
if (delayCycles < 0) return -1; // LCOV_EXCL_LINE
} }
int preLen = 0; int preLen = 0;
if (AstNodeExpr* const prep = sexprp->preExprp()) { if (AstNodeExpr* const prep = sexprp->preExprp()) {
@ -439,13 +438,11 @@ class SvaNfaBuilder final {
std::pair<int, int> delayRange; std::pair<int, int> delayRange;
if (delayp->isRangeDelay()) { if (delayp->isRangeDelay()) {
if (delayp->isUnbounded()) return {-1, -1}; if (delayp->isUnbounded()) return {-1, -1};
const int minD = getConstInt(delayp->lhsp()); const unsigned minD = getConstUInt(delayp->lhsp());
const int maxD = getConstInt(delayp->rhsp()); const unsigned maxD = getConstUInt(delayp->rhsp());
if (minD < 0 || maxD < 0 || maxD < minD) return {-1, -1};
delayRange = {minD, maxD}; delayRange = {minD, maxD};
} else { } else {
const int d = getConstInt(delayp->lhsp()); const unsigned d = getConstUInt(delayp->lhsp());
if (d < 0) return {-1, -1};
delayRange = {d, d}; delayRange = {d, d};
} }
std::pair<int, int> preRange{0, 0}; std::pair<int, int> preRange{0, 0};
@ -478,15 +475,15 @@ class SvaNfaBuilder final {
AstDelay* rangeDelayp = nullptr; AstDelay* rangeDelayp = nullptr;
clonep->foreach([&](AstDelay* dp) { clonep->foreach([&](AstDelay* dp) {
if (!rangeDelayp && dp->isRangeDelay() && !dp->isUnbounded() if (!rangeDelayp && dp->isRangeDelay() && !dp->isUnbounded()
&& getConstInt(dp->lhsp()) != getConstInt(dp->rhsp())) { && getConstUInt(dp->lhsp()) != getConstUInt(dp->rhsp())) {
rangeDelayp = dp; rangeDelayp = dp;
} }
}); });
if (rangeDelayp) { if (rangeDelayp) {
FileLine* const flp = rangeDelayp->fileline(); FileLine* const flp = rangeDelayp->fileline();
const int pinned = getConstInt(rangeDelayp->lhsp()) + (len - lo); const unsigned pinned = getConstUInt(rangeDelayp->lhsp()) + (len - lo);
AstNodeExpr* const oldMinp = rangeDelayp->lhsp(); AstNodeExpr* const oldMinp = rangeDelayp->lhsp();
oldMinp->replaceWith(new AstConst{flp, static_cast<uint32_t>(pinned)}); oldMinp->replaceWith(new AstConst{flp, pinned});
VL_DO_DANGLING(oldMinp->deleteTree(), oldMinp); VL_DO_DANGLING(oldMinp->deleteTree(), oldMinp);
// Drop the max bound so it lowers as a fixed `##d`, not `##[d:d]`. // Drop the max bound so it lowers as a fixed `##d`, not `##[d:d]`.
AstNode* const oldMaxp = rangeDelayp->rhsp()->unlinkFrBack(); AstNode* const oldMaxp = rangeDelayp->rhsp()->unlinkFrBack();
@ -501,8 +498,8 @@ class SvaNfaBuilder final {
// any exprp -- even an impure one would now evaluate exactly once per // any exprp -- even an impure one would now evaluate exactly once per
// clock instead of N times. Orphan temps from failed builds are unused // clock instead of N times. Orphan temps from failed builds are unused
// MODULETEMPs and are removed by V3Dead. // MODULETEMPs and are removed by V3Dead.
AstVar* tryHoistSampled(AstNodeExpr* exprp, FileLine* flp, int cloneCount) { AstVar* tryHoistSampled(AstNodeExpr* exprp, FileLine* flp, unsigned cloneCount) {
constexpr int kHoistThreshold = 2; constexpr unsigned kHoistThreshold = 2;
if (cloneCount < kHoistThreshold) return nullptr; if (cloneCount < kHoistThreshold) return nullptr;
AstVar* const tempVarp AstVar* const tempVarp
= new AstVar{flp, VVarType::MODULETEMP, m_propTempNames.get(exprp), exprp->dtypep()}; = new AstVar{flp, VVarType::MODULETEMP, m_propTempNames.get(exprp), exprp->dtypep()};
@ -520,9 +517,9 @@ class SvaNfaBuilder final {
// Reject concurrent assertions whose unrolled vertex count would exceed // Reject concurrent assertions whose unrolled vertex count would exceed
// --assert-unroll-limit, so a pathological count cannot blow up compile time. // --assert-unroll-limit, so a pathological count cannot blow up compile time.
static bool exceedsAssertUnrollLimit(AstNode* nodep, int requested) { static bool exceedsAssertUnrollLimit(AstNode* nodep, unsigned requested) {
const int limit = v3Global.opt.assertUnrollLimit(); const int limit = v3Global.opt.assertUnrollLimit();
if (requested <= limit) return false; if (limit >= 0 && requested <= static_cast<unsigned>(limit)) return false;
nodep->v3error("Concurrent assertion repetition count " nodep->v3error("Concurrent assertion repetition count "
<< requested << " exceeds --assert-unroll-limit (" << limit << requested << " exceeds --assert-unroll-limit (" << limit
<< "); raise '--assert-unroll-limit' to compile"); << "); raise '--assert-unroll-limit' to compile");
@ -556,7 +553,7 @@ class SvaNfaBuilder final {
return m_graph.addClockedEdge(fromp, top, throughoutCond(nullptr, flp)); return m_graph.addClockedEdge(fromp, top, throughoutCond(nullptr, flp));
} }
SvaStateVertex* addDelayChain(SvaStateVertex* startp, int size, FileLine* flp, SvaStateVertex* addDelayChain(SvaStateVertex* startp, unsigned size, FileLine* flp,
bool isFixed = true, AstNodeExpr* clearCondp = nullptr) { bool isFixed = true, AstNodeExpr* clearCondp = nullptr) {
if (isFixed && size == 0) return startp; if (isFixed && size == 0) return startp;
UASSERT_OBJ(size > 0, startp, "Delay chain needs at least one slot"); UASSERT_OBJ(size > 0, startp, "Delay chain needs at least one slot");
@ -587,13 +584,7 @@ class SvaNfaBuilder final {
bool applyRangeDelay(AstDelay* delayp, AstNodeExpr* rhsExprp, SvaStateVertex*& currentp, bool applyRangeDelay(AstDelay* delayp, AstNodeExpr* rhsExprp, SvaStateVertex*& currentp,
std::vector<SvaStateVertex*>& midSources, FileLine* flp, std::vector<SvaStateVertex*>& midSources, FileLine* flp,
bool& outErrorEmitted, RangeDelayRejectInfo* rangeRejectInfop = nullptr) { bool& outErrorEmitted, RangeDelayRejectInfo* rangeRejectInfop = nullptr) {
const int minDelay = getConstInt(delayp->lhsp()); const unsigned minDelay = getConstUInt(delayp->lhsp());
if (minDelay < 0) {
delayp->v3error("Range delay minimum is not a non-negative elaboration-time constant"
" (IEEE 1800-2023 16.7)");
outErrorEmitted = true;
return false;
}
if (delayp->isUnbounded()) { if (delayp->isUnbounded()) {
// `##[M:$]`: wait M cycles, then self-loop waiting for the match // `##[M:$]`: wait M cycles, then self-loop waiting for the match
// condition. Unbounded = liveness, so no reject. // condition. Unbounded = liveness, so no reject.
@ -603,29 +594,18 @@ class SvaNfaBuilder final {
m_inUnboundedScope = true; m_inUnboundedScope = true;
return true; return true;
} }
const int maxDelay = getConstInt(delayp->rhsp()); const unsigned maxDelay = getConstUInt(delayp->rhsp());
if (maxDelay < 0) {
delayp->v3error("Range delay maximum is not a non-negative elaboration-time constant"
" (IEEE 1800-2023 16.7)");
outErrorEmitted = true;
return false;
}
if (maxDelay < minDelay) {
delayp->v3error("Range delay maximum must be >= minimum (IEEE 1800-2023 16.7)");
outErrorEmitted = true;
return false;
}
if (minDelay == maxDelay) { if (minDelay == maxDelay) {
currentp = addDelayChain(currentp, minDelay, flp); currentp = addDelayChain(currentp, minDelay, flp);
return true; return true;
} }
const int range = maxDelay - minDelay; const unsigned range = maxDelay - minDelay;
currentp = addDelayChain(currentp, minDelay, flp); currentp = addDelayChain(currentp, minDelay, flp);
// kChainLimit bounds per-attempt unrolled vertices. Above this, a // kChainLimit bounds per-attempt unrolled vertices. Above this, a
// ring buffer (constant-size state) is used instead, so the vertex // ring buffer (constant-size state) is used instead, so the vertex
// count is O(1) in range regardless of user input; no adversarial N // count is O(1) in range regardless of user input; no adversarial N
// blowup is possible. // blowup is possible.
constexpr int kChainLimit = 256; constexpr unsigned kChainLimit = 256;
// IEEE 1800-2023 16.14.3: only a small bounded range before a plain // IEEE 1800-2023 16.14.3: only a small bounded range before a plain
// boolean enumerates every end-of-match below. The counter FSM drops // boolean enumerates every end-of-match below. The counter FSM drops
// overlapping ends and the nested-sequence merge collapses them, so // overlapping ends and the nested-sequence merge collapses them, so
@ -636,7 +616,7 @@ class SvaNfaBuilder final {
return false; return false;
} }
if (range > kChainLimit) { if (range > kChainLimit) {
currentp = addDelayChain(currentp, range + 1, flp, false, currentp = addDelayChain(currentp, range + 1U, flp, false,
rhsExprp->isMultiCycleSva() ? nullptr : rhsExprp); rhsExprp->isMultiCycleSva() ? nullptr : rhsExprp);
} else if (VN_IS(rhsExprp, SExpr)) { } else if (VN_IS(rhsExprp, SExpr)) {
// Nested-SExpr RHS: merge all [M,N] positions. Candidate-local misses // Nested-SExpr RHS: merge all [M,N] positions. Candidate-local misses
@ -648,7 +628,7 @@ class SvaNfaBuilder final {
SvaStateVertex* const mergeVtxp = scopedCreateVertex(); SvaStateVertex* const mergeVtxp = scopedCreateVertex();
mergeVtxp->m_isUnbounded = true; mergeVtxp->m_isUnbounded = true;
guardedLink(currentp, mergeVtxp, flp); guardedLink(currentp, mergeVtxp, flp);
for (int i = 0; i < range; ++i) { for (unsigned i = 0; i < range; ++i) {
SvaStateVertex* const nextVtxp = scopedCreateVertex(); SvaStateVertex* const nextVtxp = scopedCreateVertex();
guardedEdge(currentp, nextVtxp, flp); guardedEdge(currentp, nextVtxp, flp);
guardedLink(nextVtxp, mergeVtxp, flp); guardedLink(nextVtxp, mergeVtxp, flp);
@ -665,7 +645,7 @@ class SvaNfaBuilder final {
AstVar* const hoistVarp AstVar* const hoistVarp
= m_isCoverSeq ? nullptr : tryHoistSampled(rhsExprp, flp, range); = m_isCoverSeq ? nullptr : tryHoistSampled(rhsExprp, flp, range);
midSources.push_back(currentp); midSources.push_back(currentp);
for (int i = 0; i < range; ++i) { for (unsigned i = 0; i < range; ++i) {
SvaStateVertex* const nextVtxp = scopedCreateVertex(); SvaStateVertex* const nextVtxp = scopedCreateVertex();
if (m_isCoverSeq) { if (m_isCoverSeq) {
guardedEdge(currentp, nextVtxp, flp); guardedEdge(currentp, nextVtxp, flp);
@ -697,7 +677,7 @@ class SvaNfaBuilder final {
guardedLink(srcp, successNowp, condp, flp); guardedLink(srcp, successNowp, condp, flp);
SvaStateVertex* stagep = successNowp; SvaStateVertex* stagep = successNowp;
guardedLink(stagep, expiryMatchp, flp); guardedLink(stagep, expiryMatchp, flp);
for (int i = 0; i < info.range; ++i) { for (unsigned i = 0; i < info.range; ++i) {
SvaStateVertex* const nextp = scopedCreateVertex(); SvaStateVertex* const nextp = scopedCreateVertex();
guardedEdge(stagep, nextp, flp); guardedEdge(stagep, nextp, flp);
stagep = nextp; stagep = nextp;
@ -751,13 +731,7 @@ class SvaNfaBuilder final {
return BuildResult::fail(errorEmitted); return BuildResult::fail(errorEmitted);
} }
} else { } else {
const int delayCycles = getConstInt(delayp->lhsp()); const unsigned delayCycles = getConstUInt(delayp->lhsp());
if (delayCycles < 0) {
delayp->v3error("Delay value is not a non-negative"
" elaboration-time constant"
" (IEEE 1800-2023 16.7)");
return BuildResult::failWithError();
}
currentp = addDelayChain(currentp, delayCycles, flp); currentp = addDelayChain(currentp, delayCycles, flp);
} }
@ -780,16 +754,15 @@ class SvaNfaBuilder final {
" consecutive repetition (IEEE 1800-2023 16.9.2)"); " consecutive repetition (IEEE 1800-2023 16.9.2)");
return BuildResult::failWithError(); return BuildResult::failWithError();
} }
const int minN = getConstInt(repp->countp()); const unsigned minN = getConstUInt(repp->countp());
UASSERT_OBJ(minN >= 0, repp, "ConsRep count must be non-negative (V3Width invariant)");
// Sum sites across prefix + unbounded/range tail so one hoist covers // Sum sites across prefix + unbounded/range tail so one hoist covers
// every check edge of this repetition. // every check edge of this repetition.
int totalSites = minN; unsigned totalSites = minN;
if (repp->unbounded()) { if (repp->unbounded()) {
totalSites += 1; totalSites += 1;
} else if (repp->maxCountp()) { } else if (repp->maxCountp()) {
totalSites += getConstInt(repp->maxCountp()) - minN; totalSites += getConstUInt(repp->maxCountp()) - minN;
} }
if (exceedsAssertUnrollLimit(repp, totalSites)) return BuildResult::failWithError(); if (exceedsAssertUnrollLimit(repp, totalSites)) return BuildResult::failWithError();
AstVar* const hoistVarp = tryHoistSampled(exprp, flp, totalSites); AstVar* const hoistVarp = tryHoistSampled(exprp, flp, totalSites);
@ -799,7 +772,7 @@ class SvaNfaBuilder final {
std::vector<SvaStateVertex*> consMidSources; std::vector<SvaStateVertex*> consMidSources;
SvaStateVertex* currentp = entryVtxp; SvaStateVertex* currentp = entryVtxp;
for (int i = 0; i < minN; ++i) { for (unsigned i = 0; i < minN; ++i) {
if (i > 0) { if (i > 0) {
SvaStateVertex* const nextp = scopedCreateVertex(); SvaStateVertex* const nextp = scopedCreateVertex();
guardedEdge(currentp, nextp, flp); guardedEdge(currentp, nextp, flp);
@ -838,11 +811,10 @@ class SvaNfaBuilder final {
currentp->m_isUnbounded = true; currentp->m_isUnbounded = true;
m_inUnboundedScope = true; m_inUnboundedScope = true;
} else if (repp->maxCountp()) { } else if (repp->maxCountp()) {
const int maxN = getConstInt(repp->maxCountp()); const unsigned maxN = getConstUInt(repp->maxCountp());
UASSERT_OBJ(maxN >= minN, repp, "ConsRep range max < min (V3Width invariant)");
SvaStateVertex* const mergeVtxp = scopedCreateVertex(); SvaStateVertex* const mergeVtxp = scopedCreateVertex();
guardedLink(currentp, mergeVtxp, flp); guardedLink(currentp, mergeVtxp, flp);
for (int i = minN; i < maxN; ++i) { for (unsigned i = minN; i < maxN; ++i) {
SvaStateVertex* const nextVtxp = scopedCreateVertex(); SvaStateVertex* const nextVtxp = scopedCreateVertex();
guardedEdge(currentp, nextVtxp, flp); guardedEdge(currentp, nextVtxp, flp);
SvaStateVertex* const checkVtxp = scopedCreateVertex(); SvaStateVertex* const checkVtxp = scopedCreateVertex();
@ -869,7 +841,7 @@ class SvaNfaBuilder final {
bool isTopLevelStep = false) { bool isTopLevelStep = false) {
FileLine* const flp = nodep->fileline(); FileLine* const flp = nodep->fileline();
AstNodeExpr* const propp = nodep->propp(); AstNodeExpr* const propp = nodep->propp();
const int lo = getConstInt(nodep->loBoundp()); const unsigned lo = getConstUInt(nodep->loBoundp());
if (VN_IS(nodep->hiBoundp(), Unbounded)) { if (VN_IS(nodep->hiBoundp(), Unbounded)) {
// Weak always [lo:$]: unbounded upper bound (IEEE 1800-2023 16.12.11). // Weak always [lo:$]: unbounded upper bound (IEEE 1800-2023 16.12.11).
// p must hold at every clock tick at least lo cycles after the attempt // p must hold at every clock tick at least lo cycles after the attempt
@ -877,8 +849,7 @@ class SvaNfaBuilder final {
// end-of-trace obligation (weak). The self-loop keeps the attempt live // end-of-trace obligation (weak). The self-loop keeps the attempt live
// every cycle; each observed cycle is a safety obligation, so a false p // every cycle; each observed cycle is a safety obligation, so a false p
// rejects immediately. // rejects immediately.
UASSERT_OBJ(!nodep->isStrong() && lo >= 0, nodep, UASSERT_OBJ(!nodep->isStrong(), nodep, "Unbounded always must be weak (V3Width)");
"Unbounded always must be weak with non-negative lo (V3Width)");
SvaStateVertex* const livep = addDelayChain(entryVtxp, lo, flp); SvaStateVertex* const livep = addDelayChain(entryVtxp, lo, flp);
livep->m_isUnbounded = true; livep->m_isUnbounded = true;
guardedEdge(livep, livep, flp); // stay active every subsequent cycle guardedEdge(livep, livep, flp); // stay active every subsequent cycle
@ -889,8 +860,7 @@ class SvaNfaBuilder final {
if (isTopLevelStep) rejEdgep->m_rejectOnFail = true; if (isTopLevelStep) rejEdgep->m_rejectOnFail = true;
return {livep, nullptr, {}}; return {livep, nullptr, {}};
} }
const int hi = getConstInt(nodep->hiBoundp()); const unsigned hi = getConstUInt(nodep->hiBoundp());
UASSERT_OBJ(lo >= 0 && hi >= lo, nodep, "PropAlways bounds invariant (V3Width)");
// Strong s_always[m:n]: mark every in-window registered vertex so an // Strong s_always[m:n]: mark every in-window registered vertex so an
// attempt still mid-window at end-of-simulation is reported as a liveness // attempt still mid-window at end-of-simulation is reported as a liveness
// failure (IEEE strong: the n+1 ticks must exist). An attempt that has // failure (IEEE strong: the n+1 ticks must exist). An attempt that has
@ -917,11 +887,10 @@ class SvaNfaBuilder final {
BuildResult buildGotoRep(AstSGotoRep* repp, SvaStateVertex* entryVtxp) { BuildResult buildGotoRep(AstSGotoRep* repp, SvaStateVertex* entryVtxp) {
FileLine* const flp = repp->fileline(); FileLine* const flp = repp->fileline();
AstNodeExpr* const exprp = repp->exprp(); AstNodeExpr* const exprp = repp->exprp();
const int minN = getConstInt(repp->countp()); const unsigned minN = getConstUInt(repp->countp());
if (minN <= 0) return BuildResult::fail(); if (minN == 0) return BuildResult::fail();
const bool hasMax = repp->maxCountp() != nullptr; const bool hasMax = repp->maxCountp() != nullptr;
const int maxN = hasMax ? getConstInt(repp->maxCountp()) : minN; const unsigned maxN = hasMax ? getConstUInt(repp->maxCountp()) : minN;
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();
if (m_isCoverSeq) { if (m_isCoverSeq) {
@ -935,10 +904,10 @@ class SvaNfaBuilder final {
// sites for every iteration in [0..maxN). NOT($sampled(x)) matches // sites for every iteration in [0..maxN). NOT($sampled(x)) matches
// $sampled(NOT(x)) at the value level (IEEE 1800-2023 16.9.9); // $sampled(NOT(x)) at the value level (IEEE 1800-2023 16.9.9);
// purity is enforced uniformly via cloneTreePure inside sampledRefOrClone. // purity is enforced uniformly via cloneTreePure inside sampledRefOrClone.
AstVar* const hoistVarp = tryHoistSampled(exprp, flp, 2 * maxN); AstVar* const hoistVarp = tryHoistSampled(exprp, flp, 2U * maxN);
SvaStateVertex* currentp = entryVtxp; SvaStateVertex* currentp = entryVtxp;
// Build minN match-wait chains to reach the first accept point. // Build minN match-wait chains to reach the first accept point.
for (int i = 0; i < minN; ++i) { for (unsigned i = 0; i < minN; ++i) {
SvaStateVertex* const waitVtxp = scopedCreateVertex(); SvaStateVertex* const waitVtxp = scopedCreateVertex();
// Edge (not Link) for all iterations: IEEE expansion ##1 before each // Edge (not Link) for all iterations: IEEE expansion ##1 before each
// match. A Link at i==0 was wrong -- it allowed same-cycle matching // match. A Link at i==0 was wrong -- it allowed same-cycle matching
@ -961,7 +930,7 @@ class SvaNfaBuilder final {
// buildConsRep's range fan-out. // buildConsRep's range fan-out.
SvaStateVertex* const mergeVtxp = scopedCreateVertex(); SvaStateVertex* const mergeVtxp = scopedCreateVertex();
guardedLink(currentp, mergeVtxp, flp); // accept at match_M guardedLink(currentp, mergeVtxp, flp); // accept at match_M
for (int i = minN; i < maxN; ++i) { for (unsigned i = minN; i < maxN; ++i) {
SvaStateVertex* const waitVtxp = scopedCreateVertex(); SvaStateVertex* const waitVtxp = scopedCreateVertex();
guardedEdge(currentp, waitVtxp, flp); guardedEdge(currentp, waitVtxp, flp);
AstNodeExpr* const waitCondp AstNodeExpr* const waitCondp
@ -1172,9 +1141,9 @@ class SvaNfaBuilder final {
if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) { if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) {
AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay); AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay);
if (!delayp || !delayp->isCycleDelay() || delayp->isUnbounded()) return false; if (!delayp || !delayp->isCycleDelay() || delayp->isUnbounded()) return false;
const int delayCycles = getConstInt(delayp->lhsp()); const unsigned delayCycles = getConstUInt(delayp->lhsp());
if (delayCycles < 0) return false; if (delayp->isRangeDelay() && getConstUInt(delayp->rhsp()) != delayCycles)
if (delayp->isRangeDelay() && getConstInt(delayp->rhsp()) != delayCycles) return false; return false;
int preLen = 0; int preLen = 0;
if (AstNodeExpr* const prep = sexprp->preExprp()) { if (AstNodeExpr* const prep = sexprp->preExprp()) {
if (!flattenFixedSeq(prep, baseOffset, out)) return false; if (!flattenFixedSeq(prep, baseOffset, out)) return false;
@ -1246,7 +1215,7 @@ class SvaNfaBuilder final {
AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay); AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay);
if (!delayp || !delayp->isCycleDelay() || !delayp->isRangeDelay() || delayp->isUnbounded()) if (!delayp || !delayp->isCycleDelay() || !delayp->isRangeDelay() || delayp->isUnbounded())
return {}; return {};
if (getConstInt(delayp->lhsp()) == getConstInt(delayp->rhsp())) return {}; if (getConstUInt(delayp->lhsp()) == getConstUInt(delayp->rhsp())) return {};
AstNodeExpr* const prep = sexprp->preExprp(); AstNodeExpr* const prep = sexprp->preExprp();
if (prep && fixedLength(prep) != 0) return {}; if (prep && fixedLength(prep) != 0) return {};
if (fixedLength(sexprp->exprp()) != 0) return {}; if (fixedLength(sexprp->exprp()) != 0) return {};
@ -3036,7 +3005,7 @@ class AssertNfaVisitor final : public VNVisitor {
// Replace one VarRef to a captured local var with $past(rhs, K) // Replace one VarRef to a captured local var with $past(rhs, K)
// (or rhs inline when K == 0). No-op if refp is not in matchMap. // (or rhs inline when K == 0). No-op if refp is not in matchMap.
void substituteMatchItemRef(AstVarRef* refp, int K, void substituteMatchItemRef(AstVarRef* refp, unsigned K,
const std::unordered_map<const AstVar*, AstNodeExpr*>& matchMap) { const std::unordered_map<const AstVar*, AstNodeExpr*>& matchMap) {
const auto it = matchMap.find(refp->varp()); const auto it = matchMap.find(refp->varp());
if (it == matchMap.end()) return; if (it == matchMap.end()) return;
@ -3057,7 +3026,7 @@ class AssertNfaVisitor final : public VNVisitor {
// substitutes each VarRef to a captured local var with $past(rhs, K) // substitutes each VarRef to a captured local var with $past(rhs, K)
// (or rhs inline when K == 0). Reports E_UNSUPPORTED on non-constant // (or rhs inline when K == 0). Reports E_UNSUPPORTED on non-constant
// delays or composite sequence operators. // delays or composite sequence operators.
int walkSubstituteMatchItems(AstNodeExpr* nodep, int K, int walkSubstituteMatchItems(AstNodeExpr* nodep, unsigned K,
const std::unordered_map<const AstVar*, AstNodeExpr*>& matchItems, const std::unordered_map<const AstVar*, AstNodeExpr*>& matchItems,
bool& errorEmitted) { bool& errorEmitted) {
if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) { if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) {
@ -3075,7 +3044,7 @@ class AssertNfaVisitor final : public VNVisitor {
errorEmitted = true; errorEmitted = true;
return -1; return -1;
} }
const int delayCycles = VN_AS(delayp->lhsp(), Const)->toSInt(); const unsigned delayCycles = VN_AS(delayp->lhsp(), Const)->toUInt();
int preLen = 0; int preLen = 0;
if (AstNodeExpr* const prep = sexprp->preExprp()) { if (AstNodeExpr* const prep = sexprp->preExprp()) {
preLen = walkSubstituteMatchItems(prep, K, matchItems, errorEmitted); preLen = walkSubstituteMatchItems(prep, K, matchItems, errorEmitted);
@ -3121,7 +3090,7 @@ class AssertNfaVisitor final : public VNVisitor {
AstVarRef* const lhsRefp = VN_AS(assignp->lhsp(), VarRef); AstVarRef* const lhsRefp = VN_AS(assignp->lhsp(), VarRef);
matchItems[lhsRefp->varp()] = assignp->rhsp(); matchItems[lhsRefp->varp()] = assignp->rhsp();
} }
const int startK = parts.isOverlapped ? 0 : 1; const unsigned startK = parts.isOverlapped ? 0 : 1;
bool errorEmitted = false; bool errorEmitted = false;
walkSubstituteMatchItems(seqBodyp, startK, matchItems, errorEmitted); walkSubstituteMatchItems(seqBodyp, startK, matchItems, errorEmitted);
// Match-item substitution / strip mutates ancestor purity. Release // Match-item substitution / strip mutates ancestor purity. Release

55
src/V3Width.cpp
View File

@ -744,15 +744,39 @@ class WidthVisitor final : public VNVisitor {
// it's like an if() condition. // it's like an if() condition.
iterateCheckBool(nodep, "default disable iff condition", nodep->condp(), BOTH); iterateCheckBool(nodep, "default disable iff condition", nodep->condp(), BOTH);
} }
static const AstConst* widthCheckSvaDelayBound(AstDelay* nodep, AstNodeExpr* boundp,
const char* what) {
const AstConst* const constp = VN_CAST(boundp, Const);
if (!constp || (constp->dtypep()->isSigned() && constp->num().isNegative())) {
nodep->v3error(what << " is not a non-negative elaboration-time constant"
" (IEEE 1800-2023 16.7)");
return nullptr;
}
if (constp->num().mostSetBitP1() > 31) {
nodep->v3warn(
E_UNSUPPORTED,
"Unsupported: SVA cycle delay exceeds implementation limit of 2147483647");
return nullptr;
}
return constp;
}
void visit(AstDelay* nodep) override { void visit(AstDelay* nodep) override {
if (nodep->isCycleDelay() && m_underSExpr) { if (nodep->isCycleDelay() && m_underSExpr) {
// Fold parameterized SVA cycle-delay bounds // Fold parameterized SVA cycle-delay bounds
userIterateAndNext(nodep->lhsp(), WidthVP{SELF, BOTH}.p()); userIterateAndNext(nodep->lhsp(), WidthVP{SELF, BOTH}.p());
V3Const::constifyParamsNoWarnEdit(nodep->lhsp()); V3Const::constifyParamsNoWarnEdit(nodep->lhsp());
const AstConst* const minConstp = widthCheckSvaDelayBound(
nodep, nodep->lhsp(),
nodep->isRangeDelay() ? "Range delay minimum" : "Delay value");
if (nodep->rhsp() && !nodep->isUnbounded()) { if (nodep->rhsp() && !nodep->isUnbounded()) {
// Fold parametrized SVA cycle-delay max bound // Fold parametrized SVA cycle-delay max bound
userIterateAndNext(nodep->rhsp(), WidthVP{SELF, BOTH}.p()); userIterateAndNext(nodep->rhsp(), WidthVP{SELF, BOTH}.p());
V3Const::constifyParamsNoWarnEdit(nodep->rhsp()); V3Const::constifyParamsNoWarnEdit(nodep->rhsp());
const AstConst* const maxConstp
= widthCheckSvaDelayBound(nodep, nodep->rhsp(), "Range delay maximum");
if (minConstp && maxConstp && maxConstp->toUInt() < minConstp->toUInt()) {
nodep->v3error("Range delay maximum must be >= minimum (IEEE 1800-2023 16.7)");
}
} }
return; return;
} }
@ -1832,7 +1856,11 @@ class WidthVisitor final : public VNVisitor {
if (m_vup->prelim()) { if (m_vup->prelim()) {
iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH); iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH);
userIterateAndNext(nodep->countp(), WidthVP{SELF, BOTH}.p()); userIterateAndNext(nodep->countp(), WidthVP{SELF, BOTH}.p());
if (nodep->maxCountp()) widthCheckGotoRepRange(nodep, "Goto"); if (nodep->maxCountp()) {
widthCheckGotoRepRange(nodep, "Goto");
} else {
widthCheckRepCount(nodep);
}
nodep->dtypeSetBit(); nodep->dtypeSetBit();
} }
} }
@ -1841,10 +1869,33 @@ class WidthVisitor final : public VNVisitor {
if (m_vup->prelim()) { if (m_vup->prelim()) {
iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH); iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH);
userIterateAndNext(nodep->countp(), WidthVP{SELF, BOTH}.p()); userIterateAndNext(nodep->countp(), WidthVP{SELF, BOTH}.p());
if (nodep->maxCountp()) widthCheckGotoRepRange(nodep, "Nonconsecutive"); if (nodep->maxCountp()) {
widthCheckGotoRepRange(nodep, "Nonconsecutive");
} else {
widthCheckRepCount(nodep);
}
nodep->dtypeSetBit(); nodep->dtypeSetBit();
} }
} }
template <typename T_Rep>
void widthCheckRepCount(T_Rep* nodep) {
V3Const::constifyParamsNoWarnEdit(nodep->countp());
const AstConst* const constp = VN_CAST(nodep->countp(), Const);
if (!constp) {
nodep->v3error("Repetition count is not an elaboration-time constant"
" (IEEE 1800-2023 16.9.2)");
} else if (constp->dtypep()->isSigned() && constp->num().isNegative()) {
nodep->v3error("Repetition count must be non-negative"
" (IEEE 1800-2023 16.9.2)");
} else if (constp->num().mostSetBitP1() > 31) {
nodep->v3warn(
E_UNSUPPORTED,
"Unsupported: SVA repetition count exceeds implementation limit of 2147483647");
} else if (constp->isZero()) {
nodep->v3warn(E_UNSUPPORTED, "Unsupported: zero repetition count"
" (IEEE 1800-2023 16.9.2)");
}
}
// IEEE 1800-2023 16.9.2 range-form bound validation for goto/nonconsec. // IEEE 1800-2023 16.9.2 range-form bound validation for goto/nonconsec.
// Parent accessors are re-fetched after constifyParamsEdit because that // Parent accessors are re-fetched after constifyParamsEdit because that
// call can replace the node in-tree (Lesson: AstSConsRep visitor pattern). // call can replace the node in-tree (Lesson: AstSConsRep visitor pattern).

24
test_regress/t/t_assert_rep_bad_count.out
View File

@ -1,27 +1,35 @@
%Error: t/t_assert_rep_bad_count.v:14:42: Repetition count is not an elaboration-time constant (IEEE 1800-2023 16.9.2) %Error: t/t_assert_rep_bad_count.v:14:36: Repetition count is not an elaboration-time constant (IEEE 1800-2023 16.9.2)
: ... note: In instance 't' : ... note: In instance 't'
14 | assert property (@(posedge clk) a[->n] |-> b) 14 | assert property (@(posedge clk) a[->n] |-> b)
| ^~~ | ^~~
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
%Error-UNSUPPORTED: t/t_assert_rep_bad_count.v:18:42: Unsupported: zero repetition count (IEEE 1800-2023 16.9.2) %Error-UNSUPPORTED: t/t_assert_rep_bad_count.v:18:36: Unsupported: zero repetition count (IEEE 1800-2023 16.9.2)
: ... note: In instance 't' : ... note: In instance 't'
18 | assert property (@(posedge clk) a[->0] |-> b) 18 | assert property (@(posedge clk) a[->0] |-> b)
| ^~~ | ^~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: t/t_assert_rep_bad_count.v:22:43: Repetition count must be non-negative (IEEE 1800-2023 16.9.2) %Error: t/t_assert_rep_bad_count.v:22:36: Repetition count must be non-negative (IEEE 1800-2023 16.9.2)
: ... note: In instance 't' : ... note: In instance 't'
22 | assert property (@(posedge clk) a[->-1] |-> b) 22 | assert property (@(posedge clk) a[->-1] |-> b)
| ^~~ | ^~~
%Error: t/t_assert_rep_bad_count.v:28:41: Repetition count is not an elaboration-time constant (IEEE 1800-2023 16.9.2) %Error: t/t_assert_rep_bad_count.v:28:36: Repetition count is not an elaboration-time constant (IEEE 1800-2023 16.9.2)
: ... note: In instance 't' : ... note: In instance 't'
28 | assert property (@(posedge clk) a[=n] |-> b) 28 | assert property (@(posedge clk) a[=n] |-> b)
| ^~~ | ^~
%Error-UNSUPPORTED: t/t_assert_rep_bad_count.v:32:41: Unsupported: zero repetition count (IEEE 1800-2023 16.9.2) %Error-UNSUPPORTED: t/t_assert_rep_bad_count.v:32:36: Unsupported: zero repetition count (IEEE 1800-2023 16.9.2)
: ... note: In instance 't' : ... note: In instance 't'
32 | assert property (@(posedge clk) a[=0] |-> b) 32 | assert property (@(posedge clk) a[=0] |-> b)
| ^~~ | ^~
%Error: t/t_assert_rep_bad_count.v:36:42: Repetition count must be non-negative (IEEE 1800-2023 16.9.2) %Error: t/t_assert_rep_bad_count.v:36:36: Repetition count must be non-negative (IEEE 1800-2023 16.9.2)
: ... note: In instance 't' : ... note: In instance 't'
36 | assert property (@(posedge clk) a[=-1] |-> b) 36 | assert property (@(posedge clk) a[=-1] |-> b)
| ^~
%Error-UNSUPPORTED: t/t_assert_rep_bad_count.v:39:36: Unsupported: SVA repetition count exceeds implementation limit of 2147483647
: ... note: In instance 't'
39 | assert property (@(posedge clk) a[->32'h80000000] |-> b)
| ^~~ | ^~~
%Error-UNSUPPORTED: t/t_assert_rep_bad_count.v:42:36: Unsupported: SVA repetition count exceeds implementation limit of 2147483647
: ... note: In instance 't'
42 | assert property (@(posedge clk) a[=32'h80000000] |-> b)
| ^~
%Error: Exiting due to %Error: Exiting due to

6
test_regress/t/t_assert_rep_bad_count.v
View File

@ -36,4 +36,10 @@ module t (input clk);
assert property (@(posedge clk) a[=-1] |-> b) assert property (@(posedge clk) a[=-1] |-> b)
else $error("FAIL"); else $error("FAIL");
assert property (@(posedge clk) a[->32'h80000000] |-> b)
else $error("FAIL");
assert property (@(posedge clk) a[=32'h80000000] |-> b)
else $error("FAIL");
endmodule endmodule

5
test_regress/t/t_property_sexpr2_bad.out
View File

@ -7,4 +7,9 @@
: ... note: In instance 't' : ... note: In instance 't'
21 | assert property (@(posedge clk) ##(1+clk) val); 21 | assert property (@(posedge clk) ##(1+clk) val);
| ^~ | ^~
%Error-UNSUPPORTED: t/t_property_sexpr2_bad.v:23:35: Unsupported: SVA cycle delay exceeds implementation limit of 2147483647
: ... note: In instance 't'
23 | assert property (@(posedge clk) ##32'h80000000 val);
| ^~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to %Error: Exiting due to

2
test_regress/t/t_property_sexpr2_bad.v
View File

@ -19,4 +19,6 @@ module t ( /*AUTOARG*/
assert property (@(posedge clk) ##clk val); assert property (@(posedge clk) ##clk val);
assert property (@(posedge clk) ##(1+clk) val); assert property (@(posedge clk) ##(1+clk) val);
assert property (@(posedge clk) ##32'h80000000 val);
endmodule endmodule

9
test_regress/t/t_property_sexpr_range_delay_bad.out
View File

@ -19,4 +19,13 @@
: ... note: In instance 't' : ... note: In instance 't'
34 | a6: assert property (@(posedge clk) a |-> ##[NEG:$] b); 34 | a6: assert property (@(posedge clk) a |-> ##[NEG:$] b);
| ^~ | ^~
%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:36:45: Unsupported: SVA cycle delay exceeds implementation limit of 2147483647
: ... note: In instance 't'
36 | a7: assert property (@(posedge clk) a |-> ##[1:32'h80000000] b);
| ^~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:37:45: Unsupported: SVA cycle delay exceeds implementation limit of 2147483647
: ... note: In instance 't'
37 | a8: assert property (@(posedge clk) a |-> ##[32'h80000000:$] b);
| ^~
%Error: Exiting due to %Error: Exiting due to

3
test_regress/t/t_property_sexpr_range_delay_bad.v
View File

@ -33,4 +33,7 @@ module t;
localparam int NEG = -1; localparam int NEG = -1;
a6: assert property (@(posedge clk) a |-> ##[NEG:$] b); a6: assert property (@(posedge clk) a |-> ##[NEG:$] b);
a7: assert property (@(posedge clk) a |-> ##[1:32'h80000000] b);
a8: assert property (@(posedge clk) a |-> ##[32'h80000000:$] b);
endmodule endmodule