parent
6b3aebfa32
commit
967b1bae57
|
|
@ -515,18 +515,22 @@ bool VlRandomizer::nextRandomize(VlRNG& rngr, bool checkOnly) {
|
||||||
|
|
||||||
std::vector<std::string> VlRandomizer::buildUniqueExprs() const {
|
std::vector<std::string> VlRandomizer::buildUniqueExprs() const {
|
||||||
std::vector<std::string> exprs;
|
std::vector<std::string> exprs;
|
||||||
|
if (m_unique_arrays.empty()) return exprs;
|
||||||
|
const auto arrVarsp = std::make_shared<const ArrayInfoMap>(m_arr_vars);
|
||||||
for (const std::string& baseName : m_unique_arrays) {
|
for (const std::string& baseName : m_unique_arrays) {
|
||||||
const auto it = m_vars.find(baseName);
|
const auto it = m_vars.find(baseName);
|
||||||
if (it == m_vars.end()) continue;
|
if (it == m_vars.end()) continue;
|
||||||
const uint32_t size = m_unique_array_sizes.at(baseName);
|
const VlRandomVar& var = *it->second;
|
||||||
std::string distinctExpr = "(__Vbv (distinct";
|
// Select the elements the array actually holds now, by their own index
|
||||||
for (uint32_t i = 0; i < size; ++i) {
|
// or key, rather than by ordinal position
|
||||||
char hexIdx[12];
|
var.setArrayInfo(arrVarsp);
|
||||||
(void)VL_SNPRINTF(hexIdx, sizeof(hexIdx), "#x%08x", i);
|
// 'distinct' needs at least two operands; fewer elements are trivially unique
|
||||||
distinctExpr += " (select " + it->first + " " + hexIdx + ")";
|
if (var.countMatchingElements(*arrVarsp, baseName) < 2) continue;
|
||||||
}
|
std::ostringstream os;
|
||||||
distinctExpr += "))";
|
os << "(__Vbv (distinct ";
|
||||||
exprs.push_back(std::move(distinctExpr));
|
var.emitGetValue(os);
|
||||||
|
os << "))";
|
||||||
|
exprs.push_back(os.str());
|
||||||
}
|
}
|
||||||
return exprs;
|
return exprs;
|
||||||
}
|
}
|
||||||
|
|
@ -917,6 +921,7 @@ void VlRandomizer::clearConstraints() {
|
||||||
m_constraints_line.clear();
|
m_constraints_line.clear();
|
||||||
m_solveBefore.clear();
|
m_solveBefore.clear();
|
||||||
m_softConstraints.clear();
|
m_softConstraints.clear();
|
||||||
|
m_unique_arrays.clear(); // Re-registered by constraint setup
|
||||||
// Keep m_vars for class member randomization
|
// Keep m_vars for class member randomization
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -242,8 +242,7 @@ class VlRandomizer VL_NOT_FINAL {
|
||||||
std::set<std::string> m_disabledVars; // Variables with rand_mode off (skip write-back)
|
std::set<std::string> m_disabledVars; // Variables with rand_mode off (skip write-back)
|
||||||
// variables
|
// variables
|
||||||
ArrayInfoMap m_arr_vars; // Tracks each element in array structures for iteration
|
ArrayInfoMap m_arr_vars; // Tracks each element in array structures for iteration
|
||||||
std::vector<std::string> m_unique_arrays;
|
std::vector<std::string> m_unique_arrays; // Arrays whose elements must be distinct
|
||||||
std::map<std::string, uint32_t> m_unique_array_sizes;
|
|
||||||
const VlQueue<CData>* m_randmodep = nullptr; // rand_mode state;
|
const VlQueue<CData>* m_randmodep = nullptr; // rand_mode state;
|
||||||
const VlQueue<CData>* m_static_randmodep = nullptr; // Static rand_mode state (shared)
|
const VlQueue<CData>* m_static_randmodep = nullptr; // Static rand_mode state (shared)
|
||||||
std::unordered_set<std::string> m_staticVars; // Names of static rand vars
|
std::unordered_set<std::string> m_staticVars; // Names of static rand vars
|
||||||
|
|
@ -515,11 +514,10 @@ public:
|
||||||
++m_index;
|
++m_index;
|
||||||
}
|
}
|
||||||
|
|
||||||
// This is the "Sender" API for the generated code
|
// This is the "Sender" API for the generated code.
|
||||||
void rand_unique(const std::string& name, uint32_t size) {
|
// The elements to make distinct are taken from the array element table at
|
||||||
m_unique_arrays.push_back(name);
|
// solve time, so a container resized by the solver is handled correctly.
|
||||||
m_unique_array_sizes[name] = size;
|
void rand_unique(const std::string& name) { m_unique_arrays.push_back(name); }
|
||||||
}
|
|
||||||
|
|
||||||
// Recursively record all elements in an unpacked array
|
// Recursively record all elements in an unpacked array
|
||||||
template <typename T, std::size_t N_Depth>
|
template <typename T, std::size_t N_Depth>
|
||||||
|
|
|
||||||
|
|
@ -2385,7 +2385,6 @@ class ConstraintExprVisitor final : public VNVisitor {
|
||||||
pushDeletep(nodep->unlinkFrBack());
|
pushDeletep(nodep->unlinkFrBack());
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
UASSERT_OBJ(m_classp, nodep, "m_classp not set");
|
|
||||||
|
|
||||||
FileLine* const fl = nodep->fileline();
|
FileLine* const fl = nodep->fileline();
|
||||||
|
|
||||||
|
|
@ -2408,16 +2407,51 @@ class ConstraintExprVisitor final : public VNVisitor {
|
||||||
AstNodeModule* const genModp = VN_AS(genVarp->user2p(), NodeModule);
|
AstNodeModule* const genModp = VN_AS(genVarp->user2p(), NodeModule);
|
||||||
UASSERT_OBJ(genModp, nodep, "genVarp has no NodeModule set");
|
UASSERT_OBJ(genModp, nodep, "genVarp has no NodeModule set");
|
||||||
|
|
||||||
|
// Registration calls emitted where the unique statement stood, so they end up
|
||||||
|
// in the constraint setup task and re-run on every randomize()
|
||||||
|
AstNode* setupStmtsp = nullptr;
|
||||||
|
// Under a condition the distinctness must instead become part of the guarded
|
||||||
|
// constraint expression, which needs an element count known at verilation time
|
||||||
|
std::vector<std::string> smtExprs;
|
||||||
for (AstNode* itemp = nodep->rangesp(); itemp; itemp = itemp->nextp()) {
|
for (AstNode* itemp = nodep->rangesp(); itemp; itemp = itemp->nextp()) {
|
||||||
if (AstVarRef* const varRefp = VN_CAST(itemp, VarRef)) {
|
if (AstVarRef* const varRefp = VN_CAST(itemp, VarRef)) {
|
||||||
AstVar* const varp = varRefp->varp();
|
AstVar* const varp = varRefp->varp();
|
||||||
AstNodeModule* const varModp = VN_AS(varp->user2p(), NodeModule);
|
AstNodeModule* const varModp = VN_AS(varp->user2p(), NodeModule);
|
||||||
UASSERT_OBJ(varModp, nodep, "varp has no NodeModule set");
|
UASSERT_OBJ(varModp, nodep, "varp has no NodeModule set");
|
||||||
AstNodeDType* const dtypep = varp->dtypep()->skipRefp();
|
AstNodeDType* const dtypep = varp->dtypep()->skipRefp();
|
||||||
AstConst* dtypeWidthp = nullptr;
|
|
||||||
|
|
||||||
// Ensure it is ONLY 1-D by checking that the sub-type is NOT an array/queue
|
const static auto dynDTypeSupported
|
||||||
AstNodeDType* const subp = dtypep->subDTypep()->skipRefp();
|
= [](const AstNodeDType* const dtypep) -> bool {
|
||||||
|
return VN_IS(dtypep, DynArrayDType) || VN_IS(dtypep, QueueDType)
|
||||||
|
|| VN_IS(dtypep, AssocArrayDType);
|
||||||
|
};
|
||||||
|
|
||||||
|
// Establish it is an array before asking for its element type
|
||||||
|
uint64_t elemWidth;
|
||||||
|
uint32_t staticSize = 0; // Element count, zero when only known at run time
|
||||||
|
if (const AstUnpackArrayDType* const up = VN_CAST(dtypep, UnpackArrayDType)) {
|
||||||
|
const AstRange* const rangep = up->rangep();
|
||||||
|
UASSERT_OBJ(rangep && VN_IS(rangep->leftp(), Const)
|
||||||
|
&& VN_IS(rangep->rightp(), Const),
|
||||||
|
nodep, "Unpack array does not have a constant range");
|
||||||
|
staticSize = up->elementsConst();
|
||||||
|
if (staticSize > 100) {
|
||||||
|
nodep->v3warn(
|
||||||
|
CONSTRAINTIGN,
|
||||||
|
"Unsupported: Unique constraint on static arrays of size > 100");
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
elemWidth = static_cast<uint64_t>(varp->dtypep()->width());
|
||||||
|
} else if (dynDTypeSupported(dtypep)) {
|
||||||
|
elemWidth = static_cast<uint64_t>(dtypep->subDTypep()->width());
|
||||||
|
} else {
|
||||||
|
nodep->v3warn(CONSTRAINTIGN, "Unsupported: Unique constraint on "
|
||||||
|
<< dtypep->prettyDTypeName(false));
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Ensure it is ONLY 1-D by checking that the element type is not an array/queue
|
||||||
|
const AstNodeDType* const subp = dtypep->subDTypep()->skipRefp();
|
||||||
if (VN_IS(subp, NodeArrayDType) || VN_IS(subp, QueueDType)
|
if (VN_IS(subp, NodeArrayDType) || VN_IS(subp, QueueDType)
|
||||||
|| VN_IS(subp, DynArrayDType) || VN_IS(subp, AssocArrayDType)
|
|| VN_IS(subp, DynArrayDType) || VN_IS(subp, AssocArrayDType)
|
||||||
|| VN_IS(subp, WildcardArrayDType)) {
|
|| VN_IS(subp, WildcardArrayDType)) {
|
||||||
|
|
@ -2426,80 +2460,77 @@ class ConstraintExprVisitor final : public VNVisitor {
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
|
||||||
const static auto dynDTypeSupported
|
if (m_wantSingle && !staticSize) {
|
||||||
= [](const AstNodeDType* const dtypep) -> bool {
|
nodep->v3warn(CONSTRAINTIGN,
|
||||||
return VN_IS(dtypep, DynArrayDType) || VN_IS(dtypep, QueueDType)
|
"Unsupported: Unique constraint on dynamically sized array "
|
||||||
|| VN_IS(dtypep, AssocArrayDType);
|
"inside conditional constraint");
|
||||||
};
|
|
||||||
|
|
||||||
if (AstUnpackArrayDType* const up = VN_CAST(dtypep, UnpackArrayDType)) {
|
|
||||||
const AstRange* const rangep = up->rangep();
|
|
||||||
UASSERT_OBJ(rangep && VN_IS(rangep->leftp(), Const)
|
|
||||||
&& VN_IS(rangep->rightp(), Const),
|
|
||||||
nodep, "Unpack array does not have a constant range");
|
|
||||||
dtypeWidthp = new AstConst{fl, AstConst::Unsized64{},
|
|
||||||
static_cast<uint64_t>(varp->dtypep()->width())};
|
|
||||||
} else if (dynDTypeSupported(dtypep)) {
|
|
||||||
dtypeWidthp
|
|
||||||
= new AstConst{fl, AstConst::Unsized64{},
|
|
||||||
static_cast<uint64_t>(dtypep->subDTypep()->width())};
|
|
||||||
} else {
|
|
||||||
nodep->v3warn(CONSTRAINTIGN, "Unsupported: Unique constraint on "
|
|
||||||
<< dtypep->prettyDTypeName(false));
|
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
|
||||||
// convert to c string
|
if (!varp->user3()) {
|
||||||
AstNodeExpr* const varnamep = new AstCExpr{
|
varp->user3(true); // Solver owns it; __VBasicRand must not overwrite
|
||||||
fl, AstCExpr::Pure{}, "\"" + varp->name() + "\"", varp->width()};
|
// Convert to C string
|
||||||
|
AstNodeExpr* const varnamep = new AstCExpr{
|
||||||
|
fl, AstCExpr::Pure{}, "\"" + varp->name() + "\"", varp->width()};
|
||||||
|
|
||||||
AstCMethodHard* const writeVarCallp
|
AstCMethodHard* const writeVarCallp = new AstCMethodHard{
|
||||||
= new AstCMethodHard{fl, new AstVarRef{fl, genModp, genVarp, VAccess::READ},
|
fl, new AstVarRef{fl, genModp, genVarp, VAccess::READ},
|
||||||
VCMethod::RANDOMIZER_WRITE_VAR};
|
VCMethod::RANDOMIZER_WRITE_VAR};
|
||||||
writeVarCallp->addPinsp(new AstVarRef{fl, varModp, varp, VAccess::READ});
|
writeVarCallp->addPinsp(new AstVarRef{fl, varModp, varp, VAccess::READ});
|
||||||
writeVarCallp->addPinsp(dtypeWidthp);
|
writeVarCallp->addPinsp(new AstConst{fl, AstConst::Unsized64{}, elemWidth});
|
||||||
writeVarCallp->addPinsp(varnamep);
|
writeVarCallp->addPinsp(varnamep);
|
||||||
writeVarCallp->addPinsp(new AstConst{fl, 1}); // Dimension
|
writeVarCallp->addPinsp(new AstConst{fl, 1}); // Dimension
|
||||||
|
const RandomizeMode randMode = {.asInt = varp->user1()};
|
||||||
writeVarCallp->dtypeSetVoid();
|
if (randMode.usesMode) {
|
||||||
initTaskp->addStmtsp(new AstStmtExpr{fl, writeVarCallp});
|
writeVarCallp->addPinsp(
|
||||||
|
new AstConst{fl, AstConst::Unsized64{}, randMode.index});
|
||||||
AstNodeExpr* const randUniquePinsp
|
|
||||||
= new AstConst{fl, AstConst::String{}, varp->name()};
|
|
||||||
|
|
||||||
if (AstUnpackArrayDType* const adtypep
|
|
||||||
= VN_CAST(varp->dtypep(), UnpackArrayDType)) {
|
|
||||||
uint32_t arraySize = adtypep->elementsConst();
|
|
||||||
if (arraySize > 100) {
|
|
||||||
nodep->v3warn(
|
|
||||||
CONSTRAINTIGN,
|
|
||||||
"Unsupported: Unique constraint on static arrays of size > 100");
|
|
||||||
VL_DO_DANGLING(randUniquePinsp->deleteTree(), randUniquePinsp);
|
|
||||||
continue;
|
|
||||||
}
|
}
|
||||||
randUniquePinsp->addNext(new AstConst{fl, arraySize});
|
writeVarCallp->dtypeSetVoid();
|
||||||
} else if (dynDTypeSupported(dtypep)) { // LCOV_EXCL_BR_LINE
|
initTaskp->addStmtsp(new AstStmtExpr{fl, writeVarCallp});
|
||||||
const VCMethod sizeMethod = VN_IS(dtypep, AssocArrayDType)
|
}
|
||||||
? VCMethod::ASSOC_SIZE
|
|
||||||
: VCMethod::DYN_SIZE;
|
// A solver-sized container is resized between solve passes; joining the
|
||||||
AstCMethodHard* const dynSizep = new AstCMethodHard{
|
// size-constrained set gets its element table refreshed in between
|
||||||
fl, new AstVarRef{fl, varModp, varp, VAccess::READ}, sizeMethod};
|
if (varp->user4p() && m_sizeConstrainedArraysp) {
|
||||||
dynSizep->dtypeSetUInt32();
|
m_sizeConstrainedArraysp->insert(varp);
|
||||||
// unable to check dynamic array size during verilation
|
}
|
||||||
randUniquePinsp->addNext(dynSizep);
|
|
||||||
} else {
|
if (m_wantSingle) {
|
||||||
varp->v3fatalSrc("Unexpected variable type "
|
// Fewer than two elements are trivially distinct
|
||||||
<< varp->dtypep()->prettyDTypeNameQ());
|
if (staticSize < 2) continue;
|
||||||
|
std::string exprStr = "(__Vbv (distinct";
|
||||||
|
for (uint32_t i = 0; i < staticSize; ++i) {
|
||||||
|
exprStr += " (select " + varp->name() + " #x";
|
||||||
|
for (int shift = 28; shift >= 0; shift -= 4) {
|
||||||
|
exprStr += "0123456789abcdef"[(i >> shift) & 0xf];
|
||||||
|
}
|
||||||
|
exprStr += ')';
|
||||||
|
}
|
||||||
|
smtExprs.emplace_back(exprStr + "))");
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
AstNodeExpr* const namep = new AstConst{fl, AstConst::String{}, varp->name()};
|
||||||
AstCMethodHard* const randUniqueCallp
|
AstCMethodHard* const randUniqueCallp
|
||||||
= new AstCMethodHard{fl, new AstVarRef{fl, genModp, genVarp, VAccess::READ},
|
= new AstCMethodHard{fl, new AstVarRef{fl, genModp, genVarp, VAccess::READ},
|
||||||
VCMethod::RANDOMIZER_UNIQUE, randUniquePinsp};
|
VCMethod::RANDOMIZER_UNIQUE, namep};
|
||||||
randUniqueCallp->dtypep(nodep->findVoidDType());
|
randUniqueCallp->dtypep(nodep->findVoidDType());
|
||||||
initTaskp->addStmtsp(new AstStmtExpr{fl, randUniqueCallp});
|
setupStmtsp = AstNode::addNext(setupStmtsp, new AstStmtExpr{fl, randUniqueCallp});
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
if (m_wantSingle && !smtExprs.empty()) {
|
||||||
|
std::string exprStr = smtExprs.front();
|
||||||
|
if (smtExprs.size() > 1) {
|
||||||
|
exprStr = "(bvand";
|
||||||
|
for (const std::string& oneExprp : smtExprs) exprStr += " " + oneExprp;
|
||||||
|
exprStr += ')';
|
||||||
|
}
|
||||||
|
AstSFormatF* const newp = new AstSFormatF{fl, exprStr, false, nullptr};
|
||||||
|
nodep->replaceWith(newp);
|
||||||
|
VL_DO_DANGLING(pushDeletep(nodep), nodep);
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
if (setupStmtsp) nodep->addHereThisAsNext(setupStmtsp);
|
||||||
nodep->unlinkFrBack();
|
nodep->unlinkFrBack();
|
||||||
VL_DO_DANGLING(pushDeletep(nodep), nodep);
|
VL_DO_DANGLING(pushDeletep(nodep), nodep);
|
||||||
}
|
}
|
||||||
|
|
@ -3381,10 +3412,23 @@ class RandomizeVisitor final : public VNVisitor {
|
||||||
}
|
}
|
||||||
// Expand unique{a,b,c} with explicit elements into pairwise != constraints.
|
// Expand unique{a,b,c} with explicit elements into pairwise != constraints.
|
||||||
// Whole-array unique{arr} is left for ConstraintExprVisitor's rand_unique handling.
|
// Whole-array unique{arr} is left for ConstraintExprVisitor's rand_unique handling.
|
||||||
|
// Recurses into conditional and foreach bodies, so that the pairwise
|
||||||
|
// constraints stay under the guard they were written under.
|
||||||
static void expandUniqueElementList(AstNode* itemsp) {
|
static void expandUniqueElementList(AstNode* itemsp) {
|
||||||
AstNode* itemp = itemsp;
|
AstNode* itemp = itemsp;
|
||||||
while (itemp) {
|
while (itemp) {
|
||||||
AstNode* const nextp = itemp->nextp();
|
AstNode* const nextp = itemp->nextp();
|
||||||
|
if (const AstConstraintIf* const ifp = VN_CAST(itemp, ConstraintIf)) {
|
||||||
|
expandUniqueElementList(ifp->thensp());
|
||||||
|
expandUniqueElementList(ifp->elsesp());
|
||||||
|
itemp = nextp;
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
if (const AstConstraintForeach* const foreachp = VN_CAST(itemp, ConstraintForeach)) {
|
||||||
|
expandUniqueElementList(foreachp->bodyp());
|
||||||
|
itemp = nextp;
|
||||||
|
continue;
|
||||||
|
}
|
||||||
AstConstraintUnique* const uniquep = VN_CAST(itemp, ConstraintUnique);
|
AstConstraintUnique* const uniquep = VN_CAST(itemp, ConstraintUnique);
|
||||||
if (!uniquep) {
|
if (!uniquep) {
|
||||||
itemp = nextp;
|
itemp = nextp;
|
||||||
|
|
@ -3394,8 +3438,12 @@ class RandomizeVisitor final : public VNVisitor {
|
||||||
std::vector<AstNodeExpr*> exprItems;
|
std::vector<AstNodeExpr*> exprItems;
|
||||||
bool hasArrayVarRef = false;
|
bool hasArrayVarRef = false;
|
||||||
for (AstNode* rp = uniquep->rangesp(); rp; rp = rp->nextp()) {
|
for (AstNode* rp = uniquep->rangesp(); rp; rp = rp->nextp()) {
|
||||||
if (AstVarRef* const vrp = VN_CAST(rp, VarRef)) {
|
if (const AstVarRef* const vrp = VN_CAST(rp, VarRef)) {
|
||||||
if (VN_IS(vrp->varp()->dtypep()->skipRefp(), UnpackArrayDType)) {
|
// A container's elements are made distinct by rand_unique, not pairwise
|
||||||
|
const AstNodeDType* const dtypep = vrp->varp()->dtypep()->skipRefp();
|
||||||
|
if (VN_IS(dtypep, NodeArrayDType) || VN_IS(dtypep, QueueDType)
|
||||||
|
|| VN_IS(dtypep, DynArrayDType) || VN_IS(dtypep, AssocArrayDType)
|
||||||
|
|| VN_IS(dtypep, WildcardArrayDType)) {
|
||||||
hasArrayVarRef = true;
|
hasArrayVarRef = true;
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
|
@ -3419,6 +3467,10 @@ class RandomizeVisitor final : public VNVisitor {
|
||||||
uniquep->unlinkFrBack();
|
uniquep->unlinkFrBack();
|
||||||
VL_DO_DANGLING(uniquep->deleteTree(), uniquep);
|
VL_DO_DANGLING(uniquep->deleteTree(), uniquep);
|
||||||
}
|
}
|
||||||
|
} else if (exprItems.size() == 1 && !hasArrayVarRef) {
|
||||||
|
// A set of one element is unique whatever that element holds
|
||||||
|
uniquep->unlinkFrBack();
|
||||||
|
VL_DO_DANGLING(uniquep->deleteTree(), uniquep);
|
||||||
}
|
}
|
||||||
itemp = nextp;
|
itemp = nextp;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,23 @@
|
||||||
|
#!/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()
|
||||||
|
|
||||||
|
# Deliberately unsatisfiable randomize() calls check that the guarded
|
||||||
|
# constraint is applied; their warnings are not of interest here
|
||||||
|
test.execute(all_run_flags=['+verilator+wno+unsatconstr+1'])
|
||||||
|
|
||||||
|
test.passes()
|
||||||
|
|
@ -0,0 +1,102 @@
|
||||||
|
// DESCRIPTION: Verilator: Verilog Test module
|
||||||
|
//
|
||||||
|
// This file ONLY is placed under the Creative Commons Public Domain
|
||||||
|
// SPDX-FileCopyrightText: 2026 BRDR LIFE
|
||||||
|
// SPDX-License-Identifier: CC0-1.0
|
||||||
|
|
||||||
|
// A 'unique' nested in a constraint 'if' arm, over scalar rand members or over
|
||||||
|
// a statically sized array, applies only when the arm's condition holds.
|
||||||
|
|
||||||
|
// verilog_format: off
|
||||||
|
`define stop $stop
|
||||||
|
`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%x exp='h%x\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0)
|
||||||
|
`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
|
||||||
|
|
||||||
|
class C;
|
||||||
|
rand bit [1:0] x, y, z;
|
||||||
|
rand bit sel;
|
||||||
|
|
||||||
|
constraint c {
|
||||||
|
if (sel) {
|
||||||
|
unique {x, y, z};
|
||||||
|
} else {
|
||||||
|
unique {x, y};
|
||||||
|
}
|
||||||
|
}
|
||||||
|
endclass
|
||||||
|
|
||||||
|
class A;
|
||||||
|
rand bit [1:0] arr[4];
|
||||||
|
rand bit [1:0] one[1];
|
||||||
|
rand bit sel;
|
||||||
|
|
||||||
|
constraint c {
|
||||||
|
if (sel) {
|
||||||
|
unique {arr};
|
||||||
|
// A single element is trivially unique
|
||||||
|
unique {one};
|
||||||
|
}
|
||||||
|
}
|
||||||
|
endclass
|
||||||
|
|
||||||
|
module t;
|
||||||
|
initial begin
|
||||||
|
automatic C c = new;
|
||||||
|
automatic A a = new;
|
||||||
|
int ok;
|
||||||
|
|
||||||
|
// The 'then' arm holds: its operands are pairwise distinct
|
||||||
|
for (int i = 0; i < 20; ++i) begin
|
||||||
|
ok = c.randomize() with {sel == 1;};
|
||||||
|
`checkd(ok, 1);
|
||||||
|
`checkh(c.x == c.y, 1'b0);
|
||||||
|
`checkh(c.x == c.z, 1'b0);
|
||||||
|
`checkh(c.y == c.z, 1'b0);
|
||||||
|
end
|
||||||
|
// and cannot be violated
|
||||||
|
ok = c.randomize() with {
|
||||||
|
sel == 1;
|
||||||
|
x == y;
|
||||||
|
};
|
||||||
|
`checkd(ok, 0);
|
||||||
|
|
||||||
|
// The 'else' arm holds: only its own operands are constrained
|
||||||
|
for (int i = 0; i < 20; ++i) begin
|
||||||
|
ok = c.randomize() with {sel == 0;};
|
||||||
|
`checkd(ok, 1);
|
||||||
|
`checkh(c.x == c.y, 1'b0);
|
||||||
|
end
|
||||||
|
ok = c.randomize() with {
|
||||||
|
sel == 0;
|
||||||
|
y == z;
|
||||||
|
};
|
||||||
|
`checkd(ok, 1);
|
||||||
|
ok = c.randomize() with {
|
||||||
|
sel == 0;
|
||||||
|
x == y;
|
||||||
|
};
|
||||||
|
`checkd(ok, 0);
|
||||||
|
|
||||||
|
// An array 'unique' under the same guard: four distinct 2-bit values are a
|
||||||
|
// permutation of 0..3, and are unconstrained once the guard is false
|
||||||
|
for (int i = 0; i < 20; ++i) begin
|
||||||
|
ok = a.randomize() with {sel == 1;};
|
||||||
|
`checkd(ok, 1);
|
||||||
|
foreach (a.arr[j]) foreach (a.arr[k]) if (j != k) `checkh(a.arr[j] == a.arr[k], 1'b0);
|
||||||
|
end
|
||||||
|
ok = a.randomize() with {
|
||||||
|
sel == 1;
|
||||||
|
arr[0] == arr[1];
|
||||||
|
};
|
||||||
|
`checkd(ok, 0);
|
||||||
|
ok = a.randomize() with {
|
||||||
|
sel == 0;
|
||||||
|
arr[0] == arr[1];
|
||||||
|
};
|
||||||
|
`checkd(ok, 1);
|
||||||
|
|
||||||
|
$write("*-* All Finished *-*\n");
|
||||||
|
$finish;
|
||||||
|
end
|
||||||
|
endmodule
|
||||||
|
|
@ -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()
|
||||||
|
|
@ -0,0 +1,73 @@
|
||||||
|
// DESCRIPTION: Verilator: Verilog Test module
|
||||||
|
//
|
||||||
|
// This file ONLY is placed under the Creative Commons Public Domain
|
||||||
|
// SPDX-FileCopyrightText: 2026 BRDR LIFE
|
||||||
|
// SPDX-License-Identifier: CC0-1.0
|
||||||
|
|
||||||
|
// A 'unique' constraint holds over containers whose element count is only
|
||||||
|
// settled at randomize() time, and over an array it constrains on its own.
|
||||||
|
|
||||||
|
// verilog_format: off
|
||||||
|
`define stop $stop
|
||||||
|
`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%x exp='h%x\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0)
|
||||||
|
`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
|
||||||
|
|
||||||
|
class Sized;
|
||||||
|
rand bit [3:0] q[$];
|
||||||
|
rand bit [3:0] d[];
|
||||||
|
|
||||||
|
constraint sz {
|
||||||
|
q.size() == 3;
|
||||||
|
d.size() == 5;
|
||||||
|
}
|
||||||
|
constraint uniq {
|
||||||
|
unique {q};
|
||||||
|
unique {d};
|
||||||
|
}
|
||||||
|
endclass
|
||||||
|
|
||||||
|
class Tiny;
|
||||||
|
rand bit [3:0] q[$];
|
||||||
|
|
||||||
|
constraint sz {q.size() == 1;}
|
||||||
|
constraint uniq {unique {q};}
|
||||||
|
endclass
|
||||||
|
|
||||||
|
class Sole;
|
||||||
|
rand bit [1:0] arr[4];
|
||||||
|
|
||||||
|
constraint uniq {unique {arr};}
|
||||||
|
endclass
|
||||||
|
|
||||||
|
module t;
|
||||||
|
initial begin
|
||||||
|
automatic Sized sized = new;
|
||||||
|
automatic Tiny tiny = new;
|
||||||
|
automatic Sole sole = new;
|
||||||
|
int ok;
|
||||||
|
|
||||||
|
for (int n = 0; n < 10; ++n) begin
|
||||||
|
ok = sized.randomize();
|
||||||
|
`checkd(ok, 1);
|
||||||
|
`checkd(sized.q.size(), 3);
|
||||||
|
`checkd(sized.d.size(), 5);
|
||||||
|
foreach (sized.q[i]) foreach (sized.q[j]) if (i != j) `checkh(sized.q[i] == sized.q[j], 1'b0);
|
||||||
|
foreach (sized.d[i]) foreach (sized.d[j]) if (i != j) `checkh(sized.d[i] == sized.d[j], 1'b0);
|
||||||
|
|
||||||
|
// A single element is trivially unique
|
||||||
|
ok = tiny.randomize();
|
||||||
|
`checkd(ok, 1);
|
||||||
|
`checkd(tiny.q.size(), 1);
|
||||||
|
|
||||||
|
// Four distinct 2-bit values are a permutation of 0..3
|
||||||
|
ok = sole.randomize();
|
||||||
|
`checkd(ok, 1);
|
||||||
|
foreach (sole.arr[i])
|
||||||
|
foreach (sole.arr[j]) if (i != j) `checkh(sole.arr[i] == sole.arr[j], 1'b0);
|
||||||
|
end
|
||||||
|
|
||||||
|
$write("*-* All Finished *-*\n");
|
||||||
|
$finish;
|
||||||
|
end
|
||||||
|
endmodule
|
||||||
|
|
@ -0,0 +1,23 @@
|
||||||
|
#!/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()
|
||||||
|
|
||||||
|
# Deliberately unsatisfiable randomize() calls check that the constraint is
|
||||||
|
# applied; their warnings are not of interest here
|
||||||
|
test.execute(all_run_flags=['+verilator+wno+unsatconstr+1'])
|
||||||
|
|
||||||
|
test.passes()
|
||||||
|
|
@ -0,0 +1,56 @@
|
||||||
|
// DESCRIPTION: Verilator: Verilog Test module
|
||||||
|
//
|
||||||
|
// This file ONLY is placed under the Creative Commons Public Domain
|
||||||
|
// SPDX-FileCopyrightText: 2026 BRDR LIFE
|
||||||
|
// SPDX-License-Identifier: CC0-1.0
|
||||||
|
|
||||||
|
// A 'unique' constraint takes part in constraint_mode(), and a 'unique' over a
|
||||||
|
// typedef'd array resolves through the typedef.
|
||||||
|
|
||||||
|
// verilog_format: off
|
||||||
|
`define stop $stop
|
||||||
|
`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%x exp='h%x\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0)
|
||||||
|
`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
|
||||||
|
|
||||||
|
typedef bit [1:0] arr_t[4];
|
||||||
|
|
||||||
|
class C;
|
||||||
|
rand arr_t arr;
|
||||||
|
|
||||||
|
constraint uniq {unique {arr};}
|
||||||
|
endclass
|
||||||
|
|
||||||
|
module t;
|
||||||
|
initial begin
|
||||||
|
automatic C c = new;
|
||||||
|
int ok;
|
||||||
|
|
||||||
|
// Four distinct 2-bit values are a permutation of 0..3
|
||||||
|
for (int i = 0; i < 10; ++i) begin
|
||||||
|
ok = c.randomize();
|
||||||
|
`checkd(ok, 1);
|
||||||
|
foreach (c.arr[j]) foreach (c.arr[k]) if (j != k) `checkh(c.arr[j] == c.arr[k], 1'b0);
|
||||||
|
end
|
||||||
|
ok = c.randomize() with {arr[0] == arr[1];};
|
||||||
|
`checkd(ok, 0);
|
||||||
|
|
||||||
|
// Disabled, the array is unconstrained
|
||||||
|
c.uniq.constraint_mode(0);
|
||||||
|
ok = c.randomize() with {arr[0] == arr[1];};
|
||||||
|
`checkd(ok, 1);
|
||||||
|
|
||||||
|
// Enabled again, distinctness is back
|
||||||
|
c.uniq.constraint_mode(1);
|
||||||
|
ok = c.randomize() with {arr[0] == arr[1];};
|
||||||
|
`checkd(ok, 0);
|
||||||
|
for (int i = 0; i < 10; ++i) begin
|
||||||
|
ok = c.randomize();
|
||||||
|
`checkd(ok, 1);
|
||||||
|
foreach (c.arr[j]) foreach (c.arr[k]) if (j != k) `checkh(c.arr[j] == c.arr[k], 1'b0);
|
||||||
|
end
|
||||||
|
|
||||||
|
$write("*-* All Finished *-*\n");
|
||||||
|
$finish;
|
||||||
|
end
|
||||||
|
endmodule
|
||||||
|
|
@ -0,0 +1,10 @@
|
||||||
|
%Warning-CONSTRAINTIGN: t/t_constraint_unique_unsup.v:17:7: Unsupported: Unique constraint on dynamically sized array inside conditional constraint
|
||||||
|
17 | unique {q};
|
||||||
|
| ^~~~~~
|
||||||
|
... For warning description see https://verilator.org/warn/CONSTRAINTIGN?v=latest
|
||||||
|
... Use "/* verilator lint_off CONSTRAINTIGN */" and lint_on around source to disable this message.
|
||||||
|
%Warning-CONSTRAINTIGN: t/t_constraint_unique_unsup.v:21:31: Unsupported: Unique constraint on bit[3:0]
|
||||||
|
: ... note: In instance 't'
|
||||||
|
21 | constraint scalar_vs_array {unique {x, arr};}
|
||||||
|
| ^~~~~~
|
||||||
|
%Error: Exiting due to
|
||||||
|
|
@ -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('vlt')
|
||||||
|
|
||||||
|
test.lint(fails=test.vlt_all, expect_filename=test.golden_filename)
|
||||||
|
|
||||||
|
test.passes()
|
||||||
|
|
@ -0,0 +1,29 @@
|
||||||
|
// DESCRIPTION: Verilator: Verilog Test module
|
||||||
|
//
|
||||||
|
// This file ONLY is placed under the Creative Commons Public Domain
|
||||||
|
// SPDX-FileCopyrightText: 2026 BRDR LIFE
|
||||||
|
// SPDX-License-Identifier: CC0-1.0
|
||||||
|
|
||||||
|
class C;
|
||||||
|
rand bit [3:0] q[$];
|
||||||
|
rand bit [3:0] arr[4];
|
||||||
|
rand bit [3:0] x;
|
||||||
|
rand bit sel;
|
||||||
|
|
||||||
|
constraint sz {q.size() == 3;}
|
||||||
|
// A container sized at run time has no element count to guard on
|
||||||
|
constraint cond_dyn {
|
||||||
|
if (sel) {
|
||||||
|
unique {q};
|
||||||
|
}
|
||||||
|
}
|
||||||
|
// A scalar cannot be made distinct from the elements of an array
|
||||||
|
constraint scalar_vs_array {unique {x, arr};}
|
||||||
|
endclass
|
||||||
|
|
||||||
|
module t;
|
||||||
|
initial begin
|
||||||
|
automatic C c = new;
|
||||||
|
void'(c.randomize());
|
||||||
|
end
|
||||||
|
endmodule
|
||||||
|
|
@ -5,8 +5,7 @@
|
||||||
// SPDX-License-Identifier: CC0-1.0
|
// SPDX-License-Identifier: CC0-1.0
|
||||||
|
|
||||||
// Based on t_constraint_unsup_unq_arr.v
|
// Based on t_constraint_unsup_unq_arr.v
|
||||||
// We only check uniqueness for small # of elements on a large range
|
// Every element of each unique-constrained container differs from every other.
|
||||||
// as Z3 does not actually give unique elements (bug?) as of Jul 2026.
|
|
||||||
|
|
||||||
class Subclass;
|
class Subclass;
|
||||||
rand int sub_arr[];
|
rand int sub_arr[];
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue