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

Optimize bounded always properties using ring buffers (#8061) 

Signed-off-by: Artur Bieniek <abieniek@antmicro.com>
This commit is contained in:
Artur Bieniek 2026-08-10 14:45:50 +02:00 committed by GitHub
parent 121fc62aff
commit 490bd38962
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
4 changed files with 249 additions and 131 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

336
src/V3AssertNfa.cpp
View File

@ -51,6 +51,7 @@ struct SvaVertexData final {
AstVar* stateVarp = nullptr; // NBA state register for this vertex AstVar* stateVarp = nullptr; // NBA state register for this vertex
AstVar* delayRingVarp = nullptr; // Bitset ring buffer AstVar* delayRingVarp = nullptr; // Bitset ring buffer
AstVar* delayRingIdxVarp = nullptr; // Next slot written in delayRingVarp AstVar* delayRingIdxVarp = nullptr; // Next slot written in delayRingVarp
AstVar* delayRingLiveCountVarp = nullptr; // Number of set bits in delayRingVarp
AstVar* doneLVarp = nullptr; // SAnd LHS done-latch AstVar* doneLVarp = nullptr; // SAnd LHS done-latch
AstVar* doneRVarp = nullptr; // SAnd RHS done-latch AstVar* doneRVarp = nullptr; // SAnd RHS done-latch
AstNodeExpr* stateSigp = nullptr; // Combinational state signal (owned during lowering) AstNodeExpr* stateSigp = nullptr; // Combinational state signal (owned during lowering)
@ -83,6 +84,8 @@ public:
// end-of-simulation the universal-quantifier window never completed, which is // end-of-simulation the universal-quantifier window never completed, which is
// a liveness failure (IEEE 1800-2023 16.12.11 strong semantics). // a liveness failure (IEEE 1800-2023 16.12.11 strong semantics).
bool m_strongPending = false; bool m_strongPending = false;
// Ring introduced for the checked portion of a bounded strong s_always window.
bool m_strongAlwaysRing = false;
// CONSTRUCTORS // CONSTRUCTORS
explicit SvaStateVertex(V3Graph* graphp) explicit SvaStateVertex(V3Graph* graphp)
@ -204,6 +207,13 @@ struct BuildResult final {
static BuildResult failWithError() { return {nullptr, nullptr, {}, true}; } static BuildResult failWithError() { return {nullptr, nullptr, {}, true}; }
}; };
static AstConst* newTypedConstp(FileLine* const flp, const AstNodeDType* const dtypep,
const uint32_t value) {
AstConst* const constp = new AstConst{flp, AstConst::DTyped{}, dtypep};
constp->num().setLong(value);
return constp;
}
static AstNodeExpr* sampled(AstNodeExpr* exprp) { static AstNodeExpr* sampled(AstNodeExpr* exprp) {
AstSampled* const sp = new AstSampled{exprp->fileline(), exprp, exprp->dtypep()}; AstSampled* const sp = new AstSampled{exprp->fileline(), exprp, exprp->dtypep()};
return sp; return sp;
@ -288,7 +298,7 @@ class SvaNfaBuilder final {
SvaGraph& m_graph; // NFA graph being built SvaGraph& m_graph; // NFA graph being built
AstNodeModule* const m_modp; // Module to receive hoisted sampled-prop temps AstNodeModule* const m_modp; // Module to receive hoisted sampled-prop temps
V3UniqueNames& m_propTempNames; // Module-shared temp-var name source V3UniqueNames& m_propTempNames; // Module-shared temp-var name source
std::vector<AstNodeExpr*> m_throughoutStack; // Active throughout guards (IEEE 16.9.9) std::vector<AstNodeExpr*> m_temporalGuardStack; // Guards active across nested temporal states
// Outer abort conditions, AND-ed as !cond into inner abort edges // Outer abort conditions, AND-ed as !cond into inner abort edges
// (IEEE 1800-2023 16.12.14 outer-wraps-inner). // (IEEE 1800-2023 16.12.14 outer-wraps-inner).
std::vector<AstNodeExpr*> m_outerAbortStack; std::vector<AstNodeExpr*> m_outerAbortStack;
@ -317,11 +327,11 @@ class SvaNfaBuilder final {
} }
AstNodeExpr* throughoutCond(AstNodeExpr* baseCondp, FileLine* flp) { AstNodeExpr* throughoutCond(AstNodeExpr* baseCondp, FileLine* flp) {
if (m_throughoutStack.empty()) return baseCondp; if (m_temporalGuardStack.empty()) return baseCondp;
// AND all throughout conditions (supports nesting) // AND all active temporal guards (supports nesting)
// Each must use $sampled values per IEEE 16.9.9 // Each must use $sampled values.
AstNodeExpr* guardp = nullptr; AstNodeExpr* guardp = nullptr;
for (AstNodeExpr* const condp : m_throughoutStack) { for (AstNodeExpr* const condp : m_temporalGuardStack) {
AstNodeExpr* const clonep = sampled(condp->cloneTreePure(false)); AstNodeExpr* const clonep = sampled(condp->cloneTreePure(false));
if (!guardp) { if (!guardp) {
guardp = clonep; guardp = clonep;
@ -508,10 +518,10 @@ class SvaNfaBuilder final {
return true; return true;
} }
// Create vertex and inherit throughout guards from current scope (IEEE 16.9.9). // Create vertex and inherit temporal guards from the current scope.
SvaStateVertex* scopedCreateVertex() { SvaStateVertex* scopedCreateVertex() {
SvaStateVertex* const vtxp = m_graph.createStateVertex(); SvaStateVertex* const vtxp = m_graph.createStateVertex();
for (AstNodeExpr* const cp : m_throughoutStack) { for (AstNodeExpr* const cp : m_temporalGuardStack) {
vtxp->m_throughoutConds.push_back(cp->cloneTreePure(false)); vtxp->m_throughoutConds.push_back(cp->cloneTreePure(false));
} }
if (m_inUnboundedScope) vtxp->m_isUnbounded = true; if (m_inUnboundedScope) vtxp->m_isUnbounded = true;
@ -519,7 +529,7 @@ class SvaNfaBuilder final {
return vtxp; return vtxp;
} }
// AND current throughout stack into every edge/link (IEEE 16.9.9 invariant). // AND current temporal guards into every edge/link.
SvaTransEdge* guardedLink(SvaStateVertex* fromp, SvaStateVertex* top, AstNodeExpr* condp, SvaTransEdge* guardedLink(SvaStateVertex* fromp, SvaStateVertex* top, AstNodeExpr* condp,
FileLine* flp) { FileLine* flp) {
return m_graph.addLink(fromp, top, throughoutCond(condp, flp)); return m_graph.addLink(fromp, top, throughoutCond(condp, flp));
@ -869,8 +879,6 @@ class SvaNfaBuilder final {
} }
const int hi = getConstInt(nodep->hiBoundp()); const int hi = getConstInt(nodep->hiBoundp());
UASSERT_OBJ(lo >= 0 && hi >= lo, nodep, "PropAlways bounds invariant (V3Width)"); UASSERT_OBJ(lo >= 0 && hi >= lo, nodep, "PropAlways bounds invariant (V3Width)");
if (exceedsAssertUnrollLimit(nodep, hi - lo + 1)) return BuildResult::failWithError();
AstVar* const hoistVarp = tryHoistSampled(propp, flp, hi - lo + 1);
// 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
@ -879,20 +887,19 @@ class SvaNfaBuilder final {
// flagged, matching the strong reference. Weak always[m:n] is not marked. // flagged, matching the strong reference. Weak always[m:n] is not marked.
VL_RESTORER(m_markStrongPending); VL_RESTORER(m_markStrongPending);
m_markStrongPending = nodep->isStrong(); m_markStrongPending = nodep->isStrong();
// Check the first in-window tick, then reuse a guarded fixed-delay ring
// for the remaining ticks instead of creating one state per cycle.
SvaStateVertex* currentp = addDelayChain(entryVtxp, lo, flp); SvaStateVertex* currentp = addDelayChain(entryVtxp, lo, flp);
for (int k = 0; k <= hi - lo; ++k) { SvaStateVertex* const checkp = scopedCreateVertex();
if (k > 0) { SvaTransEdge* const linkp
SvaStateVertex* const nextp = scopedCreateVertex(); = guardedLink(currentp, checkp, sampled(propp->cloneTreePure(false)), flp);
guardedEdge(currentp, nextp, flp); if (isTopLevelStep) linkp->m_rejectOnFail = true;
currentp = nextp; currentp = checkp;
} m_temporalGuardStack.push_back(propp);
SvaStateVertex* const checkp = scopedCreateVertex(); currentp = addDelayChain(currentp, hi - lo, flp);
SvaTransEdge* const linkp if (nodep->isStrong() && currentp->m_delayRingSize) currentp->m_strongAlwaysRing = true;
= guardedLink(currentp, checkp, sampledRefOrClone(hoistVarp, propp, flp), flp); m_temporalGuardStack.pop_back();
if (isTopLevelStep && !m_inUnboundedScope) linkp->m_rejectOnFail = true; return {currentp, propp, {}};
currentp = checkp;
}
return {currentp, nullptr, {}};
} }
BuildResult buildGotoRep(AstSGotoRep* repp, SvaStateVertex* entryVtxp) { BuildResult buildGotoRep(AstSGotoRep* repp, SvaStateVertex* entryVtxp) {
@ -1309,9 +1316,9 @@ class SvaNfaBuilder final {
bool isTopLevelStep = false) { bool isTopLevelStep = false) {
// Mark entryVtxp so "cond false at tick 0" is detected as throughout-drop. // Mark entryVtxp so "cond false at tick 0" is detected as throughout-drop.
entryVtxp->m_throughoutConds.push_back(nodep->lhsp()->cloneTreePure(false)); entryVtxp->m_throughoutConds.push_back(nodep->lhsp()->cloneTreePure(false));
m_throughoutStack.push_back(nodep->lhsp()); m_temporalGuardStack.push_back(nodep->lhsp());
const BuildResult result = buildExpr(nodep->rhsp(), entryVtxp, isTopLevelStep); const BuildResult result = buildExpr(nodep->rhsp(), entryVtxp, isTopLevelStep);
m_throughoutStack.pop_back(); m_temporalGuardStack.pop_back();
return result; return result;
} }
@ -1479,7 +1486,7 @@ public:
// Reset scope between antecedent and consequent: liveness must not leak. // Reset scope between antecedent and consequent: liveness must not leak.
void resetScope() { void resetScope() {
m_inUnboundedScope = false; m_inUnboundedScope = false;
m_throughoutStack.clear(); m_temporalGuardStack.clear();
m_outerAbortStack.clear(); m_outerAbortStack.clear();
} }
@ -1621,6 +1628,7 @@ public:
class SvaNfaLowering final { class SvaNfaLowering final {
AstNodeModule* const m_modp; // Module to add state vars and always blocks to AstNodeModule* const m_modp; // Module to add state vars and always blocks to
AstNodeDType* const m_u32DTypep; // Shared unsigned counter dtype
V3UniqueNames m_names{"__Vnfa"}; V3UniqueNames m_names{"__Vnfa"};
// Per-lowering shared context (passed to phase sub-functions) // Per-lowering shared context (passed to phase sub-functions)
@ -1659,6 +1667,18 @@ class SvaNfaLowering final {
if (!ap) return bp; if (!ap) return bp;
return new AstLogOr{flp, ap, bp}; return new AstLogOr{flp, ap, bp};
} }
static AstNodeExpr* addThreadFailCountp(FileLine* const flp,
AstNodeExpr* const totalThreadFailCountp,
AstNodeExpr* const contributionp,
AstNodeExpr* const enablep = nullptr) {
// contribution = enable ? contribution : 0;
AstNodeExpr* const enabledContributionp
= enablep ? new AstCond{flp, enablep, contributionp,
newTypedConstp(flp, contributionp->dtypep(), 0)}
: contributionp;
if (!totalThreadFailCountp) return enabledContributionp;
return new AstAdd{flp, totalThreadFailCountp, enabledContributionp};
}
static AstNodeExpr* killActive(LowerCtx& c) { static AstNodeExpr* killActive(LowerCtx& c) {
return new AstNeq{c.flp, new AstVarRef{c.flp, c.killVarp, VAccess::READ}, return new AstNeq{c.flp, new AstVarRef{c.flp, c.killVarp, VAccess::READ},
assertKillGet(c.flp, c.assertType, c.directiveType)}; assertKillGet(c.flp, c.assertType, c.directiveType)};
@ -1687,6 +1707,11 @@ class SvaNfaLowering final {
// ring[idx] // ring[idx]
return new AstSel{flp, new AstVarRef{flp, ringp, access}, idxExprp, 1}; return new AstSel{flp, new AstVarRef{flp, ringp, access}, idxExprp, 1};
} }
static AstNodeExpr* delayRingHasLiveBitsp(FileLine* const flp, AstVar* const liveCountVarp) {
// active = live_count != 0;
return new AstNeq{flp, new AstVarRef{flp, liveCountVarp, VAccess::READ},
newTypedConstp(flp, liveCountVarp->dtypep(), 0)};
}
// Phase 3 output signals // Phase 3 output signals
struct SignalSet final { struct SignalSet final {
@ -1694,6 +1719,7 @@ class SvaNfaLowering final {
AstNodeExpr* rejectBasep = nullptr; // Reject when a terminal match fails AstNodeExpr* rejectBasep = nullptr; // Reject when a terminal match fails
AstNodeExpr* requiredStepRejectp = nullptr; // Per-source reject from rejectOnFail Links AstNodeExpr* requiredStepRejectp = nullptr; // Per-source reject from rejectOnFail Links
AstNodeExpr* throughoutRejectp = nullptr; // Reject when a throughout guard drops AstNodeExpr* throughoutRejectp = nullptr; // Reject when a throughout guard drops
AstNodeExpr* threadFailCountp = nullptr; // Number of threads rejected on this tick
}; };
// Phase 2/2b/2c: Emit NBA state-update always blocks for registered vertices, // Phase 2/2b/2c: Emit NBA state-update always blocks for registered vertices,
@ -1758,6 +1784,7 @@ class SvaNfaLowering final {
if (!vtxp->datap()->delayRingVarp) continue; if (!vtxp->datap()->delayRingVarp) continue;
AstVar* const ringp = vtxp->datap()->delayRingVarp; AstVar* const ringp = vtxp->datap()->delayRingVarp;
AstVar* const idxp = vtxp->datap()->delayRingIdxVarp; AstVar* const idxp = vtxp->datap()->delayRingIdxVarp;
AstVar* const liveCountVarp = vtxp->datap()->delayRingLiveCountVarp;
const uint32_t size = static_cast<uint32_t>(vtxp->m_delayRingSize); const uint32_t size = static_cast<uint32_t>(vtxp->m_delayRingSize);
AstNodeExpr* incomingp = nullptr; AstNodeExpr* incomingp = nullptr;
@ -1778,32 +1805,40 @@ class SvaNfaLowering final {
incomingp = orExprs(c.flp, incomingp, contribp); incomingp = orExprs(c.flp, incomingp, contribp);
} }
UASSERT_OBJ(incomingp, vtxp, "Delay ring has no incoming edge"); UASSERT_OBJ(incomingp, vtxp, "Delay ring has no incoming edge");
AstNode* updateBodyp = nullptr; // ring[idx] <= incoming;
if (vtxp->m_isFixedDelayRing) { AstAssignDly* const writeIncomingp = new AstAssignDly{
// ring[idx] <= incoming; c.flp,
updateBodyp = new AstAssignDly{ delayRingBit(c.flp, ringp, new AstVarRef{c.flp, idxp, VAccess::READ},
c.flp, VAccess::WRITE),
delayRingBit(c.flp, ringp, new AstVarRef{c.flp, idxp, VAccess::READ}, incomingp};
VAccess::WRITE), AstNode* updateBodyp = writeIncomingp;
incomingp}; if (!vtxp->m_isFixedDelayRing) {
} else { // ring[next_idx] <= 1'b0;
// ring[next_idx] <= 1'b0; ring[idx] <= incoming;
AstAssignDly* const clearExpirep = new AstAssignDly{ AstAssignDly* const clearExpirep = new AstAssignDly{
c.flp, c.flp,
delayRingBit(c.flp, ringp, nextRingIndex(c.flp, idxp, size), VAccess::WRITE), delayRingBit(c.flp, ringp, nextRingIndex(c.flp, idxp, size), VAccess::WRITE),
new AstConst{c.flp, AstConst::BitFalse{}}}; new AstConst{c.flp, AstConst::BitFalse{}}};
AstAssignDly* const writeIncomingp = new AstAssignDly{
c.flp,
delayRingBit(c.flp, ringp, new AstVarRef{c.flp, idxp, VAccess::READ},
VAccess::WRITE),
incomingp};
clearExpirep->addNext(writeIncomingp); clearExpirep->addNext(writeIncomingp);
updateBodyp = clearExpirep; updateBodyp = clearExpirep;
} }
// live_count <= live_count + incoming_bit - outgoing_bit;
const int liveCountWidth = liveCountVarp->dtypep()->width();
AstNodeExpr* const incomingIncrementp
= new AstExtend{c.flp, incomingp->cloneTreePure(false), liveCountWidth};
AstSub* const nextLiveCountp = new AstSub{
c.flp,
new AstAdd{c.flp, new AstVarRef{c.flp, liveCountVarp, VAccess::READ},
incomingIncrementp},
new AstExtend{
c.flp, delayRingBit(c.flp, ringp, new AstVarRef{c.flp, idxp, VAccess::READ}),
liveCountWidth}};
updateBodyp->addNext(new AstAssignDly{
c.flp, new AstVarRef{c.flp, liveCountVarp, VAccess::WRITE}, nextLiveCountp});
AstNodeExpr* clearCondp = nullptr; AstNodeExpr* clearCondp = killActive(c);
if (vtxp->m_delayRingClearCondp) { if (vtxp->m_delayRingClearCondp) {
clearCondp = sampled(vtxp->m_delayRingClearCondp->cloneTreePure(false)); clearCondp = orExprs(c.flp, clearCondp,
sampled(vtxp->m_delayRingClearCondp->cloneTreePure(false)));
} }
if (c.disableExprp) { if (c.disableExprp) {
clearCondp = orExprs(c.flp, clearCondp, c.disableExprp->cloneTreePure(false)); clearCondp = orExprs(c.flp, clearCondp, c.disableExprp->cloneTreePure(false));
@ -1815,15 +1850,15 @@ class SvaNfaLowering final {
: sampledp; : sampledp;
} }
if (guardp) clearCondp = orExprs(c.flp, clearCondp, new AstLogNot{c.flp, guardp}); if (guardp) clearCondp = orExprs(c.flp, clearCondp, new AstLogNot{c.flp, guardp});
if (clearCondp) { // ring <= '0; live_count <= 0;
// if (clear) ring <= '0; AstConst* const zerop = new AstConst{c.flp, AstConst::DTyped{}, ringp->dtypep()};
AstConst* const zerop = new AstConst{c.flp, AstConst::DTyped{}, ringp->dtypep()}; zerop->num().setAllBits0();
zerop->num().setAllBits0(); AstAssignDly* const clearRingp
updateBodyp = new AstIf{ = new AstAssignDly{c.flp, new AstVarRef{c.flp, ringp, VAccess::WRITE}, zerop};
c.flp, clearCondp, clearRingp->addNext(
new AstAssignDly{c.flp, new AstVarRef{c.flp, ringp, VAccess::WRITE}, zerop}, new AstAssignDly{c.flp, new AstVarRef{c.flp, liveCountVarp, VAccess::WRITE},
updateBodyp}; newTypedConstp(c.flp, liveCountVarp->dtypep(), 0)});
} updateBodyp = new AstIf{c.flp, clearCondp, clearRingp, updateBodyp};
// idx <= next_idx; // idx <= next_idx;
updateBodyp->addNext(new AstAssignDly{c.flp, updateBodyp->addNext(new AstAssignDly{c.flp,
new AstVarRef{c.flp, idxp, VAccess::WRITE}, new AstVarRef{c.flp, idxp, VAccess::WRITE},
@ -1896,8 +1931,8 @@ class SvaNfaLowering final {
AstAssignDly* const ackp AstAssignDly* const ackp
= new AstAssignDly{c.flp, new AstVarRef{c.flp, c.killVarp, VAccess::WRITE}, = new AstAssignDly{c.flp, new AstVarRef{c.flp, c.killVarp, VAccess::WRITE},
assertKillGet(c.flp, c.assertType, c.directiveType)}; assertKillGet(c.flp, c.assertType, c.directiveType)};
m_modp->addStmtsp(new AstAlways{c.flp, VAlwaysKwd::ALWAYS, c.senTreep->cloneTree(false), m_modp->addStmtsp(
new AstIf{c.flp, killActive(c), ackp, nullptr}}); new AstAlways{c.flp, VAlwaysKwd::ALWAYS, c.senTreep->cloneTree(false), ackp});
} }
// Phase 3/3a/3b: Compute terminal match/reject signals, required-step reject, // Phase 3/3a/3b: Compute terminal match/reject signals, required-step reject,
@ -1963,8 +1998,20 @@ class SvaNfaLowering final {
"No terminal edge to match vertex"); "No terminal edge to match vertex");
} }
AstNodeExpr* newThroughoutThreadFailCountp(LowerCtx& c, AstVar* const delayRingLiveCountVarp,
AstNodeExpr* const stateExprp,
AstNodeExpr* const notGuardp) {
AstNodeExpr* const activeThreadCountp
= delayRingLiveCountVarp
? static_cast<AstNodeExpr*>(
new AstVarRef{c.flp, delayRingLiveCountVarp, VAccess::READ})
: new AstExtend{c.flp, stateExprp->cloneTreePure(false), m_u32DTypep->width()};
return addThreadFailCountp(c.flp, nullptr, activeThreadCountp,
notGuardp->cloneTreePure(false));
}
// Phase 3b: Throughout-drop rejection (IEEE 16.9.9). // Phase 3b: Throughout-drop rejection (IEEE 16.9.9).
void computeThroughoutReject(LowerCtx& c, SignalSet& sigs) { void computeThroughoutReject(LowerCtx& c, SignalSet& sigs, const bool needThreadFailCount) {
for (int i = 0; i < c.N; ++i) { for (int i = 0; i < c.N; ++i) {
const auto& conds = c.vtx[i]->m_throughoutConds; const auto& conds = c.vtx[i]->m_throughoutConds;
if (conds.empty()) continue; if (conds.empty()) continue;
@ -1973,9 +2020,8 @@ class SvaNfaLowering final {
if (c.vtx[i]->datap()->stateVarp) { if (c.vtx[i]->datap()->stateVarp) {
stateExprp = new AstVarRef{c.flp, c.vtx[i]->datap()->stateVarp, VAccess::READ}; stateExprp = new AstVarRef{c.flp, c.vtx[i]->datap()->stateVarp, VAccess::READ};
} else if (c.vtx[i]->datap()->delayRingVarp && c.vtx[i]->m_isFixedDelayRing) { } else if (c.vtx[i]->datap()->delayRingVarp && c.vtx[i]->m_isFixedDelayRing) {
// fixed_chain_active = |ring; stateExprp
stateExprp = new AstRedOr{ = delayRingHasLiveBitsp(c.flp, c.vtx[i]->datap()->delayRingLiveCountVarp);
c.flp, new AstVarRef{c.flp, c.vtx[i]->datap()->delayRingVarp, VAccess::READ}};
} else { } else {
UASSERT_OBJ(c.vtx[i]->datap()->stateSigp, c.vtx[i], UASSERT_OBJ(c.vtx[i]->datap()->stateSigp, c.vtx[i],
"Throughout-conds vertex missing state representation"); "Throughout-conds vertex missing state representation");
@ -1987,12 +2033,19 @@ class SvaNfaLowering final {
guardp = guardp ? static_cast<AstNodeExpr*>(new AstLogAnd{c.flp, guardp, sp}) : sp; guardp = guardp ? static_cast<AstNodeExpr*>(new AstLogAnd{c.flp, guardp, sp}) : sp;
} }
AstNodeExpr* const notGuardp = new AstLogNot{c.flp, guardp}; AstNodeExpr* const notGuardp = new AstLogNot{c.flp, guardp};
if (needThreadFailCount) {
AstNodeExpr* const contributionp = newThroughoutThreadFailCountp(
c, c.vtx[i]->datap()->delayRingLiveCountVarp, stateExprp, notGuardp);
sigs.threadFailCountp
= addThreadFailCountp(c.flp, sigs.threadFailCountp, contributionp);
}
sigs.throughoutRejectp = orExprs(c.flp, sigs.throughoutRejectp, sigs.throughoutRejectp = orExprs(c.flp, sigs.throughoutRejectp,
new AstLogAnd{c.flp, stateExprp, notGuardp}); new AstLogAnd{c.flp, stateExprp, notGuardp});
} }
} }
SignalSet computeSignals(LowerCtx& c, std::vector<AstNodeExpr*>* outRequiredStepSrcsp, SignalSet computeSignals(LowerCtx& c, const bool needThreadFailCount,
const bool needThroughoutThreadFailCount,
std::vector<AstNodeExpr*>* outPerMidSrcsp = nullptr) { std::vector<AstNodeExpr*>* outPerMidSrcsp = nullptr) {
SignalSet sigs; SignalSet sigs;
@ -2027,14 +2080,22 @@ class SvaNfaLowering final {
condp = tep->m_condp->cloneTreePure(false); condp = tep->m_condp->cloneTreePure(false);
} }
AstNodeExpr* const notCondp = new AstLogNot{c.flp, condp}; AstNodeExpr* const notCondp = new AstLogNot{c.flp, condp};
AstNodeExpr* const failp = gateNotKill(c, new AstLogAnd{c.flp, srcSigp, notCondp}); AstNodeExpr* const rawFailp = new AstLogAnd{c.flp, srcSigp, notCondp};
if (outRequiredStepSrcsp) { if (needThreadFailCount) {
outRequiredStepSrcsp->push_back(failp->cloneTreePure(false)); // thread_fail_count += fail;
sigs.threadFailCountp = addThreadFailCountp(
c.flp, sigs.threadFailCountp,
new AstExtend{c.flp, rawFailp->cloneTreePure(false), m_u32DTypep->width()});
} }
AstNodeExpr* const failp = gateNotKill(c, rawFailp);
sigs.requiredStepRejectp = orExprs(c.flp, sigs.requiredStepRejectp, failp); sigs.requiredStepRejectp = orExprs(c.flp, sigs.requiredStepRejectp, failp);
} }
computeThroughoutReject(c, sigs); computeThroughoutReject(c, sigs, needThroughoutThreadFailCount);
if (sigs.threadFailCountp) {
sigs.threadFailCountp
= addThreadFailCountp(c.flp, nullptr, sigs.threadFailCountp, notKillActive(c));
}
sigs.terminalActivep = gateNotKill(c, sigs.terminalActivep); sigs.terminalActivep = gateNotKill(c, sigs.terminalActivep);
sigs.rejectBasep = gateNotKill(c, sigs.rejectBasep); sigs.rejectBasep = gateNotKill(c, sigs.rejectBasep);
sigs.throughoutRejectp = gateNotKill(c, sigs.throughoutRejectp); sigs.throughoutRejectp = gateNotKill(c, sigs.throughoutRejectp);
@ -2093,10 +2154,8 @@ class SvaNfaLowering final {
c.flp, c.vtx[i]->datap()->delayRingVarp, c.flp, c.vtx[i]->datap()->delayRingVarp,
new AstVarRef{c.flp, c.vtx[i]->datap()->delayRingIdxVarp, VAccess::READ}); new AstVarRef{c.flp, c.vtx[i]->datap()->delayRingIdxVarp, VAccess::READ});
} else { } else {
// state = |ring; c.vtx[i]->datap()->stateSigp
c.vtx[i]->datap()->stateSigp = new AstRedOr{ = delayRingHasLiveBitsp(c.flp, c.vtx[i]->datap()->delayRingLiveCountVarp);
c.flp,
new AstVarRef{c.flp, c.vtx[i]->datap()->delayRingVarp, VAccess::READ}};
} }
} }
} }
@ -2254,15 +2313,16 @@ public:
} }
explicit SvaNfaLowering(AstNodeModule* modp) explicit SvaNfaLowering(AstNodeModule* modp)
: m_modp{modp} {} : m_modp{modp}
, m_u32DTypep{modp->findBasicDType(VBasicDTypeKwd::UINT32)} {}
// Lower NFA graph to synthesizable AstAlways blocks and raw result signals. // Lower NFA graph to synthesizable AstAlways blocks and raw result signals.
// Links are combinational; Edges are registered (NBA). // Links are combinational; Edges are registered (NBA).
SignalSet lower(AstNodeCoverOrAssert* const assertp, SvaGraph& graph, SignalSet lower(AstNodeCoverOrAssert* const assertp, SvaGraph& graph,
AstSenTree* const senTreep, AstNodeExpr* const matchCondp, AstSenTree* const senTreep, AstNodeExpr* const matchCondp,
AstNodeExpr* const disableExprp, AstVar* const disableCntVarp, AstNodeExpr* const disableExprp, AstVar* const disableCntVarp,
AstVar* const snapshotVarp, AstVar* const snapshotVarp, const bool needThreadFailCount,
std::vector<AstNodeExpr*>* const outRequiredStepSrcsp, const bool needThroughoutThreadFailCount,
std::vector<AstNodeExpr*>* const outPerMidSrcsp) { std::vector<AstNodeExpr*>* const outPerMidSrcsp) {
FileLine* const flp = assertp->fileline(); FileLine* const flp = assertp->fileline();
AstCover* const coverp = VN_CAST(assertp, Cover); AstCover* const coverp = VN_CAST(assertp, Cover);
@ -2303,9 +2363,8 @@ public:
} }
} }
AstNodeDType* const u32DTypep = m_modp->findBasicDType(VBasicDTypeKwd::UINT32);
AstVar* const killVarp AstVar* const killVarp
= new AstVar{flp, VVarType::MODULETEMP, baseName + "__kill", u32DTypep}; = new AstVar{flp, VVarType::MODULETEMP, baseName + "__kill", m_u32DTypep};
killVarp->lifetime(VLifetime::STATIC_EXPLICIT); killVarp->lifetime(VLifetime::STATIC_EXPLICIT);
m_modp->addStmtsp(killVarp); m_modp->addStmtsp(killVarp);
for (int i = 0; i < N; ++i) { for (int i = 0; i < N; ++i) {
@ -2335,10 +2394,16 @@ public:
vtx[i]->datap()->delayRingVarp = ringp; vtx[i]->datap()->delayRingVarp = ringp;
// int unsigned idx; // int unsigned idx;
AstVar* const idxp AstVar* const idxp
= new AstVar{flp, VVarType::MODULETEMP, base + "_idx", u32DTypep}; = new AstVar{flp, VVarType::MODULETEMP, base + "_idx", m_u32DTypep};
idxp->lifetime(VLifetime::STATIC_EXPLICIT); idxp->lifetime(VLifetime::STATIC_EXPLICIT);
m_modp->addStmtsp(idxp); m_modp->addStmtsp(idxp);
vtx[i]->datap()->delayRingIdxVarp = idxp; vtx[i]->datap()->delayRingIdxVarp = idxp;
// int unsigned live_count;
AstVar* const liveCountVarp
= new AstVar{flp, VVarType::MODULETEMP, base + "_liveCount", m_u32DTypep};
liveCountVarp->lifetime(VLifetime::STATIC_EXPLICIT);
m_modp->addStmtsp(liveCountVarp);
vtx[i]->datap()->delayRingLiveCountVarp = liveCountVarp;
continue; continue;
} }
if (!vtx[i]->datap()->needsReg) continue; if (!vtx[i]->datap()->needsReg) continue;
@ -2370,21 +2435,30 @@ public:
emitKillAckNba(c); emitKillAckNba(c);
// Phase 3/3a/3b: Compute terminal match/reject signals (cleans up stateSig). // Phase 3/3a/3b: Compute terminal match/reject signals (cleans up stateSig).
const SignalSet sigs = computeSignals(c, outRequiredStepSrcsp, outPerMidSrcsp); const SignalSet sigs = computeSignals(c, needThreadFailCount,
needThroughoutThreadFailCount, outPerMidSrcsp);
// Strong s_always[m:n] end-of-simulation liveness: if any in-window state // Strong s_always[m:n] end-of-simulation liveness: if any in-window state
// is still set at $finish, the universal-quantifier window never completed // is still set at $finish, the universal-quantifier window never completed
// (IEEE 1800-2023 16.12.11 strong semantics). Fire the assertion failure // (IEEE 1800-2023 16.12.11 strong semantics). Fire the assertion failure
// from a final block; V3Assert turns the DT_ERROR display into the standard // from a final block; V3Assert turns the DT_ERROR display into the standard
// "Assertion failed in %m" message. // "Assertion failed in %m" message.
// pending = |{strong state registers, strong delay live counts != 0};
AstNodeExpr* pendingp = nullptr; AstNodeExpr* pendingp = nullptr;
for (int i = 0; i < N; ++i) { for (int i = 0; i < N; ++i) {
if (!vtx[i]->m_strongPending || !vtx[i]->datap()->stateVarp) continue; if (!vtx[i]->m_strongPending) continue;
AstNodeExpr* const svp = new AstVarRef{flp, vtx[i]->datap()->stateVarp, VAccess::READ}; AstNodeExpr* pendingExprp = nullptr;
if (!pendingp) { if (vtx[i]->datap()->stateVarp) {
pendingp = svp; pendingExprp = new AstVarRef{flp, vtx[i]->datap()->stateVarp, VAccess::READ};
} else if (vtx[i]->m_strongAlwaysRing) {
pendingExprp = delayRingHasLiveBitsp(flp, vtx[i]->datap()->delayRingLiveCountVarp);
} else { } else {
pendingp = new AstLogOr{flp, pendingp, svp}; continue;
}
if (!pendingp) {
pendingp = pendingExprp;
} else {
pendingp = new AstLogOr{flp, pendingp, pendingExprp};
} }
} }
if (pendingp) { if (pendingp) {
@ -2773,56 +2847,60 @@ class AssertNfaVisitor final : public VNVisitor {
parts.triggerExprp, flp); parts.triggerExprp, flp);
} }
// Install the pass-action handler and per-thread fail-handlers generated by // Install pass-action gating and replay simultaneous per-thread failures.
// assembleResult() on a negated assert. void attachActionHandlers(AstAssert* const assertp, AstNodeExpr* matchExprp,
void attachMatchHandlers(FileLine* flp, AstAssert* assertAssertp, AstAssert* assertWithFailp, AstSenTree* const threadFailReplaySenTreep,
AstNodeExpr* matchExprp, AstSenTree* perSrcSenTreep, AstNodeExpr* const threadFailCountp) {
const std::vector<AstNodeExpr*>& requiredStepSrcs) {
// Gate pass handler on match to prevent vacuous-pass firings. // Gate pass handler on match to prevent vacuous-pass firings.
if (matchExprp) { if (matchExprp) {
// needMatch implies passsp() was non-null when evaluated above; // needMatch implies passsp() was non-null when evaluated above;
// lowering does not mutate the assert's pass-action between the // lowering does not mutate the assert's pass-action between the
// two reads, so passsp() is still non-null here. // two reads, so passsp() is still non-null here.
AstNode* passsp = assertAssertp->passsp(); AstNode* passsp = assertp->passsp();
UASSERT_OBJ(passsp, assertAssertp, "needMatch set but passsp is null"); UASSERT_OBJ(passsp, assertp, "needMatch set but passsp is null");
passsp->unlinkFrBackWithNext(); passsp->unlinkFrBackWithNext();
assertAssertp->addPasssp(new AstIf{flp, matchExprp->cloneTreePure(false), FileLine* const flp = assertp->fileline();
passsp->cloneTree(false), nullptr}); AstIf* const ifp = new AstIf{flp, matchExprp, passsp, nullptr};
assertp->addPasssp(ifp);
// Fail-handler prefix for overlapping instances (IEEE 16.12): // Fail-handler prefix for overlapping instances (IEEE 16.12):
// fires when reject=1 && match=1 in the same cycle. // fires when reject=1 && match=1 in the same cycle.
if (AstNode* const failsp = assertAssertp->failsp()) { if (AstNode* const failsp = assertp->failsp()) {
failsp->addHereThisAsNext( failsp->addHereThisAsNext(ifp->cloneTree(false));
new AstIf{flp, matchExprp, passsp->cloneTree(false), nullptr});
} else {
VL_DO_DANGLING(pushDeletep(matchExprp), matchExprp);
} }
VL_DO_DANGLING(pushDeletep(passsp), passsp);
} }
// Extra fail-handler fires for simultaneous required-step failures if (threadFailCountp) {
// (IEEE 1800-2023: fail handler fires once per failing thread). UASSERT_OBJ(threadFailReplaySenTreep, assertp,
// perSrcSenTreep is set only when requiredStepSrcs.size() >= 2, and "Thread fail count missing sensitivity tree");
// requiredStepSrcs is populated only when assertWithFailp->failsp() is non-null. AstNode* const failsp = assertp->failsp();
if (perSrcSenTreep) { FileLine* const flp = assertp->fileline();
AstNode* const failsp = assertWithFailp->failsp(); // IEEE 1800-2023 16.12 requires one action-block evaluation per failed
AstNodeExpr* cumulativeOrp = requiredStepSrcs[0]->cloneTreePure(false); // thread. AstAssert handles the first, so replay the rest here.
for (size_t i = 1; i < requiredStepSrcs.size(); ++i) { AstVar* const remainingFailCountVarp
AstNodeExpr* const srcp = requiredStepSrcs[i]; = new AstVar{flp, VVarType::BLOCKTEMP, "__VnfaRemainingFailCount",
AstNodeExpr* const condp = new AstLogAnd{flp, srcp->cloneTreePure(false), m_modp->findBasicDType(VBasicDTypeKwd::UINT32)};
cumulativeOrp->cloneTreePure(false)}; remainingFailCountVarp->lifetime(VLifetime::AUTOMATIC_EXPLICIT);
m_modp->addStmtsp( AstBegin* const replayBlockp = new AstBegin{flp, "", remainingFailCountVarp, true};
new AstAlways{flp, VAlwaysKwd::ALWAYS, perSrcSenTreep->cloneTree(false), replayBlockp->addStmtsp(
new AstIf{flp, condp, new AstAssign{flp, new AstVarRef{flp, remainingFailCountVarp, VAccess::WRITE},
newIfAssertFailOn(failsp->cloneTree(true), threadFailCountp});
assertWithFailp->directive(), AstLoop* const replayLoopp = new AstLoop{flp};
assertWithFailp->userType()), replayLoopp->addStmtsp(new AstLoopTest{
nullptr}}); flp, replayLoopp,
cumulativeOrp = new AstLogOr{flp, cumulativeOrp, srcp->cloneTreePure(false)}; new AstGt{flp, new AstVarRef{flp, remainingFailCountVarp, VAccess::READ},
} newTypedConstp(flp, remainingFailCountVarp->dtypep(), 1)}});
VL_DO_DANGLING(pushDeletep(cumulativeOrp), cumulativeOrp); replayLoopp->addStmtsp(newIfAssertFailOn(failsp->cloneTree(true), assertp->directive(),
VL_DO_DANGLING(pushDeletep(perSrcSenTreep), perSrcSenTreep); assertp->userType()));
AstSub* const decrementedFailCountp
= new AstSub{flp, new AstVarRef{flp, remainingFailCountVarp, VAccess::READ},
newTypedConstp(flp, remainingFailCountVarp->dtypep(), 1)};
replayLoopp->addStmtsp(
new AstAssign{flp, new AstVarRef{flp, remainingFailCountVarp, VAccess::WRITE},
decrementedFailCountp});
replayBlockp->addStmtsp(replayLoopp);
m_modp->addStmtsp(
new AstAlways{flp, VAlwaysKwd::ALWAYS, threadFailReplaySenTreep, replayBlockp});
} }
for (AstNodeExpr* const srcp : requiredStepSrcs) pushDeletep(srcp);
} }
// Replace one VarRef to a captured local var with $past(rhs, K) // Replace one VarRef to a captured local var with $past(rhs, K)
@ -3037,27 +3115,24 @@ class AssertNfaVisitor final : public VNVisitor {
const bool needMatch = assertAssertp && assertAssertp->passsp() const bool needMatch = assertAssertp && assertAssertp->passsp()
&& (!parts.hasImplication || splitImplicationPasssp); && (!parts.hasImplication || splitImplicationPasssp);
AstAssert* const assertWithFailp = VN_CAST(assertp, Assert); const bool needsThreadFailReplay
const bool needPerSrcFail = assertAssertp && assertAssertp->failsp() && !parts.hasImplication;
= !isCover && !parts.hasImplication && assertWithFailp && assertWithFailp->failsp();
std::vector<AstNodeExpr*> requiredStepSrcs;
// For `cover sequence` (IEEE 1800-2023 16.14.3) collect per-edge match // For `cover sequence` (IEEE 1800-2023 16.14.3) collect per-edge match
// signals so each end-of-match fires the action independently, rather // signals so each end-of-match fires the action independently, rather
// than getting OR-folded into a single per-cycle terminalActive. // than getting OR-folded into a single per-cycle terminalActive.
// coverp / isCoverSeq are computed earlier (passed to SvaNfaBuilder). // coverp / isCoverSeq are computed earlier (passed to SvaNfaBuilder).
std::vector<AstNodeExpr*> perMidSrcs; std::vector<AstNodeExpr*> perMidSrcs;
const auto signals = m_loweringp->lower(assertp, graph, senTreep, result.finalCondp, const auto signals = m_loweringp->lower(
disableExprp, disableCntVarp, snapshotVarp, assertp, graph, senTreep, result.finalCondp, disableExprp, disableCntVarp,
needPerSrcFail ? &requiredStepSrcs : nullptr, snapshotVarp, needsThreadFailReplay, needsThreadFailReplay && !negated,
isCoverSeq ? &perMidSrcs : nullptr); isCoverSeq ? &perMidSrcs : nullptr);
AstNodeExpr* matchExprp = nullptr; AstNodeExpr* matchExprp = nullptr;
AstNodeExpr* const outputExprp = m_loweringp->assembleResult( AstNodeExpr* const outputExprp = m_loweringp->assembleResult(
assertp, negated, result.finalCondp, signals, needMatch ? &matchExprp : nullptr); assertp, negated, result.finalCondp, signals, needMatch ? &matchExprp : nullptr);
AstSenTree* const perSrcSenTreep AstSenTree* const threadFailReplaySenTreep
= (requiredStepSrcs.size() >= 2) ? senTreep->cloneTree(false) : nullptr; = signals.threadFailCountp ? senTreep->cloneTree(false) : nullptr;
if (senTreeOwned) VL_DO_DANGLING(pushDeletep(senTreep), senTreep); if (senTreeOwned) VL_DO_DANGLING(pushDeletep(senTreep), senTreep);
if (disableExprUnlinked) VL_DO_DANGLING(pushDeletep(disableExprp), disableExprp); if (disableExprUnlinked) VL_DO_DANGLING(pushDeletep(disableExprp), disableExprp);
@ -3066,9 +3141,8 @@ class AssertNfaVisitor final : public VNVisitor {
if (splitImplicationPasssp) { if (splitImplicationPasssp) {
splitImplicationPassActions(assertAssertp, parts, matchExprp); splitImplicationPassActions(assertAssertp, parts, matchExprp);
} else { } else {
attachMatchHandlers(flp, assertAssertp, assertWithFailp, attachActionHandlers(assertAssertp, matchExprp, threadFailReplaySenTreep,
needMatch ? matchExprp : nullptr, perSrcSenTreep, signals.threadFailCountp);
requiredStepSrcs);
} }
if (isCoverSeq && perMidSrcs.size() > 1) { if (isCoverSeq && perMidSrcs.size() > 1) {

2
test_regress/t/t_prop_always_wide.py
View File

@ -11,6 +11,8 @@ import vltest_bootstrap
test.scenarios('vlt') test.scenarios('vlt')
test.sim_time = 11000
test.compile() test.compile()
test.execute() test.execute()

40
test_regress/t/t_prop_always_wide.v
View File

@ -15,13 +15,39 @@ module t (
int cyc = 0; int cyc = 0;
logic a_high = 1'b1, b_high = 1'b1, c_high = 1'b1; logic a_high = 1'b1, b_high = 1'b1, c_high = 1'b1;
wire a_drop = cyc != 1025;
int nested_or_fail_q[$];
int negated_fail_q[$];
int narrow_fail_q[$];
int wide_fail_q[$];
int wide_pass_q[$]; int wide_pass_q[$];
int wide_ring_pass_q[$];
// Wide range with multi-operand pure propp -- exercises the shared // Wide range with multi-operand pure propp -- exercises the shared
// $sampled(propp) hoist path; pre-fix would clone propp 33 times. // $sampled(propp) hoist path; pre-fix would clone propp 33 times.
assert property (@(posedge clk) always[1: 33] (a_high && b_high && c_high)) assert property (@(posedge clk) always[1: 33] (a_high && b_high && c_high))
wide_pass_q.push_back(cyc); wide_pass_q.push_back(cyc);
// Wide range exercises the fixed-delay ring-buffer path
assert property (@(posedge clk) always[1:1025] (a_high && b_high && c_high))
wide_ring_pass_q.push_back(cyc);
// All 1025 live threads fail together when a_drop falls.
assert property (@(posedge clk) always[1:1025] a_drop)
else wide_fail_q.push_back(cyc);
// A one-cycle remainder uses a scalar state instead of a ring.
assert property (@(posedge clk) always[1:2] a_drop)
else narrow_fail_q.push_back(cyc);
// A nested always may fail without rejecting a successful property or.
assert property (@(posedge clk) (always [0:1] 1'b0) or a_high)
else nested_or_fail_q.push_back(cyc);
// The same drop passes a negated always; it must not replay fail actions.
assert property (@(posedge clk) not always[1:1025] a_drop)
else negated_fail_q.push_back(cyc);
always @(posedge clk) begin always @(posedge clk) begin
cyc <= cyc + 1; cyc <= cyc + 1;
if (cyc == 49) begin if (cyc == 49) begin
@ -29,6 +55,20 @@ module t (
`checkd(wide_pass_q.size(), 17); `checkd(wide_pass_q.size(), 17);
`checkd(wide_pass_q[0], 33); `checkd(wide_pass_q[0], 33);
`checkd(wide_pass_q[$], 49); `checkd(wide_pass_q[$], 49);
end
if (cyc == 1041) begin
// Constant-true [1:1025]: K=0..16 succeed at cyc K+1025 = 1025..1041.
`checkd(wide_ring_pass_q.size(), 17);
`checkd(wide_ring_pass_q[0], 1025);
`checkd(wide_ring_pass_q[$], 1041);
`checkd(wide_fail_q.size(), 1025);
`checkd(wide_fail_q[0], 1025);
`checkd(wide_fail_q[$], 1025);
`checkd(narrow_fail_q.size(), 2);
`checkd(narrow_fail_q[0], 1025);
`checkd(narrow_fail_q[$], 1025);
`checkd(nested_or_fail_q.size(), 0);
`checkd(negated_fail_q.size(), 0);
$write("*-* All Finished *-*\n"); $write("*-* All Finished *-*\n");
$finish; $finish;
end end

2
test_regress/t/t_prop_s_always_liveness.v
View File

@ -23,6 +23,8 @@ module t (
// The youngest [2:5] windows are still open at $finish, so strong s_always // The youngest [2:5] windows are still open at $finish, so strong s_always
// reports a liveness failure even with a_high always 1; weak always does not. // reports a liveness failure even with a_high always 1; weak always does not.
assert property (@(posedge clk) s_always [2:5] a_high); assert property (@(posedge clk) s_always [2:5] a_high);
assert property (@(posedge clk) s_always [2:1026] a_high);
assert property (@(posedge clk) s_always [2:3] a_high);
assert property (@(posedge clk) always [2:5] a_high); assert property (@(posedge clk) always [2:5] a_high);
assert property (@(posedge clk) s_always [2:5] a_low) assert property (@(posedge clk) s_always [2:5] a_low)