luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fix UNSATCONSTR reporting constraint indices above 9 (#7995)

This commit is contained in:
Yilou Wang 2026-07-29 00:25:19 +02:00 committed by GitHub
parent c23b0ee972
commit b5fa4212b0
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
4 changed files with 148 additions and 84 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

161
include/verilated_random.cpp
View File

@ -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<const ArrayInfoMap>(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<int> 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<int> 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<N>" literals; collect each full integer run.
// Every complete run of digits in the reply, in order
static std::vector<int> scanIntRuns(const std::string& reply) {
std::vector<int> idxs;
std::string num;
for (const char c : line) {
for (const char c : reply) {
if (std::isdigit(static_cast<unsigned char>(c))) {
num += c;
} else if (!num.empty()) {
@ -711,60 +689,77 @@ std::vector<int> VlRandomizer::readUnsatAssumptions(std::iostream& os) {
return idxs;
}
bool VlRandomizer::parseSolution(std::iostream& os, bool log) {
std::vector<int> 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<N>" 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<const ArrayInfoMap>(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<int> numbers = scanIntRuns(reply);
if (Verilated::threadContextp()->warnUnsatConstr()) {
for (const int n : numbers) {
if (static_cast<size_t>(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<int> 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";

4
include/verilated_random.h
View File

@ -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<N>" literals named by (get-unsat-assumptions).
std::vector<int> 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;

26
test_regress/t/t_constraint_unsat_index.py Executable file
View File

@ -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()

41
test_regress/t/t_constraint_unsat_index.v Normal file
View File

@ -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