diff --git a/include/verilated_random.h b/include/verilated_random.h index 96ca94e20..3b20fbba4 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -105,9 +105,7 @@ 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. +// SMT key width per associative-array level (string = 128, integral = 8 * sizeof). template struct VlRandomAssocKeyWidths final { static void push(std::vector&) {} @@ -193,9 +191,7 @@ public: } } else { if (dimension() > 0) { - // 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) + // Empty array: declare from the static key widths, not a 32-bit default. for (int i = 0; i < dimension(); ++i) { const size_t idxWidth = i < static_cast(m_fallbackIdxWidths.size()) ? m_fallbackIdxWidths[i] diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 3dfce2a4b..4066453d8 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -631,10 +631,7 @@ 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) + // Re-mark members after the class became inline-randomized above. if (classp && classp->user1() == IS_RANDOMIZED_INLINE) markMembers(classp); } void visit(AstConstraintUnique* nodep) override { @@ -1866,13 +1863,9 @@ 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. + // Keep a pre-edit clone for the rand_mode hoist below. 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, @@ -1950,9 +1943,7 @@ class ConstraintExprVisitor final : public VNVisitor { editSMT(nodep, nodep->fromp(), indexp); } else { // 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. + // Keep a pre-edit clone for the rand_mode hoist below. AstNodeExpr* const origp = nodep->cloneTree(false); AstNodeExpr* const indexp = new AstSFormatF{fl, "#x%8x", false, nodep->bitp()->unlinkFrBack(&handle)}; @@ -1963,12 +1954,7 @@ class ConstraintExprVisitor final : public VNVisitor { } } } - // 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). + // True iff exprp is an ARRAY_AT read of a class's own instance mode array. static bool isRandModeGate(const AstNodeExpr* exprp) { const AstCMethodHard* const atp = VN_CAST(exprp, CMethodHard); if (!atp || atp->method() != VCMethod::ARRAY_AT) return false; @@ -1982,15 +1968,7 @@ class ConstraintExprVisitor final : public VNVisitor { 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) ? "" : ""). - // 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 )..." : "" - // 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). + // Lift a rand_mode Cond above the (select ...) chain of a frozen array element. 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; @@ -2395,12 +2373,7 @@ 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. + // Queue/dynamic element: pre-edit clone for the rand_mode hoist, non-rand index only. bool indexIsRand = false; if (nodep->pinsp()) { nodep->pinsp()->foreach([&](const AstNodeVarRef* vrefp) { diff --git a/test_regress/t/t_randomize_scoped_arg_array_randmode.v b/test_regress/t/t_randomize_scoped_arg_array_randmode.v index 41f7887ee..20cf7b879 100644 --- a/test_regress/t/t_randomize_scoped_arg_array_randmode.v +++ b/test_regress/t/t_randomize_scoped_arg_array_randmode.v @@ -9,9 +9,7 @@ `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 idx). +// Scoped randomize(scalar) while frozen rand array members are constrained. typedef int unsigned uint; class Base; @@ -183,9 +181,7 @@ module t; 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. + // Never-populated assoc array: frozen default fails membership on the scoped call. begin EmptyAssoc ea; ea = new;