From e0f1f316aa2e7a1fb192bf56d227f4f5f9b299cf Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Fri, 13 Mar 2026 12:53:51 +0100 Subject: [PATCH] Fix randc solver hang with wide variables (#7068) (#7248) --- include/verilated_random.cpp | 261 +++++++++------------- include/verilated_random.h | 10 +- test_regress/t/t_randc_wide_constraint.py | 21 ++ test_regress/t/t_randc_wide_constraint.v | 96 ++++++++ 4 files changed, 230 insertions(+), 158 deletions(-) create mode 100755 test_regress/t/t_randc_wide_constraint.py create mode 100644 test_regress/t/t_randc_wide_constraint.v diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index 98596e01a..81f99c021 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -23,7 +23,6 @@ #include "verilated_random.h" -#include #include #include #include @@ -376,76 +375,33 @@ size_t VlRandomizer::hashConstraints() const { return h; } -void VlRandomizer::enumerateRandcValues(const std::string& varName, VlRNG& rngr) { - std::vector values; - const auto varIt = m_vars.find(varName); - if (varIt == m_vars.end()) return; - const int width = varIt->second->width(); - - std::iostream& os = getSolver(); - if (!os) return; - - // Set up a single incremental solver session for enumeration - os << "(set-option :produce-models true)\n"; - os << "(set-logic QF_ABV)\n"; - os << "(define-fun __Vbv ((b Bool)) (_ BitVec 1) (ite b #b1 #b0))\n"; - os << "(define-fun __Vbool ((v (_ BitVec 1))) Bool (= #b1 v))\n"; - - // Declare all variables (solver needs full context for cross-var constraints) - for (const auto& var : m_vars) { - if (var.second->dimension() > 0) { - auto arrVarsp = std::make_shared(m_arr_vars); - var.second->setArrayInfo(arrVarsp); +void VlRandomizer::emitRandcExclusions(std::ostream& os) const { + for (const auto& name : m_randcVarNames) { + const auto usedIt = m_randcUsedValues.find(name); + if (usedIt != m_randcUsedValues.end()) { + const int w = m_vars.at(name)->width(); + for (const uint64_t val : usedIt->second) { + os << "(assert (not (= " << name << " (_ bv" << val << " " << w << "))))\n"; + } } - os << "(declare-fun " << var.first << " () "; - var.second->emitType(os); - os << ")\n"; } +} - // Assert all user constraints - for (const std::string& constraint : m_constraints) { - os << "(assert (= #b1 " << constraint << "))\n"; +static uint64_t readVarValueU64(const void* datap, int width) { + if (width <= VL_BYTESIZE) return *static_cast(datap); + if (width <= VL_SHORTSIZE) return *static_cast(datap); + if (width <= VL_IDATASIZE) return *static_cast(datap); + if (width <= VL_QUADSIZE) return *static_cast(datap); + return 0; +} + +void VlRandomizer::recordRandcValues() { + for (const auto& name : m_randcVarNames) { + const auto varIt = m_vars.find(name); + if (varIt == m_vars.end()) continue; + const VlRandomVar& var = *varIt->second; + m_randcUsedValues[name].insert(readVarValueU64(var.datap(0), var.width())); } - - // Incrementally enumerate all valid values for this randc variable - while (true) { - os << "(check-sat)\n"; - std::string sat; - do { std::getline(os, sat); } while (sat.empty()); - if (sat != "sat") break; - - // Read just this variable's value - os << "(get-value (" << varName << "))\n"; - char c; - os >> c; // '(' - os >> c; // '(' - std::string name, value; - os >> name; // Consume variable name token from solver output - (void)name; - std::getline(os, value, ')'); - os >> c; // ')' - - // Parse the SMT value to uint64_t - VlWide qowp; - VL_SET_WQ(qowp, 0ULL); - if (!parseSMTNum(width, qowp, value)) break; - const uint64_t numVal = (width <= 32) ? qowp[0] : VL_SET_QW(qowp); - - values.push_back(numVal); - - // Exclude this value for next iteration (incremental) - os << "(assert (not (= " << varName << " (_ bv" << numVal << " " << width << "))))\n"; - } - - os << "(reset)\n"; - - // Shuffle using Fisher-Yates - for (size_t i = values.size(); i > 1; --i) { - const size_t j = VL_RANDOM_RNG_I(rngr) % i; - std::swap(values[i - 1], values[j]); - } - - m_randcValueQueues[varName] = std::deque(values.begin(), values.end()); } bool VlRandomizer::next(VlRNG& rngr) { @@ -466,81 +422,30 @@ bool VlRandomizer::next(VlRNG& rngr) { } } - // Randc queue-based cycling: enumerate valid values once, then pop per call + // Randc exclusion-based cycling: exclude previously used values per randc var. + // When solver returns unsat (all values exhausted), clear history for new cycle. if (!m_randcVarNames.empty()) { const size_t currentHash = hashConstraints(); - // Invalidate queues if constraints changed (e.g., constraint_mode toggled) + // Invalidate history if constraints changed (e.g., constraint_mode toggled) if (currentHash != m_randcConstraintHash) { - m_randcValueQueues.clear(); + m_randcUsedValues.clear(); m_randcConstraintHash = currentHash; } - // Refill empty queues (start of new cycle) - for (const auto& name : m_randcVarNames) { - auto& queue = m_randcValueQueues[name]; - if (queue.empty()) enumerateRandcValues(name, rngr); - } - } - - // Pop randc values from queues (will be pinned in solver) - std::map randcPinned; - for (const auto& name : m_randcVarNames) { - auto& queue = m_randcValueQueues[name]; - if (queue.empty()) return false; // No valid values exist - randcPinned[name] = queue.front(); - queue.pop_front(); } // If solve-before constraints are present, use phased solving if (!m_solveBefore.empty()) return nextPhased(rngr); - std::iostream& os = getSolver(); - if (!os) return false; + // Randc retry: if unsat due to randc exhaustion, clear history and retry once + const bool hasRandc = !m_randcVarNames.empty(); + for (int attempt = 0; attempt < (hasRandc ? 2 : 1); ++attempt) { + std::iostream& os = getSolver(); + if (!os) return false; - // Soft constraint relaxation (IEEE 1800-2017 18.5.13, last-wins priority): - // Try hard + soft[0..N-1], then hard + soft[1..N-1], ..., then hard only. - // First SAT phase wins. If hard-only is UNSAT, report via unsat-core. - os << "(set-option :produce-models true)\n"; - os << "(set-logic QF_ABV)\n"; - os << "(define-fun __Vbv ((b Bool)) (_ BitVec 1) (ite b #b1 #b0))\n"; - os << "(define-fun __Vbool ((v (_ BitVec 1))) Bool (= #b1 v))\n"; - for (const auto& var : m_vars) { - if (var.second->dimension() > 0) { - auto arrVarsp = std::make_shared(m_arr_vars); - var.second->setArrayInfo(arrVarsp); - } - os << "(declare-fun " << var.first << " () "; - var.second->emitType(os); - os << ")\n"; - } - - for (const std::string& constraint : m_constraints) { - os << "(assert (= #b1 " << constraint << "))\n"; - } - - // Pin randc values from pre-enumerated queues - for (const auto& pair : randcPinned) { - const int w = m_vars.at(pair.first)->width(); - os << "(assert (= " << pair.first << " (_ bv" << pair.second << " " << w << ")))\n"; - } - - const size_t nSoft = m_softConstraints.size(); - bool sat = false; - for (size_t phase = 0; phase <= nSoft && !sat; ++phase) { - const bool hasSoft = (phase < nSoft); - if (hasSoft) { - os << "(push 1)\n"; - for (size_t i = phase; i < nSoft; ++i) - os << "(assert (= #b1 " << m_softConstraints[i] << "))\n"; - } - os << "(check-sat)\n"; - sat = parseSolution(os, /*log=*/phase == nSoft); - if (!sat && hasSoft) os << "(pop 1)\n"; - } - - if (!sat) { - // If unsat, use named assertions to get unsat-core - os << "(reset)\n"; - os << "(set-option :produce-unsat-cores true)\n"; + // Soft constraint relaxation (IEEE 1800-2017 18.5.13, last-wins priority): + // Try hard + soft[0..N-1], then hard + soft[1..N-1], ..., then hard only. + // First SAT phase wins. If hard-only is UNSAT, report via unsat-core. + os << "(set-option :produce-models true)\n"; os << "(set-logic QF_ABV)\n"; os << "(define-fun __Vbv ((b Bool)) (_ BitVec 1) (ite b #b1 #b0))\n"; os << "(define-fun __Vbool ((v (_ BitVec 1))) Bool (= #b1 v))\n"; @@ -553,32 +458,76 @@ bool VlRandomizer::next(VlRNG& rngr) { var.second->emitType(os); os << ")\n"; } - int j = 0; + for (const std::string& constraint : m_constraints) { - os << "(assert (! (= #b1 " << constraint << ") :named cons" << j++ << "))\n"; + os << "(assert (= #b1 " << constraint << "))\n"; } - for (const auto& pair : randcPinned) { - const int w = m_vars.at(pair.first)->width(); - os << "(assert (= " << pair.first << " (_ bv" << pair.second << " " << w << ")))\n"; + + // Randc: exclude previously used values to enforce cyclic non-repetition + emitRandcExclusions(os); + + const size_t nSoft = m_softConstraints.size(); + bool sat = false; + for (size_t phase = 0; phase <= nSoft && !sat; ++phase) { + const bool hasSoft = (phase < nSoft); + if (hasSoft) { + os << "(push 1)\n"; + for (size_t i = phase; i < nSoft; ++i) + os << "(assert (= #b1 " << m_softConstraints[i] << "))\n"; + } + os << "(check-sat)\n"; + sat = parseSolution(os, /*log=*/phase == nSoft); + if (!sat && hasSoft) os << "(pop 1)\n"; } - os << "(check-sat)\n"; - sat = parseSolution(os, true); - (void)sat; + + if (!sat) { + os << "(reset)\n"; + // If randc vars have used values, this may be cycle exhaustion - retry + if (hasRandc && !m_randcUsedValues.empty() && attempt == 0) { + m_randcUsedValues.clear(); + continue; // Retry without exclusions + } + // Genuine unsat: report via unsat-core + os << "(set-option :produce-unsat-cores true)\n"; + os << "(set-logic QF_ABV)\n"; + os << "(define-fun __Vbv ((b Bool)) (_ BitVec 1) (ite b #b1 #b0))\n"; + os << "(define-fun __Vbool ((v (_ BitVec 1))) Bool (= #b1 v))\n"; + for (const auto& var : m_vars) { + if (var.second->dimension() > 0) { + auto arrVarsp = std::make_shared(m_arr_vars); + var.second->setArrayInfo(arrVarsp); + } + os << "(declare-fun " << var.first << " () "; + var.second->emitType(os); + os << ")\n"; + } + int j = 0; + for (const std::string& constraint : m_constraints) { + os << "(assert (! (= #b1 " << constraint << ") :named cons" << j++ << "))\n"; + } + os << "(check-sat)\n"; + sat = parseSolution(os, true); + (void)sat; + os << "(reset)\n"; + return false; + } + + for (int i = 0; i < _VL_SOLVER_HASH_LEN_TOTAL && sat; ++i) { + os << "(assert "; + randomConstraint(os, rngr, _VL_SOLVER_HASH_LEN); + os << ")\n"; + os << "\n(check-sat)\n"; + sat = parseSolution(os, false); + (void)sat; + } + + // Record solved randc values for future exclusion + recordRandcValues(); + os << "(reset)\n"; - return false; + return true; } - - for (int i = 0; i < _VL_SOLVER_HASH_LEN_TOTAL && sat; ++i) { - os << "(assert "; - randomConstraint(os, rngr, _VL_SOLVER_HASH_LEN); - os << ")\n"; - os << "\n(check-sat)\n"; - sat = parseSolution(os, false); - (void)sat; - } - - os << "(reset)\n"; - return true; + return false; // Should not reach here } bool VlRandomizer::parseSolution(std::iostream& os, bool log) { @@ -767,7 +716,7 @@ void VlRandomizer::clearAll() { m_softConstraints.clear(); m_vars.clear(); m_randcVarNames.clear(); - m_randcValueQueues.clear(); + m_randcUsedValues.clear(); m_randcConstraintHash = 0; } @@ -878,6 +827,9 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) { os << "(assert (= #b1 " << constraint << "))\n"; } + // Randc: exclude previously used values + emitRandcExclusions(os); + // Initial check-sat WITHOUT diversity (guaranteed sat if constraints are consistent) os << "(check-sat)\n"; @@ -885,9 +837,12 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) { // Final phase: use parseSolution to write ALL values to memory bool sat = parseSolution(os, true); if (!sat) { + if (!m_randcVarNames.empty()) m_randcUsedValues.clear(); os << "(reset)\n"; return false; } + // Record solved randc values for future exclusion + recordRandcValues(); // Diversity loop (same as normal next()) for (int i = 0; i < _VL_SOLVER_HASH_LEN_TOTAL && sat; ++i) { os << "(assert "; diff --git a/include/verilated_random.h b/include/verilated_random.h index 09e12adad..3202c8326 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -28,7 +28,6 @@ #include "verilated.h" -#include #include #include #include @@ -220,16 +219,17 @@ class VlRandomizer VL_NOT_FINAL { const VlQueue* m_randmodep = nullptr; // rand_mode state; int m_index = 0; // Internal counter for key generation std::set m_randcVarNames; // Names of randc variables for cyclic tracking - std::map> - m_randcValueQueues; // Remaining values per randc var (queue-based cycling) - size_t m_randcConstraintHash = 0; // Hash of constraints when queues were built + std::map> + m_randcUsedValues; // Previously used values per randc var (exclusion-based cycling) + size_t m_randcConstraintHash = 0; // Hash of constraints when history was valid std::vector> m_solveBefore; // Solve-before ordering pairs (beforeVar, afterVar) // PRIVATE METHODS void randomConstraint(std::ostream& os, VlRNG& rngr, int bits); bool parseSolution(std::iostream& file, bool log = false); - void enumerateRandcValues(const std::string& varName, VlRNG& rngr); + void emitRandcExclusions(std::ostream& os) const; // Emit randc exclusion constraints + void recordRandcValues(); // Record solved randc values for future exclusion size_t hashConstraints() const; bool nextPhased(VlRNG& rngr); // Phased solving for solve...before diff --git a/test_regress/t/t_randc_wide_constraint.py b/test_regress/t/t_randc_wide_constraint.py new file mode 100755 index 000000000..db1adb3f9 --- /dev/null +++ b/test_regress/t/t_randc_wide_constraint.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_randc_wide_constraint.v b/test_regress/t/t_randc_wide_constraint.v new file mode 100644 index 000000000..49346d61c --- /dev/null +++ b/test_regress/t/t_randc_wide_constraint.v @@ -0,0 +1,96 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-License-Identifier: CC0-1.0 + +// Test that randc with wide variables (16-bit) and constraints does not hang. +// Previously, the solver tried to enumerate all valid values upfront, +// causing a pipe deadlock. See verilator/verilator#7068. + +// 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 + +class RandcFull; + randc bit [15:0] value; + + // Full 16-bit domain (65536 valid values). + // Old enumerateRandcValues() would try to enumerate all -> hang. + constraint range_c { value >= 0; } +endclass + +class RandcSmall; + randc bit [15:0] value; + + constraint range_c { value inside {[0:7]}; } +endclass + +typedef enum logic [59:0] { + E01 = 60'h1, + E02 = 60'h2, + E03 = 60'h3, + ELARGE = 60'h1234_4567_abcd +} wide_enum_t; + +class RandcWideEnum; + randc wide_enum_t value; +endclass + +module t; + initial begin + RandcFull full_obj; + RandcSmall small_obj; + RandcWideEnum enum_obj; + int seen[int]; + int rand_ok; + + // Test 1: randc 16-bit full domain - must not hang + full_obj = new(); + for (int i = 0; i < 5; i++) begin + rand_ok = full_obj.randomize(); + `checkd(rand_ok, 1) + end + + // Test 2: randc 16-bit with small constrained domain - verify cycling + small_obj = new(); + for (int i = 0; i < 8; i++) begin + rand_ok = small_obj.randomize(); + `checkd(rand_ok, 1) + if (small_obj.value > 16'd7) begin + $write("%%Error: value %0d out of range [0:7]\n", small_obj.value); + `stop; + end + if (seen.exists(int'(small_obj.value))) begin + $write("%%Error: duplicate value %0d before cycle complete\n", small_obj.value); + `stop; + end + seen[int'(small_obj.value)] = 1; + end + `checkd(seen.size(), 8) + + // Test 3: after full cycle, new cycle should start + rand_ok = small_obj.randomize(); + `checkd(rand_ok, 1) + if (small_obj.value > 16'd7) begin + $write("%%Error: value %0d out of range after cycle reset\n", small_obj.value); + `stop; + end + + // Test 4: wide enum (60-bit) randc - verify valid enum members only + enum_obj = new(); + for (int i = 0; i < 4; i++) begin + rand_ok = enum_obj.randomize(); + `checkd(rand_ok, 1) + if (enum_obj.value != E01 && enum_obj.value != E02 + && enum_obj.value != E03 && enum_obj.value != ELARGE) begin + $write("%%Error: enum value %0h not a valid member\n", enum_obj.value); + `stop; + end + end + + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule