diff --git a/docs/internals.rst b/docs/internals.rst index 2244b530e..9267abae5 100644 --- a/docs/internals.rst +++ b/docs/internals.rst @@ -1090,9 +1090,17 @@ solver gets a setup query, then the definition of variables, then all the constraints (SMT assertions) about the variables. Since the solver has no information about the class' PRNG state, if the problem is satisfiable, the solution space is further constrained by adding extra random constraints, -and querying the values satisfying the problem statement. The constraint is -currently constructed as fixing a simple xor of randomly chosen bits of the -variables being randomized. +and querying the values satisfying the problem statement. The constraints +are currently built by the UniGen2 algorithm ("On Parallel Scalable Uniform +SAT Witness Generation", Chakraborty et al.). It first works out how many +random xor equations are needed to split the solution space into cells of a +size worth enumerating, then draws one cell and enumerates it, which gives +a near-uniform sample of the whole space. Both the estimate and the +leftover solutions are cached, so the following calls are answered without +asking the solver again. Cases outside its assumptions, such as ``randc`` +variables or soft constraints, fall back to pinning every free bit to a +random value, or, when arrays are involved, to asserting four random xor +equations in a row. The runtime classes used for handling the randomization are defined in ``verilated_random.h`` and ``verilated_random.cpp``. diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index 354eabd92..38588b244 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -578,6 +578,8 @@ void VlRandomVar::emitExtract(std::ostream& s, int i) const { s << " ((_ extract " << i << ' ' << i << ") " << m_name << ')'; } void VlRandomVar::emitType(std::ostream& s) const { s << "(_ BitVec " << width() << ')'; } +// A scalar var IS its only element, so "element j" is just the whole var. +void VlRandomVar::emitElement(std::ostream& s, int /*j*/) const { s << ' ' << m_name; } // Serialize the current runtime value as an SMT-LIB binary literal. Used by // randomize(null) to pin a var via `(assert (= var #b...))`. Binary (#b) // rather than hex (#x) sidesteps SMT-LIB's hex-width-multiple-of-4 rule. @@ -707,6 +709,15 @@ size_t VlRandomizer::hashConstraints(const std::vector& extras) con for (const auto& c : extras) { h ^= std::hash{}(c) + 0x9e3779b9 + (h << 6) + (h >> 2); } + for (const auto& var : m_vars) { + h ^= std::hash{}(var.first) + 0x9e3779b9 + (h << 6) + (h >> 2); + h ^= std::hash{}(var.second->width()) + 0x9e3779b9 + (h << 6) + (h >> 2); + h ^= std::hash{}(var.second->dimension()) + 0x9e3779b9 + (h << 6) + (h >> 2); + } + // Keys are one per array element, so a resized queue gets a different hash. + for (const auto& elem : m_arr_vars) { + h ^= std::hash{}(elem.first) + 0x9e3779b9 + (h << 6) + (h >> 2); + } return h; } @@ -739,11 +750,35 @@ void VlRandomizer::recordRandcValues() { } } -bool VlRandomizer::next_check_only(VlRNG& rngr) { return nextRandomize(rngr, true); } +bool VlRandomizer::isFrozenVar(const std::string& name, const VlRandomVar& var) const { + if (!var.randModeIdxNone()) { + const VlQueue* const modep + = m_staticVars.count(name) ? m_static_randmodep : m_randmodep; + // modep is never null in practice, the fallthrough matches the return below + if (VL_UNCOVERABLE(!modep)) return m_disabledVars.count(name) != 0; + if (!modep->at(var.randModeIdx())) return true; + } + // Struct/nested members are disabled via m_disabledVars. + // They have no randModeIdx of their own. + return m_disabledVars.count(name) != 0; +} -bool VlRandomizer::next(VlRNG& rngr) { return nextRandomize(rngr, false); } +bool VlRandomizer::hasFrozenVar() const { + bool mayBeFrozen = m_randmodep || m_static_randmodep; + // A disabled var means the class uses rand_mode, so it never shows up without one + if (VL_UNCOVERABLE(!mayBeFrozen && !m_disabledVars.empty())) mayBeFrozen = true; + if (!mayBeFrozen) return false; + for (const auto& var : m_vars) { + if (isFrozenVar(var.first, *var.second)) return true; + } + return false; +} -bool VlRandomizer::nextRandomize(VlRNG& rngr, bool checkOnly) { +bool VlRandomizer::next_check_only(VlRNGReseeds& rngr) { return nextRandomize(rngr, true); } + +bool VlRandomizer::next(VlRNGReseeds& rngr) { return nextRandomize(rngr, false); } + +bool VlRandomizer::nextRandomize(VlRNGReseeds& rngr, bool checkOnly) { if (!checkOnly && m_vars.empty() && m_unique_arrays.empty()) return true; if (checkOnly && m_vars.empty()) return true; // No rand members: trivially SAT VlSolverSession& sess = s_solverSession; @@ -762,6 +797,9 @@ bool VlRandomizer::nextRandomize(VlRNG& rngr, bool checkOnly) { } } + // Reseeded from outside, so everything cached came from the old seed. + if (m_ug2.rngReseeds != rngr.reseeds()) m_ug2 = Unigen2State{}; + // Pinned vars make phase ordering moot; skip phased path in check-only. bool result; if (!m_checkOnly && !m_solveBefore.empty()) { @@ -769,6 +807,7 @@ bool VlRandomizer::nextRandomize(VlRNG& rngr, bool checkOnly) { } else { result = nextFlat(rngr, sess, uniqueExprs); } + m_ug2.rngReseeds = rngr.reseeds(); m_checkOnly = false; return result; } @@ -841,6 +880,10 @@ void VlRandomizer::emitAsserts(std::ostream& os, const std::vector& bool VlRandomizer::nextFlat(VlRNG& rngr, VlSolverSession& sess, const std::vector& uniqueExprs) VL_REQUIRES(sess.m_mutex) { + if (m_randcVarNames.empty() && !m_checkOnly && !hasFrozenVar() + && unigen2(rngr, sess, uniqueExprs)) { + return true; + } VlSolverTxn txn{sess}; if (!txn.ok()) return false; std::iostream& os = sess.os(); @@ -891,6 +934,299 @@ bool VlRandomizer::nextFlat(VlRNG& rngr, VlSolverSession& sess, return false; // Should not reach here } +// Enumerate one cell of the solution space, and cache the solutions in m_ug2.loThreshWitnesses. +// The next call with the same constraint set will drain the cache before running the full +// mechanism again. +bool VlRandomizer::unigen2(VlRNG& rngr, VlSolverSession& sess, + const std::vector& uniqueExprs) VL_REQUIRES(sess.m_mutex) { + if (!m_softConstraints.empty()) return false; + + const size_t currentHash = hashConstraints(uniqueExprs); + // Params and batch are computed for specific constraint set, so drop them + // once it changes. + if (m_ug2.paramHash != currentHash) { + m_ug2.loThreshWitnesses.clear(); + m_ug2.paramsValid = false; + m_ug2.isLargeSpace = false; + m_ug2.paramHash = currentHash; + // First sighting of this constraint set. + // Decline now and let the next call with the same set run UG2. + return false; + } + + // Nothing cached from a previous UG2 run, so refill the batch first. + if (m_ug2.loThreshWitnesses.empty()) { + VlSolverTxn txn{sess}; + if (!txn.ok()) return false; + std::iostream& solver = sess.os(); + + solver << "(set-option :produce-models true)\n"; + solver << "(set-logic QF_ABV)\n"; + emitDefines(solver); + emitDeclares(solver, false); + emitAsserts(solver, uniqueExprs, false); + + if (!m_ug2.paramsValid) { + // Searches once per constraint set for how finely to cut the space, and + // caches parameters + if (!estimateParameters(sess, rngr)) return false; + m_ug2.paramsValid = true; + m_ug2.lastSuccessI = -1; // new params, so the old hint no longer applies + } + + // generateSamples() always finds a candidate in practice + if (VL_UNCOVERABLE(!generateSamples(sess, rngr))) return false; + } + + // Cached or just refilled - there is a witness to write into the variables + Witness witness = std::move(m_ug2.loThreshWitnesses.back()); + m_ug2.loThreshWitnesses.pop_back(); + writeBackWitness(witness); + return true; +} + +void VlRandomizer::writeBackWitness(const Witness& witness) { + for (const auto& varEntry : witness) { + const auto& varp = m_vars.at(varEntry.first); + for (const auto& elemEntry : varEntry.second) { + if (varp->dimension() > 0) { + // set() needs current array info, and a witness from the + // cached batch skips the solver, so nothing else sets it. + auto arrVarsp = std::make_shared(m_arr_vars); + varp->setArrayInfo(arrVarsp); + std::ostringstream idxStream; + idxStream << "#x" << std::hex << std::setw(8) << std::setfill('0') + << elemEntry.first; + varp->set(idxStream.str(), elemEntry.second); + } else { + varp->set("", elemEntry.second); + } + } + } +} + +// Ask for a solution, block it, ask again - so every answer is a new one. +int VlRandomizer::bsat(VlSolverSession& sess, size_t bound, std::vector& witnesses, + VlRNG* diversifyRngp) VL_REQUIRES(sess.m_mutex) { + std::iostream& solver = sess.os(); + witnesses.clear(); + witnesses.reserve(bound); + // get-value responses preserve request order, so build the (var, + // element) order once and read results back positionally. + std::vector>& order = m_ug2.bsatOrder; + order.clear(); + for (const auto& var : m_vars) { + const int elementCount = var.second->totalWidth() / var.second->width(); + for (int j = 0; j < elementCount; ++j) order.emplace_back(var.first, j); + } + + int assumeNum = 0; + while (witnesses.size() < bound) { + VlSolverStatus status = VlSolverStatus::FAIL; + if (diversifyRngp && !witnesses.empty()) { + // To increase the randomization, add an assumption for one var in one specific call + const Witness& prev = witnesses.back(); + const std::pair& pick + = order[VL_RANDOM_RNG_I(*diversifyRngp) % order.size()]; + solver << "(declare-fun d" << assumeNum << " () Bool)\n"; + solver << "(assert (= d" << assumeNum << " (not (="; + m_vars.at(pick.first)->emitElement(solver, pick.second); + solver << ' ' << prev.at(pick.first).at(pick.second) << "))))\n"; + solver << "(check-sat-assuming (d" << assumeNum << "))\n"; + ++assumeNum; + status = sess.readStatus(); + } + if (status != VlSolverStatus::SAT) { + solver << "(check-sat)\n"; + status = sess.readStatus(); + } + if (status != VlSolverStatus::SAT) { + // "unsat" is the cell running out; anything else is the solver giving up + if (VL_UNLIKELY(status != VlSolverStatus::UNSAT)) return -1; + break; + } + + solver << "(get-value ("; + for (const auto& entry : order) m_vars.at(entry.first)->emitElement(solver, entry.second); + solver << "))\n"; + + // Read the whole balanced reply first, so a malformed one cannot desync the pipe + std::string reply; + if (VL_UNLIKELY(!sess.readSExpr(reply))) return -1; + std::istringstream is{reply}; + char c = 0; + is >> c; // readSExpr only returns a reply that opens with '(' + Witness witness; + for (const auto& entry : order) { + if (VL_UNLIKELY(!(is >> c) || c != '(')) return -1; // LCOV_EXCL_BR_LINE + std::string exprHead; + is >> exprHead; // bare var name, or literally "(select" if an array element + const bool isSelect = exprHead == "(select"; + if (isSelect) readUntilBalanced(is); + if (VL_UNLIKELY(!isSelect && exprHead != entry.first)) return -1; + std::string value; + std::getline(is, value, ')'); + // The batch outlives this call, so reject a bad value before it is cached + if (VL_UNLIKELY(!validSMTNum(value))) return -1; + witness[entry.first][entry.second] = value; + } // LCOV_EXCL_BR_LINE + if (VL_UNLIKELY(!(is >> c) || c != ')')) return -1; // LCOV_EXCL_BR_LINE + + // Forbid this exact assignment so the next + // (check-sat) is forced to find a genuinely different witness. + solver << "(assert (not (and"; + for (const auto& varEntry : witness) { + for (const auto& elemEntry : varEntry.second) { + solver << " (="; + m_vars.at(varEntry.first)->emitElement(solver, elemEntry.first); + solver << ' ' << elemEntry.second << ")"; + } + } + solver << ")))\n"; + witnesses.push_back(std::move(witness)); + } // LCOV_EXCL_BR_LINE + return static_cast(witnesses.size()); +} + +// Each equation selects a random subset of bits by a coin-flip for each bit, and then sets the XOR +// of those bits to a random value. +void VlRandomizer::unigenXors(std::iostream& solver, VlRNG& rngr, int bits) { + if (bits <= 0) return; // 0 hash constraints == no extra assertion needed at all + std::vector target(bits); + for (int k = 0; k < bits; ++k) target[k] = VL_RANDOM_RNG_I(rngr) & 1; + + solver << "(assert "; + solver << "(= #b"; + for (int k = 0; k < bits; ++k) solver << (target[k] ? '1' : '0'); + if (bits > 1) solver << " (concat"; + for (int k = 0; k < bits; ++k) { + // #b0 seeds the bvxor chain so it's always >=2 operands (valid even + // if this equation's coin flips happen to select zero/one bits). + // 0 xor 0 == 0, 0 xor 1 == 1, so the seed cannot change the result. + solver << " (bvxor #b0"; + for (const auto& var : m_vars) { + for (int j = 0; j < var.second->totalWidth(); ++j) { + if (VL_RANDOM_RNG_I(rngr) & 1) var.second->emitExtract(solver, j); + } + } + solver << ')'; + } + if (bits > 1) solver << ')'; + solver << "))\n"; +} + +// --- UniGen2 constants --- +static constexpr double ug2Kappa = 0.638; // Parameter controlling the tolerance of the uniformity + // guarantee. Set at the paper's default value. +// Values used in the large space mode: +static constexpr int ug2HiThreshLargeSpace = 16; // Num of solutions to enumerate +static constexpr int ug2BatchLargeSpace = 16; // Num of solutions to cache +static constexpr int ug2HashBitsLargeSpace + = 10; // Num of XORs to add to the solver, also cap of the bsat() search + +bool VlRandomizer::estimateParameters(VlSolverSession& sess, VlRNG& rngr) + VL_REQUIRES(sess.m_mutex) { + std::iostream& solver = sess.os(); + // Below formulas are taken from the UniGen2 paper, Sec. 4, Algorithm 1 + const double pivot = ceil(4.03 * pow((1 + 1 / ug2Kappa), 2)); + m_ug2.hiThresh = static_cast(ceil(1 + sqrt(2) * (1 + ug2Kappa) * pivot)); + m_ug2.loThresh = static_cast(floor(pivot / (sqrt(2) * (1 + ug2Kappa)))); + + // A space so small can never reach loThresh, so enumerate it whole instead. + // push/pop keeps bsat() blocking clauses out of that search. + solver << "(push 1)\n"; + std::vector tinyWitnesses; + const int tinyCellSize = bsat(sess, 61, tinyWitnesses); + solver << "(pop 1)\n"; + if (tinyCellSize < 0) return false; + if (tinyCellSize >= 1 && tinyCellSize <= 60) { + m_ug2.hashBits = 0; + m_ug2.loThresh = tinyCellSize; // batch = the whole enumerated set + m_ug2.hiThresh = tinyCellSize + 1; + return true; + } + + int totalBits = 0; + for (const auto& var : m_vars) totalBits += var.second->totalWidth(); + int solCount = 0; + // Cap the search with ug2HashBitsLargeSpace: Larger spaces cannot be hashed in useful + // time, so stop and just use fixed number of XORs. Limit set empirically from measured solve + // times. + const int iMax = totalBits < ug2HashBitsLargeSpace ? totalBits : ug2HashBitsLargeSpace; + std::vector witnesses; // Reused across trials; bsat() clears it + for (int i = 1; i <= iMax; ++i) { + solver << "(push 1)\n"; + unigenXors(solver, rngr, i); + const int bound = 61; + solCount = bsat(sess, bound, witnesses); + if (solCount < 0) { + solver << "(pop 1)\n"; + return false; + } + if (solCount >= 1 && solCount < bound) { + m_ug2.hashBits + = static_cast(round(log2(solCount) + i + log2(1.8) + - log2(pivot))); // formula taken from the Unigen2 paper + solver << "(pop 1)\n"; + return true; + } + solver << "(pop 1)\n"; + } + m_ug2.isLargeSpace = true; + m_ug2.hashBits = ug2HashBitsLargeSpace; + m_ug2.hiThresh = ug2HiThreshLargeSpace; + return true; +} + +bool VlRandomizer::generateSamples(VlSolverSession& sess, VlRNG& rngr) VL_REQUIRES(sess.m_mutex) { + std::iostream& solver = sess.os(); + // Try whichever of hashBits number worked last call first + // (UniGen2 Sec. 4, "leapfrogging" in spirit but without weakening guarantees). + // On a large space no cell was ever enumerable, so just try most hash bits first for the + // smallest cell. + const int lowestCount = m_ug2.hashBits - 2; + int candidates[3] = {lowestCount, lowestCount + 1, lowestCount + 2}; + if (m_ug2.isLargeSpace) { + candidates[0] = m_ug2.hashBits; + candidates[1] = m_ug2.hashBits - 1; + candidates[2] = m_ug2.hashBits - 2; + } else if (m_ug2.lastSuccessI >= 0) { + std::swap(candidates[0], candidates[m_ug2.lastSuccessI - lowestCount]); + } + + std::vector witnesses; // Reused across candidates; bsat() clears it + for (int t = 0; t < 3; ++t) { // LCOV_EXCL_BR_LINE - Always finds a candidate in practice + const int i = candidates[t]; + if (i < 0) continue; // hashBits below 2 leaves fewer than three counts to try + + solver << "(push 1)\n"; + unigenXors(solver, rngr, i); + const int solCount + = bsat(sess, m_ug2.hiThresh, witnesses, m_ug2.isLargeSpace ? &rngr : nullptr); + if (m_ug2.loThresh <= solCount && (solCount < m_ug2.hiThresh || m_ug2.isLargeSpace)) { + m_ug2.lastSuccessI = i; + const int take + = m_ug2.isLargeSpace ? std::min(ug2BatchLargeSpace, solCount) : m_ug2.loThresh; + // Pick them at random rather than the first ones enumerated - + // partial Fisher-Yates, so the picks stay distinct. + m_ug2.loThreshWitnesses.clear(); + std::vector indices(witnesses.size()); + for (size_t k = 0; k < indices.size(); ++k) indices[k] = static_cast(k); + for (int k = 0; k < take; ++k) { + const size_t pick + = static_cast(k) + (VL_RANDOM_RNG_I(rngr) % (indices.size() - k)); + std::swap(indices[k], indices[pick]); + m_ug2.loThreshWitnesses.push_back(std::move(witnesses[indices[k]])); + } + solver << "(pop 1)\n"; + return true; + } + solver << "(pop 1)\n"; + } + m_ug2.lastSuccessI = -1; // LCOV_EXCL_LINE + return false; // LCOV_EXCL_LINE +} + void VlRandomizer::solveDiversity(VlRNG& rngr, VlSolverSession& sess) VL_REQUIRES(sess.m_mutex) { bool hasArray = false; for (const auto& var : m_vars) { @@ -1319,8 +1655,8 @@ bool VlRandomizer::nextPhased(VlRNG& rngr, VlSolverSession& sess, std::vector> layers; if (!buildSolveLayers(layers)) return false; - // One layer: all solve_before vars are independent, no ordering required - if (layers.size() <= 1) return nextFlat(rngr, sess, uniqueExprs); + // No layers means no solve_before pair survived + if (layers.empty()) return nextFlat(rngr, sess, uniqueExprs); VlSolverTxn txn{sess}; if (!txn.ok()) return false; diff --git a/include/verilated_random.h b/include/verilated_random.h index bd68f9dec..682ff2823 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -83,6 +83,10 @@ public: virtual void emitGetValue(std::ostream& s) const; virtual void emitExtract(std::ostream& s, int i) const; virtual void emitType(std::ostream& s) const; + // Emit the expression referring to element j as a whole (the full var + // for scalars, "(select arr idx...)" for array element j). Used by BSAT + // to query/re-assert one whole element's value, not a single bit. + virtual void emitElement(std::ostream& s, int j) const; // Emit the current runtime value as an SMT bit-vector literal (#b...). // Used by randomize(null) to pin a var to its existing value. virtual void emitConcreteValue(std::ostream& s) const; @@ -213,6 +217,20 @@ public: const int elementCounts = countMatchingElements(*m_arrVarsRefp, name()); return width() * elementCounts; } + void emitElement(std::ostream& s, int j) const override { + const std::string indexed_name = name() + std::to_string(j); + const auto it = m_arrVarsRefp->find(indexed_name); + // Callers take j from totalWidth(), which counts these same keys, so the element + // should always be there + if (VL_UNCOVERABLE(it == m_arrVarsRefp->end())) { + // LCOV_EXCL_START + VL_FATAL_MT(__FILE__, __LINE__, "randomize", "indexed_name not found in m_arr_vars"); + return; + // LCOV_EXCL_STOP + } + s << ' '; + emitSelect(s, it->second->m_indices, it->second->m_idxWidths); + } // LCOV_EXCL_BR_LINE void emitExtract(std::ostream& s, int i) const override { const int j = i / width(); i = i % width(); @@ -256,6 +274,9 @@ class VlRandomizer VL_NOT_FINAL { std::vector> m_solveBefore; // Solve-before ordering pairs (beforeVar, afterVar) bool m_checkOnly = false; // Set for randomize(null) + bool isFrozenVar(const std::string& name, + const VlRandomVar& var) const; // true if this var is currently frozen + bool hasFrozenVar() const; // true if any var is currently rand_mode(0)-frozen // PRIVATE METHODS void randomConstraint(std::ostream& os, VlRNG& rngr, int bits); @@ -271,13 +292,54 @@ class VlRandomizer VL_NOT_FINAL { void emitRandcExclusions(std::ostream& os) const; // Emit randc exclusion constraints void recordRandcValues(); // Record solved randc values for future exclusion size_t hashConstraints(const std::vector& extras) const; - bool nextRandomize(VlRNG& rngr, bool checkOnly); + bool nextRandomize(VlRNGReseeds& rngr, bool checkOnly); // "(distinct ...)" expression per unique-constrained array std::vector buildUniqueExprs() const; void emitDefines(std::ostream& os) const; void emitDeclares(std::ostream& os, bool pinCurrent) const; void emitAsserts(std::ostream& os, const std::vector& extras, bool named) const; bool nextFlat(VlRNG& rngr, VlSolverSession& sess, const std::vector& uniqueExprs); + + // --- UniGen2 (a near-uniform constrained randomization sampler) fields --- + // Implementation based on the following paper: + // "On Parallel Scalable Uniform SAT Witness Generation", Chakraborty et al. + + using Witness = std::map>; // One sampled solution + + // Sample one random solution. False if a sample couldn't be produced + bool unigen2(VlRNG& rngr, VlSolverSession& sess, const std::vector& uniqueExprs); + // Find out how finely to cut the solution space, and what cell size to accept + bool estimateParameters(VlSolverSession& sess, VlRNG& rngr); + // Collect up to `bound` different solutions of whatever is asserted right now. + // diversifyRngp adds a randomization step that spreads the solutions apart + int bsat(VlSolverSession& sess, size_t bound, std::vector& witnesses, + VlRNG* diversifyRngp = nullptr); + // Add `bits` random XOR equations, which cut the solution space into cells holding + // roughly 1/2**bits of all the solutions + void unigenXors(std::iostream& os, VlRNG& rngr, int bits); + // Draw a cell and refill the batch of solutions from it + bool generateSamples(VlSolverSession& sess, VlRNG& rngr); + // Copy one solution into the SV variables + void writeBackWitness(const Witness& witness); + + // UniGen2: sampling state + struct Unigen2State final { + std::vector loThreshWitnesses; // Consumable batch of solutions: loThresh random + // picks out of the cell BSAT enumerated + std::vector> bsatOrder; // (var, element) query order + bool isLargeSpace = false; // Large solution space (more than 61 * 2^10 solutions) + // Below properties are what estimateParameters worked out, kept until the constraints + // change so the expensive search is not repeated on every call. + bool paramsValid = false; // Whether the values below are set + size_t paramHash = 0; // Constraint set they were computed for + int hashBits = 0; // How many XOR equations to cut the space with + int loThresh = 0; // Smallest usable cell, and how many samples to take + int hiThresh = 0; // First cell size counted as too big + uint64_t rngReseeds = 0; // rngr.reseeds() as of the last call + int lastSuccessI = -1; // Hash-bit count that worked last time, -1 if none + }; + Unigen2State m_ug2; + void solveDiversity(VlRNG& rngr, VlSolverSession& sess); void solveDiversityPins(VlRNG& rngr, VlSolverSession& sess); void solveDiversityXor(VlRNG& rngr, VlSolverSession& sess); @@ -302,10 +364,10 @@ public: // METHODS // Finds the next solution satisfying the constraints - bool next(VlRNG& rngr); + bool next(VlRNGReseeds& rngr); // Validate the constraints against the current runtime values of every // registered rand variable without picking new ones. - bool next_check_only(VlRNG& rngr); + bool next_check_only(VlRNGReseeds& rngr); // --- Process the key for associative array --- @@ -721,7 +783,7 @@ public: // Light wrapper for RNG used by std::randomize() to support scope-level randomization. class VlStdRandomizer final : public VlRandomizer { // MEMBERS - VlRNG m_rng; // Random number generator + VlRNGReseeds m_rng; // Random number generator public: // CONSTRUCTORS diff --git a/include/verilated_types.h b/include/verilated_types.h index e96de5a29..67bc5e88e 100644 --- a/include/verilated_types.h +++ b/include/verilated_types.h @@ -276,7 +276,7 @@ constexpr IData VL_CLOG2_CE_Q(QData lhs) VL_PURE { // Random // Random Number Generator with internal state -class VlRNG final { +class VlRNG VL_NOT_FINAL { std::array m_state; public: @@ -295,6 +295,22 @@ public: static VlRNG& vl_thread_rng() VL_MT_SAFE; }; +// VlRNG that also counts how often it was reseeded, for randomize() to notice. +class VlRNGReseeds final : public VlRNG { + uint64_t m_reseeds = 0; // Times the state was set from outside + +public: + void srandom(uint64_t n) VL_MT_UNSAFE { + VlRNG::srandom(n); + ++m_reseeds; + } + void set_randstate(const std::string& state) VL_MT_UNSAFE { + VlRNG::set_randstate(state); + ++m_reseeds; + } + uint64_t reseeds() const VL_MT_UNSAFE { return m_reseeds; } +}; + //=================================================================== // Metadata of processes using VlProcessRef = std::shared_ptr; diff --git a/src/V3EmitCHeaders.cpp b/src/V3EmitCHeaders.cpp index 888f0e6bf..08e20eae0 100644 --- a/src/V3EmitCHeaders.cpp +++ b/src/V3EmitCHeaders.cpp @@ -144,7 +144,7 @@ class EmitCHeader final : public EmitCConstInit { if (const AstClass* const classp = VN_CAST(modp, Class)) { if (classp->needRNG()) { putsDecoration(nullptr, "\n// INTERNAL VARIABLES\n"); - puts("VlRNG __Vm_rng;\n"); + puts("VlRNGReseeds __Vm_rng;\n"); } } else { // not class putsDecoration(nullptr, "\n// INTERNAL VARIABLES\n"); diff --git a/test_regress/t/randomize_uniform_common.py b/test_regress/t/randomize_uniform_common.py new file mode 100644 index 000000000..e3d1efd28 --- /dev/null +++ b/test_regress/t/randomize_uniform_common.py @@ -0,0 +1,57 @@ +# 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 math +import re + +# Jensen-Shannon divergence (JSD) measures how far the "shape" of the +# observed distribution is from perfectly uniform. +# 0 means identical to uniform; it grows as the observed +# distribution gets more skewed. Scaled here x100, to notice differences easier +JSD_MAX = 2.5 + + +def jensen_shannon_divergence_pct(observed_counts, solutions): + n_obs = sum(observed_counts.values()) + p = [1.0 / len(solutions) for _ in solutions] # uniform + q = [observed_counts.get(s, 0) / n_obs for s in solutions] # observed + m = [(pi + qi) / 2 for pi, qi in zip(p, q)] + + def kl(a, b): + return sum(ai * math.log(ai / bi) for ai, bi in zip(a, b) if ai > 0) + + return (kl(p, m) + kl(q, m)) / 2 * 100 + + +def run(test, solutions, line_pattern, key=lambda line: line): + """Check that randomize() samples `solutions` close enough to uniformly. + + line_pattern picks out the run-log lines carrying a sample, and key turns + such a line into the value used to look it up in `solutions`. + """ + if not test.have_solver: + test.skip("No constraint solver installed") + + test.compile() + + test.execute() + + observed = {} + with open(test.run_log_filename, 'r', encoding='latin-1') as fh: + for line in fh: + line = line.strip() + if re.fullmatch(line_pattern, line): + value = key(line) + observed[value] = observed.get(value, 0) + 1 + + jsd = jensen_shannon_divergence_pct(observed, solutions) + if jsd > JSD_MAX: + test.error("JSD %.6f exceeds max %.6f -- distribution is not uniform enough" % + (jsd, JSD_MAX)) + + test.passes() diff --git a/test_regress/t/t_randomize_reseed_batch.py b/test_regress/t/t_randomize_reseed_batch.py new file mode 100755 index 000000000..db1adb3f9 --- /dev/null +++ b/test_regress/t/t_randomize_reseed_batch.py @@ -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() diff --git a/test_regress/t/t_randomize_reseed_batch.v b/test_regress/t/t_randomize_reseed_batch.v new file mode 100644 index 000000000..1f5e19603 --- /dev/null +++ b/test_regress/t/t_randomize_reseed_batch.v @@ -0,0 +1,61 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +// Reseeding with srandom() or set_randstate() must make randomize() reproducible +// regardless of what ran before, so a sampler caching solutions across calls has +// to drop them on either. + +// verilog_format: off +`define stop $stop +`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 + +module t; + class C; + rand bit [7:0] a; + constraint c { a < 20; } + endclass + + initial begin + automatic C used = new; + automatic C fresh = new; + automatic int ok; + // Only difference between the two: `used` has randomized before the reseed + repeat (3) begin + ok = used.randomize(); + `checkd(ok, 1); + end + used.srandom(42); + fresh.srandom(42); + ok = used.randomize(); + `checkd(ok, 1); + ok = fresh.randomize(); + `checkd(ok, 1); + `checkd(used.a, fresh.a); + + // Same again through get_randstate/set_randstate, which can restore the very + // state the object already holds + begin + automatic C warm = new; + automatic C cold = new; + automatic string state; + repeat (2) begin + ok = warm.randomize(); + `checkd(ok, 1); + end + state = warm.get_randstate(); + warm.set_randstate(state); + cold.set_randstate(state); + ok = warm.randomize(); + `checkd(ok, 1); + ok = cold.randomize(); + `checkd(ok, 1); + `checkd(warm.a, cold.a); + end + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule diff --git a/test_regress/t/t_randomize_shift_distribution.py b/test_regress/t/t_randomize_shift_distribution.py index 56d461811..9f6720e09 100755 --- a/test_regress/t/t_randomize_shift_distribution.py +++ b/test_regress/t/t_randomize_shift_distribution.py @@ -8,14 +8,10 @@ # SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 import vltest_bootstrap +import randomize_uniform_common test.scenarios('simulator') -if not test.have_solver: - test.skip("No constraint solver installed") +SOLUTIONS = list(range(1 << 6)) # value < (1 << m_size), m_size set to 6 at run time -test.compile() - -test.execute(all_run_flags=["+verilator+seed+1"]) - -test.passes() +randomize_uniform_common.run(test, SOLUTIONS, r'\d+', key=int) diff --git a/test_regress/t/t_randomize_shift_distribution.v b/test_regress/t/t_randomize_shift_distribution.v index a12b6ceed..171f7dce9 100644 --- a/test_regress/t/t_randomize_shift_distribution.v +++ b/test_regress/t/t_randomize_shift_distribution.v @@ -2,12 +2,17 @@ // // This file ONLY is placed under the Creative Commons Public Domain. // SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-FileCopyrightText: 2026 Antmicro // SPDX-License-Identifier: CC0-1.0 +// Checks that randomize() over a uvm_reg_field-shaped range whose bound shifts +// by a member set at run time reaches the whole solution space. Samples are +// printed so the driver can check uniformity (Jensen-Shannon divergence). +// Widths too large to enumerate are only checked against the range itself. + // verilog_format: off `define stop $stop `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); -`define check_le(gotv,maxv) do if ((gotv) > (maxv)) begin $write("%%Error: %s:%0d: got=%0d exp<=%0d\n", `__FILE__,`__LINE__, (gotv), (maxv)); `stop; end while(0); // verilog_format: on typedef logic unsigned [63:0] uvm_reg_data_t; @@ -15,7 +20,6 @@ typedef logic unsigned [63:0] uvm_reg_data_t; class uvm_reg_field; rand uvm_reg_data_t value; int unsigned m_size; - int unsigned m_ones[64]; constraint c_field_valid { if (64 > m_size) { value < (64'h1 << m_size); @@ -25,71 +29,48 @@ class uvm_reg_field; value = 0; m_size = size; endfunction - function void tally; - for (int b = 0; b < 64; b++) if (value[b]) m_ones[b]++; - endfunction -endclass - -class regA; - rand uvm_reg_field fa1, fa15, fa31, fa32; - function new; - fa1 = new; - fa15 = new; - fa31 = new; - fa32 = new; - fa1.configure(1); - fa15.configure(15); - fa31.configure(31); - fa32.configure(32); - endfunction endclass module t; - regA r; - int unsigned i; - // 200 trials over uvm_reg_field-shaped `value < (1<> wide[i].m_size, 0); + end end - for (int b = 0; b < 31; b++) - if (r.fa31.m_ones[b] < LO) begin - $write("%%Error: fa31[%0d] ones=%0d < %0d\n", b, r.fa31.m_ones[b], LO); - `stop; - end - for (int b = 0; b < 32; b++) - if (r.fa32.m_ones[b] < LO) begin - $write("%%Error: fa32[%0d] ones=%0d < %0d\n", b, r.fa32.m_ones[b], LO); - `stop; - end - // High bits beyond m_size must remain 0. - for (int b = 1; b < 64; b++) `checkd(r.fa1.m_ones[b], 0); - for (int b = 15; b < 64; b++) `checkd(r.fa15.m_ones[b], 0); - for (int b = 31; b < 64; b++) `checkd(r.fa31.m_ones[b], 0); - for (int b = 32; b < 64; b++) `checkd(r.fa32.m_ones[b], 0); + $write("*-* All Finished *-*\n"); $finish; end diff --git a/test_regress/t/t_randomize_solver_pipe.py b/test_regress/t/t_randomize_solver_pipe.py index a884a1c77..0a7b3cb53 100755 --- a/test_regress/t/t_randomize_solver_pipe.py +++ b/test_regress/t/t_randomize_solver_pipe.py @@ -67,4 +67,27 @@ test.file_grep(logfile, r'NPASS=(\d+)', 11) test.file_grep_not(logfile, r'Solver failed repeatedly') test.file_grep_not(logfile, r'Solver died') +# A reply the unigen2 sampler can't read while it measures the solution space. +# Falls back to the plain solve, so every randomize still succeeds +logfile = test.obj_dir + '/sim_ug2_estimate.log' +test.execute(logfile=logfile, + run_env='VERILATOR_SOLVER="' + test.t_dir + '/randomize_solver_tamper.py" ' + + 'TAMPER=model_trunc TAMPER_AT=8 ') +test.file_grep(logfile, r'NPASS=(\d+)', 12) + +# A value the sampler can't parse, and a status it can't use, seen while it +# enumerates a cell. +logfile = test.obj_dir + '/sim_ug2_value.log' +test.execute(logfile=logfile, + run_env='VERILATOR_SOLVER="' + test.t_dir + '/randomize_solver_tamper.py" ' + + 'TAMPER=bad_base TAMPER_AT=5 ') +test.file_grep(logfile, r'NPASS=(\d+)', 9) + +# A reply naming a variable the sampler didn't ask for. +logfile = test.obj_dir + '/sim_ug2_var.log' +test.execute(logfile=logfile, + run_env='VERILATOR_SOLVER="' + test.t_dir + '/randomize_solver_tamper.py" ' + + 'TAMPER=unknown_var TAMPER_AT=10 ') +test.file_grep(logfile, r'NPASS=(\d+)', 12) + test.passes() diff --git a/test_regress/t/t_randomize_uniform_array_mixed.py b/test_regress/t/t_randomize_uniform_array_mixed.py new file mode 100755 index 000000000..655c0ca5a --- /dev/null +++ b/test_regress/t/t_randomize_uniform_array_mixed.py @@ -0,0 +1,20 @@ +#!/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 +import randomize_uniform_common + +test.scenarios('simulator') + +# (sel, arr[0], arr[1]): sel==1 -> arr[0] > arr[1]; sel==0 -> arr[0] <= arr[1] +SOLUTIONS = [ + '%d %d %d' % ((1 if arr0 > arr1 else 0), arr0, arr1) for arr0 in range(8) for arr1 in range(8) +] + +randomize_uniform_common.run(test, SOLUTIONS, r'\d+ \d+ \d+') diff --git a/test_regress/t/t_randomize_uniform_array_mixed.v b/test_regress/t/t_randomize_uniform_array_mixed.v new file mode 100644 index 000000000..d70051151 --- /dev/null +++ b/test_regress/t/t_randomize_uniform_array_mixed.v @@ -0,0 +1,55 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +// Checks that randomize() with an array mixed with a plain scalar in the +// same class, linked by a conditional constraint, covers the whole solution +// space, not just a lucky subset of it. Each sample is also printed so the +// driver can check the distribution's uniformity (Jensen-Shannon divergence) +// from the samples, not just coverage. + +// verilog_format: off +`define stop $stop +`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 + +module t; + class C; + rand bit [2:0] arr[2]; + rand bit sel; + constraint c { + if (sel) { arr[0] > arr[1]; } + else { arr[0] <= arr[1]; } + } + endclass + + // Every (arr[0],arr[1]) pair in [0:7]^2 has exactly one sel value that + // satisfies the constraint, so all 8*8 pairs are solutions. + localparam int NUM_SOLUTIONS = 64; + localparam int NUM_ITERS = 25 * NUM_SOLUTIONS; + + initial begin + automatic C c = new; + automatic int seen[int]; + automatic int distinct = 0; + automatic int key; + automatic int ok; + for (int i = 0; i < NUM_ITERS; ++i) begin + ok = c.randomize(); + `checkd(ok, 1); + // Exactly one ordering holds for each sel value + `checkd(c.sel, bit'(c.arr[0] > c.arr[1])); + key = int'({c.sel, c.arr[0], c.arr[1]}); // 7-bit packed key, fits in int + if (!seen.exists(key)) begin + seen[key] = 1; + distinct++; + end + $display("%0d %0d %0d", c.sel, c.arr[0], c.arr[1]); + end + `checkd(distinct, NUM_SOLUTIONS); + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule diff --git a/test_regress/t/t_randomize_uniform_bitcount.py b/test_regress/t/t_randomize_uniform_bitcount.py new file mode 100755 index 000000000..495303720 --- /dev/null +++ b/test_regress/t/t_randomize_uniform_bitcount.py @@ -0,0 +1,17 @@ +#!/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 +import randomize_uniform_common + +test.scenarios('simulator') + +SOLUTIONS = [i for i in range(256) if bin(i).count('1') == 4] # C(8,4) = 70 + +randomize_uniform_common.run(test, SOLUTIONS, r'\d+', key=int) diff --git a/test_regress/t/t_randomize_uniform_bitcount.v b/test_regress/t/t_randomize_uniform_bitcount.v new file mode 100644 index 000000000..8bbca99f5 --- /dev/null +++ b/test_regress/t/t_randomize_uniform_bitcount.v @@ -0,0 +1,52 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +// Checks that randomize() with a non-trivial scalar constraint (exactly N +// set bits, a non-contiguous solution set scattered across the domain) +// reaches nearly all of the solution space, not just a lucky subset of it. Each +// sample is also printed so the driver can check the distribution's +// uniformity (Jensen-Shannon divergence) from the samples, not just coverage. + +// verilog_format: off +`define stop $stop +`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); +`define check_range(gotv,minv,maxv) do if ((gotv) < (minv) || (gotv) > (maxv)) begin $write("%%Error: %s:%0d: got=%0d exp=[%0d:%0d]\n", `__FILE__,`__LINE__, (gotv), (minv), (maxv)); `stop; end while(0); +// verilog_format: on + +module t; + class C; + rand bit [7:0] x; + constraint c { $countones(x) == 4; } + endclass + + localparam int NUM_SOLUTIONS = 70; // C(8,4) + localparam int NUM_ITERS = 25 * NUM_SOLUTIONS; + + localparam int MIN_COVERAGE_PCT = 90; + localparam int MAX_COVERAGE_PCT = 100; + localparam int MIN_DISTINCT = (NUM_SOLUTIONS * MIN_COVERAGE_PCT) / 100; + localparam int MAX_DISTINCT = (NUM_SOLUTIONS * MAX_COVERAGE_PCT) / 100; + + initial begin + automatic C c = new; + automatic bit seen[256]; + automatic int distinct = 0; + automatic int ok; + for (int i = 0; i < NUM_ITERS; ++i) begin + ok = c.randomize(); + `checkd(ok, 1); + `checkd($countones(c.x), 4); + if (!seen[c.x]) begin + seen[c.x] = 1'b1; + distinct++; + end + $display("%0d", c.x); + end + `check_range(distinct, MIN_DISTINCT, MAX_DISTINCT); + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule