Fix scoped randomize with array members under rand_mode

This commit is contained in:
Yilou Wang 2026-07-04 10:48:04 +02:00
parent d84af81a11
commit 59414eda71
4 changed files with 381 additions and 12 deletions

View File

@ -105,12 +105,30 @@ public:
return count;
}
};
// Compile-time SMT key widths of nested associative-array levels; matches the
// key formats emitted by V3Randomize (string = 128, integral = 8 * sizeof).
// Recursion stops at non-assoc levels, which keep the 32-bit default.
template <typename T>
struct VlRandomAssocKeyWidths {
static void push(std::vector<size_t>&) {}
};
template <typename T_Key, typename T_Value>
struct VlRandomAssocKeyWidths<VlAssocArray<T_Key, T_Value>> {
static void push(std::vector<size_t>& widths) {
widths.push_back(std::is_same<T_Key, std::string>::value ? 128 : sizeof(T_Key) * 8);
VlRandomAssocKeyWidths<T_Value>::push(widths);
}
};
template <typename T>
class VlRandomArrayVarTemplate final : public VlRandomVar {
// Static key widths per level for the empty-array declaration fallback
const std::vector<size_t> m_fallbackIdxWidths;
public:
VlRandomArrayVarTemplate(const std::string& name, int width, void* datap, int dimension,
std::uint32_t randModeIdx)
: VlRandomVar{name, width, datap, dimension, randModeIdx} {}
std::uint32_t randModeIdx, const std::vector<size_t>& idxWidths = {})
: VlRandomVar{name, width, datap, dimension, randModeIdx}
, m_fallbackIdxWidths{idxWidths} {}
void* datap(int idx) const override {
const std::string indexed_name = name() + std::to_string(idx);
const auto it = m_arrVarsRefp->find(indexed_name);
@ -175,7 +193,15 @@ public:
}
} else {
if (dimension() > 0) {
for (int i = 0; i < dimension(); ++i) s << "(Array (_ BitVec 32) ";
// No recorded element (array empty at write_var time): fall back
// to the static per-level key widths so the declared domain still
// matches the constraint text (e.g. 128-bit string keys)
for (int i = 0; i < dimension(); ++i) {
const size_t idxWidth = i < static_cast<int>(m_fallbackIdxWidths.size())
? m_fallbackIdxWidths[i]
: 32;
s << "(Array (_ BitVec " << idxWidth << ") ";
}
s << "(_ BitVec " << width() << ")";
for (int i = 0; i < dimension(); ++i) s << ")";
} else {
@ -433,9 +459,11 @@ public:
write_var(VlAssocArray<T_Key, T_Value>& var, int width, const char* name, int dimension,
std::uint32_t randmodeIdx = std::numeric_limits<std::uint32_t>::max()) {
if (m_vars.find(name) == m_vars.end()) {
std::vector<size_t> keyWidths;
VlRandomAssocKeyWidths<VlAssocArray<T_Key, T_Value>>::push(keyWidths);
m_vars[name]
= std::make_shared<const VlRandomArrayVarTemplate<VlAssocArray<T_Key, T_Value>>>(
name, width, &var, dimension, randmodeIdx);
name, width, &var, dimension, randmodeIdx, keyWidths);
}
if (dimension > 0) {
m_index = 0;

View File

@ -631,6 +631,11 @@ class RandomizeMarkVisitor final : public VNVisitor {
}
handleRandomizeArgument(argp->exprp(), fromVarp, false);
}
// Re-mark members now that the class is IS_RANDOMIZED_INLINE: the
// markMembers call above ran before the upgrade, so non-argument
// members would have no rand_mode machinery and be re-randomized
// instead of staying frozen (IEEE 1800-2023 18.11)
if (classp && classp->user1() == IS_RANDOMIZED_INLINE) markMembers(classp);
}
void visit(AstConstraintUnique* nodep) override {
VL_RESTORER(m_stmtp);
@ -900,13 +905,13 @@ class ConstraintExprVisitor final : public VNVisitor {
handle.relink(getConstFormat(nodep));
return true;
}
void editSMT(AstNodeExpr* nodep, AstNodeExpr* lhsp = nullptr, AstNodeExpr* rhsp = nullptr,
AstNodeExpr* thsp = nullptr) {
AstSFormatF* 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)
if (smtExpr == "") {
nodep->v3warn(E_UNSUPPORTED, "Unsupported expression inside constraint");
return;
return nullptr;
}
if (lhsp)
@ -957,6 +962,7 @@ class ConstraintExprVisitor final : public VNVisitor {
}
nodep->replaceWith(newp);
VL_DO_DANGLING(pushDeletep(nodep), nodep);
return newp;
}
AstNodeExpr* editSingle(FileLine* fl, AstNode* itemsp) {
@ -1860,13 +1866,19 @@ class ConstraintExprVisitor final : public VNVisitor {
void visit(AstAssocSel* nodep) override {
if (editFormat(nodep)) return;
FileLine* const fl = nodep->fileline();
// Like visit(AstArraySel), keep a pre-edit clone so a rand_mode-gated base
// array can be hoisted below (inactive branch = element's current value).
// Assoc keys are always runtime-formatted below (never solver symbols),
// so the hoist is valid for rand keys too.
AstNodeExpr* const origp = nodep->cloneTree(false);
AstSFormatF* newp = nullptr;
// Adaptive formatting and type handling for associative array keys
if (VN_IS(nodep->bitp(), VarRef) && VN_AS(nodep->bitp(), VarRef)->isString()) {
VNRelinker handle;
AstNodeExpr* const idxp = new AstSFormatF{fl, (m_structSel ? "%32x" : "#x%32x"), false,
nodep->bitp()->unlinkFrBack(&handle)};
handle.relink(idxp);
editSMT(nodep, nodep->fromp(), idxp);
newp = editSMT(nodep, nodep->fromp(), idxp);
} else if (VN_IS(nodep->bitp(), CvtPackString)
&& VN_IS(nodep->bitp()->dtypep(), BasicDType)) {
AstCvtPackString* const stringp = VN_AS(nodep->bitp(), CvtPackString);
@ -1881,7 +1893,7 @@ class ConstraintExprVisitor final : public VNVisitor {
AstNodeExpr* const idxp = new AstSFormatF{fl, (m_structSel ? "%32x" : "#x%32x"), false,
stringp->lhsp()->unlinkFrBack(&handle)};
handle.relink(idxp);
editSMT(nodep, nodep->fromp(), idxp);
newp = editSMT(nodep, nodep->fromp(), idxp);
} else {
if (VN_IS(nodep->bitp()->dtypep(), BasicDType)
|| (VN_IS(nodep->bitp()->dtypep(), StructDType)
@ -1903,13 +1915,16 @@ class ConstraintExprVisitor final : public VNVisitor {
AstNodeExpr* const idxp
= new AstSFormatF{fl, fmt, false, nodep->bitp()->unlinkFrBack(&handle)};
handle.relink(idxp);
editSMT(nodep, nodep->fromp(), idxp);
newp = editSMT(nodep, nodep->fromp(), idxp);
} else {
nodep->bitp()->v3error(
"Illegal non-integral expression or subexpression in random constraint."
" (IEEE 1800-2023 18.3)");
}
}
if (!newp || !hoistRandModeOverSelect(newp, origp)) {
VL_DO_DANGLING(origp->deleteTree(), origp);
}
}
void visit(AstArraySel* nodep) override {
if (editFormat(nodep)) return;
@ -1934,13 +1949,80 @@ class ConstraintExprVisitor final : public VNVisitor {
handle.relink(indexp);
editSMT(nodep, nodep->fromp(), indexp);
} else {
// Index is constant or non-rand -- format as hex literal
// Index is constant or non-rand -- format as hex literal.
// Keep a pre-edit clone: if the base var is gated by a runtime
// rand_mode test, the inactive branch below must evaluate the
// element's current value.
AstNodeExpr* const origp = nodep->cloneTree(false);
AstNodeExpr* const indexp
= new AstSFormatF{fl, "#x%8x", false, nodep->bitp()->unlinkFrBack(&handle)};
handle.relink(indexp);
editSMT(nodep, nodep->fromp(), indexp);
AstSFormatF* const newp = editSMT(nodep, nodep->fromp(), indexp);
if (!newp || !hoistRandModeOverSelect(newp, origp)) {
VL_DO_DANGLING(origp->deleteTree(), origp);
}
}
}
// True only for the runtime rand_mode gate built by visit(AstNodeVarRef*):
// an ARRAY_AT read whose target is some class's cached instance mode var
// (the var's user2p and the class's user2p point at each other). A user
// ternary between two rand arrays also reaches the walk below as a
// formatted Cond, but its condition never reads a mode array. Static
// rand mode arrays are not detected (not hoisted).
static bool isRandModeGate(const AstNodeExpr* exprp) {
const AstCMethodHard* const atp = VN_CAST(exprp, CMethodHard);
if (!atp || atp->method() != VCMethod::ARRAY_AT) return false;
const AstVar* varp = nullptr;
if (const AstVarRef* const refp = VN_CAST(atp->fromp(), VarRef)) {
varp = refp->varp();
} else if (const AstMemberSel* const mselp = VN_CAST(atp->fromp(), MemberSel)) {
varp = mselp->varp();
}
if (!varp) return false;
const AstClass* const classp = VN_CAST(varp->user2p(), Class);
return classp && classp->user2p() == varp;
}
// A rand var gated by a runtime rand_mode test was formatted by
// visit(AstNodeVarRef*) as (mode.at(i) ? "<name>" : "<whole value>").
// Inside a "(select %s %s)" chain the inactive branch would splice the
// WHOLE array's value in as a scalar literal -- not valid SMT (z3:
// "unknown constant"/"select requires 1 arguments"). Rebuild as
// mode.at(i) ? "(select <name> <idx>)..." : "<element value>"
// hoisting the mode test above the whole select chain; the inactive
// branch formats the current value of the selected element instead.
// Returns true if it consumed origp (the pre-edit clone of the select).
bool hoistRandModeOverSelect(AstSFormatF* newp, AstNodeExpr* origp) {
// Only for selects yielding a non-array element (full chains)
if (VN_IS(origp->dtypep()->skipRefp(), UnpackArrayDType)) return false;
// Walk nested "(select %s %s)" frames down to a mode-gating AstCond
std::vector<AstSFormatF*> frames;
AstCond* modeCondp = nullptr;
for (AstSFormatF* curp = newp; curp && curp->name() == "(select %s %s)";) {
AstNodeExpr* const firstp = curp->exprsp();
frames.push_back(curp);
if (AstCond* const condp = VN_CAST(firstp, Cond)) {
if (isRandModeGate(condp->condp())) modeCondp = condp;
break;
}
curp = VN_CAST(firstp, SFormatF);
}
if (!modeCondp) return false;
FileLine* const fl = newp->fileline();
AstNodeExpr* const modep = modeCondp->condp()->unlinkFrBack();
AstNodeExpr* activep = modeCondp->thenp()->unlinkFrBack();
// Rebuild the select chain text around the SMT name, innermost first
for (auto it = frames.rbegin(); it != frames.rend(); ++it) {
AstNodeExpr* const idxFmtp = VN_AS((*it)->exprsp()->nextp(), NodeExpr);
idxFmtp->unlinkFrBack();
activep
= new AstSFormatF{fl, "(select %s %s)", false, AstNode::addNext(activep, idxFmtp)};
}
AstCond* const hoistp = new AstCond{fl, modep, activep, getConstFormat(origp)};
hoistp->user1(true); // Mark as formatted
newp->replaceWith(hoistp);
VL_DO_DANGLING(pushDeletep(newp), newp);
return true;
}
void visit(AstMemberSel* nodep) override {
// Check if rootVar is globalConstrained
if (nodep->varp()->rand().isRandomizable() && nodep->fromp()) {
@ -2313,6 +2395,19 @@ class ConstraintExprVisitor final : public VNVisitor {
FileLine* const fl = nodep->fileline();
if (nodep->method() == VCMethod::ARRAY_AT && nodep->fromp()->user1()) {
// Queue/dynamic-array element access. Like visit(AstArraySel), keep a
// pre-edit clone so a rand_mode-gated base array can be hoisted below
// (its inactive branch must evaluate the element's current value, not
// the whole array -- whose const format is empty for a queue). Only
// for a non-rand index; a rand index against a frozen array would
// need the whole array as an SMT term.
bool indexIsRand = false;
if (nodep->pinsp()) {
nodep->pinsp()->foreach([&](const AstNodeVarRef* vrefp) {
if (vrefp->varp()->rand().isRandomizable()) indexIsRand = true;
});
}
AstNodeExpr* const origp = indexIsRand ? nullptr : nodep->cloneTree(false);
iterateChildren(nodep);
AstNodeExpr* pinp = nodep->pinsp()->unlinkFrBack();
if (VN_IS(pinp, SFormatF) && m_structSel) VN_AS(pinp, SFormatF)->name("%x");
@ -2324,6 +2419,9 @@ class ConstraintExprVisitor final : public VNVisitor {
newp = new AstSFormatF{fl, "(select %s %s)", false, argsp};
nodep->replaceWith(newp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
if (origp && !hoistRandModeOverSelect(newp, origp)) {
VL_DO_DANGLING(origp->deleteTree(), origp);
}
return;
}

View File

@ -0,0 +1,21 @@
#!/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')
if not test.have_solver:
test.skip("No constraint solver installed")
test.compile()
test.execute()
test.passes()

View File

@ -0,0 +1,222 @@
// 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
// Scoped this.randomize(scalar) while OTHER rand members are arrays that stay
// frozen (rand_mode machinery engaged): the frozen array's element constraint
// must format as a valid (select ...) pin, not (select <whole-array> idx).
typedef int unsigned uint;
class Base;
rand uint delay;
rand uint guard; // gets rand_mode(0) to engage the per-var mode machinery
constraint delay_c {delay inside {[1:100]};}
function int rd();
return this.randomize(delay);
endfunction
endclass
class Unpacked extends Base;
rand uint a[3];
constraint c {foreach (a[i]) a[i] inside {[1:10]};}
endclass
class Unpacked2D extends Base;
rand uint a[2][2];
constraint c {foreach (a[i, j]) a[i][j] inside {[1:10]};}
endclass
class Queue extends Base;
rand uint a[$];
constraint c {
a.size() == 3;
foreach (a[i]) a[i] inside {[1:10]};
}
endclass
class Dyn extends Base;
rand uint a[];
constraint c {
a.size() == 3;
foreach (a[i]) a[i] inside {[1:10]};
}
endclass
/* verilator lint_off SIDEEFFECT */
class AssocStr extends Base;
rand uint amap[string];
constraint c {
amap["alice"] inside {[1:10]};
amap["bob"] inside {[20:30]};
}
function new();
amap = '{"alice": 5, "bob": 25};
endfunction
endclass
class EmptyAssoc extends Base; // never populated: frozen default 0 violates
rand uint amap[string];
constraint c {amap["alice"] inside {[1:10]};}
endclass
class AssocInt extends Base;
rand uint imap[int];
constraint c {foreach (imap[k]) imap[k] inside {[1:10]};}
/* verilator lint_on SIDEEFFECT */
function new();
imap[2] = 1;
imap[5] = 1;
endfunction
endclass
class NoModes; // no rand_mode() call anywhere; scoped arg only
rand uint x, y;
rand uint arr[2];
constraint c {
x inside {[1:100]};
y inside {[1:100]};
foreach (arr[i]) arr[i] inside {[1:10]};
}
function int rx();
return this.randomize(x);
endfunction
endclass
module t;
int ok;
initial begin
Unpacked u;
Unpacked2D u2;
Queue q;
Dyn d;
uint snap1[3];
uint snap2[2][2];
uint snapq[$];
uint snapd[];
u = new;
ok = u.randomize();
`checkd(ok, 1);
u.guard.rand_mode(0);
snap1 = u.a;
for (int i = 0; i < 5; ++i) begin
ok = u.rd();
`checkd(ok, 1);
if (u.a !== snap1) `checkd(0, 1);
if (u.delay < 1 || u.delay > 100) `checkd(0, 1);
end
u2 = new;
ok = u2.randomize();
`checkd(ok, 1);
u2.guard.rand_mode(0);
snap2 = u2.a;
for (int i = 0; i < 5; ++i) begin
ok = u2.rd();
`checkd(ok, 1);
if (u2.a !== snap2) `checkd(0, 1);
end
q = new;
ok = q.randomize();
`checkd(ok, 1);
q.guard.rand_mode(0);
snapq = q.a;
for (int i = 0; i < 5; ++i) begin
ok = q.rd();
`checkd(ok, 1);
if (q.a !== snapq) `checkd(0, 1);
end
d = new;
ok = d.randomize();
`checkd(ok, 1);
d.guard.rand_mode(0);
snapd = d.a;
for (int i = 0; i < 5; ++i) begin
ok = d.rd();
`checkd(ok, 1);
if (d.a !== snapd) `checkd(0, 1);
end
// Associative array with string-literal keys stays frozen.
begin
AssocStr as;
uint snapa, snapb;
as = new;
ok = as.randomize();
`checkd(ok, 1);
as.guard.rand_mode(0);
snapa = as.amap["alice"];
snapb = as.amap["bob"];
for (int i = 0; i < 5; ++i) begin
ok = as.rd();
`checkd(ok, 1);
`checkd(as.amap["alice"], snapa);
`checkd(as.amap["bob"], snapb);
if (as.delay < 1 || as.delay > 100) `checkd(0, 1);
end
end
// Associative array with int keys under foreach stays frozen.
begin
AssocInt ai;
uint snap2, snap5;
ai = new;
ok = ai.randomize();
`checkd(ok, 1);
ai.guard.rand_mode(0);
snap2 = ai.imap[2];
snap5 = ai.imap[5];
for (int i = 0; i < 5; ++i) begin
ok = ai.rd();
`checkd(ok, 1);
`checkd(ai.imap[2], snap2);
`checkd(ai.imap[5], snap5);
end
end
// Never-populated assoc array: the declared solver domain must still match
// the constraint keys (128-bit string); the frozen default 0 then honestly
// violates membership on the scoped call.
begin
EmptyAssoc ea;
ea = new;
ea.guard.rand_mode(0);
for (int i = 0; i < 3; ++i) begin
ok = ea.rd();
`checkd(ok, 0);
end
end
// Scoped randomize with NO rand_mode machinery engaged elsewhere:
// non-argument members stay frozen (IEEE 1800-2023 18.11).
begin
NoModes nm;
uint snapy;
uint snaparr[2];
nm = new;
ok = nm.randomize();
`checkd(ok, 1);
snapy = nm.y;
snaparr = nm.arr;
for (int i = 0; i < 10; ++i) begin
ok = nm.rx();
`checkd(ok, 1);
`checkd(nm.y, snapy);
if (nm.arr !== snaparr) `checkd(0, 1);
if (nm.x < 1 || nm.x > 100) `checkd(0, 1);
end
end
$write("*-* All Finished *-*\n");
$finish;
end
endmodule