From 5cb6f370e9970d38195455f43f6a2c01523b785a Mon Sep 17 00:00:00 2001 From: Arkadiusz Kozdra Date: Wed, 28 Aug 2024 16:11:39 +0200 Subject: [PATCH] Internals: Emit rand constraint right away. No functional change intended. (#5409) This change gets rid of most of the shared pointers and useless memory allocations. Also takes advantage of higher-arity bvxor/concat to reduce amount of data sent to the solver. Signed-off-by: Arkadiusz Kozdra --- include/verilated_random.cpp | 59 ++++++++++++++---------------------- include/verilated_random.h | 47 ++-------------------------- 2 files changed, 26 insertions(+), 80 deletions(-) diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index f7e85d1fe..d0ccefa70 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -253,23 +253,6 @@ static Process& getSolver() { //====================================================================== // VlRandomizer:: Methods -void VlRandomVar::emit(std::ostream& s) const { s << m_name; } -void VlRandomConst::emit(std::ostream& s) const { - s << "#b"; - for (int i = 0; i < m_width; i++) s << (VL_BITISSET_Q(m_val, m_width - i - 1) ? '1' : '0'); -} -void VlRandomBinOp::emit(std::ostream& s) const { - s << '(' << m_op << ' '; - m_lhs->emit(s); - s << ' '; - m_rhs->emit(s); - s << ')'; -} -void VlRandomExtract::emit(std::ostream& s) const { - s << "((_ extract " << m_idx << ' ' << m_idx << ") "; - m_expr->emit(s); - s << ')'; -} bool VlRandomVar::set(std::string&& val) const { VlWide qowp; VL_SET_WQ(qowp, 0ULL); @@ -307,27 +290,31 @@ bool VlRandomVar::set(std::string&& val) const { return true; } -std::shared_ptr VlRandomizer::randomConstraint(VlRNG& rngr, int bits) { - unsigned long long hash = VL_RANDOM_RNG_I(rngr) & ((1 << bits) - 1); - std::shared_ptr concat = nullptr; - std::vector> varbits; - for (const auto& var : m_vars) { - for (int i = 0; i < var.second->width(); i++) - varbits.emplace_back(std::make_shared(var.second, i)); - } +void VlRandomizer::randomConstraint(std::ostream& os, VlRNG& rngr, int bits) { + const IData hash = VL_RANDOM_RNG_I(rngr) & ((1 << bits) - 1); + int varBits = 0; + for (const auto& var : m_vars) varBits += var.second->width(); + os << "(= #b"; + for (int i = bits - 1; i >= 0; i--) os << (VL_BITISSET_I(hash, i) ? '1' : '0'); + if (bits > 1) os << " (concat"; for (int i = 0; i < bits; i++) { - std::shared_ptr bit = nullptr; - for (unsigned j = 0; j * 2 < varbits.size(); j++) { - unsigned idx = j + VL_RANDOM_RNG_I(rngr) % (varbits.size() - j); - auto sel = varbits[idx]; - std::swap(varbits[idx], varbits[j]); - bit = bit == nullptr ? sel : std::make_shared("bvxor", bit, sel); + IData varBitsLeft = varBits; + IData varBitsWant = (varBits + 1) / 2; + if (varBits > 2) os << " (bvxor"; + for (const auto& var : m_vars) { + for (int j = 0; j < var.second->width(); j++, varBitsLeft--) { + const bool doEmit = (VL_RANDOM_RNG_I(rngr) % varBitsLeft) < varBitsWant; + if (doEmit) { + os << " ((_ extract " << j << ' ' << j << ") " << var.second->name() << ')'; + if (--varBitsWant == 0) break; + } + } + if (varBitsWant == 0) break; } - concat = concat == nullptr ? bit - : std::make_shared("concat", concat, bit); + if (varBits > 2) os << ')'; } - return std::make_shared( - "=", concat, std::make_shared(hash, bits)); + if (bits > 1) os << ')'; + os << ')'; } bool VlRandomizer::next(VlRNG& rngr) { @@ -356,7 +343,7 @@ bool VlRandomizer::next(VlRNG& rngr) { for (int i = 0; i < _VL_SOLVER_HASH_LEN_TOTAL && sat; i++) { f << "(assert "; - randomConstraint(rngr, _VL_SOLVER_HASH_LEN)->emit(f); + randomConstraint(f, rngr, _VL_SOLVER_HASH_LEN); f << ")\n"; f << "\n(check-sat)\n"; sat = parseSolution(f); diff --git a/include/verilated_random.h b/include/verilated_random.h index 2612a6f2d..bd82d8628 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -30,11 +30,7 @@ //============================================================================= // VlRandomExpr and subclasses represent expressions for the constraint solver. -class VlRandomExpr VL_NOT_FINAL { -public: - virtual void emit(std::ostream& s) const = 0; -}; -class VlRandomVar final : public VlRandomExpr { +class VlRandomVar final { const char* const m_name; // Variable name void* const m_datap; // Reference to variable data const int m_width; // Variable width in bits @@ -52,44 +48,6 @@ public: std::uint32_t randModeIdx() const { return m_randModeIdx; } bool randModeIdxNone() const { return randModeIdx() == std::numeric_limits::max(); } bool set(std::string&&) const; - void emit(std::ostream& s) const override; -}; - -class VlRandomConst final : public VlRandomExpr { - const QData m_val; // Constant value - const int m_width; // Constant width in bits - -public: - VlRandomConst(QData val, int width) - : m_val{val} - , m_width{width} { - assert(width <= sizeof(m_val) * 8); - } - void emit(std::ostream& s) const override; -}; - -class VlRandomExtract final : public VlRandomExpr { - const std::shared_ptr m_expr; // Sub-expression - const unsigned m_idx; // Extracted index - -public: - VlRandomExtract(std::shared_ptr expr, unsigned idx) - : m_expr{expr} - , m_idx{idx} {} - void emit(std::ostream& s) const override; -}; - -class VlRandomBinOp final : public VlRandomExpr { - const char* const m_op; // Binary operation identifier - const std::shared_ptr m_lhs, m_rhs; // Sub-expressions - -public: - VlRandomBinOp(const char* op, std::shared_ptr lhs, - std::shared_ptr rhs) - : m_op{op} - , m_lhs{lhs} - , m_rhs{rhs} {} - void emit(std::ostream& s) const override; }; //============================================================================= @@ -103,7 +61,7 @@ class VlRandomizer final { const VlQueue* m_randmode; // rand_mode state; // PRIVATE METHODS - std::shared_ptr randomConstraint(VlRNG& rngr, int bits); + void randomConstraint(std::ostream& os, VlRNG& rngr, int bits); bool parseSolution(std::iostream& file); public: @@ -119,6 +77,7 @@ public: std::uint32_t randmodeIdx = std::numeric_limits::max()) { auto it = m_vars.find(name); if (it != m_vars.end()) return; + // TODO: make_unique once VlRandomizer is per-instance not per-ref m_vars[name] = std::make_shared(name, width, &var, randmodeIdx); } void hard(std::string&& constraint);