From 1717df02611a8ebd7f3494bf8a1290142ef4e7bd Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Sun, 22 Feb 2026 17:33:18 +0100 Subject: [PATCH] Support solve..before constraints (#5647) (#7123) --- include/verilated_random.cpp | 220 ++++++++++++++++++ include/verilated_random.h | 5 + src/V3AstAttr.h | 2 + src/V3Randomize.cpp | 47 +++- test_regress/t/t_constraint_solve_before.py | 21 ++ test_regress/t/t_constraint_solve_before.v | 112 +++++++++ .../t_constraint_solve_before_expr_unsup.out | 7 + .../t/t_constraint_solve_before_expr_unsup.py | 16 ++ .../t/t_constraint_solve_before_expr_unsup.v | 21 ++ test_regress/t/t_randomize.out | 4 - 10 files changed, 450 insertions(+), 5 deletions(-) create mode 100755 test_regress/t/t_constraint_solve_before.py create mode 100644 test_regress/t/t_constraint_solve_before.v create mode 100644 test_regress/t/t_constraint_solve_before_expr_unsup.out create mode 100755 test_regress/t/t_constraint_solve_before_expr_unsup.py create mode 100644 test_regress/t/t_constraint_solve_before_expr_unsup.v diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index e87b78f7c..2a1f3d562 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -490,6 +490,9 @@ bool VlRandomizer::next(VlRNG& rngr) { 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; @@ -723,6 +726,7 @@ void VlRandomizer::hard(std::string&& constraint, const char* filename, uint32_t void VlRandomizer::clearConstraints() { m_constraints.clear(); m_constraints_line.clear(); + m_solveBefore.clear(); // Keep m_vars for class member randomization } @@ -736,6 +740,222 @@ void VlRandomizer::clearAll() { void VlRandomizer::markRandc(const char* name) { m_randcVarNames.insert(name); } +void VlRandomizer::solveBefore(const char* beforeName, const char* afterName) { + m_solveBefore.emplace_back(std::string(beforeName), std::string(afterName)); +} + +bool VlRandomizer::nextPhased(VlRNG& rngr) { + // Phased solving for solve...before constraints. + // Variables are solved in layers determined by topological sort of the + // solve-before dependency graph. Each layer is solved with ALL constraints + // (preserving the solution space) but earlier layers' values are pinned. + + // Step 1: Build dependency graph (before -> {after vars}) + std::map> graph; + std::map inDegree; + std::set solveBeforeVars; + + for (const auto& pair : m_solveBefore) { + const std::string& before = pair.first; + const std::string& after = pair.second; + // Only consider variables that are actually registered + if (m_vars.find(before) == m_vars.end() || m_vars.find(after) == m_vars.end()) continue; + graph[before].insert(after); + solveBeforeVars.insert(before); + solveBeforeVars.insert(after); + if (inDegree.find(before) == inDegree.end()) inDegree[before] = 0; + if (inDegree.find(after) == inDegree.end()) inDegree[after] = 0; + } + + // Compute in-degrees (after depends on before, so edge is before->after, + // but for solving order: before has no incoming edge from after) + // Actually: "solve x before y" means x should be solved first. + // Dependency: y depends on x. Edge: x -> y. in-degree of y increases. + for (const auto& entry : graph) { + for (const auto& to : entry.second) { inDegree[to]++; } + } + + // Step 2: Topological sort into layers (Kahn's algorithm) + std::vector> layers; + std::set remaining = solveBeforeVars; + + while (!remaining.empty()) { + std::vector currentLayer; + for (const auto& var : remaining) { + if (inDegree[var] == 0) currentLayer.push_back(var); + } + if (currentLayer.empty()) { + VL_WARN_MT("", 0, "randomize", "Circular dependency in solve-before constraints"); + return false; + } + std::sort(currentLayer.begin(), currentLayer.end()); + for (const auto& var : currentLayer) { + remaining.erase(var); + if (graph.count(var)) { + for (const auto& to : graph[var]) { inDegree[to]--; } + } + } + layers.push_back(std::move(currentLayer)); + } + + // If only one layer, no phased solving needed -- fall through to normal path + // (all solve_before vars are independent, no actual ordering required) + if (layers.size() <= 1) { + // Clear solve_before temporarily and call normal next() + const auto saved = std::move(m_solveBefore); + m_solveBefore.clear(); + const bool result = next(rngr); + m_solveBefore = std::move(saved); + return result; + } + + // Step 3: Solve phase by phase + std::map solvedValues; // varName -> SMT value literal + + for (size_t phase = 0; phase < layers.size(); phase++) { + const bool isFinalPhase = (phase == layers.size() - 1); + + std::iostream& os = getSolver(); + if (!os) return false; + + // Solver session setup + 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 + 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"; + } + + // Pin all previously solved variables + for (const auto& entry : solvedValues) { + os << "(assert (= " << entry.first << " " << entry.second << "))\n"; + } + + // Assert ALL constraints + for (const std::string& constraint : m_constraints) { + os << "(assert (= #b1 " << constraint << "))\n"; + } + + // Initial check-sat WITHOUT diversity (guaranteed sat if constraints are consistent) + os << "(check-sat)\n"; + + if (isFinalPhase) { + // Final phase: use parseSolution to write ALL values to memory + bool sat = parseSolution(os, true); + if (!sat) { + os << "(reset)\n"; + return false; + } + // Diversity loop (same as normal next()) + 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"; + } else { + // Intermediate phase: extract values for current layer variables only + std::string satResponse; + do { std::getline(os, satResponse); } while (satResponse.empty()); + + if (satResponse != "sat") { + os << "(reset)\n"; + return false; + } + + // Build get-value variable list for this layer + const auto& layerVars = layers[phase]; + auto getValueCmd = [&]() { + os << "(get-value ("; + for (const auto& varName : layerVars) { + if (m_vars.count(varName)) os << varName << " "; + } + os << "))\n"; + }; + + // Helper to parse ((name1 value1) (name2 value2) ...) response + auto parseGetValue = [&]() -> bool { + char c; + os >> c; // outer '(' + while (true) { + os >> c; + if (c == ')') break; // outer closing + if (c != '(') return false; + std::string name; + os >> name; + + // Read value handling nested parens for (_ bvN W) format + os >> std::ws; + std::string value; + char firstChar; + os.get(firstChar); + if (firstChar == '(') { + // Compound value like (_ bv5 32) + value = "("; + int depth = 1; + while (depth > 0) { + os.get(c); + value += c; + if (c == '(') + depth++; + else if (c == ')') + depth--; + } + // Read closing ')' of the pair + os >> c; + } else { + // Atom value like #x00000005 or #b101 + value += firstChar; + while (os.get(c) && c != ')') { value += c; } + // Trim trailing whitespace + const size_t end = value.find_last_not_of(" \t\n\r"); + if (end != std::string::npos) value = value.substr(0, end + 1); + } + + solvedValues[name] = value; + } + return true; + }; + + // Get baseline values (deterministic, always valid) + getValueCmd(); + if (!parseGetValue()) { + os << "(reset)\n"; + return false; + } + + // Try diversity: add random constraint, re-check. If sat, get + // updated (more diverse) values. If unsat, keep baseline values. + os << "(assert "; + randomConstraint(os, rngr, _VL_SOLVER_HASH_LEN); + os << ")\n"; + os << "(check-sat)\n"; + satResponse.clear(); + do { std::getline(os, satResponse); } while (satResponse.empty()); + if (satResponse == "sat") { + getValueCmd(); + parseGetValue(); + } + + os << "(reset)\n"; + } + } + + return true; +} + #ifdef VL_DEBUG void VlRandomizer::dump() const { for (const auto& var : m_vars) { diff --git a/include/verilated_random.h b/include/verilated_random.h index 31aea0fc7..53c09f071 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -214,12 +214,15 @@ class VlRandomizer VL_NOT_FINAL { 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::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); size_t hashConstraints() const; + bool nextPhased(VlRNG& rngr); // Phased solving for solve...before public: // CONSTRUCTORS @@ -593,6 +596,8 @@ public: void clearConstraints(); void clearAll(); // Clear both constraints and variables void markRandc(const char* name); // Mark variable as randc for cyclic tracking + void solveBefore(const char* beforeName, + const char* afterName); // Register solve-before ordering void set_randmode(const VlQueue& randmode) { m_randmodep = &randmode; } #ifdef VL_DEBUG void dump() const; diff --git a/src/V3AstAttr.h b/src/V3AstAttr.h index afb6220eb..e879adfed 100644 --- a/src/V3AstAttr.h +++ b/src/V3AstAttr.h @@ -817,6 +817,7 @@ public: RANDOMIZER_HARD, RANDOMIZER_UNIQUE, RANDOMIZER_MARK_RANDC, + RANDOMIZER_SOLVE_BEFORE, RANDOMIZER_WRITE_VAR, RNG_GET_RANDSTATE, RNG_SET_RANDSTATE, @@ -952,6 +953,7 @@ inline std::ostream& operator<<(std::ostream& os, const VCMethod& rhs) { {RANDOMIZER_HARD, "hard", false}, \ {RANDOMIZER_UNIQUE, "rand_unique", false}, \ {RANDOMIZER_MARK_RANDC, "markRandc", false}, \ + {RANDOMIZER_SOLVE_BEFORE, "solveBefore", false}, \ {RANDOMIZER_WRITE_VAR, "write_var", false}, \ {RNG_GET_RANDSTATE, "__Vm_rng.get_randstate", true}, \ {RNG_SET_RANDSTATE, "__Vm_rng.set_randstate", false}, \ diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 621206d63..719d9eb42 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -753,6 +753,17 @@ class ConstraintExprVisitor final : public VNVisitor { return ""; } + // Extract SMT variable name from a solve-before expression. + // Returns empty string if the expression is not a simple variable reference. + std::string extractSolveBeforeVarName(AstNodeExpr* exprp) { + if (const AstMemberSel* const memberSelp = VN_CAST(exprp, MemberSel)) { + return buildMemberPath(memberSelp); + } else if (const AstVarRef* const varrefp = VN_CAST(exprp, VarRef)) { + return varrefp->name(); + } + return ""; + } + AstSFormatF* getConstFormat(AstNodeExpr* nodep) { return new AstSFormatF{nodep->fileline(), (nodep->width() & 3) ? "#b%b" : "#x%x", false, nodep}; @@ -1754,7 +1765,41 @@ class ConstraintExprVisitor final : public VNVisitor { VL_DO_DANGLING(nodep->deleteTree(), nodep); } void visit(AstConstraintBefore* nodep) override { - nodep->v3warn(CONSTRAINTIGN, "Constraint expression ignored (imperfect distribution)"); + // Generate solveBefore() calls for each (lhs, rhs) variable pair. + // Do NOT iterate children -- these are variable references, not constraint expressions. + FileLine* const fl = nodep->fileline(); + AstNodeModule* const genModp = VN_AS(m_genp->user2p(), NodeModule); + + for (AstNodeExpr* lhsp = nodep->lhssp(); lhsp; lhsp = VN_CAST(lhsp->nextp(), NodeExpr)) { + const std::string lhsName = extractSolveBeforeVarName(lhsp); + if (lhsName.empty()) { + lhsp->v3warn(CONSTRAINTIGN, + "Unsupported: non-variable expression in solve...before"); + continue; + } + for (AstNodeExpr* rhsp = nodep->rhssp(); rhsp; + rhsp = VN_CAST(rhsp->nextp(), NodeExpr)) { + const std::string rhsName = extractSolveBeforeVarName(rhsp); + if (rhsName.empty()) { + rhsp->v3warn(CONSTRAINTIGN, + "Unsupported: non-variable expression in solve...before"); + continue; + } + AstCMethodHard* const callp = new AstCMethodHard{ + fl, new AstVarRef{fl, genModp, m_genp, VAccess::READWRITE}, + VCMethod::RANDOMIZER_SOLVE_BEFORE}; + callp->dtypeSetVoid(); + AstNodeExpr* const beforeNamep + = new AstCExpr{fl, AstCExpr::Pure{}, "\"" + lhsName + "\""}; + beforeNamep->dtypeSetUInt32(); + AstNodeExpr* const afterNamep + = new AstCExpr{fl, AstCExpr::Pure{}, "\"" + rhsName + "\""}; + afterNamep->dtypeSetUInt32(); + callp->addPinsp(beforeNamep); + callp->addPinsp(afterNamep); + nodep->addHereThisAsNext(callp->makeStmt()); + } + } VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep); } void visit(AstConstraintUnique* nodep) override { diff --git a/test_regress/t/t_constraint_solve_before.py b/test_regress/t/t_constraint_solve_before.py new file mode 100755 index 000000000..db1adb3f9 --- /dev/null +++ b/test_regress/t/t_constraint_solve_before.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_constraint_solve_before.v b/test_regress/t/t_constraint_solve_before.v new file mode 100644 index 000000000..a415f7432 --- /dev/null +++ b/test_regress/t/t_constraint_solve_before.v @@ -0,0 +1,112 @@ +// 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 + +// 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 + +// Test solve...before constraint (IEEE 1800-2017 18.5.11) +// Verifies phased solving: 'before' variables are determined first, +// then 'after' variables are solved with all constraints applied. + +/* verilator lint_off UNSIGNED */ + +module t; + + // Test 1: solve with conditional constraints + class Packet; + rand bit [2:0] mode; + rand bit [7:0] data; + + constraint c_order { + solve mode before data; + mode inside {[0:3]}; + if (mode == 0) data == 8'h00; + else if (mode == 1) data inside {[8'h01:8'h0f]}; + else data < 8'h80; + } + endclass + + // Test 2: basic solve before with range constraints + class Simple; + rand bit [3:0] x; + rand bit [3:0] y; + + constraint c { + solve x before y; + x inside {[1:5]}; + y > x; + y < 4'hf; + } + endclass + + // Test 3: multi-level solve before (a -> b -> c) + class MultiLevel; + rand bit [3:0] a; + rand bit [3:0] b; + rand bit [3:0] c; + + constraint c_order { + solve a before b; + solve b before c; + a inside {[1:3]}; + b > a; + b < 8; + c > b; + c < 4'hf; + } + endclass + + initial begin + Packet p; + Simple s; + MultiLevel m; + int ok; + + // Test 1: Packet with conditional constraints + p = new; + repeat (20) begin + `checkd(p.randomize(), 1) + `check_range(p.mode, 0, 3) + if (p.mode == 0) `checkd(p.data, 0) + if (p.mode == 1) begin + `check_range(p.data, 1, 15) + end + if (p.mode >= 2) begin + ok = (p.data < 8'h80) ? 1 : 0; + `checkd(ok, 1) + end + end + + // Test 2: Simple range constraints + s = new; + repeat (20) begin + `checkd(s.randomize(), 1) + `check_range(s.x, 1, 5) + ok = (s.y > s.x) ? 1 : 0; + `checkd(ok, 1) + ok = (s.y < 4'hf) ? 1 : 0; + `checkd(ok, 1) + end + + // Test 3: Multi-level chain + m = new; + repeat (20) begin + `checkd(m.randomize(), 1) + `check_range(m.a, 1, 3) + ok = (m.b > m.a && m.b < 8) ? 1 : 0; + `checkd(ok, 1) + ok = (m.c > m.b && m.c < 4'hf) ? 1 : 0; + `checkd(ok, 1) + end + + $write("*-* All Finished *-*\n"); + $finish; + end + +endmodule diff --git a/test_regress/t/t_constraint_solve_before_expr_unsup.out b/test_regress/t/t_constraint_solve_before_expr_unsup.out new file mode 100644 index 000000000..41d9d6a4b --- /dev/null +++ b/test_regress/t/t_constraint_solve_before_expr_unsup.out @@ -0,0 +1,7 @@ +%Warning-CONSTRAINTIGN: t/t_constraint_solve_before_expr_unsup.v:12:27: Unsupported: non-variable expression in solve...before + : ... note: In instance 't' + 12 | constraint c { solve arr[0] before y; } + | ^ + ... For warning description see https://verilator.org/warn/CONSTRAINTIGN?v=latest + ... Use "/* verilator lint_off CONSTRAINTIGN */" and lint_on around source to disable this message. +%Error: Exiting due to diff --git a/test_regress/t/t_constraint_solve_before_expr_unsup.py b/test_regress/t/t_constraint_solve_before_expr_unsup.py new file mode 100755 index 000000000..a00127d05 --- /dev/null +++ b/test_regress/t/t_constraint_solve_before_expr_unsup.py @@ -0,0 +1,16 @@ +#!/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('linter') + +test.lint(fails=test.vlt_all, expect_filename=test.golden_filename) + +test.passes() diff --git a/test_regress/t/t_constraint_solve_before_expr_unsup.v b/test_regress/t/t_constraint_solve_before_expr_unsup.v new file mode 100644 index 000000000..2bedabd54 --- /dev/null +++ b/test_regress/t/t_constraint_solve_before_expr_unsup.v @@ -0,0 +1,21 @@ +// 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 + +class Cls; + rand int x; + rand int y; + rand int arr[4]; + + constraint c { solve arr[0] before y; } // BAD: non-variable expression +endclass + +module t; + // verilator lint_off IMPLICITSTATIC + initial begin + Cls c = new; + void'(c.randomize()); + end +endmodule diff --git a/test_regress/t/t_randomize.out b/test_regress/t/t_randomize.out index 0bc25bf43..1e9892a78 100644 --- a/test_regress/t/t_randomize.out +++ b/test_regress/t/t_randomize.out @@ -4,8 +4,4 @@ | ^~~~ ... For warning description see https://verilator.org/warn/CONSTRAINTIGN?v=latest ... Use "/* verilator lint_off CONSTRAINTIGN */" and lint_on around source to disable this message. -%Warning-CONSTRAINTIGN: t/t_randomize.v:43:23: Constraint expression ignored (imperfect distribution) - : ... note: In instance 't' - 43 | constraint order { solve length before header; } - | ^~~~~ %Error: Exiting due to