From 279392e0cfa010b956733bacbffb59d4eb7a25ed Mon Sep 17 00:00:00 2001 From: Vince Harron Date: Thu, 28 May 2026 12:01:54 -0700 Subject: [PATCH] Fixed exponential backtracking and false UNSAT errors. Replaces the inefficient bucket pre-selection strategy with a Hard Disjunction of all ranges in the distribution. This allows the SMT solver (Z3) to natively explore the valid state space, resolving the performance bottleneck and correctness issues when dist interacts with complex constraints. I also ensured that the new AST nodes are correctly marked as random-dependent (user1(true)), preventing incorrect constant-folding during SMT generation. --- docs/CONTRIBUTORS | 1 + src/V3Randomize.cpp | 285 +++++++++++++----- .../t/t_constraint_dist_loop_inter.py | 20 ++ test_regress/t/t_constraint_dist_loop_inter.v | 49 +++ 4 files changed, 273 insertions(+), 82 deletions(-) create mode 100755 test_regress/t/t_constraint_dist_loop_inter.py create mode 100644 test_regress/t/t_constraint_dist_loop_inter.v diff --git a/docs/CONTRIBUTORS b/docs/CONTRIBUTORS index 880b5608a..668b77bff 100644 --- a/docs/CONTRIBUTORS +++ b/docs/CONTRIBUTORS @@ -293,6 +293,7 @@ Vassilis Papaefstathiou Veripool API Bot Victor Besyakov Vikash Patel +Vince Harron Vito Gamberini Wei-Lun Chiu William D. Jones diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 3fcaf5535..7b8a9b259 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -4329,22 +4329,43 @@ class RandomizeVisitor final : public VNVisitor { return new AstConstraintIf{fl, condp, thenBodyp, nullptr}; } - // Replace AstDist with weighted bucket selection via AstConstraintIf chain. + // Replace AstDist with weighted bucket selection via hidden random variables. // Supports both constant and variable weight expressions. - void lowerDistConstraints(AstTask* taskp, AstNode* constrItemsp) { + // Replace AstDist with weighted bucket selection via hidden random variables. + // Supports both constant and variable weight expressions. + // Returns a pointer to the replacement node if the entire subtree was lowered. + AstNode* lowerDistConstraints(AstTask* taskp, AstNode* constrItemsp, + AstNodeForeach* foreachp = nullptr, + AstFunc* randomizep = nullptr, AstVar* genp = nullptr) { + AstNode* headp = constrItemsp; for (AstNode *nextip, *itemp = constrItemsp; itemp; itemp = nextip) { nextip = itemp->nextp(); // Recursively handle ConstraintIf nodes (dist can be inside if/else) if (AstConstraintIf* const cifp = VN_CAST(itemp, ConstraintIf)) { - if (cifp->thensp()) lowerDistConstraints(taskp, cifp->thensp()); - if (cifp->elsesp()) lowerDistConstraints(taskp, cifp->elsesp()); + AstNode* const newThenp + = lowerDistConstraints(taskp, cifp->thensp(), foreachp, randomizep, genp); + if (newThenp != cifp->thensp()) { + if (cifp->thensp()) pushDeletep(cifp->thensp()->unlinkFrBackWithNext()); + if (newThenp) cifp->addThensp(newThenp); + } + AstNode* const newElsep + = lowerDistConstraints(taskp, cifp->elsesp(), foreachp, randomizep, genp); + if (newElsep != cifp->elsesp()) { + if (cifp->elsesp()) pushDeletep(cifp->elsesp()->unlinkFrBackWithNext()); + if (newElsep) cifp->addElsesp(newElsep); + } continue; } // Recursively handle ConstraintForeach nodes (dist can be inside foreach) if (AstConstraintForeach* const cfep = VN_CAST(itemp, ConstraintForeach)) { - if (cfep->bodyp()) lowerDistConstraints(taskp, cfep->bodyp()); + AstNode* const newBodyp + = lowerDistConstraints(taskp, cfep->bodyp(), cfep, randomizep, genp); + if (newBodyp != cfep->bodyp()) { + if (cfep->bodyp()) pushDeletep(cfep->bodyp()->unlinkFrBackWithNext()); + if (newBodyp) cfep->addBodyp(newBodyp); + } continue; } @@ -4362,9 +4383,10 @@ class RandomizeVisitor final : public VNVisitor { } if (VN_IS(chainEndp, Dist)) { AstConstraintIf* const liftedp = liftLogIfChainToConstraintIf(topLogIfp); + if (itemp == headp) headp = liftedp; constrExprp->replaceWith(liftedp); VL_DO_DANGLING(pushDeletep(constrExprp), constrExprp); - lowerDistConstraints(taskp, liftedp->thensp()); + lowerDistConstraints(taskp, liftedp->thensp(), foreachp, randomizep, genp); continue; } } @@ -4419,10 +4441,9 @@ class RandomizeVisitor final : public VNVisitor { if (buckets.empty()) { // All weights are zero: dist is vacuously true (unconstrained) - AstConstraintExpr* const truep - = new AstConstraintExpr{fl, new AstConst{fl, AstConst::BitTrue{}}}; - constrExprp->replaceWith(truep); - VL_DO_DANGLING(pushDeletep(constrExprp), constrExprp); + AstNodeExpr* const truep = new AstConst{fl, AstConst::BitTrue{}}; + truep->dtypeSetBit(); + constrExprp->exprp(truep); continue; } @@ -4438,102 +4459,201 @@ class RandomizeVisitor final : public VNVisitor { } } - // Store totalWeight in temp var (evaluated once, used twice) + // Fix for Issue 1 & 2: Use a hidden random variable to select the bucket. + // This ensures weighted distribution while allowing the SMT solver to + // natively handle global consistency. const int distId = m_distNum++; - const std::string totalName = "__Vdist_total" + cvtToStr(distId); - AstVar* const totalVarp - = new AstVar{fl, VVarType::BLOCKTEMP, totalName, taskp->findUInt64DType()}; - totalVarp->noSubst(true); - totalVarp->lifetime(VLifetime::AUTOMATIC_EXPLICIT); - totalVarp->funcLocal(true); - totalVarp->isInternal(true); - taskp->addStmtsp(totalVarp); - taskp->addStmtsp( - new AstAssign{fl, new AstVarRef{fl, totalVarp, VAccess::WRITE}, totalWeightExprp}); + const std::string weightName = "__Vdistw" + cvtToStr(distId); + AstNodeDType* const weightDtp = m_modp->findUInt64DType(); + AstVar* weightVarp; - // bucketVar = (rand64() % totalWeight) + 1 - const std::string bucketName = "__Vdist_bucket" + cvtToStr(distId); - AstVar* const bucketVarp - = new AstVar{fl, VVarType::BLOCKTEMP, bucketName, taskp->findUInt64DType()}; - bucketVarp->noSubst(true); - bucketVarp->lifetime(VLifetime::AUTOMATIC_EXPLICIT); - bucketVarp->funcLocal(true); - bucketVarp->isInternal(true); - taskp->addStmtsp(bucketVarp); + if (foreachp) { + // Inside a foreach: create a hidden array to hold weights per element + AstNodeDType* const arrayDtp = new AstDynArrayDType{fl, weightDtp}; + arrayDtp->dtypep(arrayDtp); + v3Global.rootp()->typeTablep()->addTypesp(arrayDtp); - AstNodeExpr* randp = new AstRand{fl, nullptr, false}; - randp->dtypeSetUInt64(); - taskp->addStmtsp(new AstAssign{ - fl, new AstVarRef{fl, bucketVarp, VAccess::WRITE}, - new AstAdd{ - fl, new AstConst{fl, AstConst::Unsized64{}, 1}, - new AstModDiv{fl, randp, new AstVarRef{fl, totalVarp, VAccess::READ}}}}); + weightVarp = new AstVar{fl, VVarType::MEMBER, weightName, arrayDtp}; + weightVarp->rand(VRandAttr::RAND); + weightVarp->user2p(m_modp); + m_modp->addStmtsp(weightVarp); - // Build cumulative sum expressions forward: cumSum[i] = w[0]+...+w[i] - std::vector cumSums; + // Ensure the hidden weight array is resized to match the design array + AstTask* const resizeAllTaskp = getCreateAggrResizeTask(VN_AS(m_modp, Class)); + AstNodeExpr* const arraySizeExprp = new AstCMethodHard{ + fl, static_cast(foreachp->headerp()->fromp()->cloneTreePure(false)), + VCMethod::DYN_SIZE}; + arraySizeExprp->dtypeSetUInt32(); + AstCMethodHard* const resizeCallp + = new AstCMethodHard{fl, new AstVarRef{fl, m_modp, weightVarp, VAccess::WRITE}, + VCMethod::DYN_RESIZE, arraySizeExprp}; + resizeCallp->dtypeSetVoid(); + resizeAllTaskp->addStmtsp(resizeCallp->makeStmt()); + + if (randomizep && genp) { + // Manual write_var for hidden choice array (must happen after resize) + AstCMethodHard* const methodp = new AstCMethodHard{ + fl, + new AstVarRef{fl, VN_AS(genp->user2p(), NodeModule), genp, + VAccess::READWRITE}, + VCMethod::RANDOMIZER_WRITE_VAR}; + methodp->dtypeSetVoid(); + methodp->addPinsp(new AstVarRef{fl, m_modp, weightVarp, VAccess::WRITE}); + methodp->addPinsp(new AstConst{fl, AstConst::Unsized64{}, 64}); + methodp->addPinsp(new AstCExpr{fl, AstCExpr::Pure{}, "\"" + weightName + "\""}); + methodp->addPinsp(new AstConst{fl, AstConst::Unsized64{}, 1}); // Dimension + randomizep->addStmtsp(methodp->makeStmt()); + } + } else { + // Scalar dist: create a single hidden member + weightVarp = new AstVar{fl, VVarType::MEMBER, weightName, weightDtp}; + weightVarp->rand(VRandAttr::RAND); + weightVarp->user2p(m_modp); + m_modp->addStmtsp(weightVarp); + + if (genp) { + // Manual write_var for hidden choice variable + AstCMethodHard* const methodp = new AstCMethodHard{ + fl, + new AstVarRef{fl, VN_AS(genp->user2p(), NodeModule), genp, + VAccess::READWRITE}, + VCMethod::RANDOMIZER_WRITE_VAR}; + methodp->dtypeSetVoid(); + methodp->addPinsp(new AstVarRef{fl, m_modp, weightVarp, VAccess::WRITE}); + methodp->addPinsp(new AstConst{fl, AstConst::Unsized64{}, 64}); + methodp->addPinsp(new AstCExpr{fl, AstCExpr::Pure{}, "\"" + weightName + "\""}); + methodp->addPinsp(new AstConst{fl, AstConst::Unsized64{}, 0}); // Dimension + taskp->addStmtsp(methodp->makeStmt()); + } + } + + // Mark variable as already processed by write_var pass and handled by solver + weightVarp->user3(true); + weightVarp->globalConstrained(true); + + // choiceVar = weightVarp or weightVarp[i] + AstNodeExpr* choicep = new AstVarRef{fl, m_modp, weightVarp, VAccess::READ}; + choicep->user1(true); + if (foreachp) { + // Use the same loop variables as the foreach + AstNodeExpr* indexp = nullptr; + for (AstNode* loopVarp = foreachp->headerp()->elementsp(); loopVarp; + loopVarp = loopVarp->nextp()) { + if (VN_IS(loopVarp, Empty)) continue; + AstNodeExpr* const refp + = new AstVarRef{fl, m_modp, VN_AS(loopVarp, Var), VAccess::READ}; + if (!indexp) + indexp = refp; + else + indexp = new AstArraySel{fl, indexp, refp}; + } + choicep = new AstArraySel{fl, choicep, indexp}; + choicep->user1(true); + } + + // Build weighted disjunction: + // (choice < totalWeight) && (or (choice in bucket0_range && item in bucket0) ...) + AstNodeExpr* unionExprp = nullptr; + + // Re-implementing with proper variable weight support AstNodeExpr* runningSump = nullptr; - for (size_t i = 0; i < buckets.size(); ++i) { + for (auto& bucket : buckets) { + AstNodeExpr* lowerp; if (!runningSump) { - runningSump = buckets[i].weightExprp->cloneTreePure(false); + lowerp = new AstConst{fl, AstConst::Unsized64{}, 0}; + runningSump = bucket.weightExprp->cloneTreePure(false); } else { + lowerp = static_cast(runningSump->cloneTreePure(false)); runningSump = new AstAdd{fl, runningSump, - buckets[i].weightExprp->cloneTreePure(false)}; + bucket.weightExprp->cloneTreePure(false)}; runningSump->dtypeSetUInt64(); } - cumSums.push_back(runningSump->cloneTreePure(true)); - } + AstNodeExpr* const upperp + = static_cast(runningSump->cloneTreePure(false)); - // Build ConstraintIf chain backward (last bucket is unconditional default) - AstNode* chainp = nullptr; - for (int i = static_cast(buckets.size()) - 1; i >= 0; --i) { - AstNodeExpr* constraintExprp; - if (const AstInsideRange* const irp = VN_CAST(buckets[i].rangep, InsideRange)) { - AstNodeExpr* const exprCopy1p = distp->exprp()->cloneTreePure(false); - exprCopy1p->user1(true); - AstNodeExpr* const exprCopy2p = distp->exprp()->cloneTreePure(false); - exprCopy2p->user1(true); - AstGte* const gtep - = new AstGte{fl, exprCopy1p, irp->lhsp()->cloneTreePure(false)}; - gtep->user1(true); - AstLte* const ltep - = new AstLte{fl, exprCopy2p, irp->rhsp()->cloneTreePure(false)}; - ltep->user1(true); - constraintExprp = new AstLogAnd{fl, gtep, ltep}; - constraintExprp->user1(true); + // bucketActive = choiceVar >= lowerp && choiceVar < upperp + AstNodeExpr* const choiceClonep + = static_cast(choicep->cloneTreePure(false)); + choiceClonep->user1(true); + AstNodeExpr* const gtep = new AstGte{fl, choiceClonep, lowerp}; + gtep->user1(true); + + AstNodeExpr* const choiceClone2p + = static_cast(choicep->cloneTreePure(false)); + choiceClone2p->user1(true); + AstNodeExpr* const ltp = new AstLt{fl, choiceClone2p, upperp}; + ltp->user1(true); + + AstNodeExpr* const bucketActivep = new AstLogAnd{fl, gtep, ltp}; + bucketActivep->user1(true); + + // rangeExpr = item in Range + AstNodeExpr* rangeExprp; + if (const AstInsideRange* const irp = VN_CAST(bucket.rangep, InsideRange)) { + AstNodeExpr* const itemClonep + = static_cast(distp->exprp()->cloneTreePure(false)); + itemClonep->user1(true); + AstNodeExpr* const itemGtep + = new AstGte{fl, itemClonep, + static_cast(irp->lhsp()->cloneTreePure(false))}; + itemGtep->user1(true); + + AstNodeExpr* const itemClone2p + = static_cast(distp->exprp()->cloneTreePure(false)); + itemClone2p->user1(true); + AstNodeExpr* const itemLtep + = new AstLte{fl, itemClone2p, + static_cast(irp->rhsp()->cloneTreePure(false))}; + itemLtep->user1(true); + rangeExprp = new AstLogAnd{fl, itemGtep, itemLtep}; } else { - AstNodeExpr* const exprCopyp = distp->exprp()->cloneTreePure(false); - exprCopyp->user1(true); - constraintExprp - = new AstEq{fl, exprCopyp, buckets[i].rangep->cloneTreePure(false)}; - constraintExprp->user1(true); + AstNodeExpr* const itemClonep + = static_cast(distp->exprp()->cloneTreePure(false)); + itemClonep->user1(true); + rangeExprp + = new AstEq{fl, itemClonep, + static_cast(bucket.rangep->cloneTreePure(false))}; } + rangeExprp->user1(true); - AstConstraintExpr* const thenp = new AstConstraintExpr{fl, constraintExprp}; + // combined = bucketActive && rangeExpr + AstNodeExpr* const combinedp = new AstLogAnd{fl, bucketActivep, rangeExprp}; + combinedp->user1(true); - if (!chainp) { - chainp = thenp; - } else { - AstNodeExpr* const condp - = new AstLte{fl, new AstVarRef{fl, bucketVarp, VAccess::READ}, cumSums[i]}; - chainp = new AstConstraintIf{fl, condp, thenp, chainp}; + if (!unionExprp) + unionExprp = combinedp; + else { + unionExprp = new AstLogOr{fl, unionExprp, combinedp}; + unionExprp->user1(true); } } - if (chainp) { - constrExprp->replaceWith(chainp); - VL_DO_DANGLING(pushDeletep(constrExprp), constrExprp); - } + // Final constraint: (choiceVar < totalWeight) && unionExprp + AstNodeExpr* const choiceCloneFinalp + = static_cast(choicep->cloneTreePure(false)); + choiceCloneFinalp->user1(true); + AstNodeExpr* const boundp + = new AstLt{fl, choiceCloneFinalp, + static_cast(totalWeightExprp->cloneTreePure(false))}; + boundp->user1(true); - // Clean up nodes used only as clone templates (never inserted into tree) + AstNodeExpr* const finalConstrp = new AstLogAnd{fl, boundp, unionExprp}; + finalConstrp->user1(true); + finalConstrp->dtypeSetBit(); + + // Update original dist expression + constrExprp->exprp(finalConstrp); + + // Clean up nodes used only as clone templates for (auto& bucket : buckets) { VL_DO_DANGLING(pushDeletep(bucket.weightExprp), bucket.weightExprp); } + VL_DO_DANGLING(pushDeletep(totalWeightExprp), totalWeightExprp); VL_DO_DANGLING(pushDeletep(runningSump), runningSump); - // Last cumSum is unused (last bucket is unconditional default) - pushDeletep(cumSums.back()); + VL_DO_DANGLING(pushDeletep(choicep), choicep); } + return headp; } - // VISITORS void visit(AstNodeModule* nodep) override { VL_RESTORER(m_modp); @@ -4597,7 +4717,8 @@ class RandomizeVisitor final : public VNVisitor { } if (constrp->itemsp()) expandUniqueElementList(constrp->itemsp()); - if (constrp->itemsp()) lowerDistConstraints(taskp, constrp->itemsp()); + if (constrp->itemsp()) + lowerDistConstraints(taskp, constrp->itemsp(), nullptr, randomizep, genp); std::set& sizeArrays = m_sizeConstrainedArrays[classp]; ConstraintExprVisitor{classp, m_memberMap, constrp->itemsp(), nullptr, genp, randModeVarp, diff --git a/test_regress/t/t_constraint_dist_loop_inter.py b/test_regress/t/t_constraint_dist_loop_inter.py new file mode 100755 index 000000000..e39f55c4d --- /dev/null +++ b/test_regress/t/t_constraint_dist_loop_inter.py @@ -0,0 +1,20 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# This file ONLY is placed under the Creative Commons Public Domain. +# SPDX-FileCopyrightText: Copyright 2026 Google LLC +# SPDX-License-Identifier: CC0-1.0 + +import vltest_bootstrap + +test.scenarios('simulator') + +if not test.have_solver: + test.skip("No constraint solver installed") + +# Allow the UNSIGNED warning which is expected for 'byte >= 0' +test.compile(verilator_flags2=['-Wno-UNSIGNED', '-LDFLAGS', '-lpthread']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_constraint_dist_loop_inter.v b/test_regress/t/t_constraint_dist_loop_inter.v new file mode 100644 index 000000000..332a34f03 --- /dev/null +++ b/test_regress/t/t_constraint_dist_loop_inter.v @@ -0,0 +1,49 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: Copyright 2026 Google LLC +// SPDX-License-Identifier: CC0-1.0 + +class C; + rand byte data[]; + rand int size_val; + + constraint c_size { + size_val == 20; + data.size() == size_val; + } + + constraint c_data { + foreach (data[i]) { + // Pick values in two disconnected ranges + data[i] dist { [0:10] := 1, [100:110] := 1 }; + // Inter-element constraint: sorted + if (i > 0) data[i] > data[i-1]; + } + } +endclass + +module t; + initial begin + static C c = new; + if (c.randomize() == 0) begin + $display("%%Error: Randomization failed"); + $stop; + end + + // Check results + foreach (c.data[i]) begin + if (!((c.data[i] >= 0 && c.data[i] <= 10) || (c.data[i] >= 100 && c.data[i] <= 110))) begin + $display("%%Error: Element %0d out of range: %0d", i, c.data[i]); + $stop; + end + if (i > 0 && c.data[i] <= c.data[i-1]) begin + $display("%%Error: Elements %0d and %0d not sorted: %0d, %0d", i-1, i, c.data[i-1], c.data[i]); + $stop; + end + end + + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule