Fix NFA assertion crash and mis-counted property if/case (#8074)
This commit is contained in:
Yilou Wang
GitHub
parent
b032379de2
commit
8a29360ade
|
|
@ -21,6 +21,9 @@
|
|||
// - Replace converted assertions with combinational match/reject checks
|
||||
// so V3AssertPre sees no multi-cycle SExpr (unsupported ones fall through).
|
||||
//
|
||||
// Members marked OWNED hold an AST tree this pass allocated and must delete;
|
||||
// they are not linked into the netlist.
|
||||
//
|
||||
//*************************************************************************
|
||||
|
||||
#include "V3PchAstNoMT.h" // VL_MT_DISABLED_CODE_UNIT
|
||||
|
|
@ -55,7 +58,7 @@ struct SvaVertexData final {
|
|||
AstVar* delayRingWrappedVarp = nullptr; // All slots written since the last clear
|
||||
AstVar* doneLVarp = nullptr; // SAnd LHS 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
|
||||
bool needsReg = false; // True if vertex has incoming clocked edge
|
||||
};
|
||||
|
||||
|
|
@ -65,12 +68,14 @@ class SvaStateVertex final : public V3GraphVertex {
|
|||
public:
|
||||
// True if this is the sequence-match terminal vertex
|
||||
bool m_isMatch = false;
|
||||
// Owned throughout-guard condition clones; IEEE 1800-2023 16.9.9
|
||||
// OWNED throughout-guard condition clones; IEEE 1800-2023 16.9.9
|
||||
std::vector<AstNodeExpr*> m_throughoutConds;
|
||||
// Nonzero for a bitset ring-buffer vertex for ## delays.
|
||||
bool m_isFixedDelayRing = false;
|
||||
int m_delayRingSize = 0; // Fixed delay cycles. Range: max-min+1.
|
||||
AstNodeExpr* m_delayRingClearCondp = nullptr; // local RHS for pure-boolean range
|
||||
// OWNED; enclosing-abort fire condition clearing in-flight ring bits
|
||||
AstNodeExpr* m_abortClearp = nullptr;
|
||||
// Liveness terminal (IEEE weak semantics): reject must not fire from this source
|
||||
bool m_isUnbounded = false;
|
||||
// Temporal sequence AND combiner; IEEE 1800-2023 16.9.5
|
||||
|
|
@ -95,6 +100,7 @@ public:
|
|||
for (AstNodeExpr* cp : m_throughoutConds) VL_DO_DANGLING(cp->deleteTree(), cp);
|
||||
if (m_delayRingClearCondp)
|
||||
VL_DO_DANGLING(m_delayRingClearCondp->deleteTree(), m_delayRingClearCondp);
|
||||
if (m_abortClearp) VL_DO_DANGLING(m_abortClearp->deleteTree(), m_abortClearp);
|
||||
if (m_andLhsCondp) VL_DO_DANGLING(m_andLhsCondp->deleteTree(), m_andLhsCondp);
|
||||
if (m_andRhsCondp) VL_DO_DANGLING(m_andRhsCondp->deleteTree(), m_andRhsCondp);
|
||||
}
|
||||
|
|
@ -183,8 +189,8 @@ public:
|
|||
std::vector<const SvaTransEdge*> allEdges() const {
|
||||
std::vector<const SvaTransEdge*> result;
|
||||
for (const V3GraphVertex& vtxr : m_graph.vertices()) {
|
||||
for (const V3GraphEdge& er : vtxr.outEdges()) {
|
||||
result.push_back(static_cast<const SvaTransEdge*>(&er));
|
||||
for (const V3GraphEdge& edger : vtxr.outEdges()) {
|
||||
result.push_back(static_cast<const SvaTransEdge*>(&edger));
|
||||
}
|
||||
}
|
||||
return result;
|
||||
|
|
@ -208,6 +214,11 @@ struct BuildResult final {
|
|||
static BuildResult failWithError() { return {nullptr, nullptr, {}, true}; }
|
||||
};
|
||||
|
||||
// Parser-marked SAnd of overlapped implications: a property if/else/case.
|
||||
static bool hasPropertyControlConjunction(const AstNodeExpr* nodep) {
|
||||
return nodep->exists([](const AstSAnd* andp) { return andp->propertyControl(); });
|
||||
}
|
||||
|
||||
static AstConst* newTypedConstp(FileLine* const flp, const AstNodeDType* const dtypep,
|
||||
const uint32_t value) {
|
||||
AstConst* const constp = new AstConst{flp, AstConst::DTyped{}, dtypep};
|
||||
|
|
@ -722,6 +733,7 @@ class SvaNfaBuilder final {
|
|||
// Do not mark liveness sources: first boolean check is deferred.
|
||||
edgep->m_rejectOnFail = true;
|
||||
}
|
||||
freeUnlinkedCondp(pre.finalCondp);
|
||||
currentp = condVtxp;
|
||||
} else {
|
||||
currentp = pre.termVertexp;
|
||||
|
|
@ -965,12 +977,20 @@ class SvaNfaBuilder final {
|
|||
return {mergeVtxp, nullptr, {}};
|
||||
}
|
||||
|
||||
// Free a dropped sub-result condition that is not linked into the AST
|
||||
// (abort folds synthesize unparented finalCondp trees).
|
||||
static void freeUnlinkedCondp(AstNodeExpr* condp) {
|
||||
if (condp && !condp->backp()) VL_DO_DANGLING(condp->deleteTree(), condp);
|
||||
}
|
||||
|
||||
// Build merge vertex for SOr / LogOr: both branches feed into one vertex.
|
||||
BuildResult buildOrMerge(AstNodeExpr* lhsp, AstNodeExpr* rhsp, SvaStateVertex* entryVtxp,
|
||||
FileLine* flp) {
|
||||
const BuildResult lhs = buildExpr(lhsp, entryVtxp);
|
||||
const BuildResult rhs = buildExpr(rhsp, entryVtxp);
|
||||
if (!lhs.valid() || !rhs.valid()) { // LCOV_EXCL_START -- sub-build fail bail
|
||||
freeUnlinkedCondp(lhs.finalCondp);
|
||||
freeUnlinkedCondp(rhs.finalCondp);
|
||||
return BuildResult::fail(lhs.errorEmitted || rhs.errorEmitted);
|
||||
} // LCOV_EXCL_STOP
|
||||
// IEEE 1800-2023 16.14.3: a cover sequence counts every end-of-match. A
|
||||
|
|
@ -980,6 +1000,8 @@ class SvaNfaBuilder final {
|
|||
// is handled by the OR-fold.
|
||||
if (m_isCoverSeq && (lhs.termVertexp != entryVtxp || rhs.termVertexp != entryVtxp)) {
|
||||
warnEndpointUnsupported(flp, "a sequence operand of 'or'");
|
||||
freeUnlinkedCondp(lhs.finalCondp);
|
||||
freeUnlinkedCondp(rhs.finalCondp);
|
||||
return BuildResult::failWithError();
|
||||
}
|
||||
SvaStateVertex* const mergeVtxp = scopedCreateVertex();
|
||||
|
|
@ -995,6 +1017,8 @@ class SvaNfaBuilder final {
|
|||
} else {
|
||||
guardedLink(rhs.termVertexp, mergeVtxp, flp);
|
||||
}
|
||||
freeUnlinkedCondp(lhs.finalCondp);
|
||||
freeUnlinkedCondp(rhs.finalCondp);
|
||||
return {mergeVtxp, nullptr, {}};
|
||||
}
|
||||
|
||||
|
|
@ -1010,6 +1034,8 @@ class SvaNfaBuilder final {
|
|||
const bool rhsScope = m_inUnboundedScope;
|
||||
m_inUnboundedScope = savedScope || lhsScope || rhsScope;
|
||||
if (!lhs.valid() || !rhs.valid()) { // LCOV_EXCL_START -- sub-build fail bail
|
||||
freeUnlinkedCondp(lhs.finalCondp);
|
||||
freeUnlinkedCondp(rhs.finalCondp);
|
||||
return BuildResult::fail(lhs.errorEmitted || rhs.errorEmitted);
|
||||
} // LCOV_EXCL_STOP
|
||||
|
||||
|
|
@ -1021,12 +1047,20 @@ class SvaNfaBuilder final {
|
|||
"Single-cycle SAnd operands must have finalCondp");
|
||||
AstNodeExpr* const condp = new AstLogAnd{flp, lhs.finalCondp->cloneTreePure(false),
|
||||
rhs.finalCondp->cloneTreePure(false)};
|
||||
freeUnlinkedCondp(lhs.finalCondp);
|
||||
freeUnlinkedCondp(rhs.finalCondp);
|
||||
return {entryVtxp, condp, {}};
|
||||
}
|
||||
// Range-delay mid-window sources in either sub-branch would need
|
||||
// to be folded into the latch's match-now signal, which the
|
||||
// current combiner does not support. Defer (UNSUPPORTED).
|
||||
if (!lhs.midSources.empty() || !rhs.midSources.empty()) return BuildResult::fail();
|
||||
// current combiner does not support.
|
||||
if (!lhs.midSources.empty() || !rhs.midSources.empty()) {
|
||||
flp->v3warn(E_UNSUPPORTED,
|
||||
"Unsupported: ranged cycle delay in an operand of property 'and'");
|
||||
freeUnlinkedCondp(lhs.finalCondp);
|
||||
freeUnlinkedCondp(rhs.finalCondp);
|
||||
return BuildResult::failWithError();
|
||||
}
|
||||
SvaStateVertex* const combVtxp = scopedCreateVertex();
|
||||
combVtxp->m_isAndCombiner = true;
|
||||
combVtxp->m_andLhsTermp = lhs.termVertexp;
|
||||
|
|
@ -1064,6 +1098,8 @@ class SvaNfaBuilder final {
|
|||
}
|
||||
}
|
||||
}
|
||||
freeUnlinkedCondp(lhs.finalCondp);
|
||||
freeUnlinkedCondp(rhs.finalCondp);
|
||||
return {combVtxp, nullptr, {}};
|
||||
}
|
||||
|
||||
|
|
@ -1421,16 +1457,74 @@ class SvaNfaBuilder final {
|
|||
return resultp;
|
||||
}
|
||||
|
||||
// True when a same-tick Link chain already accounts the attempt: a
|
||||
// required-step Link covers both outcomes; followed-by pairs both edges.
|
||||
static bool chainAccountsSource(const SvaStateVertex* srcp,
|
||||
const std::unordered_set<const V3GraphEdge*>& preEdges) {
|
||||
bool plainNonSink = false;
|
||||
bool markedSink = false;
|
||||
for (const V3GraphEdge& edger : srcp->outEdges()) {
|
||||
if (preEdges.count(&edger)) continue;
|
||||
const SvaTransEdge& tedger = static_cast<const SvaTransEdge&>(edger);
|
||||
if (tedger.m_consumesCycle) continue;
|
||||
const bool sink = static_cast<const SvaStateVertex*>(tedger.toVtxp())->m_isRejectSink;
|
||||
if (tedger.m_rejectOnFail) {
|
||||
if (!sink) return true;
|
||||
markedSink = true;
|
||||
} else if (!sink) {
|
||||
plainNonSink = true;
|
||||
}
|
||||
}
|
||||
return plainNonSink && markedSink;
|
||||
}
|
||||
|
||||
// Reject edge: fires when the source is live and the abort samples true.
|
||||
void addAbortRejectEdge(SvaStateVertex* srcp, SvaStateVertex* sinkp, AstNodeExpr* condp,
|
||||
FileLine* flp) {
|
||||
AstNodeExpr* const notFirep = new AstLogNot{flp, sampled(abortFireExpr(condp, flp))};
|
||||
m_graph.addLink(srcp, sinkp, notFirep)->m_rejectOnFail = true;
|
||||
return;
|
||||
}
|
||||
|
||||
// On the fire tick: kill body threads; accept kinds also forgive step misses.
|
||||
void gateBodyEdgesOnAbort(const std::unordered_set<const V3GraphEdge*>& preEdges,
|
||||
AstNodeExpr* condp, VAbortKind kind, FileLine* flp) {
|
||||
for (V3GraphVertex& vtxr : m_graph.m_graph.vertices()) {
|
||||
for (V3GraphEdge& edger : vtxr.outEdges()) {
|
||||
if (preEdges.count(&edger)) continue;
|
||||
SvaTransEdge* const tedgep = static_cast<SvaTransEdge*>(&edger);
|
||||
if (tedgep->m_rejectOnFail) {
|
||||
if (!kind.isAccept()) continue;
|
||||
AstNodeExpr* const firep = sampled(abortFireExpr(condp, flp));
|
||||
tedgep->m_condp
|
||||
= tedgep->m_condp ? new AstLogOr{flp, tedgep->m_condp, firep} : firep;
|
||||
} else if (tedgep->m_consumesCycle) {
|
||||
AstNodeExpr* const notFirep
|
||||
= new AstLogNot{flp, sampled(abortFireExpr(condp, flp))};
|
||||
tedgep->m_condp = tedgep->m_condp
|
||||
? new AstLogAnd{flp, tedgep->m_condp, notFirep}
|
||||
: notFirep;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
BuildResult buildAbortOn(AstNodeExpr* condp, AstNodeExpr* bodyp, SvaStateVertex* entryVtxp,
|
||||
VAbortKind kind, FileLine* flp) {
|
||||
// Snapshot pre-body vertices so post-build diff yields the body's sub-NFA.
|
||||
VAbortKind kind, FileLine* flp, bool isTopLevelStep) {
|
||||
// Snapshot pre-body vertices/edges so post-build diff yields the body's sub-NFA.
|
||||
std::unordered_set<const V3GraphVertex*> preExisting;
|
||||
for (const V3GraphVertex& vtxr : m_graph.m_graph.vertices()) preExisting.insert(&vtxr);
|
||||
std::unordered_set<const V3GraphEdge*> preEdges;
|
||||
for (V3GraphVertex& vtxr : m_graph.m_graph.vertices()) {
|
||||
preExisting.insert(&vtxr);
|
||||
for (V3GraphEdge& edger : vtxr.outEdges()) preEdges.insert(&edger);
|
||||
}
|
||||
|
||||
m_outerAbortStack.push_back(condp);
|
||||
const BuildResult bodyResult = buildExpr(bodyp, entryVtxp, /*isTopLevelStep=*/false);
|
||||
const BuildResult bodyResult = buildExpr(bodyp, entryVtxp, isTopLevelStep);
|
||||
m_outerAbortStack.pop_back();
|
||||
UASSERT_OBJ(bodyResult.valid(), bodyp, "abort body must be a valid SVA expression");
|
||||
if (!bodyResult.valid()) return bodyResult;
|
||||
|
||||
gateBodyEdgesOnAbort(preEdges, condp, kind, flp);
|
||||
|
||||
// Live-thread sources for the abort edge: entry + new body vertices,
|
||||
// minus reject sinks (they carry reject fuel, not live-thread fuel).
|
||||
|
|
@ -1439,6 +1533,11 @@ class SvaNfaBuilder final {
|
|||
for (V3GraphVertex& vtxr : m_graph.m_graph.vertices()) {
|
||||
if (preExisting.count(&vtxr)) continue;
|
||||
auto* const sp = static_cast<SvaStateVertex*>(&vtxr);
|
||||
if (sp->m_delayRingSize) {
|
||||
AstNodeExpr* const firep = abortFireExpr(condp, flp);
|
||||
sp->m_abortClearp
|
||||
= sp->m_abortClearp ? new AstLogOr{flp, sp->m_abortClearp, firep} : firep;
|
||||
}
|
||||
if (sp->m_isRejectSink) continue;
|
||||
abortSources.push_back(sp);
|
||||
}
|
||||
|
|
@ -1450,15 +1549,18 @@ class SvaNfaBuilder final {
|
|||
|
||||
if (kind.isAccept()) {
|
||||
// Match-only sink fed by $sampled(abort-fire) from every live source;
|
||||
// registered as midSource so it never contributes a reject. The body
|
||||
// terminal is already in abortSources, so we don't fold abort-fire
|
||||
// into bodyResult.finalCondp.
|
||||
// registered as midSource so it never contributes a reject.
|
||||
SvaStateVertex* const acceptSinkp = scopedCreateVertex();
|
||||
for (SvaStateVertex* const srcp : abortSources)
|
||||
guardedLink(srcp, acceptSinkp, sampledAbortFire(), flp);
|
||||
std::vector<SvaStateVertex*> midSources = bodyResult.midSources;
|
||||
midSources.push_back(acceptSinkp);
|
||||
return {bodyResult.termVertexp, bodyResult.finalCondp, std::move(midSources)};
|
||||
AstNodeExpr* finalCondp = bodyResult.finalCondp;
|
||||
if (finalCondp) {
|
||||
if (finalCondp->backp()) finalCondp = finalCondp->cloneTreePure(false);
|
||||
finalCondp = new AstLogOr{flp, finalCondp, abortFireExpr(condp, flp)};
|
||||
}
|
||||
return {bodyResult.termVertexp, finalCondp, std::move(midSources)};
|
||||
}
|
||||
|
||||
// rejectOnFail treats m_condp as the success condition and fires on
|
||||
|
|
@ -1466,10 +1568,15 @@ class SvaNfaBuilder final {
|
|||
SvaStateVertex* const rejectSinkp = m_graph.createStateVertex();
|
||||
rejectSinkp->m_isRejectSink = true;
|
||||
for (SvaStateVertex* const srcp : abortSources)
|
||||
m_graph.addLink(srcp, rejectSinkp, new AstLogNot{flp, sampledAbortFire()})
|
||||
->m_rejectOnFail
|
||||
= true;
|
||||
return bodyResult;
|
||||
if (!chainAccountsSource(srcp, preEdges))
|
||||
addAbortRejectEdge(srcp, rejectSinkp, condp, flp);
|
||||
AstNodeExpr* finalCondp = bodyResult.finalCondp;
|
||||
if (finalCondp) {
|
||||
if (finalCondp->backp()) finalCondp = finalCondp->cloneTreePure(false);
|
||||
finalCondp
|
||||
= new AstLogAnd{flp, finalCondp, new AstLogNot{flp, abortFireExpr(condp, flp)}};
|
||||
}
|
||||
return {bodyResult.termVertexp, finalCondp, bodyResult.midSources};
|
||||
}
|
||||
|
||||
public:
|
||||
|
|
@ -1482,10 +1589,11 @@ public:
|
|||
, m_isSeqEvent{isSeqEvent} {}
|
||||
|
||||
// Reset scope between antecedent and consequent: liveness must not leak.
|
||||
// m_outerAbortStack survives: an abort wrapping the implication covers the
|
||||
// consequent too (IEEE 1800-2023 16.12.14).
|
||||
void resetScope() {
|
||||
m_inUnboundedScope = false;
|
||||
m_temporalGuardStack.clear();
|
||||
m_outerAbortStack.clear();
|
||||
}
|
||||
|
||||
BuildResult buildExpr(AstNodeExpr* nodep, SvaStateVertex* entryVtxp,
|
||||
|
|
@ -1540,7 +1648,8 @@ public:
|
|||
return buildSWithin(withinp, entryVtxp, isTopLevelStep);
|
||||
}
|
||||
if (AstAbortOn* const ap = VN_CAST(nodep, AbortOn)) {
|
||||
return buildAbortOn(ap->condp(), ap->propp(), entryVtxp, ap->kind(), ap->fileline());
|
||||
return buildAbortOn(ap->condp(), ap->propp(), entryVtxp, ap->kind(), ap->fileline(),
|
||||
isTopLevelStep);
|
||||
}
|
||||
if (VN_IS(nodep, SNonConsRep)) return BuildResult::fail();
|
||||
if (AstImplication* const implp = VN_CAST(nodep, Implication)) {
|
||||
|
|
@ -1746,21 +1855,19 @@ class SvaNfaLowering final {
|
|||
// latches the OR of its incoming contributions.
|
||||
void emitStateRegisterNba(LowerCtx& c) {
|
||||
AstNode* bodyp = nullptr;
|
||||
bool hasDelayRing = false;
|
||||
for (int i = 0; i < c.N; ++i) {
|
||||
if (c.vtx[i]->datap()->delayRingVarp) hasDelayRing = true;
|
||||
if (!c.vtx[i]->datap()->stateVarp) continue;
|
||||
|
||||
AstNodeExpr* nextStatep = nullptr;
|
||||
for (const V3GraphEdge& er : c.vtx[i]->inEdges()) {
|
||||
const SvaTransEdge& te = static_cast<const SvaTransEdge&>(er);
|
||||
if (!te.m_consumesCycle) continue;
|
||||
const int fromIdx = te.fromVtxp()->color();
|
||||
UASSERT_OBJ(c.vtx[fromIdx]->datap()->stateSigp, te.fromVtxp(),
|
||||
for (const V3GraphEdge& edger : c.vtx[i]->inEdges()) {
|
||||
const SvaTransEdge& tedger = static_cast<const SvaTransEdge&>(edger);
|
||||
if (!tedger.m_consumesCycle) continue;
|
||||
const int fromIdx = tedger.fromVtxp()->color();
|
||||
UASSERT_OBJ(c.vtx[fromIdx]->datap()->stateSigp, tedger.fromVtxp(),
|
||||
"Clocked-edge source missing stateSig");
|
||||
|
||||
AstNodeExpr* srcSigp = c.vtx[fromIdx]->datap()->stateSigp->cloneTreePure(false);
|
||||
srcSigp = andCond(c.flp, srcSigp, te.m_condp);
|
||||
srcSigp = andCond(c.flp, srcSigp, tedger.m_condp);
|
||||
|
||||
if (c.disableExprp) {
|
||||
AstNodeExpr* const notDisp
|
||||
|
|
@ -1781,8 +1888,8 @@ class SvaNfaLowering final {
|
|||
}
|
||||
|
||||
// Capture disableCnt in Phase-2 NBA before any reactive re-evaluation.
|
||||
// snapshotVarp and disableCntVarp are allocated together.
|
||||
if (c.snapshotVarp && (bodyp || hasDelayRing)) {
|
||||
// Emitted even for stateless graphs; snapshotOk gates rejects there too.
|
||||
if (c.snapshotVarp) {
|
||||
UASSERT_OBJ(c.disableCntVarp, c.senTreep, "snapshotVarp set without disableCntVarp");
|
||||
// disable_snapshot <= disable_count;
|
||||
AstAssignDly* const snapshotp
|
||||
|
|
@ -1807,15 +1914,15 @@ class SvaNfaLowering final {
|
|||
const uint32_t size = static_cast<uint32_t>(vtxp->m_delayRingSize);
|
||||
|
||||
AstNodeExpr* incomingp = nullptr;
|
||||
for (const SvaTransEdge* const tep : c.edges) {
|
||||
if (static_cast<int>(tep->toVtxp()->color()) != ri) continue;
|
||||
UASSERT_OBJ(tep->m_consumesCycle == vtxp->m_isFixedDelayRing, vtxp,
|
||||
for (const SvaTransEdge* const tedgep : c.edges) {
|
||||
if (static_cast<int>(tedgep->toVtxp()->color()) != ri) continue;
|
||||
UASSERT_OBJ(tedgep->m_consumesCycle == vtxp->m_isFixedDelayRing, vtxp,
|
||||
"Delay-ring incoming edge kind mismatch");
|
||||
const int fi = tep->fromVtxp()->color();
|
||||
const int fi = tedgep->fromVtxp()->color();
|
||||
UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp, c.vtx[fi],
|
||||
"Delay-ring incoming source missing stateSig");
|
||||
AstNodeExpr* contribp = c.vtx[fi]->datap()->stateSigp->cloneTreePure(false);
|
||||
contribp = andCond(c.flp, contribp, tep->m_condp);
|
||||
contribp = andCond(c.flp, contribp, tedgep->m_condp);
|
||||
if (c.disableExprp) {
|
||||
AstNodeExpr* const notDisp
|
||||
= new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)};
|
||||
|
|
@ -1858,6 +1965,10 @@ class SvaNfaLowering final {
|
|||
clearCondp = orExprs(c.flp, clearCondp,
|
||||
sampled(vtxp->m_delayRingClearCondp->cloneTreePure(false)));
|
||||
}
|
||||
if (vtxp->m_abortClearp) {
|
||||
clearCondp = orExprs(c.flp, clearCondp,
|
||||
sampled(vtxp->m_abortClearp->cloneTreePure(false)));
|
||||
}
|
||||
if (c.disableExprp) {
|
||||
clearCondp = orExprs(c.flp, clearCondp, c.disableExprp->cloneTreePure(false));
|
||||
}
|
||||
|
|
@ -1960,14 +2071,14 @@ class SvaNfaLowering final {
|
|||
// end-of-match fires the action independently, no OR-fold).
|
||||
void computeTerminalMatchAndReject(LowerCtx& c, AstNodeExpr* snapshotOkp, SignalSet& sigs,
|
||||
std::vector<AstNodeExpr*>* outPerMidSrcsp = nullptr) {
|
||||
for (const SvaTransEdge* const tep : c.edges) {
|
||||
if (tep->toVtxp() != c.graph.m_matchVertexp) continue;
|
||||
const int fi = tep->fromVtxp()->color();
|
||||
UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp, tep->fromVtxp(),
|
||||
for (const SvaTransEdge* const tedgep : c.edges) {
|
||||
if (tedgep->toVtxp() != c.graph.m_matchVertexp) continue;
|
||||
const int fi = tedgep->fromVtxp()->color();
|
||||
UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp, tedgep->fromVtxp(),
|
||||
"Terminal-link source missing stateSig");
|
||||
|
||||
AstNodeExpr* srcSigp = c.vtx[fi]->datap()->stateSigp->cloneTreePure(false);
|
||||
srcSigp = andCond(c.flp, srcSigp, tep->m_condp);
|
||||
srcSigp = andCond(c.flp, srcSigp, tedgep->m_condp);
|
||||
if (snapshotOkp) {
|
||||
srcSigp = new AstLogAnd{c.flp, srcSigp, snapshotOkp->cloneTreePure(false)};
|
||||
}
|
||||
|
|
@ -1984,19 +2095,19 @@ class SvaNfaLowering final {
|
|||
outPerMidSrcsp->push_back(perMidp);
|
||||
}
|
||||
|
||||
if (tep->fromVtxp()->m_delayRingSize && !tep->fromVtxp()->m_isFixedDelayRing) {
|
||||
if (tedgep->fromVtxp()->m_delayRingSize && !tedgep->fromVtxp()->m_isFixedDelayRing) {
|
||||
sigs.terminalActivep
|
||||
= orExprs(c.flp, sigs.terminalActivep, srcSigp->cloneTreePure(false));
|
||||
// reject |= ring[next_idx] && final_condition;
|
||||
AstNodeExpr* expireContribp = delayRingOutput(c.flp, tep->fromVtxp());
|
||||
expireContribp = andCond(c.flp, expireContribp, tep->m_condp);
|
||||
AstNodeExpr* expireContribp = delayRingOutput(c.flp, tedgep->fromVtxp());
|
||||
expireContribp = andCond(c.flp, expireContribp, tedgep->m_condp);
|
||||
if (snapshotOkp) {
|
||||
expireContribp
|
||||
= new AstLogAnd{c.flp, expireContribp, snapshotOkp->cloneTreePure(false)};
|
||||
}
|
||||
sigs.rejectBasep = orExprs(c.flp, sigs.rejectBasep, expireContribp);
|
||||
VL_DO_DANGLING(srcSigp->deleteTree(), srcSigp);
|
||||
} else if (tep->fromVtxp()->m_isUnbounded || tep->fromVtxp()->m_isAndCombiner) {
|
||||
} else if (tedgep->fromVtxp()->m_isUnbounded || tedgep->fromVtxp()->m_isAndCombiner) {
|
||||
sigs.terminalActivep = orExprs(c.flp, sigs.terminalActivep, srcSigp);
|
||||
} else {
|
||||
sigs.terminalActivep
|
||||
|
|
@ -2075,21 +2186,24 @@ class SvaNfaLowering final {
|
|||
// Phase 3a: required-step rejection.
|
||||
// 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->m_condVtxp),
|
||||
tep->fromVtxp(),
|
||||
for (const SvaTransEdge* const tedgep : c.edges) {
|
||||
if (!tedgep->m_rejectOnFail) continue;
|
||||
const int fi = tedgep->fromVtxp()->color();
|
||||
UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp && (tedgep->m_condp || tedgep->m_condVtxp),
|
||||
tedgep->fromVtxp(),
|
||||
"rejectOnFail Link must have condp/condVtxp and source stateSig");
|
||||
AstNodeExpr* const srcSigp = c.vtx[fi]->datap()->stateSigp->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,
|
||||
if (tedgep->m_condVtxp) {
|
||||
const int ci = tedgep->m_condVtxp->color();
|
||||
UASSERT_OBJ(c.vtx[ci]->datap()->stateSigp, tedgep->m_condVtxp,
|
||||
"rejectOnFail condVtxp missing stateSig");
|
||||
condp = c.vtx[ci]->datap()->stateSigp->cloneTreePure(false);
|
||||
if (tedgep->m_condp) {
|
||||
condp = new AstLogOr{c.flp, condp, tedgep->m_condp->cloneTreePure(false)};
|
||||
}
|
||||
} else {
|
||||
condp = tep->m_condp->cloneTreePure(false);
|
||||
condp = tedgep->m_condp->cloneTreePure(false);
|
||||
}
|
||||
AstNodeExpr* const notCondp = new AstLogNot{c.flp, condp};
|
||||
AstNodeExpr* const rawFailp = new AstLogAnd{c.flp, srcSigp, notCondp};
|
||||
|
|
@ -2204,13 +2318,14 @@ class SvaNfaLowering final {
|
|||
// Propagate Link edges
|
||||
for (int fi = 0; fi < c.N; ++fi) {
|
||||
if (!c.vtx[fi]->datap()->stateSigp) continue;
|
||||
for (const V3GraphEdge& er : c.vtx[fi]->outEdges()) {
|
||||
const SvaTransEdge& te = static_cast<const SvaTransEdge&>(er);
|
||||
if (te.m_consumesCycle) continue;
|
||||
const int ti = te.toVtxp()->color();
|
||||
if (te.toVtxp()->m_isMatch || te.toVtxp()->m_isRejectSink) continue;
|
||||
AstNodeExpr* const contributionp = andCond(
|
||||
c.flp, c.vtx[fi]->datap()->stateSigp->cloneTreePure(false), te.m_condp);
|
||||
for (const V3GraphEdge& edger : c.vtx[fi]->outEdges()) {
|
||||
const SvaTransEdge& tedger = static_cast<const SvaTransEdge&>(edger);
|
||||
if (tedger.m_consumesCycle) continue;
|
||||
const int ti = tedger.toVtxp()->color();
|
||||
if (tedger.toVtxp()->m_isMatch || tedger.toVtxp()->m_isRejectSink) continue;
|
||||
AstNodeExpr* const contributionp
|
||||
= andCond(c.flp, c.vtx[fi]->datap()->stateSigp->cloneTreePure(false),
|
||||
tedger.m_condp);
|
||||
if (!c.vtx[ti]->datap()->stateSigp) {
|
||||
c.vtx[ti]->datap()->stateSigp = contributionp;
|
||||
changed = true;
|
||||
|
|
@ -2364,10 +2479,11 @@ public:
|
|||
|
||||
// Identify registered vertices (targets of clocked edges).
|
||||
for (int i = 0; i < N; ++i) {
|
||||
for (const V3GraphEdge& er : vtx[i]->outEdges()) {
|
||||
const SvaTransEdge& te = static_cast<const SvaTransEdge&>(er);
|
||||
const int toIdx = te.toVtxp()->color();
|
||||
if (te.m_consumesCycle && toIdx != matchIdx && !te.toVtxp()->m_isRejectSink) {
|
||||
for (const V3GraphEdge& edger : vtx[i]->outEdges()) {
|
||||
const SvaTransEdge& tedger = static_cast<const SvaTransEdge&>(edger);
|
||||
const int toIdx = tedger.toVtxp()->color();
|
||||
if (tedger.m_consumesCycle && toIdx != matchIdx
|
||||
&& !tedger.toVtxp()->m_isRejectSink) {
|
||||
vtx[toIdx]->datap()->needsReg = true;
|
||||
}
|
||||
}
|
||||
|
|
@ -3019,9 +3135,20 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
return false;
|
||||
}
|
||||
|
||||
void processAssertion(AstNodeCoverOrAssert* assertp) {
|
||||
if (assertp->immediate()) return;
|
||||
// Outcome counts for a property if/case are wrong in an outcome-multiplying
|
||||
// context. Returns that context, or nullptr when the shape is supported.
|
||||
static const char* unsupportedPropertyControl(const AstNodeCoverOrAssert* assertp,
|
||||
const AstNodeExpr* seqBodyp, bool negated) {
|
||||
if (!hasPropertyControlConjunction(seqBodyp)) return nullptr;
|
||||
if (negated) return "negation";
|
||||
if (VN_IS(assertp, Cover)) return "cover";
|
||||
if (VN_AS(assertp, Assert)->passsp()) return "a pass action";
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
// Inline property/sequence refs and reject unsupported shapes.
|
||||
// Returns the PropSpec to lower, or nullptr when fully handled here.
|
||||
AstPropSpec* prepareAssertionProp(AstNodeCoverOrAssert* assertp) {
|
||||
if (AstPropSpec* const specp = VN_CAST(assertp->propp(), PropSpec)) {
|
||||
if (AstFuncRef* const funcrefp = VN_CAST(specp->propp(), FuncRef)) {
|
||||
if (const AstProperty* const propyp = VN_CAST(funcrefp->taskp(), Property)) {
|
||||
|
|
@ -3033,20 +3160,36 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
inlineAllSequenceRefs(assertp->propp());
|
||||
|
||||
if (AstPropSpec* const specp = VN_CAST(assertp->propp(), PropSpec)) {
|
||||
if (hoistClockedSeq(specp)) return;
|
||||
if (hoistClockedSeq(specp)) return nullptr;
|
||||
}
|
||||
|
||||
AstPropSpec* const propp = VN_AS(assertp->propp(), PropSpec);
|
||||
const bool isCover = VN_IS(assertp, Cover);
|
||||
if (!isCover && effectiveAssertPropStrength(propp) == VPropStrength::STRONG) {
|
||||
if (!VN_IS(assertp, Cover)
|
||||
&& effectiveAssertPropStrength(propp) == VPropStrength::STRONG) {
|
||||
propp->v3warn(E_UNSUPPORTED,
|
||||
"Unsupported: strong property in " + assertp->verilogKwd() + ".");
|
||||
replaceBodyOnBuildError(assertp->fileline(), propp, /*errorEmitted=*/true);
|
||||
return;
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
if (!hasMultiCycleExpr(propp)) return;
|
||||
if (isBareTopLevelUntil(propp)) return;
|
||||
if (!hasMultiCycleExpr(propp)) return nullptr;
|
||||
// A nested property instance keeps its body behind the call; lowering would drop it.
|
||||
if (propp->exists([](const AstFuncRef* refp) { return VN_IS(refp->taskp(), Property); })) {
|
||||
assertp->v3warn(E_UNSUPPORTED,
|
||||
"Unsupported: property instance inside a multi-cycle property "
|
||||
"expression");
|
||||
VL_DO_DANGLING(pushDeletep(assertp->unlinkFrBack()), assertp);
|
||||
return nullptr;
|
||||
}
|
||||
if (isBareTopLevelUntil(propp)) return nullptr;
|
||||
return propp;
|
||||
}
|
||||
|
||||
void processAssertion(AstNodeCoverOrAssert* assertp) {
|
||||
if (assertp->immediate()) return;
|
||||
|
||||
AstPropSpec* const propp = prepareAssertionProp(assertp);
|
||||
if (!propp) return;
|
||||
|
||||
PropertyParts parts = decomposeProperty(propp);
|
||||
UASSERT_OBJ(parts.seqExprp, propp, "Property body must be an expression");
|
||||
|
|
@ -3059,6 +3202,9 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
seqBodyp = notp->lhsp();
|
||||
}
|
||||
|
||||
const char* const propertyControlp
|
||||
= unsupportedPropertyControl(assertp, seqBodyp, negated);
|
||||
|
||||
// Substitute property-local match-item refs in consequent with
|
||||
// $past(rhs, K) before NFA build (IEEE 1800-2023 16.10).
|
||||
if (liftMatchItemSubstitutions(parts, seqBodyp)) {
|
||||
|
|
@ -3068,8 +3214,6 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
return;
|
||||
}
|
||||
|
||||
AstSenTree* senTreep = assertp->sentreep();
|
||||
bool senTreeOwned = false; // True if we created senTreep locally
|
||||
AstCover* const coverp = VN_CAST(assertp, Cover);
|
||||
const bool isCoverSeq = coverp && coverp->isCoverSeq();
|
||||
// A sequence event control is not an assertion directive; no default
|
||||
|
|
@ -3082,12 +3226,10 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
if (!propp->disablep() && m_defaultDisablep && !isSeqEvent) {
|
||||
propp->disablep(m_defaultDisablep->condp()->cloneTreePure(true));
|
||||
}
|
||||
if (!senTreep && propp->sensesp()) {
|
||||
senTreep = new AstSenTree{propp->fileline(), propp->sensesp()->cloneTree(true)};
|
||||
senTreeOwned = true;
|
||||
}
|
||||
if (!propp->sensesp()) return;
|
||||
AstSenTree* senTreep
|
||||
= new AstSenTree{propp->fileline(), propp->sensesp()->cloneTree(true)};
|
||||
AstNodeExpr* disableExprp = propp->disablep();
|
||||
if (!senTreep) return;
|
||||
|
||||
// NFA lowering clones repeated operands and may hoist them into an
|
||||
// always_comb block. Resolve implicit sampled-value clocks first, while
|
||||
|
|
@ -3111,7 +3253,15 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
// from this attempt become orphan MODULETEMPs; V3Dead removes
|
||||
// them along with the dead always_comb driver.
|
||||
replaceBodyOnBuildError(flp, propp, result.errorEmitted);
|
||||
if (senTreeOwned) VL_DO_DANGLING(pushDeletep(senTreep), senTreep);
|
||||
VL_DO_DANGLING(pushDeletep(senTreep), senTreep);
|
||||
return;
|
||||
}
|
||||
// After the build, so a construct the builder rejects reports itself.
|
||||
if (propertyControlp) {
|
||||
seqBodyp->v3warn(E_UNSUPPORTED,
|
||||
"Unsupported: temporal property if/case with " << propertyControlp);
|
||||
replaceBodyOnBuildError(flp, propp, /*errorEmitted=*/true);
|
||||
VL_DO_DANGLING(pushDeletep(senTreep), senTreep);
|
||||
return;
|
||||
}
|
||||
|
||||
|
|
@ -3149,7 +3299,7 @@ class AssertNfaVisitor final : public VNVisitor {
|
|||
AstSenTree* const threadFailReplaySenTreep
|
||||
= signals.threadFailCountp ? senTreep->cloneTree(false) : nullptr;
|
||||
|
||||
if (senTreeOwned) VL_DO_DANGLING(pushDeletep(senTreep), senTreep);
|
||||
VL_DO_DANGLING(pushDeletep(senTreep), senTreep);
|
||||
if (disableExprUnlinked) VL_DO_DANGLING(pushDeletep(disableExprp), disableExprp);
|
||||
if (result.finalCondp && !result.finalCondp->backp()) pushDeletep(result.finalCondp);
|
||||
|
||||
|
|
|
|||
|
|
@ -3987,12 +3987,16 @@ public:
|
|||
class AstSAnd final : public AstNodeBiop {
|
||||
// Sequence 'and' (IEEE 1800-2023 16.9.5): both operand sequences must match.
|
||||
// Operates on match sets, not values. For boolean operands, lowered to AstLogAnd.
|
||||
const bool m_propertyControl; // Parser-generated property if/case branch conjunction
|
||||
public:
|
||||
AstSAnd(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp)
|
||||
: ASTGEN_SUPER_SAnd(fl, lhsp, rhsp) {
|
||||
AstSAnd(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp, bool propertyControl = false)
|
||||
: ASTGEN_SUPER_SAnd(fl, lhsp, rhsp)
|
||||
, m_propertyControl{propertyControl} {
|
||||
dtypeSetBit();
|
||||
}
|
||||
ASTGEN_MEMBERS_AstSAnd;
|
||||
void dump(std::ostream& str) const override;
|
||||
void dumpJson(std::ostream& str) const override;
|
||||
void numberOperate(V3Number& out, const V3Number& lhs, const V3Number& rhs) override {
|
||||
out.opLogAnd(lhs, rhs);
|
||||
}
|
||||
|
|
@ -4006,6 +4010,10 @@ public:
|
|||
bool sizeMattersRhs() const override { return false; }
|
||||
int instrCount() const override { return widthInstrs() + INSTR_COUNT_BRANCH; }
|
||||
bool isMultiCycleSva() const override { return true; }
|
||||
bool sameNode(const AstNode* samep) const override { // LCOV_EXCL_LINE
|
||||
return m_propertyControl == VN_DBG_AS(samep, SAnd)->m_propertyControl; // LCOV_EXCL_LINE
|
||||
}
|
||||
bool propertyControl() const { return m_propertyControl; }
|
||||
};
|
||||
class AstSIntersect final : public AstNodeBiop {
|
||||
// Sequence 'intersect' (IEEE 1800-2023 16.9.6): both operands match with equal length.
|
||||
|
|
|
|||
|
|
@ -483,6 +483,14 @@ void AstSConsRep::dumpJson(std::ostream& str) const {
|
|||
dumpJsonBoolFuncIf(str, unbounded);
|
||||
dumpJsonGen(str);
|
||||
} // LCOV_EXCL_STOP
|
||||
void AstSAnd::dump(std::ostream& str) const {
|
||||
this->AstNodeExpr::dump(str);
|
||||
if (propertyControl()) str << " [PROPERTY_CONTROL]";
|
||||
}
|
||||
void AstSAnd::dumpJson(std::ostream& str) const {
|
||||
dumpJsonBoolFuncIf(str, propertyControl);
|
||||
dumpJsonGen(str);
|
||||
}
|
||||
void AstPropAlways::dump(std::ostream& str) const {
|
||||
this->AstNodeExpr::dump(str);
|
||||
if (isStrong()) str << " [strong]";
|
||||
|
|
|
|||
|
|
@ -137,7 +137,7 @@ AstNodeExpr* V3ParseImp::makePropertyCase(FileLine* flp, AstNodeExpr* exprp, Ast
|
|||
new AstLogNot{itemp->fileline(), matchedp->cloneTreePure(false)}}
|
||||
: itemMatchp->cloneTreePure(false);
|
||||
AstNodeExpr* const branchp = new AstImplication{itemp->fileline(), guardp, propp, true};
|
||||
resultp = resultp ? new AstSAnd{flp, resultp, branchp} : branchp;
|
||||
resultp = resultp ? new AstSAnd{flp, resultp, branchp, /*propertyControl=*/true} : branchp;
|
||||
matchedp = matchedp ? new AstLogOr{itemp->fileline(), matchedp, itemMatchp} : itemMatchp;
|
||||
}
|
||||
itemsp->deleteTree();
|
||||
|
|
@ -150,7 +150,7 @@ AstNodeExpr* V3ParseImp::makePropertyCase(FileLine* flp, AstNodeExpr* exprp, Ast
|
|||
AstNodeExpr* const noMatchp
|
||||
= static_cast<AstNodeExpr*>(new AstLogNot{defaultFlp, matchedp->cloneTreePure(false)});
|
||||
AstNodeExpr* const branchp = new AstImplication{defaultFlp, noMatchp, defaultPropp, true};
|
||||
resultp = new AstSAnd{flp, resultp, branchp};
|
||||
resultp = new AstSAnd{flp, resultp, branchp, /*propertyControl=*/true};
|
||||
}
|
||||
matchedp->deleteTree();
|
||||
exprp->deleteTree();
|
||||
|
|
|
|||
|
|
@ -6719,7 +6719,8 @@ property_exprCaseIf<nodeExprp>: // IEEE: part of property_expr for if/case
|
|||
| yIF '(' expr/*expression_or_dist*/ ')' pexpr yELSE pexpr
|
||||
{ AstNodeExpr* const elseCondp = new AstLogNot{$1, $3->cloneTreePure(false)};
|
||||
$$ = new AstSAnd{$1, new AstImplication{$1, $3, $5, true},
|
||||
new AstImplication{$1, elseCondp, $7, true}}; }
|
||||
new AstImplication{$1, elseCondp, $7, true},
|
||||
/*propertyControl=*/true}; }
|
||||
;
|
||||
|
||||
property_case_itemList<caseItemp>: // IEEE: {property_case_item}
|
||||
|
|
|
|||
|
|
@ -4,6 +4,5 @@
|
|||
[115] %Error: t_prop_s_always_eos_count.v:44: Assertion failed in top.t
|
||||
[115] %Error: t_prop_s_always_eos_count.v:48: Assertion failed in top.t
|
||||
[115] %Error: t_prop_s_always_eos_count.v:56: Assertion failed in top.t
|
||||
[115] %Error: t_prop_s_always_eos_count.v:62: Assertion failed in top.t
|
||||
[115] %Error: t_prop_s_always_eos_count.v:70: Assertion failed in top.t
|
||||
[115] %Error: t_prop_s_always_eos_count.v:73: Assertion failed in top.t
|
||||
|
|
|
|||
|
|
@ -0,0 +1,20 @@
|
|||
#!/usr/bin/env python3
|
||||
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
|
||||
#
|
||||
# This program is free software; you can redistribute it and/or modify it
|
||||
# under the terms of either the GNU Lesser General Public License Version 3
|
||||
# or the Perl Artistic License Version 2.0.
|
||||
# SPDX-FileCopyrightText: 2026 Wilson Snyder
|
||||
# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
|
||||
|
||||
import vltest_bootstrap
|
||||
|
||||
test.scenarios('simulator')
|
||||
|
||||
test.sim_time = 16000
|
||||
|
||||
test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing'])
|
||||
|
||||
test.execute()
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,116 @@
|
|||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||
// SPDX-FileCopyrightText: 2026 PlanV GmbH
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
// verilog_format: off
|
||||
`define stop $stop
|
||||
`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
|
||||
// verilog_format: on
|
||||
|
||||
module t;
|
||||
|
||||
bit clk = 0;
|
||||
int cyc = 0;
|
||||
bit a = 0, b = 0, c = 0, abrt = 0;
|
||||
int fail_bool = 0;
|
||||
int fail_seq = 0;
|
||||
int pass_always = 0;
|
||||
int fail_always = 0;
|
||||
int fail_ring = 0;
|
||||
int fail_first = 0;
|
||||
int pass_rej = 0;
|
||||
int fail_rej = 0;
|
||||
int fail_nested = 0;
|
||||
int fail_range = 0;
|
||||
int fail_ring2 = 0;
|
||||
int fail_rep_a = 0;
|
||||
int fail_rep_r = 0;
|
||||
int fail_delay = 0;
|
||||
int fail_fby = 0;
|
||||
int fail_and = 0;
|
||||
int fail_unb = 0;
|
||||
|
||||
always @(posedge clk) begin
|
||||
cyc <= cyc + 1;
|
||||
a <= cyc[0];
|
||||
b <= cyc[1];
|
||||
c <= cyc[2];
|
||||
abrt <= (cyc == 7);
|
||||
end
|
||||
|
||||
assert property (@(posedge clk) sync_accept_on (abrt) (b |-> c))
|
||||
else fail_bool++;
|
||||
assert property (@(posedge clk) sync_accept_on (abrt) ((a ##1 b) |-> c))
|
||||
else fail_seq++;
|
||||
|
||||
assert property (@(posedge clk) sync_accept_on (1'b1) (1'b1 |-> (1'b1 ##1 1'b0))) pass_always++;
|
||||
else fail_always++;
|
||||
|
||||
assert property (@(posedge clk) sync_accept_on (abrt) (1'b1 ##2 c))
|
||||
else fail_ring++;
|
||||
|
||||
assert property (@(posedge clk) sync_accept_on (1'b0) (b ##1 1'b1))
|
||||
else fail_first++;
|
||||
|
||||
assert property (@(posedge clk) sync_reject_on (abrt) (1'b1 ##1 1'b1)) pass_rej++;
|
||||
else fail_rej++;
|
||||
|
||||
assert property (@(posedge clk)
|
||||
sync_accept_on (abrt) (1'b1 |-> sync_reject_on (1'b0) (1'b1 ##1 c)))
|
||||
else fail_nested++;
|
||||
|
||||
assert property (@(posedge clk) sync_accept_on (abrt) (1'b1 ##[1:2] (a ##1 b)))
|
||||
else fail_range++;
|
||||
|
||||
assert property (@(posedge clk) sync_accept_on (abrt) sync_accept_on (b) (1'b1 ##2 c))
|
||||
else fail_ring2++;
|
||||
|
||||
assert property (@(posedge clk) sync_accept_on (abrt) (a [* 2]))
|
||||
else fail_rep_a++;
|
||||
|
||||
assert property (@(posedge clk) sync_reject_on (abrt) (b [* 2]))
|
||||
else fail_rep_r++;
|
||||
|
||||
assert property (@(posedge clk) sync_reject_on (abrt) (##1 c))
|
||||
else fail_delay++;
|
||||
|
||||
cover property (@(posedge clk) (a ##1 b) or(sync_reject_on (abrt) (b ##1 c)));
|
||||
|
||||
assert property (@(posedge clk) sync_reject_on (1'b0) (a #-# b))
|
||||
else fail_fby++;
|
||||
|
||||
assert property (@(posedge clk) (sync_accept_on (abrt) b) and c)
|
||||
else fail_and++;
|
||||
|
||||
assert property (@(posedge clk) sync_reject_on (abrt) (a and always [1:$] b))
|
||||
else fail_unb++;
|
||||
|
||||
cover property (@(posedge clk) (a and b) ##1 c);
|
||||
|
||||
|
||||
initial begin
|
||||
repeat (40) #5 clk = ~clk;
|
||||
`checkd(fail_bool, 5);
|
||||
`checkd(fail_seq, 3);
|
||||
`checkd(pass_always, 20);
|
||||
`checkd(fail_always, 0); // zero-ok
|
||||
`checkd(fail_ring, 8);
|
||||
`checkd(fail_first, 11);
|
||||
`checkd(pass_rej, 17);
|
||||
`checkd(fail_rej, 2);
|
||||
`checkd(fail_nested, 10);
|
||||
`checkd(fail_range, 6);
|
||||
`checkd(fail_ring2, 1);
|
||||
`checkd(fail_rep_a, 19);
|
||||
`checkd(fail_rep_r, 16);
|
||||
`checkd(fail_delay, 12);
|
||||
`checkd(fail_fby, 16);
|
||||
`checkd(fail_and, 16);
|
||||
`checkd(fail_unb, 3); // One other sim: 19
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
|
||||
endmodule
|
||||
|
|
@ -38,54 +38,52 @@ module t (
|
|||
|
||||
// Test 1: accept_on (async) -- property succeeds when cnd_a fires
|
||||
assert property (@(posedge clk) disable iff (cyc < 2) accept_on (cnd_a) body)
|
||||
else count_fail1 <= count_fail1 + 1;
|
||||
else count_fail1 <= count_fail1 + 1;
|
||||
|
||||
// Test 2: reject_on (async) -- property fails when cnd_r fires
|
||||
assert property (@(posedge clk) disable iff (cyc < 2) reject_on (cnd_r) body)
|
||||
else count_fail2 <= count_fail2 + 1;
|
||||
else count_fail2 <= count_fail2 + 1;
|
||||
|
||||
// Test 3: sync_accept_on -- sampled at matured clocking event
|
||||
assert property (@(posedge clk) disable iff (cyc < 2) sync_accept_on (cnd_a) body)
|
||||
else count_fail3 <= count_fail3 + 1;
|
||||
else count_fail3 <= count_fail3 + 1;
|
||||
|
||||
// Test 4: sync_reject_on
|
||||
assert property (@(posedge clk) disable iff (cyc < 2) sync_reject_on (cnd_r) body)
|
||||
else count_fail4 <= count_fail4 + 1;
|
||||
else count_fail4 <= count_fail4 + 1;
|
||||
|
||||
// Test 5: outer accept_on wraps inner reject_on -- outer wins per 16.12.14
|
||||
assert property (@(posedge clk) disable iff (cyc < 2)
|
||||
accept_on (cnd_a) reject_on (cnd_r) body)
|
||||
else count_fail5 <= count_fail5 + 1;
|
||||
assert property (@(posedge clk) disable iff (cyc < 2) accept_on (cnd_a) reject_on (cnd_r) body)
|
||||
else count_fail5 <= count_fail5 + 1;
|
||||
|
||||
// Test 6: outer reject_on wraps inner accept_on
|
||||
assert property (@(posedge clk) disable iff (cyc < 2)
|
||||
reject_on (cnd_r) accept_on (cnd_a) body)
|
||||
else count_fail6 <= count_fail6 + 1;
|
||||
assert property (@(posedge clk) disable iff (cyc < 2) reject_on (cnd_r) accept_on (cnd_a) body)
|
||||
else count_fail6 <= count_fail6 + 1;
|
||||
|
||||
// Test 7: named property form with accept_on inside
|
||||
property p_named;
|
||||
accept_on (cnd_a) body;
|
||||
endproperty
|
||||
assert property (@(posedge clk) disable iff (cyc < 2) p_named)
|
||||
else count_fail7 <= count_fail7 + 1;
|
||||
else count_fail7 <= count_fail7 + 1;
|
||||
|
||||
// Test 8: disable iff over a sync_accept_on with a second disabled window
|
||||
assert property (@(posedge clk) disable iff (cyc < 2 || (cyc >= 50 && cyc < 60))
|
||||
sync_accept_on (cnd) body)
|
||||
else count_fail8 <= count_fail8 + 1;
|
||||
else count_fail8 <= count_fail8 + 1;
|
||||
|
||||
// Test 9 / 10: async vs sync divergence hook -- identical encoding must
|
||||
// produce identical fail counts under current implementation
|
||||
assert property (@(posedge clk) disable iff (cyc < 2) accept_on (cnd_a) body)
|
||||
else count_fail9 <= count_fail9 + 1;
|
||||
else count_fail9 <= count_fail9 + 1;
|
||||
|
||||
assert property (@(posedge clk) disable iff (cyc < 2) sync_accept_on (cnd_a) body)
|
||||
else count_fail10 <= count_fail10 + 1;
|
||||
else count_fail10 <= count_fail10 + 1;
|
||||
|
||||
always @(posedge clk) begin
|
||||
`ifdef TEST_VERBOSE
|
||||
$write("[%0t] cyc==%0d crc=%x body=%b cnd_a=%b cnd_r=%b cnd=%b\n",
|
||||
$time, cyc, crc, body, cnd_a, cnd_r, cnd);
|
||||
$write("[%0t] cyc==%0d crc=%x body=%b cnd_a=%b cnd_r=%b cnd=%b\n", $time, cyc, crc, body,
|
||||
cnd_a, cnd_r, cnd);
|
||||
`endif
|
||||
cyc <= cyc + 1;
|
||||
crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
|
||||
|
|
@ -94,16 +92,16 @@ module t (
|
|||
end
|
||||
else if (cyc == 99) begin
|
||||
`checkh(crc, 64'hc77bb9b3784ea091);
|
||||
`checkd(count_fail1, 28); // Other sims: 14, one other: 15
|
||||
`checkd(count_fail1, 14);
|
||||
`checkd(count_fail2, 64); // One other sim: 66
|
||||
`checkd(count_fail3, 28); // Other sims: 14
|
||||
`checkd(count_fail3, 14);
|
||||
`checkd(count_fail4, 64);
|
||||
`checkd(count_fail5, 45); // Other sims: 31, one other: 32
|
||||
`checkd(count_fail6, 64); // Other sims: 59, one other: 60
|
||||
`checkd(count_fail7, 28); // Other sims: 14, one other: 15
|
||||
`checkd(count_fail8, 13); // Other sims: 10
|
||||
`checkd(count_fail9, 28); // Other sims: 14, one other: 15
|
||||
`checkd(count_fail10, 28); // Other sims: 14
|
||||
`checkd(count_fail5, 31); // One other sim: 32
|
||||
`checkd(count_fail6, 59); // One other sim: 60
|
||||
`checkd(count_fail7, 14); // One other sim: 15
|
||||
`checkd(count_fail8, 10);
|
||||
`checkd(count_fail9, 14); // One other sim: 15
|
||||
`checkd(count_fail10, 14);
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
|
|
|
|||
|
|
@ -0,0 +1,52 @@
|
|||
%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:26:63: Unsupported: temporal property if/case with a pass action
|
||||
: ... note: In instance 't'
|
||||
26 | assert property (@(posedge clk) if (a) 1'b1 ##1 b else 1'b1 ##2 c) $display("pass");
|
||||
| ^~
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:27:62: Unsupported: temporal property if/case with cover
|
||||
: ... note: In instance 't'
|
||||
27 | cover property (@(posedge clk) if (a) 1'b1 ##1 b else 1'b1 ##2 c);
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:28:68: Unsupported: temporal property if/case with negation
|
||||
: ... note: In instance 't'
|
||||
28 | assert property (@(posedge clk) not (if (a) 1'b1 ##1 b else 1'b1 ##2 c));
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:30:35: Unsupported: temporal property if/case with a pass action
|
||||
: ... note: In instance 't'
|
||||
30 | assert property (@(posedge clk) case (a) 1'b0: 1'b1 ##1 b; 1'b1: 1'b1 ##2 c; default: 1'b1 ##1 d;
|
||||
| ^~~~
|
||||
%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:35:65: Unsupported: multi-cycle sequence expression inside consecutive repetition (IEEE 1800-2023 16.9.2)
|
||||
: ... note: In instance 't'
|
||||
35 | assert property (@(posedge clk) sync_accept_on (a) ((b ##1 c) [* 2]));
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:38:52: Unsupported: multi-cycle sequence expression inside consecutive repetition (IEEE 1800-2023 16.9.2)
|
||||
: ... note: In instance 't'
|
||||
38 | assert property (@(posedge clk) if (a) ((b ##1 c)[*2]) else d) $display("pass");
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:41:3: Unsupported: property instance inside a multi-cycle property expression
|
||||
: ... note: In instance 't'
|
||||
41 | assert property (@(posedge clk) p_nested or e);
|
||||
| ^~~~~~
|
||||
%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:59:52: Unsupported: ranged cycle delay in an operand of property 'and'
|
||||
59 | assert property (@(posedge clk) (1'b1 ##[1:2] b) and c);
|
||||
| ^~~
|
||||
%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:60:37: Unsupported: ranged cycle delay in an operand of property 'and'
|
||||
60 | assert property (@(posedge clk) c and (1'b1 ##[1:2] b));
|
||||
| ^~~
|
||||
%Warning-COVERIGN: t/t_property_nfa_msgs_unsup.v:63:45: Ignoring unsupported: cover sequence with a sequence operand of 'or'
|
||||
63 | cover sequence (@(posedge clk) ((a and b) or(c ##1 d)));
|
||||
| ^~
|
||||
... For warning description see https://verilator.org/warn/COVERIGN?v=latest
|
||||
... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message.
|
||||
%Error: t/t_property_nfa_msgs_unsup.v:56:22: Concurrent assertion has no clock (IEEE 1800-2023 16.16)
|
||||
: ... note: In instance 't'
|
||||
: ... Suggest provide a clocking event, a default clocking, or a clocked procedural context
|
||||
56 | assert property (a [* 2]);
|
||||
| ^~
|
||||
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
|
||||
%Error: t/t_property_nfa_msgs_unsup.v:56:3: Concurrent assertion has no clock (IEEE 1800-2023 16.16)
|
||||
: ... note: In instance 't'
|
||||
: ... Suggest provide a clocking event, a default clocking, or a clocked procedural context
|
||||
56 | assert property (a [* 2]);
|
||||
| ^~~~~~
|
||||
%Error: Exiting due to
|
||||
|
|
@ -0,0 +1,33 @@
|
|||
#!/usr/bin/env python3
|
||||
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
|
||||
#
|
||||
# This program is free software; you can redistribute it and/or modify it
|
||||
# under the terms of either the GNU Lesser General Public License Version 3
|
||||
# or the Perl Artistic License Version 2.0.
|
||||
# SPDX-FileCopyrightText: 2026 Wilson Snyder
|
||||
# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
|
||||
|
||||
import glob
|
||||
import json
|
||||
import vltest_bootstrap
|
||||
|
||||
test.scenarios('vlt')
|
||||
|
||||
test.lint(expect_filename=test.golden_filename,
|
||||
verilator_flags2=[
|
||||
'--assert', '--timing', '--error-limit', '100', '--dumpi-tree', '3',
|
||||
'--dumpi-tree-json', '3', '--no-json-edit-nums'
|
||||
],
|
||||
fails=True)
|
||||
|
||||
test.file_grep_any(glob.glob(test.obj_dir + "/V" + test.name + "_*.tree"),
|
||||
r'SAND.*\[PROPERTY_CONTROL\]')
|
||||
|
||||
jsons = glob.glob(test.obj_dir + "/V" + test.name + "_*.tree.json")
|
||||
if not jsons:
|
||||
test.error("No .tree.json dumped")
|
||||
for fn in jsons:
|
||||
with open(fn, 'r', encoding="utf8") as fh:
|
||||
json.load(fh)
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,65 @@
|
|||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||
// SPDX-FileCopyrightText: 2026 PlanV GmbH
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
// Each property exercises one unsupported-diagnostic path of the NFA lowering
|
||||
|
||||
module t (
|
||||
input clk
|
||||
);
|
||||
|
||||
bit a = 0, b = 0, c = 0, d = 0, e = 0;
|
||||
|
||||
property p_nested;
|
||||
a ##1 b;
|
||||
endproperty
|
||||
|
||||
sequence s_nested; a ##1 b; endsequence
|
||||
|
||||
function automatic bit fbool();
|
||||
return a;
|
||||
endfunction
|
||||
|
||||
// Property if/else control the fail-only count engine cannot lower
|
||||
assert property (@(posedge clk) if (a) 1'b1 ##1 b else 1'b1 ##2 c) $display("pass");
|
||||
cover property (@(posedge clk) if (a) 1'b1 ##1 b else 1'b1 ##2 c);
|
||||
assert property (@(posedge clk) not (if (a) 1'b1 ##1 b else 1'b1 ##2 c));
|
||||
|
||||
assert property (@(posedge clk) case (a) 1'b0: 1'b1 ##1 b; 1'b1: 1'b1 ##2 c; default: 1'b1 ##1 d;
|
||||
endcase)
|
||||
$display("pass");
|
||||
|
||||
// An unsupported body under an abort reports itself, not an internal error
|
||||
assert property (@(posedge clk) sync_accept_on (a) ((b ##1 c) [* 2]));
|
||||
|
||||
// A body the builder rejects wins over the property if/case message
|
||||
assert property (@(posedge clk) if (a) ((b ##1 c)[*2]) else d) $display("pass");
|
||||
|
||||
// A named property instance nested in a composite is rejected, not dropped
|
||||
assert property (@(posedge clk) p_nested or e);
|
||||
|
||||
// A named sequence instance is inlined, not rejected
|
||||
assert property (@(posedge clk) s_nested or e);
|
||||
|
||||
// A function call is not a property instance
|
||||
assert property (@(posedge clk) fbool() ##1 b);
|
||||
|
||||
// A user-written 'and' of implications is not a property if/case
|
||||
assert property (@(posedge clk) (a |-> 1'b1 ##1 b) and(c |-> 1'b1 ##2 d));
|
||||
|
||||
// Property if/else without an action is lowered, not rejected
|
||||
assert property (@(posedge clk) if (a) 1'b1 ##1 b else 1'b1 ##2 c);
|
||||
|
||||
// A multi-cycle property with no clocking event is left to later passes
|
||||
assert property (a [* 2]);
|
||||
|
||||
// An 'and' operand carrying mid-window sources defers to later passes
|
||||
assert property (@(posedge clk) (1'b1 ##[1:2] b) and c);
|
||||
assert property (@(posedge clk) c and (1'b1 ##[1:2] b));
|
||||
|
||||
// A boolean 'and' operand of a rejected cover-sequence 'or' is freed
|
||||
cover sequence (@(posedge clk) ((a and b) or(c ##1 d)));
|
||||
|
||||
endmodule
|
||||
Loading…
Reference in New Issue