This commit is contained in:
Kornel Uriasz 2026-07-14 18:17:45 +00:00 committed by GitHub
commit 92a7525f72
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
4 changed files with 206 additions and 41 deletions

View File

@ -1171,3 +1171,12 @@ void VlRandomizer::dump() const {
for (const std::string& c : m_constraints) VL_PRINTF("Constraint: %s\n", c.c_str()); for (const std::string& c : m_constraints) VL_PRINTF("Constraint: %s\n", c.c_str());
} }
#endif #endif
//======================================================================
//Helper method for dynamic array handling in SMT expressions
std::string to_hex(const IData& value, int width, char fill) {
std::ostringstream oss;
oss << std::hex << std::setfill(fill) << std::setw(width) << value;
return oss.str();
}

View File

@ -758,4 +758,9 @@ public:
bool next() { return VlRandomizer::next(m_rng); } bool next() { return VlRandomizer::next(m_rng); }
}; };
//======================================================================
//Helper method for dynamic array handling in SMT expressions
std::string to_hex(const IData& value, int width = 8, char fill = '0');
#endif // Guard #endif // Guard

View File

@ -764,7 +764,7 @@ class ConstraintExprVisitor final : public VNVisitor {
bool m_wantSingle = false; // Whether to merge constraint expressions with LOGAND bool m_wantSingle = false; // Whether to merge constraint expressions with LOGAND
VMemberMap& m_memberMap; // Member names cached for fast lookup VMemberMap& m_memberMap; // Member names cached for fast lookup
bool m_structSel = false; // Marks when inside structSel bool m_structSel = false; // Marks when inside structSel
// (used to format "%s.%s" for struct arrays) // (used to format "%s.%s" for struct arrays and nested structs)
std::set<std::string>& m_writtenVars; // Track which variable paths have write_var generated std::set<std::string>& m_writtenVars; // Track which variable paths have write_var generated
// (shared across all constraints) // (shared across all constraints)
std::set<std::string> m_inlineWrittenVars; // Per-instance tracking for inline constraints std::set<std::string> m_inlineWrittenVars; // Per-instance tracking for inline constraints
@ -797,17 +797,59 @@ class ConstraintExprVisitor final : public VNVisitor {
return ""; return "";
} }
// Extract SMT variable name from a solve-before expression. static AstNodeExpr* getFromp(const AstNodeExpr* const nodep) {
// Returns empty string if the expression is not a simple variable reference. if (const AstCMethodHard* cmethp = VN_CAST(nodep, CMethodHard)) return cmethp->fromp();
std::string extractSolveBeforeVarName(AstNodeExpr* exprp) { return getSelFromp(nodep);
if (const AstMemberSel* const memberSelp = VN_CAST(exprp, MemberSel)) {
return buildMemberPath(memberSelp);
} else if (const AstVarRef* const varrefp = VN_CAST(exprp, VarRef)) {
return varrefp->name();
} }
static std::string extractSolveBeforeBaseName(const AstNodeExpr* exprp) {
while (const AstNodeExpr* const fromp = getFromp(exprp)) exprp = fromp;
if (const AstVarRef* const vrefp = VN_CAST(exprp, VarRef)) return vrefp->name();
return ""; return "";
} }
static void buildNamePrefix(AstCExpr* exprp, const AstNodeExpr* const nodep) {
if (const AstVarRef* const refp = VN_CAST(nodep, VarRef)) {
exprp->add("(\""s + refp->name());
return;
}
const AstNodeExpr* const fromp = getFromp(nodep);
if (fromp) buildNamePrefix(exprp, fromp);
if (const AstStructSel* const selp = VN_CAST(nodep, StructSel)) {
exprp->add("." + selp->name());
} else if (const AstMemberSel* const mselp = VN_CAST(nodep, MemberSel)) {
exprp->add("." + mselp->name());
} else if (const AstCMethodHard* const cmethp = VN_CAST(nodep, CMethodHard)) {
if (cmethp->method() == VCMethod::ARRAY_AT) {
AstNodeExpr* const argp = cmethp->pinsp();
exprp->add(".\" + to_hex(");
exprp->add(argp->cloneTreePure(false));
exprp->add(") + \"");
} else {
cmethp->v3fatalSrc("Unexpected CMethodHard: " << cmethp->prettyTypeName());
return;
}
}
}
// Build a C++ expression (as AstNodeExpr) that evaluates to a const char*
// containing the SMT variable name for a solve-before variable reference.
// Handles simple vars, struct selects, and array element selects (for foreach).
static AstCExpr* buildPathExpr(FileLine* const fl, const AstNodeExpr* nodep,
const std::string selName) {
AstCExpr* const exprp = new AstCExpr{fl, ""};
buildNamePrefix(exprp, nodep);
if (selName != "") {
exprp->add(".");
exprp->add(selName);
}
exprp->add("\")");
return exprp;
}
// Build a C++ expression (as AstNodeExpr) that evaluates to a const char* // Build a C++ expression (as AstNodeExpr) that evaluates to a const char*
// containing the SMT variable name for a solve-before variable reference. // containing the SMT variable name for a solve-before variable reference.
// Handles simple vars, member selects, and array element selects (for foreach). // Handles simple vars, member selects, and array element selects (for foreach).
@ -824,9 +866,9 @@ class ConstraintExprVisitor final : public VNVisitor {
} }
// Helper: get fromp from MemberSel or StructSel // Helper: get fromp from MemberSel or StructSel
static AstNodeExpr* getSelFromp(AstNodeExpr* exprp) { static AstNodeExpr* getSelFromp(const AstNodeExpr* exprp) {
if (AstMemberSel* const mp = VN_CAST(exprp, MemberSel)) return mp->fromp(); if (const AstMemberSel* const mp = VN_CAST(exprp, MemberSel)) return mp->fromp();
if (AstStructSel* const sp = VN_CAST(exprp, StructSel)) return sp->fromp(); if (const AstStructSel* const sp = VN_CAST(exprp, StructSel)) return sp->fromp();
return nullptr; return nullptr;
} }
@ -862,15 +904,19 @@ class ConstraintExprVisitor final : public VNVisitor {
p->dtypeSetString(); p->dtypeSetString();
return p; return p;
} }
if (VN_IS(selFromp, MemberSel)) { if (VN_IS(selFromp, MemberSel) || VN_IS(selFromp, StructSel)
const std::string path || VN_IS(selFromp, CMethodHard)) {
= buildMemberPath(VN_AS(selFromp, MemberSel)) + "." + selName; AstCExpr* const p = buildPathExpr(fl, selFromp, selName);
AstCExpr* const p = new AstCExpr{fl, AstCExpr::Pure{}, "\"" + path + "\"s"};
p->dtypeSetString(); p->dtypeSetString();
return p; return p;
} }
return nullptr; return nullptr;
} }
if (VN_IS(exprp, CMethodHard)) {
AstCExpr* const p = buildPathExpr(fl, exprp, "");
p->dtypeSetString();
return p;
}
if (const AstArraySel* const selp = VN_CAST(exprp, ArraySel)) { if (const AstArraySel* const selp = VN_CAST(exprp, ArraySel)) {
// arr[i] -> dynamic name // arr[i] -> dynamic name
std::string baseName; std::string baseName;
@ -1093,7 +1139,8 @@ class ConstraintExprVisitor final : public VNVisitor {
// Check if this variable is marked as globally constrained // Check if this variable is marked as globally constrained
const bool isGlobalConstrained = nodep->varp()->globalConstrained(); const bool isGlobalConstrained = nodep->varp()->globalConstrained();
AstMemberSel* membersel = nullptr; AstMemberSel* memberselp = nullptr;
bool structSelOrCMeth = false;
std::string smtName; std::string smtName;
if (VN_IS(nodep->backp(), MemberSel)) { if (VN_IS(nodep->backp(), MemberSel)) {
// Build complete path from topmost MemberSel // Build complete path from topmost MemberSel
@ -1101,14 +1148,31 @@ class ConstraintExprVisitor final : public VNVisitor {
while (VN_IS(topMemberSel->backp(), MemberSel)) { while (VN_IS(topMemberSel->backp(), MemberSel)) {
topMemberSel = topMemberSel->backp(); topMemberSel = topMemberSel->backp();
} }
membersel = VN_AS(topMemberSel, MemberSel)->cloneTree(false); memberselp = VN_AS(topMemberSel, MemberSel)->cloneTree(false);
smtName = buildMemberPath(membersel); smtName = buildMemberPath(memberselp);
} else if (VN_IS(nodep->backp(), StructSel) || VN_IS(nodep->backp(), CMethodHard)) {
// Build complete path for topmost StructSel or CMethodHard::ARRAY_AT
AstNode* topNodep = nodep->backp();
while (VN_IS(topNodep->backp(), StructSel) || VN_IS(topNodep->backp(), CMethodHard)) {
topNodep = topNodep->backp();
}
if (VN_IS(topNodep, StructSel) || VN_IS(topNodep, CMethodHard)) {
structSelOrCMeth = true;
}
memberselp = VN_CAST(topNodep, MemberSel);
if (memberselp) smtName = buildMemberPath(memberselp);
// Above functions returned empty string, unrecognized node type,
// Using nodep->name();
if (smtName == "") smtName = nodep->name();
} else { } else {
// No MemberSel: just variable name // No MemberSel, StructSel or CMethodHard:at : just variable name
smtName = nodep->name(); smtName = nodep->name();
} }
if (membersel) varp = membersel->varp(); if (memberselp) varp = memberselp->varp();
AstNodeModule* const classOrPackagep = nodep->classOrPackagep(); AstNodeModule* const classOrPackagep = nodep->classOrPackagep();
const RandomizeMode randMode = {.asInt = varp->user1()}; const RandomizeMode randMode = {.asInt = varp->user1()};
if (!randMode.usesMode && editFormat(nodep)) return; if (!randMode.usesMode && editFormat(nodep)) return;
@ -1121,9 +1185,9 @@ class ConstraintExprVisitor final : public VNVisitor {
// from reformatting the SMT variable name into a hex literal // from reformatting the SMT variable name into a hex literal
exprp = new AstSFormatF{nodep->fileline(), smtName, false, nullptr}; exprp = new AstSFormatF{nodep->fileline(), smtName, false, nullptr};
// Get const format, using membersel if available for correct width/value // Get const format, using memberselp if available for correct width/value
AstNodeExpr* constFormatp AstNodeExpr* constFormatp = memberselp ? getConstFormat(memberselp->cloneTree(false))
= membersel ? getConstFormat(membersel->cloneTree(false)) : getConstFormat(nodep); : getConstFormat(nodep);
// Static rand vars route through the var's owning class's static array // Static rand vars route through the var's owning class's static array
// (may differ from m_classp when the rand var lives in a sub-object). // (may differ from m_classp when the rand var lives in a sub-object).
@ -1137,12 +1201,12 @@ class ConstraintExprVisitor final : public VNVisitor {
randModeAccess = new AstVarRef{ randModeAccess = new AstVarRef{
varp->fileline(), VN_AS(ownerStaticRandModeVarp->user2p(), NodeModule), varp->fileline(), VN_AS(ownerStaticRandModeVarp->user2p(), NodeModule),
ownerStaticRandModeVarp, VAccess::READ}; ownerStaticRandModeVarp, VAccess::READ};
} else if (membersel) { } else if (memberselp) {
AstNodeModule* const varClassp = VN_AS(varp->user2p(), NodeModule); AstNodeModule* const varClassp = VN_AS(varp->user2p(), NodeModule);
AstVar* const effectiveRandModeVarp = getRandModeVarFromClass(varClassp); AstVar* const effectiveRandModeVarp = getRandModeVarFromClass(varClassp);
if (effectiveRandModeVarp) { if (effectiveRandModeVarp) {
// Member's class has randmode, use it // Member's class has randmode, use it
AstNodeExpr* parentAccess = membersel->fromp()->cloneTree(false); AstNodeExpr* parentAccess = memberselp->fromp()->cloneTree(false);
AstMemberSel* randModeSel AstMemberSel* randModeSel
= new AstMemberSel{varp->fileline(), parentAccess, effectiveRandModeVarp}; = new AstMemberSel{varp->fileline(), parentAccess, effectiveRandModeVarp};
randModeSel->dtypep(effectiveRandModeVarp->dtypep()); randModeSel->dtypep(effectiveRandModeVarp->dtypep());
@ -1179,12 +1243,12 @@ class ConstraintExprVisitor final : public VNVisitor {
// variable keys on user3(). // variable keys on user3().
const bool alreadyWritten = isGlobalConstrained ? m_writtenVars.count(smtName) > 0 const bool alreadyWritten = isGlobalConstrained ? m_writtenVars.count(smtName) > 0
: m_inlineInitTaskp ? m_inlineWrittenVars.count(smtName) > 0 : m_inlineInitTaskp ? m_inlineWrittenVars.count(smtName) > 0
: membersel ? m_writtenVars.count(smtName) > 0 : memberselp ? m_writtenVars.count(smtName) > 0
: varp->user3(); : varp->user3();
const bool shouldWriteVar = !alreadyWritten; const bool shouldWriteVar = !alreadyWritten;
if (shouldWriteVar) { if (shouldWriteVar) {
// Track this variable path as written // Track this variable path as written
if (isGlobalConstrained || (membersel && !m_inlineInitTaskp)) if (isGlobalConstrained || (memberselp && !m_inlineInitTaskp))
m_writtenVars.insert(smtName); m_writtenVars.insert(smtName);
if (m_inlineInitTaskp) m_inlineWrittenVars.insert(smtName); if (m_inlineInitTaskp) m_inlineWrittenVars.insert(smtName);
// For global constraints, delete nodep after processing // For global constraints, delete nodep after processing
@ -1205,7 +1269,7 @@ class ConstraintExprVisitor final : public VNVisitor {
} }
} }
if (isClassRefArray && !membersel) { if (isClassRefArray && !memberselp) {
FileLine* const fl = varp->fileline(); FileLine* const fl = varp->fileline();
AstClass* const elemClassp = elemClassRefDtp->classp(); AstClass* const elemClassp = elemClassRefDtp->classp();
AstNodeModule* const varClassp = VN_AS(varp->user2p(), NodeModule); AstNodeModule* const varClassp = VN_AS(varp->user2p(), NodeModule);
@ -1350,18 +1414,18 @@ class ConstraintExprVisitor final : public VNVisitor {
} }
methodp->dtypeSetVoid(); methodp->dtypeSetVoid();
AstNodeModule* classp; AstNodeModule* classp;
if (membersel) { if (memberselp) {
// For membersel, find the root varref to get the class // For memberselp, find the root varref to get the class
AstNode* rootNode = membersel->fromp(); AstNode* rootNode = memberselp->fromp();
while (AstMemberSel* nestedMemberSel = VN_CAST(rootNode, MemberSel)) { while (AstMemberSel* nestedMemberSel = VN_CAST(rootNode, MemberSel)) {
rootNode = nestedMemberSel->fromp(); rootNode = nestedMemberSel->fromp();
} }
if (AstNodeVarRef* rootVarRef = VN_CAST(rootNode, NodeVarRef)) { if (AstNodeVarRef* rootVarRef = VN_CAST(rootNode, NodeVarRef)) {
classp = VN_AS(rootVarRef->varp()->user2p(), NodeModule); classp = VN_AS(rootVarRef->varp()->user2p(), NodeModule);
} else { } else {
classp = VN_AS(membersel->user2p(), NodeModule); classp = VN_AS(memberselp->user2p(), NodeModule);
} }
methodp->addPinsp(membersel); methodp->addPinsp(memberselp);
} else { } else {
classp = VN_AS(varp->user2p(), NodeModule); classp = VN_AS(varp->user2p(), NodeModule);
AstVarRef* const varRefp AstVarRef* const varRefp
@ -1380,14 +1444,14 @@ class ConstraintExprVisitor final : public VNVisitor {
methodp->addPinsp(varnamep); methodp->addPinsp(varnamep);
methodp->addPinsp( methodp->addPinsp(
new AstConst{varp->dtypep()->fileline(), AstConst::Unsized64{}, dimension}); new AstConst{varp->dtypep()->fileline(), AstConst::Unsized64{}, dimension});
if (randMode.usesMode && !(isGlobalConstrained && membersel)) { if (randMode.usesMode && !(isGlobalConstrained && memberselp)) {
methodp->addPinsp( methodp->addPinsp(
new AstConst{varp->fileline(), AstConst::Unsized64{}, randMode.index}); new AstConst{varp->fileline(), AstConst::Unsized64{}, randMode.index});
} }
AstNodeFTask* initTaskp = m_inlineInitTaskp; AstNodeFTask* initTaskp = m_inlineInitTaskp;
if (!initTaskp) { if (!initTaskp) {
varp->user3(true); varp->user3(true);
if (membersel) { if (memberselp || structSelOrCMeth) {
initTaskp = VN_AS(m_memberMap.findMember(classp, "randomize"), NodeFTask); initTaskp = VN_AS(m_memberMap.findMember(classp, "randomize"), NodeFTask);
// Inherited rand members may belong to a base class // Inherited rand members may belong to a base class
// that has no randomize(); use the caller's function // that has no randomize(); use the caller's function
@ -1416,11 +1480,11 @@ class ConstraintExprVisitor final : public VNVisitor {
markp->dtypeSetVoid(); markp->dtypeSetVoid();
initTaskp->addStmtsp(markp->makeStmt()); initTaskp->addStmtsp(markp->makeStmt());
} }
if (isGlobalConstrained && membersel && randMode.usesMode) { if (isGlobalConstrained && memberselp && randMode.usesMode) {
AstNodeModule* const varClassp = VN_AS(varp->user2p(), NodeModule); AstNodeModule* const varClassp = VN_AS(varp->user2p(), NodeModule);
AstVar* const subRandModeVarp = getRandModeVarFromClass(varClassp); AstVar* const subRandModeVarp = getRandModeVarFromClass(varClassp);
if (subRandModeVarp) { if (subRandModeVarp) {
AstNodeExpr* const parentAccess = membersel->fromp()->cloneTree(false); AstNodeExpr* const parentAccess = memberselp->fromp()->cloneTree(false);
AstMemberSel* const randModeSel AstMemberSel* const randModeSel
= new AstMemberSel{varp->fileline(), parentAccess, subRandModeVarp}; = new AstMemberSel{varp->fileline(), parentAccess, subRandModeVarp};
randModeSel->dtypep(subRandModeVarp->dtypep()); randModeSel->dtypep(subRandModeVarp->dtypep());
@ -1473,8 +1537,8 @@ class ConstraintExprVisitor final : public VNVisitor {
} }
} }
} else { } else {
// Variable already written, clean up cloned membersel if any // Variable already written, clean up cloned memberselp if any
if (membersel) VL_DO_DANGLING(membersel->deleteTree(), membersel); if (memberselp) VL_DO_DANGLING(memberselp->deleteTree(), memberselp);
// Delete nodep if it's a global constraint (not deleted yet) // Delete nodep if it's a global constraint (not deleted yet)
if (isGlobalConstrained && !nodep->backp()) VL_DO_DANGLING(pushDeletep(nodep), nodep); if (isGlobalConstrained && !nodep->backp()) VL_DO_DANGLING(pushDeletep(nodep), nodep);
} }
@ -1849,6 +1913,7 @@ class ConstraintExprVisitor final : public VNVisitor {
} }
void visit(AstStructSel* nodep) override { void visit(AstStructSel* nodep) override {
if (editFormat(nodep)) return; if (editFormat(nodep)) return;
VL_RESTORER(m_structSel);
m_structSel = true; m_structSel = true;
if (VN_IS(nodep->fromp()->dtypep()->skipRefp(), StructDType)) { if (VN_IS(nodep->fromp()->dtypep()->skipRefp(), StructDType)) {
AstNodeExpr* const fromp = nodep->fromp(); AstNodeExpr* const fromp = nodep->fromp();
@ -1893,7 +1958,6 @@ class ConstraintExprVisitor final : public VNVisitor {
newp = new AstSFormatF{fl, nodep->fromp()->name() + "." + nodep->name(), false, newp = new AstSFormatF{fl, nodep->fromp()->name() + "." + nodep->name(), false,
nullptr}; nullptr};
} }
m_structSel = false;
nodep->replaceWith(newp); nodep->replaceWith(newp);
VL_DO_DANGLING(pushDeletep(nodep), nodep); VL_DO_DANGLING(pushDeletep(nodep), nodep);
} }

View File

@ -22,6 +22,23 @@ begin \
end \ end \
if (ok != 1) $stop; \ if (ok != 1) $stop; \
end end
`define check_rand_min_count(cl, field, exp_val, min_count) \
begin \
automatic longint prev_result; \
automatic int ok, count = 0; \
if (!bit'(cl.randomize())) $stop; \
prev_result = longint'(field); \
if (field == exp_val) count++; \
repeat(99) begin \
longint result; \
if (!bit'(cl.randomize())) $stop; \
result = longint'(field); \
if (field == exp_val) count++; \
if (result != prev_result) ok = 1; \
prev_result = result; \
end \
if (count < min_count) $stop; \
end
// verilog_format: on // verilog_format: on
class C; class C;
@ -61,12 +78,82 @@ class D;
}; };
endclass endclass
class E;
typedef struct { rand bit [31:0]a; } cfg_t;
rand cfg_t cfg[];
function new();
cfg = new [10];
endfunction
constraint e {
foreach (cfg[i]) {
// (i/2)*2 math is used to make sure we use i in array index and
// not exceed table size
solve cfg[(i/2)*2].a before cfg[(i/2)*2 + 1].a ;
cfg[(i/2)*2 + 1].a != cfg[(i/2)*2].a;
}
}
endclass
class F;
typedef struct { rand bit [7:0]d; }subcfg_t;
typedef struct { subcfg_t subcfg[]; } cfg_t;
rand cfg_t cfg[];
rand bit b;
function new();
cfg = new [10];
foreach (cfg[i]) begin
cfg[i].subcfg = new [10];
end
endfunction
constraint f {
foreach (cfg[i]) {
solve b before cfg[i].subcfg[0].d;
cfg[i].subcfg[0].d[6] == b;
}
}
endclass
class G;
typedef struct { rand bit [31:0]a; rand bit c; } cfg_t;
rand cfg_t cfg[];
rand bit b;
function new();
cfg = new [6];
endfunction
constraint g {
foreach (cfg[i]) {
solve b before cfg[i].a, cfg[i].c;
b -> cfg[i].c == 1;
b -> cfg[i].a == 0;
}
}
endclass
module t; module t;
initial begin initial begin
automatic C c = new; automatic C c = new;
automatic D d = new; automatic D d = new;
automatic E e = new;
automatic F f = new;
automatic G g = new;
`check_rand(c, c.x, 4 < c.x && c.x < 7); `check_rand(c, c.x, 4 < c.x && c.x < 7);
`check_rand(d, d.posit, (d.posit ? 4 : -3) < d.x && d.x < (d.posit ? 7 : 0)); `check_rand(d, d.posit, (d.posit ? 4 : -3) < d.x && d.x < (d.posit ? 7 : 0));
foreach (e.cfg[i]) begin
`check_rand(e, e.cfg[i].a, (e.cfg[(i/2)*2].a != e.cfg[(i/2)*2 + 1].a));
end
foreach (f.cfg[i]) begin
`check_rand(f, f.cfg[i].subcfg[0].d, (f.cfg[i].subcfg[0].d[6] == f.b));
end
foreach (g.cfg[i]) begin
`check_rand_min_count(g, g.cfg[i].a, 0, 14);
end
$write("*-* All Finished *-*\n"); $write("*-* All Finished *-*\n");
$finish; $finish;
end end