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

Support conditional constraints (#5245)

Browse Source
This commit is contained in:
Arkadiusz Kozdra
2024-07-10 11:30:18 -04:00
committed by GitHub
parent 11da07d3b9
commit 570e1bc35a
8 changed files with 460 additions and 168 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/V3Randomize.cpp
+116 -22
View File
@@ -48,7 +48,7 @@ class RandomizeMarkVisitor final : public VNVisitorConst {
BaseToDerivedMap m_baseToDerivedMap; // Mapping from base classes to classes that extend them
AstClass* m_classp = nullptr; // Current class
AstConstraintExpr* m_constraintExprp = nullptr; // Current constraint expression
const AstNode* m_constraintExprp = nullptr; // Current constraint expression
// METHODS
void markMembers(const AstClass* nodep) {
@@ -119,6 +119,15 @@ class RandomizeMarkVisitor final : public VNVisitorConst {
m_constraintExprp = nodep;
iterateChildrenConst(nodep);
}
void visit(AstConstraintIf* nodep) override {
{
VL_RESTORER(m_constraintExprp);
m_constraintExprp = nodep;
iterateConst(nodep->condp());
}
iterateAndNextConstNull(nodep->thensp());
iterateAndNextConstNull(nodep->elsesp());
}
void visit(AstNodeVarRef* nodep) override {
if (!m_constraintExprp) return;
if (!nodep->varp()->isRand()) return;
@@ -149,6 +158,7 @@ class ConstraintExprVisitor final : public VNVisitor {
AstNodeFTask* const m_taskp; // method to add write_var calls to
AstVar* const m_genp; // VlRandomizer variable of the class
bool m_wantSingle = false; // Whether to merge constraint expressions with LOGAND
bool editFormat(AstNodeExpr* nodep) {
if (nodep->user1()) return false;
@@ -160,7 +170,8 @@ class ConstraintExprVisitor final : public VNVisitor {
handle.relink(newp);
return true;
}
void editSMT(AstNodeExpr* nodep, AstNodeExpr* lhsp = nullptr, AstNodeExpr* rhsp = nullptr) {
void editSMT(AstNodeExpr* nodep, AstNodeExpr* lhsp = nullptr, AstNodeExpr* rhsp = nullptr,
AstNodeExpr* thsp = nullptr) {
// Replace incomputable (result-dependent) expression with SMT expression
std::string smtExpr = nodep->emitSMT(); // Might need child width (AstExtend)
UASSERT_OBJ(smtExpr != "", nodep,
@@ -168,6 +179,7 @@ class ConstraintExprVisitor final : public VNVisitor {
if (lhsp) lhsp = VN_AS(iterateSubtreeReturnEdits(lhsp->unlinkFrBack()), NodeExpr);
if (rhsp) rhsp = VN_AS(iterateSubtreeReturnEdits(rhsp->unlinkFrBack()), NodeExpr);
if (thsp) thsp = VN_AS(iterateSubtreeReturnEdits(thsp->unlinkFrBack()), NodeExpr);
AstNodeExpr* argsp = nullptr;
for (string::iterator pos = smtExpr.begin(); pos != smtExpr.end(); ++pos) {
@@ -187,17 +199,52 @@ class ConstraintExprVisitor final : public VNVisitor {
argsp = AstNode::addNext(argsp, rhsp);
rhsp = nullptr;
break;
case 't':
pos[0] = '@';
UASSERT_OBJ(thsp, nodep, "emitSMT() references undef node");
argsp = AstNode::addNext(argsp, thsp);
thsp = nullptr;
break;
default: nodep->v3fatalSrc("Unknown emitSMT format code: %" << pos[0]); break;
}
}
}
UASSERT_OBJ(!lhsp, nodep, "Missing emitSMT %l for " << lhsp);
UASSERT_OBJ(!rhsp, nodep, "Missing emitSMT %r for " << rhsp);
UASSERT_OBJ(!thsp, nodep, "Missing emitSMT %t for " << thsp);
AstSFormatF* const newp = new AstSFormatF{nodep->fileline(), smtExpr, false, argsp};
nodep->replaceWith(newp);
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
AstNodeExpr* editSingle(FileLine* fl, AstNode* itemsp) {
if (!itemsp) return nullptr;
VL_RESTORER(m_wantSingle);
m_wantSingle = true;
{
AstBegin* const tempp
= new AstBegin{fl, "[EditWrapper]", itemsp->unlinkFrBackWithNext()};
VL_DO_DANGLING(iterateAndNextNull(tempp->stmtsp()), itemsp);
itemsp = tempp->stmtsp();
if (itemsp) itemsp->unlinkFrBackWithNext();
VL_DO_DANGLING(tempp->deleteTree(), tempp);
}
if (!itemsp) return nullptr;
AstNodeExpr* exprsp = VN_CAST(itemsp, NodeExpr);
UASSERT_OBJ(exprsp, itemsp, "Single not expression?");
if (!exprsp->nextp()) return exprsp;
std::ostringstream fmt;
fmt << "(and";
for (AstNode* itemp = exprsp; itemp; itemp = itemp->nextp()) fmt << " %@";
fmt << ')';
return new AstSFormatF{fl, fmt.str(), false, exprsp};
}
// VISITORS
void visit(AstNodeVarRef* nodep) override {
if (editFormat(nodep)) return;
@@ -233,13 +280,75 @@ class ConstraintExprVisitor final : public VNVisitor {
if (editFormat(nodep)) return;
editSMT(nodep, nodep->lhsp());
}
void visit(AstNodeTriop* nodep) override {
if (editFormat(nodep)) return;
editSMT(nodep, nodep->lhsp(), nodep->rhsp(), nodep->thsp());
}
void visit(AstNodeCond* nodep) override {
if (editFormat(nodep)) return;
if (!nodep->condp()->user1()) {
// Do not burden the solver if cond computable: (cond ? "then" : "else")
iterate(nodep->thenp());
iterate(nodep->elsep());
return;
}
// Fall back to "(ite cond then else)"
visit(static_cast<AstNodeTriop*>(nodep));
}
void visit(AstReplicate* nodep) override {
// Biop, but RHS is harmful
if (editFormat(nodep)) return;
editSMT(nodep, nodep->srcp());
}
void visit(AstSFormatF* nodep) override {}
void visit(AstConstraintExpr* nodep) override { iterateChildren(nodep); }
void visit(AstStmtExpr* nodep) override {}
void visit(AstConstraintIf* nodep) override {
AstNodeExpr* newp = nullptr;
FileLine* const fl = nodep->fileline();
AstNodeExpr* const thenp = editSingle(fl, nodep->thensp());
AstNodeExpr* const elsep = editSingle(fl, nodep->elsesp());
if (thenp && elsep) {
newp = new AstCond{fl, nodep->condp()->unlinkFrBack(), thenp, elsep};
} else if (thenp) {
newp = new AstLogIf{fl, nodep->condp()->unlinkFrBack(), thenp};
} else if (elsep) {
newp = new AstLogIf{fl, new AstNot{fl, nodep->condp()->unlinkFrBack()}, elsep};
}
if (newp) {
newp->user1(true); // Assume result-dependent
nodep->replaceWith(new AstConstraintExpr{fl, newp});
} else {
nodep->unlinkFrBack();
}
VL_DO_DANGLING(nodep->deleteTree(), nodep);
}
void visit(AstConstraintForeach* nodep) override {
nodep->v3warn(CONSTRAINTIGN, "Constraint expression ignored (unsupported)");
VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
}
void visit(AstConstraintBefore* nodep) override {
nodep->v3warn(CONSTRAINTIGN, "Constraint expression ignored (unsupported)");
VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
}
void visit(AstConstraintUnique* nodep) override {
nodep->v3warn(CONSTRAINTIGN, "Constraint expression ignored (unsupported)");
VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
}
void visit(AstConstraintExpr* nodep) override {
iterateChildren(nodep);
if (m_wantSingle) {
nodep->replaceWith(nodep->exprp()->unlinkFrBack());
VL_DO_DANGLING(nodep->deleteTree(), nodep);
return;
}
// Only hard constraints are currently supported
AstCMethodHard* const callp = new AstCMethodHard{
nodep->fileline(), new AstVarRef{nodep->fileline(), m_genp, VAccess::READWRITE},
"hard", nodep->exprp()->unlinkFrBack()};
callp->dtypeSetVoid();
nodep->replaceWith(callp->makeStmt());
VL_DO_DANGLING(nodep->deleteTree(), nodep);
}
void visit(AstCMethodHard* nodep) override {
if (editFormat(nodep)) return;
@@ -268,10 +377,10 @@ class ConstraintExprVisitor final : public VNVisitor {
public:
// CONSTRUCTORS
explicit ConstraintExprVisitor(AstConstraintExpr* nodep, AstNodeFTask* taskp, AstVar* genp)
explicit ConstraintExprVisitor(AstNode* nodep, AstNodeFTask* taskp, AstVar* genp)
: m_taskp(taskp)
, m_genp(genp) {
iterate(nodep);
iterateAndNextNull(nodep);
}
};
@@ -555,23 +664,8 @@ class RandomizeVisitor final : public VNVisitor {
}
randomizep->addStmtsp(setupTaskRefp->makeStmt());
while (nodep->itemsp()) {
AstConstraintExpr* const condsp = VN_CAST(nodep->itemsp(), ConstraintExpr);
if (!condsp) {
nodep->itemsp()->v3warn(CONSTRAINTIGN,
"Constraint expression ignored (unsupported)");
pushDeletep(nodep->itemsp()->unlinkFrBack());
continue;
}
{ ConstraintExprVisitor{condsp->unlinkFrBack(), newp, genp}; }
// Only hard constraints are now supported
AstCMethodHard* const methodp = new AstCMethodHard{
condsp->fileline(), new AstVarRef{condsp->fileline(), genp, VAccess::READWRITE},
"hard", condsp->exprp()->unlinkFrBack()};
methodp->dtypeSetVoid();
taskp->addStmtsp(new AstStmtExpr{condsp->fileline(), methodp});
VL_DO_DANGLING(condsp->deleteTree(), condsp);
}
{ ConstraintExprVisitor{nodep->itemsp(), newp, genp}; }
if (nodep->itemsp()) taskp->addStmtsp(nodep->itemsp()->unlinkFrBackWithNext());
VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
}
void visit(AstRandCase* nodep) override {