diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index e94f64518..bd0f775c1 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -559,7 +559,7 @@ bool VlRandomizer::next(VlRNG& rngr) { relaxSoftConstraints(os); os << "(check-sat)\n"; - bool sat = parseSolution(os, false); + bool sat = parseSolution(os); if (!sat) { os << "(reset)\n"; @@ -573,26 +573,7 @@ bool VlRandomizer::next(VlRNG& rngr) { // the solver's free assignment. if (m_checkOnly) return false; // 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; + reportUnsatSetup(os); os << "(reset)\n"; return false; } @@ -637,7 +618,7 @@ bool VlRandomizer::next(VlRNG& rngr) { for (int k = 0; k < npins; k++) if (!dropped[k]) os << " a" << k; os << "))\n"; - if (parseSolution(os, false)) break; + if (parseSolution(os)) break; // get-unsat-assumptions only echoes still-active literals, // so the first in-range index is a live conflicting bit. const std::vector core = readUnsatAssumptions(os); @@ -654,7 +635,7 @@ bool VlRandomizer::next(VlRNG& rngr) { randomConstraint(os, rngr, _VL_SOLVER_HASH_LEN); os << ")\n"; os << "\n(check-sat)\n"; - sat = parseSolution(os, false); + sat = parseSolution(os); (void)sat; } } @@ -692,14 +673,11 @@ void VlRandomizer::relaxSoftConstraints(std::iostream& os) { } } -std::vector VlRandomizer::readUnsatAssumptions(std::iostream& os) { - os << "(get-unsat-assumptions)\n"; - std::string line; - do { std::getline(os, line); } while (line.empty()); - // The response lists only "a" literals; collect each full integer run. +// Every complete run of digits in the reply, in order +static std::vector scanIntRuns(const std::string& reply) { std::vector idxs; std::string num; - for (const char c : line) { + for (const char c : reply) { if (std::isdigit(static_cast(c))) { num += c; } else if (!num.empty()) { @@ -711,60 +689,77 @@ std::vector VlRandomizer::readUnsatAssumptions(std::iostream& os) { return idxs; } -bool VlRandomizer::parseSolution(std::iostream& os, bool log) { +std::vector VlRandomizer::readUnsatAssumptions(std::iostream& os) { + os << "(get-unsat-assumptions)\n"; + std::string line; + do { std::getline(os, line); } while (line.empty()); + // The response lists only "a" literals; collect each full integer run. + return scanIntRuns(line); +} + +// Re-solve with named asserts so an unsat core can name the failing constraints +void VlRandomizer::reportUnsatSetup(std::iostream& os) { + 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"; + std::string status; + do { std::getline(os, status); } while (status.empty()); + if (status == "unsat") reportUnsatCore(os); +} + +void VlRandomizer::reportUnsatCore(std::iostream& os) { + os << "(get-unsat-core)\n"; + std::string reply; + std::getline(os, reply); + const std::vector numbers = scanIntRuns(reply); + if (Verilated::threadContextp()->warnUnsatConstr()) { + for (const int n : numbers) { + if (static_cast(n) < m_constraints_line.size()) { + const std::string& constraint_info = m_constraints_line[n]; + // Parse "filename:linenum source" format, parts optional + std::string filename; + int linenum = 0; + std::string source = constraint_info; + const size_t colon_pos = constraint_info.find(':'); + if (colon_pos != std::string::npos) { + filename = constraint_info.substr(0, colon_pos); + const size_t space_pos = constraint_info.find(" ", colon_pos); + const size_t num_end + = space_pos == std::string::npos ? constraint_info.size() : space_pos; + linenum = std::atoi( + constraint_info.substr(colon_pos + 1, num_end - colon_pos - 1).c_str()); + source = space_pos == std::string::npos + ? "" + : constraint_info.substr(space_pos + 3); + } + std::string msg = "UNSATCONSTR: Unsatisfied constraint"; + const size_t start = source.find_first_not_of(" \t"); + if (start != std::string::npos) msg += ": '" + source.substr(start) + "'"; + VL_WARN_MT(filename.c_str(), linenum, "", msg.c_str()); + } + } + } +} + +bool VlRandomizer::parseSolution(std::iostream& os) { std::string sat; do { std::getline(os, sat); } while (sat == ""); - if (sat == "unsat") { - if (!log) return false; - os << "(get-unsat-core) \n"; - sat.clear(); - std::getline(os, sat); - std::vector numbers; - std::string currentNum; - for (const char c : sat) { - if (std::isdigit(c)) { - currentNum += c; - numbers.push_back(std::stoi(currentNum)); - currentNum.clear(); - } - } - if (Verilated::threadContextp()->warnUnsatConstr()) { - for (const int n : numbers) { - if (n < m_constraints_line.size()) { - const std::string& constraint_info = m_constraints_line[n]; - // Parse "filename:linenum source" format - const size_t colon_pos = constraint_info.find(':'); - if (colon_pos != std::string::npos) { - const std::string filename = constraint_info.substr(0, colon_pos); - const size_t space_pos = constraint_info.find(" ", colon_pos); - std::string linenum_str; - std::string source; - if (space_pos != std::string::npos) { - linenum_str - = constraint_info.substr(colon_pos + 1, space_pos - colon_pos - 1); - source = constraint_info.substr(space_pos + 3); - } else { - linenum_str = constraint_info.substr(colon_pos + 1); - } - const int linenum = std::stoi(linenum_str); - std::string msg = "UNSATCONSTR: Unsatisfied constraint"; - if (!source.empty()) { - // Trim leading whitespace and add quotes - const size_t start = source.find_first_not_of(" \t"); - if (start != std::string::npos) { - msg += ": '" + source.substr(start) + "'"; - } - } - VL_WARN_MT(filename.c_str(), linenum, "", msg.c_str()); - } else { - VL_PRINTF("%%Warning-UNSATCONSTR: Unsatisfied constraint: %s\n", - constraint_info.c_str()); - } - } - } - } - return false; - } + if (sat == "unsat") return false; if (sat != "sat") { std::stringstream msg; msg << "Internal: Solver error: " << sat; @@ -1034,7 +1029,7 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) { if (isFinalPhase) { // Final phase: use parseSolution to write ALL values to memory - bool sat = parseSolution(os, true); + bool sat = parseSolution(os); if (!sat) { if (!m_randcVarNames.empty()) m_randcUsedValues.clear(); os << "(reset)\n"; @@ -1048,7 +1043,7 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) { randomConstraint(os, rngr, _VL_SOLVER_HASH_LEN); os << ")\n"; os << "\n(check-sat)\n"; - sat = parseSolution(os, false); + sat = parseSolution(os); (void)sat; } os << "(reset)\n"; diff --git a/include/verilated_random.h b/include/verilated_random.h index 31135bd97..a3a0da569 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -258,12 +258,14 @@ class VlRandomizer VL_NOT_FINAL { // PRIVATE METHODS void randomConstraint(std::ostream& os, VlRNG& rngr, int bits); - bool parseSolution(std::iostream& os, bool log = false); + bool parseSolution(std::iostream& os); bool checkSat(std::iostream& os); // Assert the maximal compatible soft-constraint set onto the open session. void relaxSoftConstraints(std::iostream& os); // Indices of the "a" literals named by (get-unsat-assumptions). std::vector readUnsatAssumptions(std::iostream& os); + void reportUnsatSetup(std::iostream& os); + void reportUnsatCore(std::iostream& os); void emitRandcExclusions(std::ostream& os) const; // Emit randc exclusion constraints void recordRandcValues(); // Record solved randc values for future exclusion size_t hashConstraints() const; diff --git a/test_regress/t/t_constraint_unsat_index.py b/test_regress/t/t_constraint_unsat_index.py new file mode 100755 index 000000000..55c4838b0 --- /dev/null +++ b/test_regress/t/t_constraint_unsat_index.py @@ -0,0 +1,26 @@ +#!/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('vlt') + +if not test.have_solver: + test.skip("No constraint solver installed") + +test.compile() + +# Constraint indices above 9 were parsed digit-by-digit from the core reply +test.execute() + +test.file_grep(test.run_log_filename, r"a > 8'd200") +test.file_grep(test.run_log_filename, r"a < 8'd100") +test.file_grep(test.run_log_filename, r'All Finished') + +test.passes() diff --git a/test_regress/t/t_constraint_unsat_index.v b/test_regress/t/t_constraint_unsat_index.v new file mode 100644 index 000000000..bea1b3868 --- /dev/null +++ b/test_regress/t/t_constraint_unsat_index.v @@ -0,0 +1,41 @@ +// 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 Packet; + rand bit [7:0] a; + rand bit [7:0] b; + constraint c_pad { + b > 8'd1; + b > 8'd2; + b > 8'd3; + b > 8'd4; + b > 8'd5; + b > 8'd6; + b > 8'd7; + b > 8'd8; + b > 8'd9; + b > 8'd10; + } + constraint c_a { + a > 8'd200; + a < 8'd100; + } +endclass + +module t; + initial begin + automatic Packet p = new; + repeat (3) begin + p.c_a.constraint_mode(0); + if (p.randomize() == 0) $stop; + if (!(p.b > 8'd10)) $stop; + p.c_a.constraint_mode(1); + if (p.randomize() != 0) $stop; + end + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule