luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fix dynamic array handling in solve...before (#7922)

This commit is contained in:
Kornel Uriasz 2026-07-15 16:48:54 +02:00 committed by GitHub
parent baf012cf6a
commit 232b2eb04c
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
5 changed files with 224 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
include/verilated_random.h
View File

@ -758,4 +758,13 @@ public:
bool next() { return VlRandomizer::next(m_rng); }
};
//======================================================================
//Helper method for dynamic array handling in SMT expressions
inline std::string vlToSolverHex(const IData& value) {
std::ostringstream oss;
oss << std::hex << std::setfill('0') << std::setw(8) << value;
return oss.str();
}
#endif // Guard

102
src/V3Randomize.cpp
View File

@ -764,7 +764,7 @@ class ConstraintExprVisitor final : public VNVisitor {
bool m_wantSingle = false; // Whether to merge constraint expressions with LOGAND
VMemberMap& m_memberMap; // Member names cached for fast lookup
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
// (shared across all constraints)
std::set<std::string> m_inlineWrittenVars; // Per-instance tracking for inline constraints
@ -797,17 +797,59 @@ class ConstraintExprVisitor final : public VNVisitor {
return "";
}
// Extract SMT variable name from a solve-before expression.
// Returns empty string if the expression is not a simple variable reference.
std::string extractSolveBeforeVarName(AstNodeExpr* exprp) {
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 AstNodeExpr* getFromp(const AstNodeExpr* const nodep) {
if (const AstCMethodHard* cmethp = VN_CAST(nodep, CMethodHard)) return cmethp->fromp();
return getSelFromp(nodep);
}
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 "";
}
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 (VN_IS(nodep, MemberSel)) {
nodep->v3warn(E_UNSUPPORTED,
"Unsupported: Nested array element access in global constraint");
return;
} else if (const AstCMethodHard* const cmethp = VN_CAST(nodep, CMethodHard)) {
if (cmethp->method() == VCMethod::ARRAY_AT) {
AstNodeExpr* const argp = cmethp->pinsp();
exprp->add(".\" + vlToSolverHex(");
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*
// containing the SMT variable name for a solve-before variable reference.
// Handles simple vars, member selects, and array element selects (for foreach).
@ -816,9 +858,9 @@ class ConstraintExprVisitor final : public VNVisitor {
AstCExpr* buildArraySelNameExpr(FileLine* fl, const std::string& baseName,
const AstArraySel* selp) {
AstCExpr* const p = new AstCExpr{fl, ""};
p->add("(\""s + baseName + "[\" + std::to_string(");
p->add("(\""s + baseName + ".\" + vlToSolverHex(");
p->add(selp->bitp()->cloneTreePure(false));
p->add(") + \"]\")");
p->add("))");
p->dtypeSetString();
return p;
}
@ -849,9 +891,9 @@ class ConstraintExprVisitor final : public VNVisitor {
}
if (baseName.empty()) return nullptr;
AstCExpr* const p = new AstCExpr{fl, ""};
p->add("(\""s + baseName + "[\" + std::to_string(");
p->add("(\""s + baseName + ".\" + vlToSolverHex(");
p->add(arrSelp->bitp()->cloneTreePure(false));
p->add(") + \"]." + selName + "\")");
p->add("))");
p->dtypeSetString();
return p;
}
@ -862,15 +904,19 @@ class ConstraintExprVisitor final : public VNVisitor {
p->dtypeSetString();
return p;
}
if (VN_IS(selFromp, MemberSel)) {
const std::string path
= buildMemberPath(VN_AS(selFromp, MemberSel)) + "." + selName;
AstCExpr* const p = new AstCExpr{fl, AstCExpr::Pure{}, "\"" + path + "\"s"};
if (VN_IS(selFromp, MemberSel) || VN_IS(selFromp, StructSel)
|| VN_IS(selFromp, CMethodHard)) {
AstCExpr* const p = buildPathExpr(fl, selFromp, selName);
p->dtypeSetString();
return p;
}
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)) {
// arr[i] -> dynamic name
std::string baseName;
@ -1094,6 +1140,7 @@ class ConstraintExprVisitor final : public VNVisitor {
const bool isGlobalConstrained = nodep->varp()->globalConstrained();
AstMemberSel* memberselp = nullptr;
bool structSelOrCMeth = false;
std::string smtName;
if (VN_IS(nodep->backp(), MemberSel)) {
// Build complete path from topmost MemberSel
@ -1103,8 +1150,25 @@ class ConstraintExprVisitor final : public VNVisitor {
}
memberselp = VN_AS(topMemberSel, MemberSel)->cloneTree(false);
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 {
// No MemberSel: just variable name
// No MemberSel, StructSel or CMethodHard:at : just variable name
smtName = nodep->name();
}
@ -1387,7 +1451,7 @@ class ConstraintExprVisitor final : public VNVisitor {
AstNodeFTask* initTaskp = m_inlineInitTaskp;
if (!initTaskp) {
varp->user3(true);
if (memberselp) {
if (memberselp || structSelOrCMeth) {
initTaskp = VN_AS(m_memberMap.findMember(classp, "randomize"), NodeFTask);
// Inherited rand members may belong to a base class
// that has no randomize(); use the caller's function

109
test_regress/t/t_constraint_foreach.v
View File

@ -22,6 +22,23 @@ begin \
end \
if (ok != 1) $stop; \
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
class C;
@ -61,12 +78,104 @@ class D;
};
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 c; 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[0] != 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
class H;
rand integer a[];
rand integer b;
function new();
a = new [6];
endfunction
constraint h {
foreach (a[i]) {
solve b before a[i];
a[i] != b;
}
}
endclass
module t;
initial begin
automatic C c = new;
automatic D d = new;
automatic E e = new;
automatic F f = new;
automatic G g = new;
automatic H h = new;
`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));
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[0] != f.b));
end
foreach (g.cfg[i]) begin
`check_rand_min_count(g, g.cfg[i].a, 0, 14);
end
foreach (h.a[i]) begin
`check_rand(h, h.a[i], (h.a[i] != h.b));
end
$write("*-* All Finished *-*\n");
$finish;
end

14
test_regress/t/t_constraint_global_arr_unsup.out
View File

@ -17,4 +17,18 @@
%Error-UNSUPPORTED: t/t_constraint_global_arr_unsup.v:59:16: Unsupported: Array element access in global constraint
59 | m_assoc[0].m_x == 500;
| ^~~
%Error-UNSUPPORTED: t/t_constraint_global_arr_unsup.v:65:34: Unsupported: Nested array element access in global constraint
: ... note: In instance 't_constraint_global_arr_unsup'
65 | solve m_mid_arr[((i*2)/2)].m_obj.m_x before m_mid_arr[((i*2)/2) + 1].m_obj.m_x;
| ^~~~~
%Error-UNSUPPORTED: t/t_constraint_global_arr_unsup.v:65:76: Unsupported: Nested array element access in global constraint
: ... note: In instance 't_constraint_global_arr_unsup'
65 | solve m_mid_arr[((i*2)/2)].m_obj.m_x before m_mid_arr[((i*2)/2) + 1].m_obj.m_x;
| ^~~~~
%Error-UNSUPPORTED: t/t_constraint_global_arr_unsup.v:67:34: Unsupported: Nested array element access in global constraint
67 | m_mid_arr[((i*2)/2)].m_obj.m_x != m_mid_arr[((i*2)/2) + 1].m_obj.m_x;
| ^~~
%Error-UNSUPPORTED: t/t_constraint_global_arr_unsup.v:67:72: Unsupported: Nested array element access in global constraint
67 | m_mid_arr[((i*2)/2)].m_obj.m_x != m_mid_arr[((i*2)/2) + 1].m_obj.m_x;
| ^~~
%Error: Exiting due to

9
test_regress/t/t_constraint_global_arr_unsup.v
View File

@ -58,6 +58,15 @@ class Outer;
constraint c_assoc {
m_assoc[0].m_x == 500;
}
// Case 6: Array elements member access in solve...before foreach loop
constraint c_foreach {
foreach (m_mid_arr[i]) {
solve m_mid_arr[((i*2)/2)].m_obj.m_x before m_mid_arr[((i*2)/2) + 1].m_obj.m_x;
m_mid_arr[((i*2)/2)].m_obj.m_x != m_mid_arr[((i*2)/2) + 1].m_obj.m_x;
}
}
endclass
module t_constraint_global_arr_unsup;