diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index 2a1f3d562..4ed746e86 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -496,6 +496,9 @@ bool VlRandomizer::next(VlRNG& rngr) { 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"; @@ -520,9 +523,20 @@ bool VlRandomizer::next(VlRNG& rngr) { os << "(assert (= " << pair.first << " (_ bv" << pair.second << " " << w << ")))\n"; } - os << "(check-sat)\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"; + } - bool sat = parseSolution(os, true); if (!sat) { // If unsat, use named assertions to get unsat-core os << "(reset)\n"; @@ -541,8 +555,11 @@ bool VlRandomizer::next(VlRNG& rngr) { } int j = 0; for (const std::string& constraint : m_constraints) { - os << "(assert (! (= #b1 " << constraint << ") :named cons" << j << "))\n"; - j++; + os << "(assert (! (= #b1 " << constraint << ") :named cons" << j++ << "))\n"; + } + for (const auto& pair : randcPinned) { + const int w = m_vars.at(pair.first)->width(); + os << "(assert (= " << pair.first << " (_ bv" << pair.second << " " << w << ")))\n"; } os << "(check-sat)\n"; sat = parseSolution(os, true); @@ -550,6 +567,7 @@ bool VlRandomizer::next(VlRNG& rngr) { 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); @@ -723,15 +741,22 @@ void VlRandomizer::hard(std::string&& constraint, const char* filename, uint32_t } } +void VlRandomizer::soft(std::string&& constraint, const char* /*filename*/, uint32_t /*linenum*/, + const char* /*source*/) { + m_softConstraints.emplace_back(std::move(constraint)); +} + void VlRandomizer::clearConstraints() { m_constraints.clear(); m_constraints_line.clear(); m_solveBefore.clear(); + m_softConstraints.clear(); // Keep m_vars for class member randomization } void VlRandomizer::clearAll() { m_constraints.clear(); + m_softConstraints.clear(); m_vars.clear(); m_randcVarNames.clear(); m_randcValueQueues.clear(); diff --git a/include/verilated_random.h b/include/verilated_random.h index 53c09f071..993778b55 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -200,9 +200,10 @@ public: // Object holding constraints and variable references. class VlRandomizer VL_NOT_FINAL { // MEMBERS - std::vector m_constraints; // Solver-dependent constraints + std::vector m_constraints; // Solver-dependent hard constraints std::vector m_constraints_line; // fileline content of the constraint for unsat constraints + std::vector m_softConstraints; // Soft constraints std::map> m_vars; // Solver-dependent // variables ArrayInfoMap m_arr_vars; // Tracks each element in array structures for iteration @@ -593,6 +594,8 @@ public: void hard(std::string&& constraint, const char* filename = "", uint32_t linenum = 0, const char* source = ""); + void soft(std::string&& constraint, const char* filename = "", uint32_t linenum = 0, + const char* source = ""); void clearConstraints(); void clearAll(); // Clear both constraints and variables void markRandc(const char* name); // Mark variable as randc for cyclic tracking diff --git a/src/V3AstAttr.h b/src/V3AstAttr.h index e879adfed..bfe9ba1fb 100644 --- a/src/V3AstAttr.h +++ b/src/V3AstAttr.h @@ -815,6 +815,7 @@ public: RANDOMIZER_CLEARCONSTRAINTS, RANDOMIZER_CLEARALL, RANDOMIZER_HARD, + RANDOMIZER_SOFT, RANDOMIZER_UNIQUE, RANDOMIZER_MARK_RANDC, RANDOMIZER_SOLVE_BEFORE, @@ -951,6 +952,7 @@ inline std::ostream& operator<<(std::ostream& os, const VCMethod& rhs) { {RANDOMIZER_CLEARCONSTRAINTS, "clearConstraints", false}, \ {RANDOMIZER_CLEARALL, "clearAll", false}, \ {RANDOMIZER_HARD, "hard", false}, \ + {RANDOMIZER_SOFT, "soft", false}, \ {RANDOMIZER_UNIQUE, "rand_unique", false}, \ {RANDOMIZER_MARK_RANDC, "markRandc", false}, \ {RANDOMIZER_SOLVE_BEFORE, "solveBefore", false}, \ diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index b80679b27..f03093ca5 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -1906,12 +1906,14 @@ class ConstraintExprVisitor final : public VNVisitor { VL_DO_DANGLING(nodep->deleteTree(), nodep); return; } - // Only hard constraints are currently supported + // Emit as soft or hard constraint per IEEE 1800-2017 18.5.13 + const VCMethod method + = nodep->isSoft() ? VCMethod::RANDOMIZER_SOFT : VCMethod::RANDOMIZER_HARD; AstCMethodHard* const callp = new AstCMethodHard{ nodep->fileline(), new AstVarRef{nodep->fileline(), VN_AS(m_genp->user2p(), NodeModule), m_genp, VAccess::READWRITE}, - VCMethod::RANDOMIZER_HARD, nodep->exprp()->unlinkFrBack()}; + method, nodep->exprp()->unlinkFrBack()}; callp->dtypeSetVoid(); // Pass filename, lineno, and source as separate arguments // This allows EmitC to call protect() on filename, similar to VL_STOP diff --git a/test_regress/t/t_randomize_soft.py b/test_regress/t/t_randomize_soft.py new file mode 100755 index 000000000..db1adb3f9 --- /dev/null +++ b/test_regress/t/t_randomize_soft.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_soft.v b/test_regress/t/t_randomize_soft.v new file mode 100644 index 000000000..2fe4cfa1c --- /dev/null +++ b/test_regress/t/t_randomize_soft.v @@ -0,0 +1,99 @@ +// 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 soft constraint solving per IEEE 1800-2017 section 18.5.13 + +// 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 + +// Case 1: Only soft, no hard -- soft should be satisfied +class Case1; + rand int x; + constraint c_soft { soft x == 5; } +endclass + +// Case 2: Two soft on same var -- last-wins (c_b declared after c_a) +class Case2; + rand int x; + constraint c_a { soft x == 5; } + constraint c_b { soft x == 10; } +endclass + +// Case 3: Soft on different vars -- both should be satisfied +class Case3; + rand int x; + rand int y; + constraint c_x { soft x == 7; } + constraint c_y { soft y == 3; } +endclass + +// Case 4: Soft range partially covered by hard -- SAT at intersection +class Case4; + rand int x; + constraint c_soft { soft x inside {[1:10]}; } + constraint c_hard { x inside {[5:15]}; } +endclass + +// Case 5: Soft completely overridden by hard -- hard wins +class Case5; + rand int x; + constraint c_soft { soft x == 5; } + constraint c_hard { x > 10; } +endclass + +module t; + Case1 c1; + Case2 c2; + Case3 c3; + Case4 c4; + Case5 c5; + int rand_ok; + + initial begin + c1 = new; + c2 = new; + c3 = new; + c4 = new; + c5 = new; + + repeat (20) begin + // Case 1: only soft, no hard -- soft satisfied + rand_ok = c1.randomize(); + `checkd(rand_ok, 1) + `checkd(c1.x, 5) + + // Case 2: two soft on same var -- last-wins + rand_ok = c2.randomize(); + `checkd(rand_ok, 1) + `checkd(c2.x, 10) + + // Case 3: soft on different vars -- both satisfied + rand_ok = c3.randomize(); + `checkd(rand_ok, 1) + `checkd(c3.x, 7) + `checkd(c3.y, 3) + + // Case 4: soft range partially covered by hard -- intersection [5:10] + rand_ok = c4.randomize(); + `checkd(rand_ok, 1) + `check_range(c4.x, 5, 10) + + // Case 5: soft completely overridden by hard -- hard wins + rand_ok = c5.randomize(); + `checkd(rand_ok, 1) + if (c5.x <= 10) begin + $write("%%Error: %s:%0d: x=%0d should be > 10\n", `__FILE__, `__LINE__, c5.x); + `stop; + end + end + + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule