luke/verilator
1
0
Fork 0
mirror of https://github.com/verilator/verilator.git synced 2026-09-04 16:40:12 +02:00
Code Issues Packages Projects Releases Wiki Activity

Fix randomize misreading solver replies and applying partial models (Part3a of #7991) (#8136)

Browse Source
This commit is contained in:
Yilou Wang
2026-08-24 18:14:06 -04:00
committed by GitHub
parent 2cd0efbc0f
commit 67cbc36ef0
5 changed files with 744 additions and 106 deletions
Download Patch File Download Diff File Expand all files Collapse all files
include/verilated_random.cpp
+280 -88
View File
@@ -29,6 +29,7 @@
#include <iostream>
#include <sstream>
#include <streambuf>
#include <tuple>
// Diversity (scalar rand vars): tie each free bit to a random target via a
// boolean assumption literal, then force the bits with (check-sat-assuming).
@@ -265,6 +266,125 @@ private:
}
};
//======================================================================
// Solver reply protocol
enum class VlSolverStatus : uint8_t { SAT, UNSAT, UNKNOWN, FAIL };
static bool isSolverError(const std::string& reply) { return reply.compare(0, 6, "(error") == 0; }
// One non-blank reply line, trimmed; false once the solver stops answering
static bool readLine(std::istream& is, std::string& liner) {
while (std::getline(is, liner)) {
const size_t first = liner.find_first_not_of(" \t\r");
if (first == std::string::npos) continue;
const size_t last = liner.find_last_not_of(" \t\r");
liner = liner.substr(first, last - first + 1);
return true;
}
return false;
}
static bool scanParenDepth(const std::string& str, int& depthr, bool& inStringr) {
for (const char c : str) {
if (inStringr) {
if (c == '"') inStringr = false;
} else if (c == '"') {
inStringr = true;
} else if (c == '(') {
++depthr;
} else if (c == ')') {
if (depthr == 0) return false;
--depthr;
}
}
return true;
}
// Append lines until the error s-expression started in liner is paren-balanced
static void finishErrorReply(std::istream& is, std::string& liner) {
int depth = 0;
bool inString = false;
if (!scanParenDepth(liner, depth, inString)) return;
while (depth > 0) {
std::string chunk;
if (!readLine(is, chunk)) return;
liner += ' ';
liner += chunk;
if (!scanParenDepth(chunk, depth, inString)) return;
}
}
static void warnSolverReply(const std::string& reply) {
static bool s_warned = false;
if (s_warned) return;
s_warned = true;
const std::string msg
= "Solver did not answer with a status, so randomize() returns 0; warned once: " + reply;
VL_WARN_MT(__FILE__, __LINE__, "randomize", msg.c_str());
}
// Read one solver status; only a print-success echo may precede it
static VlSolverStatus readStatus(std::istream& is) {
std::string line;
while (readLine(is, line)) {
if (line == "success") continue;
if (line == "sat") return VlSolverStatus::SAT;
if (line == "unsat") return VlSolverStatus::UNSAT;
if (line == "unknown") {
static bool s_warnedUnknown = false;
if (!s_warnedUnknown) {
s_warnedUnknown = true;
VL_WARN_MT(__FILE__, __LINE__, "randomize",
"Solver returned unknown (timed out or incomplete), so randomize() "
"may return 0; warned once");
}
return VlSolverStatus::UNKNOWN;
}
// Consume the whole error, so the next read starts on a reply boundary
if (isSolverError(line)) finishErrorReply(is, line);
warnSolverReply(line);
return VlSolverStatus::FAIL;
}
return VlSolverStatus::FAIL;
}
// Read one complete paren-balanced s-expression, which may span lines
static bool readSExpr(std::istream& is, std::string& outr) {
outr.clear();
std::string pre;
int depth = 0;
bool inString = false;
char c = 0;
while (is.get(c)) {
if (depth == 0) {
if (c == '(') {
if (!pre.empty()) break;
outr += c;
depth = 1;
} else if (c == '\n') {
if (pre == "success") pre.clear();
if (!pre.empty()) break;
} else if (c != ' ' && c != '\t' && c != '\r') {
pre += c;
}
continue;
}
outr += c;
if (inString) {
if (c == '"') inString = false;
} else if (c == '"') {
inString = true;
} else if (c == '(') {
++depth;
} else if (c == ')') {
assert(depth > 0);
if (--depth == 0) return true;
}
}
return false;
}
static VlRProcess& getSolver() {
static VlRProcess s_solver;
static bool s_done = false;
@@ -287,9 +407,7 @@ static VlRProcess& getSolver() {
s_solver << "(set-logic QF_ABV)\n";
s_solver << "(check-sat)\n";
s_solver << "(reset)\n";
std::string s;
getline(s_solver, s);
if (s == "sat") return s_solver;
if (readStatus(s_solver) == VlSolverStatus::SAT) return s_solver;
std::stringstream msg;
msg << "Unable to communicate with SAT solver, please check its installation or specify a "
@@ -299,8 +417,6 @@ static VlRProcess& getSolver() {
msg << '\n';
const std::string str = msg.str();
VL_WARN_MT("", 0, "randomize", str.c_str());
while (getline(s_solver, s)) {}
return s_solver;
}
@@ -370,33 +486,57 @@ void VlRandomVar::emitConcreteValue(std::ostream& s) const {
}
}
int VlRandomVar::totalWidth() const { return m_width; }
static bool parseSMTNum(int obits, WDataOutP owp, const std::string& val) {
int i;
for (i = 0; val[i] && val[i] != '#'; ++i) {}
if (val[i++] != '#') return false;
// True if val is "#b/#o/#x/#h" followed by digits legal for that base
static bool validSMTNum(const std::string& val) {
size_t i = val.find('#');
if (i == std::string::npos || ++i >= val.size()) return false;
int base;
switch (val[i++]) {
case 'b': _vl_vsss_based(owp, obits, 1, &val[i], 0, val.size() - i); break;
case 'o': _vl_vsss_based(owp, obits, 3, &val[i], 0, val.size() - i); break;
case 'b': base = 2; break;
case 'o': base = 8; break;
case 'h': // FALLTHRU
case 'x': _vl_vsss_based(owp, obits, 4, &val[i], 0, val.size() - i); break;
default:
VL_WARN_MT(__FILE__, __LINE__, "randomize",
"Internal: Unable to parse solver's randomized number");
return false;
case 'x': base = 16; break;
default: return false;
}
const size_t end = val.find_last_not_of(" \t\r");
if (end < i) return false;
for (; i <= end; ++i) {
const char c = val[i];
int digit;
if (c >= '0' && c <= '9') {
digit = c - '0';
} else if (c >= 'a' && c <= 'f') {
digit = c - 'a' + 10;
} else if (c >= 'A' && c <= 'F') {
digit = c - 'A' + 10;
} else {
return false;
}
if (digit >= base) return false;
}
return true;
}
bool VlRandomVar::set(const std::string& idx, const std::string& val) const {
// val must have passed validSMTNum
static void parseSMTNum(int obits, WDataOutP owp, const std::string& val) {
size_t i = val.find('#') + 1;
switch (val[i++]) {
case 'b': _vl_vsss_based(owp, obits, 1, &val[i], 0, val.size() - i); break;
case 'o': _vl_vsss_based(owp, obits, 3, &val[i], 0, val.size() - i); break;
default: _vl_vsss_based(owp, obits, 4, &val[i], 0, val.size() - i); break;
}
}
void VlRandomVar::set(const std::string& idx, const std::string& val) const {
VlWide<VL_WQ_WORDS_E> qowp;
VL_SET_WQ(qowp, 0ULL);
WDataOutP owp = qowp;
const int obits = width();
VlWide<VL_WQ_WORDS_E> qiwp;
VL_SET_WQ(qiwp, 0ULL);
if (!idx.empty() && !parseSMTNum(64, qiwp, idx)) return false;
if (!idx.empty()) parseSMTNum(64, qiwp, idx);
const int nidx = qiwp[0];
if (obits > VL_QUADSIZE) owp = WDataOutP::external(reinterpret_cast<EData*>(datap(nidx)));
if (!parseSMTNum(obits, owp, val)) return false;
parseSMTNum(obits, owp, val);
if (obits <= VL_BYTESIZE) {
CData* const p = static_cast<CData*>(datap(nidx));
@@ -413,7 +553,6 @@ bool VlRandomVar::set(const std::string& idx, const std::string& val) const {
} else {
_vl_clean_inplace_w(obits, owp);
}
return true;
}
void VlRandomizer::randomConstraint(std::ostream& os, VlRNG& rngr, int bits) {
@@ -601,24 +740,29 @@ bool VlRandomizer::nextFlat(VlRNG& rngr, const std::vector<std::string>& uniqueE
relaxSoftConstraints(os);
os << "(check-sat)\n";
const bool sat = parseSolution(os);
const VlSolverStatus status = readStatus(os);
if (!sat) {
if (status != VlSolverStatus::SAT) {
os << "(reset)\n";
if (status != VlSolverStatus::UNSAT) return false;
// If randc vars have used values, this may be cycle exhaustion - retry
if (hasRandc && !m_randcUsedValues.empty() && attempt == 0) {
m_randcUsedValues.clear();
continue; // Retry without exclusions
}
// Skip the unsat-core path in check-only: it re-declares vars
// without pinning, so parseSolution would clobber user state with
// the solver's free assignment.
// without pinning, so the solver's free assignment would clobber
// user state.
if (m_checkOnly) return false;
// Genuine unsat: report via unsat-core
reportUnsatSetup(os, uniqueExprs);
os << "(reset)\n";
return false;
}
if (!applyModel(os)) {
os << "(reset)\n";
return false;
}
if (!m_checkOnly) {
solveDiversity(rngr, os);
@@ -669,58 +813,55 @@ void VlRandomizer::solveDiversityPins(VlRNG& rngr, std::iostream& os) {
if (!dropped[k]) os << " a" << k;
}
os << "))\n";
if (parseSolution(os)) return;
const VlSolverStatus status = readStatus(os);
if (status == VlSolverStatus::SAT) {
applyModel(os);
return;
}
// Unknown or failure: the base solution already written stands
if (status != VlSolverStatus::UNSAT) return;
// 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);
bool droppedOne = false;
for (const int idx : core) {
if (idx < npins) {
dropped[idx] = true;
droppedOne = true;
break;
}
}
if (!droppedOne) return;
}
}
void VlRandomizer::solveDiversityXor(VlRNG& rngr, std::iostream& os) {
bool sat = true;
for (int i = 0; i < _VL_SOLVER_HASH_LEN_TOTAL && sat; ++i) {
for (int i = 0; i < _VL_SOLVER_HASH_LEN_TOTAL; ++i) {
os << "(assert ";
randomConstraint(os, rngr, _VL_SOLVER_HASH_LEN);
os << ")\n";
os << "\n(check-sat)\n";
sat = parseSolution(os);
if (readStatus(os) != VlSolverStatus::SAT) break;
if (!applyModel(os)) break;
}
}
// False once the solver is gone, so no reply loop can spin forever
static bool readNonBlankLine(std::istream& is, std::string& liner) {
do {
if (!std::getline(is, liner)) return false;
} while (liner.empty());
return true;
}
bool VlRandomizer::checkSat(std::iostream& os) {
std::string result;
if (!readNonBlankLine(os, result)) return false;
return result == "sat";
}
// Re-add softs highest-priority first, dropping incompatible ones.
void VlRandomizer::relaxSoftConstraints(std::iostream& os) {
// Re-add softs highest-priority first, dropping incompatible ones.
const size_t nSoft = m_softConstraints.size();
if (nSoft == 0) return;
if (m_softConstraints.empty()) return;
os << "(push 1)\n";
for (const auto& s : m_softConstraints) os << "(assert (= #b1 " << s << "))\n";
os << "(check-sat)\n";
if (checkSat(os)) return;
const VlSolverStatus status = readStatus(os);
if (status == VlSolverStatus::SAT || status == VlSolverStatus::FAIL) return;
os << "(pop 1)\n";
for (auto it = m_softConstraints.rbegin(); it != m_softConstraints.rend(); ++it) {
os << "(push 1)\n";
os << "(assert (= #b1 " << *it << "))\n";
os << "(check-sat)\n";
if (!checkSat(os)) os << "(pop 1)\n";
const VlSolverStatus probe = readStatus(os);
if (probe == VlSolverStatus::FAIL) return;
if (probe != VlSolverStatus::SAT) os << "(pop 1)\n";
}
}
@@ -729,7 +870,8 @@ static std::vector<int> scanIntRuns(const std::string& reply) {
std::vector<int> idxs;
std::string num;
for (const char c : reply) {
if (std::isdigit(static_cast<unsigned char>(c))) {
// Cap the run so a garbled reply cannot overflow std::stoi
if (std::isdigit(static_cast<unsigned char>(c)) && num.size() < 9) {
num += c;
} else if (!num.empty()) {
idxs.push_back(std::stoi(num));
@@ -742,10 +884,14 @@ static std::vector<int> scanIntRuns(const std::string& reply) {
std::vector<int> VlRandomizer::readUnsatAssumptions(std::iostream& os) {
os << "(get-unsat-assumptions)\n";
std::string line;
if (!readNonBlankLine(os, line)) return {};
std::string reply;
if (!readSExpr(os, reply)) return {};
if (isSolverError(reply)) {
warnSolverReply(reply);
return {};
}
// The response lists only "a<N>" literals; collect each full integer run.
return scanIntRuns(line);
return scanIntRuns(reply);
}
// Re-solve with named asserts so an unsat core can name the failing constraints
@@ -757,15 +903,17 @@ void VlRandomizer::reportUnsatSetup(std::iostream& os,
emitDeclares(os, false);
emitAsserts(os, uniqueExprs, true);
os << "(check-sat)\n";
std::string status;
if (!readNonBlankLine(os, status)) return;
if (status == "unsat") reportUnsatCore(os);
if (readStatus(os) == VlSolverStatus::UNSAT) reportUnsatCore(os);
}
void VlRandomizer::reportUnsatCore(std::iostream& os) {
os << "(get-unsat-core)\n";
std::string reply;
std::getline(os, reply);
if (!readSExpr(os, reply)) return;
if (isSolverError(reply)) {
warnSolverReply(reply);
return;
}
const std::vector<int> numbers = scanIntRuns(reply);
if (Verilated::threadContextp()->warnUnsatConstr()) {
for (const int n : numbers) {
@@ -796,23 +944,16 @@ void VlRandomizer::reportUnsatCore(std::iostream& os) {
}
}
bool VlRandomizer::parseSolution(std::iostream& os) {
std::string sat;
if (!readNonBlankLine(os, sat)) return false;
if (sat == "unsat") return false;
if (sat != "sat") {
std::stringstream msg;
msg << "Internal: Solver error: " << sat;
const std::string str = msg.str();
VL_WARN_MT(__FILE__, __LINE__, "randomize", str.c_str());
return false;
}
bool VlRandomizer::applyModel(std::iostream& os) {
size_t requested = 0;
std::stringstream getValueStr;
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);
requested += var.second->countMatchingElements(m_arr_vars, var.second->name());
} else {
++requested;
}
var.second->emitGetValue(getValueStr);
}
@@ -822,15 +963,26 @@ bool VlRandomizer::parseSolution(std::iostream& os) {
return true;
}
os << "(get-value (" << getValueStr.str() << "))\n";
// Quasi-parse S-expression of the form ((x #xVALUE) (y #bVALUE) (z #xVALUE))
char c;
if (!(os >> c) || c != '(') {
VL_WARN_MT(__FILE__, __LINE__, "randomize",
"Internal: Unable to parse solver's response: invalid S-expression");
std::string reply;
if (!readSExpr(os, reply)) return false;
if (isSolverError(reply)) {
warnSolverReply(reply);
return false;
}
std::istringstream is{reply};
return parseModel(is, requested);
}
bool VlRandomizer::parseModel(std::istream& is, size_t requested) {
// Quasi-parse S-expression of the form ((x #xVALUE) (y #bVALUE) (z #xVALUE))
char c = 0;
is >> c; // The '(' opening the readSExpr-balanced reply
// Stage writes; commit only after the whole reply parses so failure keeps prior values
std::vector<std::tuple<const VlRandomVar*, std::string, std::string>> staged;
// Every requested term must come back exactly once, whether or not it is written
std::set<std::string> answered;
while (true) {
if (!(os >> c)) return false;
if (VL_UNCOVERABLE(!(is >> c))) return false; // Balanced reply breaks at ')' first
if (c == ')') break;
if (c != '(') {
VL_WARN_MT(__FILE__, __LINE__, "randomize",
@@ -841,16 +993,27 @@ bool VlRandomizer::parseSolution(std::iostream& os) {
std::string idx;
std::string value;
std::vector<std::string> indices;
os >> name;
is >> name;
indices.clear();
if (name == "(select") {
const std::string selectExpr = readUntilBalanced(os);
const std::string selectExpr = readUntilBalanced(is);
name = parseNestedSelect(selectExpr, indices);
}
std::getline(os, value, ')');
std::getline(is, value, ')');
const auto it = m_vars.find(name);
if (it == m_vars.end()) continue;
if (it == m_vars.end()) {
VL_WARN_MT(__FILE__, __LINE__, "randomize",
"Internal: Unable to parse solver's response: unknown variable");
return false;
}
const VlRandomVar& varr = *it->second;
std::string key = name;
for (const auto& index : indices) key += index;
if (!answered.insert(key).second) {
VL_WARN_MT(__FILE__, __LINE__, "randomize",
"Internal: Unable to parse solver's response: repeated variable");
return false;
}
if (!varr.randModeIdxNone()) {
// Static rand vars have their rand_mode in a class-package shared queue,
// not the per-instance one.
@@ -870,6 +1033,11 @@ bool VlRandomizer::parseSolution(std::iostream& os) {
continue;
}
std::string trimmed_hex = hex_index.substr(start + 2);
if (!validSMTNum(hex_index)) {
VL_WARN_MT(__FILE__, __LINE__, "randomize",
"Internal: Unable to parse solver's response: invalid array index");
return false;
}
if (trimmed_hex.size() <= 8) { // Small numbers: <= 32 bits
// Convert to decimal and output directly
@@ -896,8 +1064,22 @@ bool VlRandomizer::parseSolution(std::iostream& os) {
"indexed_name not found in m_arr_vars");
}
}
varr.set(idx, value);
// Reject before any commit, so a bad value later in the reply cannot
// leave earlier ones written
if (!validSMTNum(value)) {
VL_WARN_MT(__FILE__, __LINE__, "randomize",
"Internal: Unable to parse solver's response: invalid value");
return false;
}
staged.emplace_back(&varr, idx, value);
}
if (answered.size() != requested) {
VL_WARN_MT(__FILE__, __LINE__, "randomize",
"Internal: Unable to parse solver's response: incomplete model");
return false;
}
for (const auto& entry : staged)
std::get<0>(entry)->set(std::get<1>(entry), std::get<2>(entry));
return true;
}
@@ -1050,11 +1232,13 @@ bool VlRandomizer::solvePhases(VlRNG& rngr, const std::vector<std::vector<std::s
// Initial check-sat WITHOUT diversity (guaranteed sat if constraints are consistent)
os << "(check-sat)\n";
if (readStatus(os) != VlSolverStatus::SAT) {
os << "(reset)\n";
return false;
}
if (isFinalPhase) {
// Final phase: use parseSolution to write ALL values to memory
const bool sat = parseSolution(os);
if (!sat) {
if (!applyModel(os)) {
os << "(reset)\n";
return false;
}
@@ -1063,10 +1247,6 @@ bool VlRandomizer::solvePhases(VlRNG& rngr, const std::vector<std::vector<std::s
recordRandcValues();
os << "(reset)\n";
} else {
if (!checkSat(os)) {
os << "(reset)\n";
return false;
}
if (!solvePhaseValues(os, rngr, layers[phase], solvedValues)) {
os << "(reset)\n";
return false;
@@ -1101,7 +1281,7 @@ bool VlRandomizer::solvePhaseValues(std::iostream& os, VlRNG& rngr,
};
// Get baseline values (deterministic, always valid)
emitGetValueCmd();
if (!parsePhaseValues(os, solvedValuesr)) return false;
if (!readPhaseValues(os, solvedValuesr)) return false;
// Try diversity: add random constraint, re-check. If sat, get
// updated (more diverse) values. If unsat, keep baseline values.
@@ -1109,13 +1289,25 @@ bool VlRandomizer::solvePhaseValues(std::iostream& os, VlRNG& rngr,
randomConstraint(os, rngr, _VL_SOLVER_HASH_LEN);
os << ")\n";
os << "(check-sat)\n";
if (checkSat(os)) {
if (readStatus(os) == VlSolverStatus::SAT) {
emitGetValueCmd();
(void)parsePhaseValues(os, solvedValuesr);
(void)readPhaseValues(os, solvedValuesr);
}
return true;
}
bool VlRandomizer::readPhaseValues(std::iostream& os,
std::map<std::string, std::string>& solvedValuesr) {
std::string reply;
if (!readSExpr(os, reply)) return false;
if (isSolverError(reply)) {
warnSolverReply(reply);
return false;
}
std::istringstream is{reply};
return parsePhaseValues(is, solvedValuesr);
}
bool VlRandomizer::parsePhaseValues(std::istream& is,
std::map<std::string, std::string>& solvedValuesr) {
// Parse ((name value) ...): one paren-depth counter drives every match.
include/verilated_random.h
+5 -3
View File
@@ -79,7 +79,7 @@ public:
virtual void* datap(int /*idx*/) const { return m_datap; }
std::uint32_t randModeIdx() const { return m_randModeIdx; }
bool randModeIdxNone() const { return randModeIdx() == std::numeric_limits<unsigned>::max(); }
bool set(const std::string& idx, const std::string& val) const;
void set(const std::string& idx, const std::string& val) const;
virtual void emitGetValue(std::ostream& s) const;
virtual void emitExtract(std::ostream& s, int i) const;
virtual void emitType(std::ostream& s) const;
@@ -257,8 +257,9 @@ class VlRandomizer VL_NOT_FINAL {
// PRIVATE METHODS
void randomConstraint(std::ostream& os, VlRNG& rngr, int bits);
bool parseSolution(std::iostream& os);
bool checkSat(std::iostream& os);
// Fetch the model and write it into the registered variables.
bool applyModel(std::iostream& os);
bool parseModel(std::istream& is, size_t requested);
// 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).
@@ -287,6 +288,7 @@ class VlRandomizer VL_NOT_FINAL {
bool solvePhaseValues(std::iostream& os, VlRNG& rngr,
const std::vector<std::string>& layerVars,
std::map<std::string, std::string>& solvedValuesr);
bool readPhaseValues(std::iostream& os, std::map<std::string, std::string>& solvedValuesr);
bool parsePhaseValues(std::istream& is, std::map<std::string, std::string>& solvedValuesr);
public:
test_regress/t/randomize_solver_tamper.py
+304 -15
View File
@@ -7,19 +7,67 @@
# SPDX-FileCopyrightText: 2026 Wilson Snyder
# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
#
# Forwards the SMT-LIB conversation to a real solver, then kills it.
# Forwards the SMT-LIB conversation to a real solver, tampering the replies.
#
# Input arguments from environment variables:
# TAMPER: none | die_at | die_status_at | mute_at | garbage_at
# die_at - kill the solver and exit, closing every pipe end
# die_status_at - same, counting sat/unsat status lines instead of models
# mute_at - close the reply pipe but keep this wrapper running
# garbage_at - replace every Nth model reply with a non-S-expression line
# TAMPER: bad_base | bad_digits | bad_index | bad_value | bare_hash | binary
# | core_junk | crlf | die_at | die_status_at | dup_model | err_assume
# | err_core | err_multiline | err_once | err_phase | err_reply
# | err_trunc | err_unbal | err_unbal_cont | garbage_assume | garbage_at
# | garbage_model | garbage_status | high_digit | indent | low_digit
# | model_trunc | multiline | mute_at | no_digits | none | octal
# | oor_assume | phase_model | phase_trunc | short_model | success
# | unknown_once | unknown_twice | unknown_var | unsupported_once
# | upper_hex
# bad_base - replace the Nth model reply with a base character that is not b, o, x or h
# bad_digits - replace the Nth model reply with one value holding digits outside its base
# bad_index - replace the first array model reply with a bad select index
# bad_value - replace the Nth model reply with one well-formed value lacking a base
# bare_hash - replace the Nth model reply with one value that is only "#"
# binary - replace the Nth model reply with binary values
# core_junk - prepend garbage to the core reply and close the pipe
# crlf - end every line with CRLF
# die_at - kill the solver at the Nth model reply and exit, closing every pipe end
# die_status_at - kill the solver at the Nth status line and exit, closing every pipe end
# dup_model - replace the Nth model reply with one answering a variable twice
# err_assume - replace the first unsat-assumptions reply with (error ...)
# err_core - replace the first unsat-core reply with (error ...)
# err_multiline - answer the Nth status with an (error ...) split over two lines
# err_once - answer the Nth status with one (error ...) line
# err_phase - replace the first phase value reply with (error ...)
# err_reply - replace the Nth S-expression reply with (error ...)
# err_trunc - answer the Nth status with an unterminated (error and close the pipe
# err_unbal - answer the Nth status with an error closing an extra paren
# err_unbal_cont - answer the Nth status with an error, the extra paren on a continuation line
# garbage_assume - answer the unsat assumptions with a non-S-expression word
# garbage_at - replace every Nth model reply with a non-S-expression line
# garbage_model - replace the Nth model reply with a partly valid one
# garbage_status - replace the Nth status with a word that is not a status
# high_digit - replace the Nth model reply with a digit valid only in a wider base
# indent - prepend whitespace to every reply line
# low_digit - replace the Nth model reply with a character below any digit or letter
# model_trunc - answer the Nth model with an unterminated reply and close the pipe
# multiline - split every S-expression reply one token per line
# mute_at - close the reply pipe at the Nth model reply but keep this wrapper running
# no_digits - replace the Nth model reply with a value whose base has no digits
# none - forward every reply unchanged
# octal - replace the Nth model reply with octal values
# oor_assume - answer the unsat assumptions with an out-of-range literal
# phase_model - replace the final phased model reply with (error ...)
# phase_trunc - answer an unterminated phase value reply and close the pipe
# short_model - replace the Nth model reply with one omitting a requested variable
# success - echo a print-success line before every reply
# unknown_once - answer the Nth status with unknown
# unknown_twice - answer two statuses with unknown
# unknown_var - replace the Nth model reply with one naming a variable never requested
# unsupported_once - answer the Nth status with unsupported
# upper_hex - replace the Nth model reply with uppercase hex digits
# TAMPER_AT: reply index to act on (default 3)
# pylint: disable=C0103,C0114,consider-using-with
import os
import re
import shutil
import subprocess
import sys
@@ -28,6 +76,23 @@ import time
mode = os.environ.get("TAMPER", "none")
at = int(os.environ.get("TAMPER_AT", "3"))
# Modes acting on the TAMPER_AT'th status line rather than the Nth model reply
STATUS_MODES = ("die_status_at", "err_multiline", "err_once", "err_trunc", "err_unbal",
"err_unbal_cont", "garbage_status", "unknown_once", "unknown_twice",
"unsupported_once")
# Modes acting on the TAMPER_AT'th S-expression reply of any kind
REPLY_MODES = ("err_reply", )
# Modes acting on the first array model reply, which arrives as (select ...) terms
SELECT_MODES = ("bad_index", )
# phase_model acts on the final phased model; the others on any phase value reply
PHASE_MODES = ("err_phase", "phase_model", "phase_trunc")
# Modes acting on an unsat-assumptions reply, which lists a<N> literals
ASSUME_MODES = ("err_assume", "garbage_assume", "oor_assume")
# Modes acting on an unsat-core reply, which lists cons<N> names
CORE_MODES = ("core_junk", "err_core")
# Modes rewriting every line, so they never consume the index
STREAM_MODES = ("crlf", "indent", "multiline", "success")
def real_solver():
"""Return argv for the first SMT solver found in PATH"""
@@ -40,23 +105,247 @@ def real_solver():
proc = subprocess.Popen(real_solver(), stdin=sys.stdin, stdout=subprocess.PIPE, text=True)
def emit(text):
"""Write one reply line downstream, unbuffered"""
sys.stdout.write(text + ("\r\n" if mode == "crlf" else "\n"))
sys.stdout.flush()
def forward(text, at_start):
"""Pass a real reply through, applying the whole-stream rewrites"""
# Solvers echo success per command, so never inside a wrapped S-expression
if mode == "success" and at_start:
emit("success")
if mode == "multiline" and text.startswith("(") and not text.startswith("(error"):
for tok in text.split():
emit(tok)
elif mode == "indent":
emit(" \t" + text)
else:
emit(text)
def scan_depth(text, left, in_string):
"""Paren depth of text, ignoring parens inside SMT string literals"""
for char in text:
if in_string:
in_string = char != '"'
elif char == '"':
in_string = True
elif char == "(":
left += 1
elif char == ")":
left -= 1
return left, in_string
def read_full(first):
"""Return the complete S-expression reply that starts at first"""
chunks = [first]
left, in_string = scan_depth(first, 0, False)
while left > 0:
cont = proc.stdout.readline()
if not cont:
break
chunks.append(cont.rstrip("\n"))
left, in_string = scan_depth(cont, left, in_string)
return chunks
def swallow(first):
"""Drop the rest of a real S-expression reply that was replaced"""
read_full(first)
replies = 0
acting = False
done = False
depth = 0 # Paren depth of the reply being forwarded, so wrapped ones stay intact
inside = False # Inside an SMT string literal, where parens do not nest
for line in proc.stdout:
line = line.rstrip("\n")
counted = line in ("sat", "unsat",
"unknown") if mode == "die_status_at" else line.startswith("((")
at_reply_start = depth == 0
depth, inside = scan_depth(line, depth, inside)
is_status = line in ("sat", "unsat", "unknown")
if mode in STATUS_MODES:
counted = is_status
elif mode in REPLY_MODES:
# Only a first line opens a reply; a wrapped continuation is not a new one
counted = at_reply_start and line.startswith("(")
elif mode in SELECT_MODES:
counted = at_reply_start and line.startswith("(((select")
elif mode in PHASE_MODES:
counted = at_reply_start and line.startswith("((x")
elif mode in ASSUME_MODES:
counted = at_reply_start and re.match(r"\(a\d", line) is not None
elif mode in CORE_MODES:
counted = at_reply_start and line.startswith("(cons")
else:
counted = at_reply_start and line.startswith("((")
if counted:
replies += 1
acting = counted and replies >= at
if acting and mode == "garbage_at":
line = "junk"
replies = 0
sys.stdout.write(line + "\n")
sys.stdout.flush()
acting = counted and replies >= at and not done and mode not in STREAM_MODES
if not acting:
forward(line, at_reply_start)
continue
done = True
if mode == "bad_base":
emit("((a #z01) (b #x12))")
swallow(line)
continue
if mode == "bad_digits":
emit("((a #x0b) (b #xgg))")
swallow(line)
continue
if mode == "bad_index":
emit("(((select q #xgg) #x15) ((select q #x00000001) #x15)"
" ((select q #x00000002) #x15))")
swallow(line)
continue
# A well-formed reply whose second value is unusable: the first must not
# reach the variable either
if mode == "bad_value":
emit("((a #x0b) (b bogus))")
swallow(line)
continue
if mode == "bare_hash":
emit("((a #x0b) (b #))")
swallow(line)
continue
if mode == "binary":
emit("((a #b00001011) (b #b00010010))")
swallow(line)
continue
if mode == "core_junk":
emit("junk((cons0))")
proc.kill()
proc.wait()
sys.exit(0)
if mode == "dup_model":
emit("((a #x0b) (a #x0c) (b #x05))")
swallow(line)
continue
if mode == "err_assume":
emit('(error "injected assumptions error")')
swallow(line)
continue
if mode == "err_core":
emit('(error "injected core error")')
swallow(line)
continue
if mode == "err_multiline":
emit('(error "injected')
emit('multiline error")')
continue
if mode == "err_once":
emit('(error "injected command rejected")')
continue
# The first phase value reply always precedes the final phased model
if mode == "err_phase":
emit('(error "injected phase value error")')
swallow(line)
continue
if mode == "err_reply":
emit('(error "injected reply error")')
swallow(line)
continue
if mode == "err_trunc":
emit('(error "unterminated')
proc.kill()
proc.wait()
sys.exit(0)
if mode == "err_unbal":
emit('(error "unbalanced"))')
continue
if mode == "err_unbal_cont":
emit('(error "unbalanced"')
emit('))')
continue
if mode == "garbage_assume":
emit("junk")
swallow(line)
continue
# garbage_at repeats, so it re-arms instead of latching
if mode == "garbage_at":
replies = 0
done = False
emit("junk")
continue
if mode == "garbage_model":
emit("((a #x0b) junk)")
swallow(line)
continue
if mode == "garbage_status":
emit("flurble")
continue
if mode == "high_digit":
emit("((a #x0b) (b #b2))")
swallow(line)
continue
if mode == "low_digit":
emit("((a #x0b) (b #x!))")
swallow(line)
continue
if mode == "model_trunc":
emit("((a #x0b)")
proc.kill()
proc.wait()
sys.exit(0)
if mode == "no_digits":
emit("((a #x0b) (b #x))")
swallow(line)
continue
if mode == "octal":
emit("((a #o13) (b #o12))")
swallow(line)
continue
if mode == "oor_assume":
emit("(a99999999999999)")
swallow(line)
continue
# Only the final phase queries every variable, so only that reply names y
if mode == "phase_model":
replies = 0 # Re-arm until the final phase is seen
done = False
parts = read_full(line)
if "(y " in " ".join(parts):
emit('(error "injected phased model error")')
else:
for part in parts:
forward(part, part is parts[0])
continue
if mode == "phase_trunc":
emit("((x")
proc.kill()
proc.wait()
sys.exit(0)
if mode == "short_model":
emit("((a #x0b))")
swallow(line)
continue
if mode == "unknown_once":
emit("unknown")
continue
if mode == "unknown_twice":
emit("unknown")
done = replies >= at + 1
continue
if mode == "unknown_var":
emit("((zzz #x01) (b #x12))")
swallow(line)
continue
if mode == "unsupported_once":
emit("unsupported")
continue
if mode == "upper_hex":
emit("((a #xAB) (b #x12))")
swallow(line)
continue
forward(line, at_reply_start)
if mode in ("die_at", "die_status_at"):
proc.kill()
proc.wait()
test_regress/t/t_randomize_solver_reply.py
Executable
+69
View File
@@ -0,0 +1,69 @@
#!/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()
# 16 randomize calls; each entry names the reply the solver mangles
runs = [
('bad_base', 1, 15), # a base character that is not b, o, x or h
('bad_digits', 1, 15), # digits outside the stated base are not a number
('bad_index', 1, 15), # a malformed array select index
('bad_value', 1, 15), # a value with no base must not commit the earlier one
('bare_hash', 1, 15), # a value that is only "#"
('binary', 1, 16), # binary values
('core_junk', 1, 4), # garbage opens the core reply, then the pipe closes
('crlf', 1, 16), # CRLF line endings
('dup_model', 1, 15), # the same variable answered twice
('err_assume', 1, 16), # error in place of the unsat assumptions
('err_core', 1, 16), # error in place of the unsat core
('err_multiline', 2, 15), # solver rejects a command with an error spanning two lines
('err_once', 2, 15), # solver rejects a command instead of answering
('err_phase', 1, 15), # error in place of an intermediate phase value reply
('err_reply', 1, 15), # error in place of an S-expression reply
('err_trunc', 2, 0), # unterminated error, then the pipe closes
('err_unbal', 2, 15), # a rejection error closing more parens than it opens
('err_unbal_cont', 2, 15), # a rejection error with the extra paren on a continuation line
('garbage_assume', 1, 16), # a bare word in place of the unsat assumptions
('garbage_model', 1, 15), # half-valid model must not reach the variables
('garbage_status', 2, 15), # a word that is not a status
('garbage_status', 8, 15), # a phased check-sat that does not answer with a status
('high_digit', 1, 15), # a digit legal for some base but not the stated one
('indent', 1, 16), # leading whitespace before every reply
('low_digit', 1, 15), # a character below any digit or letter
('model_trunc', 1, 0), # unterminated model, then the pipe closes
('multiline', 1, 16), # S-expression split one token per line
('no_digits', 1, 15), # a base marker with no digits after it
('octal', 1, 16), # octal values
('oor_assume', 1, 16), # unsat assumptions naming only an out-of-range literal
('phase_model', 1, 15), # error in place of the final phased model
('phase_trunc', 1, 2), # unterminated phase value reply, then the pipe closes
('short_model', 1, 15), # a model missing a requested variable is not a model
('success', 1, 16), # print-success echo ahead of every reply
('unknown_once', 2, 15), # unknown answers one check-sat
('unknown_twice', 2, 15), # a second unknown must not warn again
('unknown_var', 1, 15), # a variable that was never requested
('unsupported_once', 2, 15), # command not supported, so no status ever comes
('upper_hex', 1, 16), # uppercase hex digits
]
for mode, at, npass in runs:
logfile = test.obj_dir + '/sim_' + mode + '_' + str(at) + '.log'
test.execute(logfile=logfile,
run_env='VERILATOR_SOLVER="' + test.t_dir + '/randomize_solver_tamper.py" ' +
'TAMPER=' + mode + ' TAMPER_AT=' + str(at))
test.file_grep(logfile, r'NPASS=(\d+)', npass)
test.passes()
test_regress/t/t_randomize_solver_reply.v
+86
View File
@@ -0,0 +1,86 @@
// 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);
// verilog_format: on
// Model and diversity assumption replies
class Packet;
rand bit [7:0] a;
rand bit [7:0] b;
constraint c {
a > 8'd10;
b < 8'd200;
a != b;
}
endclass
// Soft constraint relaxation replies
class Softy;
rand bit [7:0] s;
constraint sc {
soft s == 8'd42;
s > 8'd100;
}
endclass
// Phased solve...before replies
class Phased;
rand bit [3:0] x;
rand bit [3:0] y;
constraint order_c {solve x before y;}
constraint rel_c {y > x;}
endclass
// Array element replies, which arrive as (select ...) terms
class Arr;
rand bit [7:0] q[3];
constraint ac {foreach (q[i]) q[i] > 8'd20;}
endclass
// Unsatisfiable, so the unsat core is queried
class Unsat;
rand bit [7:0] u;
constraint uc {
u > 8'd200;
u < 8'd100;
}
endclass
module t;
initial begin
automatic Packet p = new;
automatic Softy s = new;
automatic Phased ph = new;
automatic Arr ar = new;
automatic Unsat un = new;
automatic int npass = 0;
automatic int rc;
for (int i = 0; i < 4; ++i) begin
// Below the constraint, so any model the runtime applies overwrites it
p.a = 8'd5;
rc = p.randomize();
// A randomize that failed must leave the variable alone
if (rc != 0) npass++;
else `checkd(p.a, 8'd5);
rc = s.randomize();
if (rc != 0) npass++;
rc = ph.randomize();
if (rc != 0) npass++;
ar.q[0] = 8'd7;
rc = ar.randomize();
if (rc != 0) npass++;
else `checkd(ar.q[0], 8'd7);
rc = un.randomize();
`checkd(rc, 0); // zero-ok: constraints are unsatisfiable
end
$write("NPASS=%0d\n", npass);
$write("*-* All Finished *-*\n");
$finish;
end
endmodule