address review: refine and rename func, and reject solve before on assoc arr as unsupported

This commit is contained in:
Yilou Wang 2026-07-09 16:51:53 +02:00
parent ccca5273a4
commit 401dda07ae
7 changed files with 82 additions and 6 deletions

View File

@ -998,15 +998,15 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) {
// Step 3: Solve phase by phase // Step 3: Solve phase by phase
std::map<std::string, std::string> solvedValues; // varName -> SMT value literal std::map<std::string, std::string> solvedValues; // varName -> SMT value literal
bool hasNonEnumArray = false; bool needsAllLogic = false;
for (const auto& var : m_vars) { for (const auto& var : m_vars) {
if (var.second->dimension() == 0) continue; if (var.second->dimension() == 0) continue;
if (var.second->countMatchingElements(m_arr_vars, var.second->name()) == 0) { if (!var.second->hasMatchingElements(m_arr_vars, var.second->name())) {
hasNonEnumArray = true; needsAllLogic = true;
break; break;
} }
} }
const char* const logicp = hasNonEnumArray ? "ALL" : "QF_ABV"; const char* const logicp = needsAllLogic ? "ALL" : "QF_ABV";
for (size_t phase = 0; phase < layers.size(); phase++) { for (size_t phase = 0; phase < layers.size(); phase++) {
const bool isFinalPhase = (phase == layers.size() - 1); const bool isFinalPhase = (phase == layers.size() - 1);
@ -1085,8 +1085,7 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) {
auto arrVarsp = std::make_shared<const ArrayInfoMap>(m_arr_vars); auto arrVarsp = std::make_shared<const ArrayInfoMap>(m_arr_vars);
it->second->setArrayInfo(arrVarsp); it->second->setArrayInfo(arrVarsp);
// Enumerable arrays: query each element for a QF_ABV-safe pin. // Enumerable arrays: query each element for a QF_ABV-safe pin.
if (it->second->countMatchingElements(m_arr_vars, it->second->name()) if (it->second->hasMatchingElements(m_arr_vars, it->second->name())) {
> 0) {
it->second->emitGetValue(os); it->second->emitGetValue(os);
continue; continue;
} }

View File

@ -104,6 +104,9 @@ public:
count_cache[base_name] = count; count_cache[base_name] = count;
return count; return count;
} }
bool hasMatchingElements(const ArrayInfoMap& arr_vars, const std::string& base_name) const {
return arr_vars.find(base_name + "0") != arr_vars.end();
}
}; };
template <typename T> template <typename T>
class VlRandomArrayVarTemplate final : public VlRandomVar { class VlRandomArrayVarTemplate final : public VlRandomVar {

View File

@ -2162,6 +2162,16 @@ class ConstraintExprVisitor final : public VNVisitor {
// Generate solveBefore() calls for each (lhs, rhs) variable pair. // Generate solveBefore() calls for each (lhs, rhs) variable pair.
// Do NOT iterate children -- these are variable references, not constraint expressions. // Do NOT iterate children -- these are variable references, not constraint expressions.
FileLine* const fl = nodep->fileline(); FileLine* const fl = nodep->fileline();
for (AstNodeExpr* const listp : {nodep->lhssp(), nodep->rhssp()}) {
for (AstNodeExpr* ep = listp; ep; ep = VN_CAST(ep->nextp(), NodeExpr)) {
if (VN_IS(ep->dtypep()->skipRefp(), AssocArrayDType)) {
ep->v3warn(E_UNSUPPORTED,
"Unsupported: 'solve ... before' with associative array");
VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
return;
}
}
}
AstNodeModule* const genModp = VN_AS(m_genp->user2p(), NodeModule); AstNodeModule* const genModp = VN_AS(m_genp->user2p(), NodeModule);
for (AstNodeExpr* lhsp = nodep->lhssp(); lhsp; lhsp = VN_CAST(lhsp->nextp(), NodeExpr)) { for (AstNodeExpr* lhsp = nodep->lhssp(); lhsp; lhsp = VN_CAST(lhsp->nextp(), NodeExpr)) {

View File

@ -72,6 +72,17 @@ class ScFirst; // scalar solved before an array
} }
endclass endclass
class DynArr; // dynamic array solved before a scalar
rand int unsigned d[];
rand int unsigned s;
constraint c {
d.size() == 3;
solve d before s;
foreach (d[i]) d[i] inside {[1:10]};
s == d[0] + d[1] + d[2];
}
endclass
module t; module t;
OneD o1; OneD o1;
TwoD o2; TwoD o2;
@ -79,6 +90,7 @@ module t;
Chain oc; Chain oc;
Que oq; Que oq;
ScFirst osf; ScFirst osf;
DynArr odn;
int ok; int ok;
initial begin initial begin
o1 = new; o1 = new;
@ -87,6 +99,7 @@ module t;
oc = new; oc = new;
oq = new; oq = new;
osf = new; osf = new;
odn = new;
for (int i = 0; i < 10; ++i) begin for (int i = 0; i < 10; ++i) begin
ok = o1.randomize(); ok = o1.randomize();
`checkd(ok, 1); `checkd(ok, 1);
@ -115,6 +128,11 @@ module t;
`checkd(ok, 1); `checkd(ok, 1);
`checkd(osf.a[0], osf.xw); `checkd(osf.a[0], osf.xw);
`checkd(osf.a[1], osf.xw + 1); `checkd(osf.a[1], osf.xw + 1);
ok = odn.randomize();
`checkd(ok, 1);
`checkd(odn.d.size(), 3);
`checkd(odn.s, odn.d[0] + odn.d[1] + odn.d[2]);
end end
$write("*-* All Finished *-*\n"); $write("*-* All Finished *-*\n");
$finish; $finish;

View File

@ -0,0 +1,6 @@
%Error-UNSUPPORTED: t/t_constraint_solve_before_assoc_unsup.v:11:11: Unsupported: 'solve ... before' with associative array
: ... note: In instance 't'
11 | solve m before s;
| ^
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to

View File

@ -0,0 +1,16 @@
#!/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('linter')
test.lint(fails=True, expect_filename=test.golden_filename)
test.passes()

View File

@ -0,0 +1,24 @@
// 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
class Assoc;
rand int unsigned m[int];
rand int unsigned s;
constraint c {
solve m before s;
m.size() == 2;
}
endclass
module t;
Assoc o;
initial begin
o = new;
void'(o.randomize());
$write("*-* All Finished *-*\n");
$finish;
end
endmodule