luke/verilator
1
0
Fork 0
mirror of https://github.com/verilator/verilator.git synced 2026-09-05 00:41:39 +02:00
Code Issues Packages Projects Releases Wiki Activity

Support simple cycle delay sequence expressions inside assertion properties (#6508)

Browse Source 
Signed-off-by: Bartłomiej Chmiel <[email protected]>
Co-authored-by: Wilson Snyder <[email protected]>
This commit is contained in:
Bartłomiej Chmiel
2025-10-10 16:16:15 +02:00
committed by GitHub
co-authored by Wilson Snyder
parent 2ac7cf51a9
commit 31e73f1645
29 changed files with 1488 additions and 390 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/V3AssertPre.cpp
+106 -23
View File
@@ -56,10 +56,15 @@ private:
AstNodeExpr* m_disablep = nullptr; // Last disable
// Other:
V3UniqueNames m_cycleDlyNames{"__VcycleDly"}; // Cycle delay counter name generator
V3UniqueNames m_propPrecondNames{"__VpropPrecond"}; // Cycle delay temporaries name generator
bool m_inAssign = false; // True if in an AssignNode
bool m_inAssignDlyLhs = false; // True if in AssignDly's LHS
bool m_inSynchDrive = false; // True if in synchronous drive
std::vector<AstVarXRef*> m_xrefsp; // list of xrefs that need name fixup
AstNodeExpr* m_hasUnsupp = nullptr; // True if assert has unsupported construct inside
AstPExpr* m_pExpr = nullptr; // Current AstPExpr
bool m_hasSExpr = false; // True if assert has AstSExpr inside
bool m_inSExpr = false; // True if in AstSExpr
// METHODS
@@ -335,16 +340,21 @@ private:
VL_DO_DANGLING(valuep->deleteTree(), valuep);
return;
}
AstSenItem* sensesp = nullptr;
if (!m_defaultClockingp) {
nodep->v3error("Usage of cycle delays requires default clocking"
" (IEEE 1800-2023 14.11)");
VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
VL_DO_DANGLING(valuep->deleteTree(), valuep);
return;
if (!m_pExpr && !m_inSExpr) {
nodep->v3error("Usage of cycle delays requires default clocking"
" (IEEE 1800-2023 14.11)");
VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
VL_DO_DANGLING(valuep->deleteTree(), valuep);
return;
}
sensesp = m_senip;
} else {
sensesp = m_defaultClockingp->sensesp();
}
AstEventControl* const controlp = new AstEventControl{
nodep->fileline(),
new AstSenTree{flp, m_defaultClockingp->sensesp()->cloneTree(false)}, nullptr};
nodep->fileline(), new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr};
const std::string delayName = m_cycleDlyNames.get(nodep);
AstVar* const cntVarp = new AstVar{flp, VVarType::BLOCKTEMP, delayName + "__counter",
nodep->findBasicDType(VBasicDTypeKwd::UINT32)};
@@ -408,6 +418,33 @@ private:
}
}
nodep->user1(true);
} else if (m_inSExpr && !nodep->user1()) {
AstVar* const preVarp
= new AstVar{nodep->varp()->fileline(), VVarType::BLOCKTEMP,
m_propPrecondNames.get(nodep->varp()) + "__" + nodep->varp()->name(),
nodep->varp()->dtypep()};
preVarp->lifetime(VLifetime::STATIC_EXPLICIT);
m_modp->addStmtsp(preVarp);
AstVarRef* const origp
= new AstVarRef{nodep->fileline(), nodep->varp(), VAccess::READ};
origp->user1(true);
AstVarRef* const precondp
= new AstVarRef{preVarp->fileline(), preVarp, VAccess::WRITE};
precondp->user1(true);
// Pack assignments in sampled as in concurrent assertions they are needed.
// Then, in assert's propp, sample only non-precondition variables.
AstSampled* const sampledp = new AstSampled{origp->fileline(), origp};
sampledp->dtypeFrom(origp);
UASSERT(m_pExpr, "Should be under assertion");
AstAssign* const assignp = new AstAssign{m_pExpr->fileline(), precondp, sampledp};
m_pExpr->addPrecondp(assignp);
AstVarRef* const precondReadp
= new AstVarRef{preVarp->fileline(), preVarp, VAccess::READ};
precondReadp->user1(true);
nodep->replaceWith(precondReadp);
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
}
void visit(AstMemberSel* nodep) override {
@@ -461,10 +498,33 @@ private:
void visit(AstNodeCoverOrAssert* nodep) override {
if (nodep->sentreep()) return; // Already processed
VL_RESTORER(m_hasSExpr);
VL_RESTORER(m_hasUnsupp);
clearAssertInfo();
m_pExpr = new AstPExpr{nodep->propp()->fileline()};
m_pExpr->dtypeFrom(nodep->propp());
// Find Clocking's buried under nodep->exprsp
iterateChildren(nodep);
if (!nodep->immediate()) nodep->sentreep(newSenTree(nodep));
if (m_hasSExpr && m_hasUnsupp) {
if (VN_IS(m_hasUnsupp, Implication)) {
m_hasUnsupp->v3warn(E_UNSUPPORTED,
"Unsupported: Implication with sequence expression");
} else {
m_hasUnsupp->v3warn(E_UNSUPPORTED,
"Unsupported: Disable iff with sequence expression");
}
if (m_pExpr) VL_DO_DANGLING(pushDeletep(m_pExpr), m_pExpr);
} else if (m_pExpr && m_pExpr->precondp()) {
m_pExpr->condp(VN_AS(nodep->propp()->unlinkFrBackWithNext(), NodeExpr));
nodep->propp(m_pExpr);
iterateAndNextNull(m_pExpr->precondp());
} else if (m_pExpr) {
VL_DO_DANGLING(pushDeletep(m_pExpr), m_pExpr);
}
clearAssertInfo();
}
void visit(AstFalling* nodep) override {
@@ -488,12 +548,12 @@ private:
if (exprp->width() > 1) exprp = new AstSel{fl, exprp, 0, 1};
AstSenTree* sentreep = nodep->sentreep();
if (sentreep) sentreep->unlinkFrBack();
AstNodeExpr* const pastp = new AstPast{fl, exprp};
AstPast* const pastp = new AstPast{fl, exprp};
pastp->dtypeFrom(exprp);
pastp->sentreep(newSenTree(nodep, sentreep));
exprp = new AstAnd{fl, pastp, new AstNot{fl, exprp->cloneTreePure(false)}};
exprp->dtypeSetBit();
nodep->replaceWith(exprp);
nodep->sentreep(newSenTree(nodep, sentreep));
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
void visit(AstFuture* nodep) override {
@@ -503,6 +563,10 @@ private:
if (sentreep) VL_DO_DANGLING(pushDeletep(sentreep->unlinkFrBack()), sentreep);
nodep->sentreep(newSenTree(nodep));
}
void visit(AstLogNot* nodep) override {
if (m_inSExpr) nodep->v3error("Syntax error: unexpected 'not' in sequence expression");
iterateChildren(nodep);
}
void visit(AstPast* nodep) override {
if (nodep->sentreep()) return; // Already processed
iterateChildren(nodep);
@@ -529,12 +593,12 @@ private:
if (exprp->width() > 1) exprp = new AstSel{fl, exprp, 0, 1};
AstSenTree* sentreep = nodep->sentreep();
if (sentreep) sentreep->unlinkFrBack();
AstNodeExpr* const pastp = new AstPast{fl, exprp};
AstPast* const pastp = new AstPast{fl, exprp};
pastp->dtypeFrom(exprp);
pastp->sentreep(newSenTree(nodep, sentreep));
exprp = new AstAnd{fl, new AstNot{fl, pastp}, exprp->cloneTreePure(false)};
exprp->dtypeSetBit();
nodep->replaceWith(exprp);
nodep->sentreep(newSenTree(nodep, sentreep));
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
void visit(AstStable* nodep) override {
@@ -544,12 +608,12 @@ private:
AstNodeExpr* exprp = nodep->exprp()->unlinkFrBack();
AstSenTree* sentreep = nodep->sentreep();
if (sentreep) sentreep->unlinkFrBack();
AstNodeExpr* const pastp = new AstPast{fl, exprp};
AstPast* const pastp = new AstPast{fl, exprp};
pastp->dtypeFrom(exprp);
pastp->sentreep(newSenTree(nodep, sentreep));
exprp = new AstEq{fl, pastp, exprp->cloneTreePure(false)};
exprp->dtypeSetBit();
nodep->replaceWith(exprp);
nodep->sentreep(newSenTree(nodep, sentreep));
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
void visit(AstSteady* nodep) override {
@@ -568,21 +632,27 @@ private:
void visit(AstImplication* nodep) override {
if (nodep->sentreep()) return; // Already processed
m_hasUnsupp = nodep;
FileLine* const fl = nodep->fileline();
iterateChildren(nodep);
FileLine* const flp = nodep->fileline();
AstNodeExpr* const rhsp = nodep->rhsp()->unlinkFrBack();
AstNodeExpr* lhsp = nodep->lhsp()->unlinkFrBack();
if (nodep->isOverlapped()) {
nodep->replaceWith(new AstLogOr{flp, new AstLogNot{flp, lhsp}, rhsp});
} else {
if (m_disablep) {
lhsp = new AstAnd{flp, new AstNot{flp, m_disablep->cloneTreePure(false)}, lhsp};
}
if (m_disablep) {
lhsp = new AstAnd{fl, new AstNot{fl, m_disablep->cloneTreePure(false)}, lhsp};
AstPast* const pastp = new AstPast{flp, lhsp};
pastp->dtypeFrom(lhsp);
pastp->sentreep(newSenTree(nodep));
AstNodeExpr* const exprp = new AstOr{flp, new AstNot{flp, pastp}, rhsp};
exprp->dtypeSetBit();
nodep->replaceWith(exprp);
}
AstNodeExpr* const pastp = new AstPast{fl, lhsp};
pastp->dtypeFrom(lhsp);
AstNodeExpr* const exprp = new AstOr{fl, new AstNot{fl, pastp}, rhsp};
exprp->dtypeSetBit();
nodep->replaceWith(exprp);
nodep->sentreep(newSenTree(nodep));
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
@@ -614,6 +684,7 @@ private:
}
if (AstNodeExpr* const disablep = nodep->disablep()) {
m_disablep = disablep;
m_hasUnsupp = disablep;
if (VN_IS(nodep->backp(), Cover)) {
blockp = new AstAnd{disablep->fileline(),
new AstNot{disablep->fileline(), disablep->unlinkFrBack()},
@@ -627,6 +698,18 @@ private:
nodep->replaceWith(blockp);
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
void visit(AstSExpr* nodep) override {
VL_RESTORER(m_inSExpr);
m_inSExpr = true;
m_hasSExpr = true;
UASSERT_OBJ(m_pExpr, nodep, "Should be under assertion");
m_pExpr->addPrecondp(nodep->delayp()->unlinkFrBack());
iterateChildren(nodep);
nodep->replaceWith(nodep->exprp()->unlinkFrBack());
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
void visit(AstNodeModule* nodep) override {
VL_RESTORER(m_defaultClockingp);
VL_RESTORER(m_defaultDisablep);