1152 lines
42 KiB
C++
1152 lines
42 KiB
C++
// -*- mode: C++; c-file-style: "cc-mode" -*-
|
|
//*************************************************************************
|
|
//
|
|
// Code available from: https://verilator.org
|
|
//
|
|
// 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: 2001-2026 Wilson Snyder
|
|
// SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
|
|
//
|
|
//=========================================================================
|
|
///
|
|
/// \file
|
|
/// \brief Verilated randomization implementation code
|
|
///
|
|
/// This file must be compiled and linked against all Verilated objects
|
|
/// that use randomization features.
|
|
///
|
|
/// See the internals documentation docs/internals.rst for details.
|
|
///
|
|
//=========================================================================
|
|
|
|
#include "verilated_random.h"
|
|
|
|
#include <cassert>
|
|
#include <fstream>
|
|
#include <iomanip>
|
|
#include <iostream>
|
|
#include <sstream>
|
|
#include <streambuf>
|
|
|
|
// 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).
|
|
// If UNSAT, (get-unsat-assumptions) names the literals clashing with the
|
|
// feasible hard+soft base; drop one per round and recheck until SAT, which
|
|
// keeps the maximal set of bits compatible with the constraints. Only these
|
|
// private literals are assumed (never user constraints), and assumptions are
|
|
// ephemeral, so hard/soft/randc semantics are untouched and rounds need no
|
|
// push/pop or re-asserting. The surviving assumptions steer each free bit
|
|
// from the random target, spreading a wide range uniformly (fixing the
|
|
// boundary bias under `value < (1<<N)`, issue #7563) while keeping run-to-run
|
|
// diversity on tightly coupled bits. Array/queue rand vars skip pinning
|
|
// (per-element ranges aren't power-of-2 boundaries) and use the XOR rounds.
|
|
#define _VL_SOLVER_HASH_LEN 1
|
|
#define _VL_SOLVER_HASH_LEN_TOTAL 4
|
|
|
|
// clang-format off
|
|
#if defined(__unix__) || defined(__unix) || (defined(__APPLE__) && defined(__MACH__))
|
|
# define _VL_SOLVER_PIPE // Allow pipe SMT solving. Needs fork()
|
|
#endif
|
|
|
|
#ifdef _VL_SOLVER_PIPE
|
|
# include <sys/wait.h>
|
|
# include <fcntl.h>
|
|
#endif
|
|
|
|
#if defined(_WIN32) || defined(__MINGW32__)
|
|
# include <io.h> // open, read, write, close
|
|
#endif
|
|
// clang-format on
|
|
|
|
class VlRProcess final : private std::streambuf, public std::iostream {
|
|
static constexpr int BUFFER_SIZE = 4096;
|
|
const char* const* m_cmd = nullptr; // fork() process argv
|
|
#ifdef _VL_SOLVER_PIPE
|
|
pid_t m_pid = 0; // fork() process id
|
|
#else
|
|
int m_pid = 0; // fork() process id - always zero as disabled
|
|
#endif
|
|
bool m_pidExited = true; // If subprocess has exited and can be opened
|
|
int m_pidStatus = 0; // fork() process exit status, valid if m_pidExited
|
|
int m_writeFd = -1; // File descriptor TO subprocess
|
|
int m_readFd = -1; // File descriptor FROM subprocess
|
|
char m_readBuf[BUFFER_SIZE];
|
|
char m_writeBuf[BUFFER_SIZE];
|
|
|
|
std::unique_ptr<std::ofstream> m_logfp; // Log file stream
|
|
uint64_t m_logLastTime = ~0ULL; // Last timestamp for logfile
|
|
|
|
public:
|
|
typedef std::streambuf::traits_type traits_type;
|
|
|
|
protected:
|
|
int overflow(int c = traits_type::eof()) override {
|
|
const char c2 = static_cast<char>(c);
|
|
if (pbase() == pptr()) return 0;
|
|
const size_t size = pptr() - pbase();
|
|
log(" ", std::string(pbase(), size));
|
|
const ssize_t n = ::write(m_writeFd, pbase(), size);
|
|
if (VL_UNLIKELY(n == -1)) perror("write");
|
|
if (n <= 0) {
|
|
wait_report();
|
|
return traits_type::eof();
|
|
}
|
|
if (n == size)
|
|
setp(m_writeBuf, m_writeBuf + sizeof(m_writeBuf));
|
|
else
|
|
setp(m_writeBuf + n, m_writeBuf + sizeof(m_writeBuf));
|
|
if (c != traits_type::eof()) sputc(c2);
|
|
return 0;
|
|
}
|
|
int underflow() override {
|
|
sync();
|
|
const ssize_t n = ::read(m_readFd, m_readBuf, sizeof(m_readBuf));
|
|
if (VL_UNLIKELY(n == -1)) perror("read");
|
|
if (n <= 0) {
|
|
wait_report();
|
|
return traits_type::eof();
|
|
}
|
|
log("< ", std::string(m_readBuf, n));
|
|
setg(m_readBuf, m_readBuf, m_readBuf + n);
|
|
return traits_type::to_int_type(m_readBuf[0]);
|
|
}
|
|
int sync() override {
|
|
overflow();
|
|
return 0;
|
|
}
|
|
|
|
public:
|
|
explicit VlRProcess(const char* const* const cmd = nullptr)
|
|
: std::streambuf{}
|
|
, std::iostream{this}
|
|
, m_cmd{cmd} {
|
|
logOpen();
|
|
open(cmd);
|
|
}
|
|
|
|
void wait_report() {
|
|
if (m_pidExited) return;
|
|
#ifdef _VL_SOLVER_PIPE
|
|
if (waitpid(m_pid, &m_pidStatus, 0) != m_pid) return;
|
|
if (m_pidStatus) {
|
|
std::stringstream msg;
|
|
msg << "Subprocess command `" << m_cmd[0];
|
|
for (const char* const* arg = m_cmd + 1; *arg; ++arg) msg << ' ' << *arg;
|
|
msg << "' failed: ";
|
|
if (WIFSIGNALED(m_pidStatus))
|
|
msg << strsignal(WTERMSIG(m_pidStatus))
|
|
<< (WCOREDUMP(m_pidStatus) ? " (core dumped)" : "");
|
|
else if (WIFEXITED(m_pidStatus))
|
|
msg << "exit status " << WEXITSTATUS(m_pidStatus);
|
|
const std::string str = msg.str();
|
|
VL_WARN_MT("", 0, "VlRProcess", str.c_str());
|
|
}
|
|
#endif
|
|
m_pidExited = true;
|
|
m_pid = 0;
|
|
closeFds();
|
|
}
|
|
|
|
void closeFds() {
|
|
if (m_writeFd != -1) {
|
|
close(m_writeFd);
|
|
m_writeFd = -1;
|
|
}
|
|
if (m_readFd != -1) {
|
|
close(m_readFd);
|
|
m_readFd = -1;
|
|
}
|
|
}
|
|
|
|
bool open(const char* const* const cmd) {
|
|
setp(std::begin(m_writeBuf), std::end(m_writeBuf));
|
|
setg(m_readBuf, m_readBuf, m_readBuf);
|
|
#ifdef _VL_SOLVER_PIPE
|
|
if (!cmd || !cmd[0]) return false;
|
|
m_cmd = cmd;
|
|
int fd_stdin[2]; // Can't use std::array
|
|
int fd_stdout[2]; // Can't use std::array
|
|
constexpr int P_RD = 0;
|
|
constexpr int P_WR = 1;
|
|
|
|
if (VL_UNLIKELY(pipe(fd_stdin) != 0)) {
|
|
perror("VlRProcess::open: pipe");
|
|
return false;
|
|
}
|
|
if (VL_UNLIKELY(pipe(fd_stdout) != 0)) {
|
|
perror("VlRProcess::open: pipe");
|
|
close(fd_stdin[P_RD]);
|
|
close(fd_stdin[P_WR]);
|
|
return false;
|
|
}
|
|
|
|
if (fd_stdin[P_RD] <= 2 || fd_stdin[P_WR] <= 2 || fd_stdout[P_RD] <= 2
|
|
|| fd_stdout[P_WR] <= 2) {
|
|
// We'd have to rearrange all of the FD usages in this case.
|
|
// Too unlikely; verilator isn't a daemon.
|
|
fprintf(stderr, "stdin/stdout closed before pipe opened\n");
|
|
close(fd_stdin[P_RD]);
|
|
close(fd_stdin[P_WR]);
|
|
close(fd_stdout[P_RD]);
|
|
close(fd_stdout[P_WR]);
|
|
return false;
|
|
}
|
|
|
|
log("", "# Open: "s + cmd[0]);
|
|
const pid_t pid = fork();
|
|
if (VL_UNLIKELY(pid < 0)) {
|
|
perror("VlRProcess::open: fork");
|
|
close(fd_stdin[P_RD]);
|
|
close(fd_stdin[P_WR]);
|
|
close(fd_stdout[P_RD]);
|
|
close(fd_stdout[P_WR]);
|
|
return false;
|
|
}
|
|
if (pid == 0) {
|
|
// Child
|
|
close(fd_stdin[P_WR]);
|
|
dup2(fd_stdin[P_RD], STDIN_FILENO);
|
|
close(fd_stdout[P_RD]);
|
|
dup2(fd_stdout[P_WR], STDOUT_FILENO);
|
|
execvp(cmd[0], const_cast<char* const*>(cmd));
|
|
std::stringstream msg;
|
|
msg << "VlRProcess::open: execvp(" << cmd[0] << ")";
|
|
const std::string str = msg.str();
|
|
perror(str.c_str());
|
|
_exit(127);
|
|
}
|
|
// Parent
|
|
m_pid = pid;
|
|
m_pidExited = false;
|
|
m_pidStatus = 0;
|
|
m_readFd = fd_stdout[P_RD];
|
|
m_writeFd = fd_stdin[P_WR];
|
|
|
|
close(fd_stdin[P_RD]);
|
|
close(fd_stdout[P_WR]);
|
|
|
|
return true;
|
|
#else
|
|
return false;
|
|
#endif
|
|
}
|
|
|
|
private:
|
|
void logOpen() {
|
|
const std::string filename = Verilated::threadContextp()->solverLogFilename();
|
|
if (filename.empty()) return;
|
|
m_logfp = std::make_unique<std::ofstream>(filename);
|
|
if (m_logfp.get() && m_logfp.get()->fail()) m_logfp = nullptr;
|
|
if (!m_logfp) {
|
|
const std::string msg = "%Error: Can't write '"s + filename + "'";
|
|
VL_FATAL_MT("", 0, "", msg.c_str());
|
|
return;
|
|
}
|
|
*m_logfp << "# Verilator solver log\n";
|
|
}
|
|
void log(const std::string& prefix, const std::string& text) {
|
|
if (VL_LIKELY(!m_logfp.get()) || text.empty()) return;
|
|
if (m_logLastTime != Verilated::threadContextp()->time()) {
|
|
m_logLastTime = Verilated::threadContextp()->time();
|
|
*m_logfp << "# [" << Verilated::threadContextp()->timeWithUnitString() << "]\n";
|
|
}
|
|
std::size_t startPos = 0;
|
|
while (1) {
|
|
const std::size_t endPos = text.find('\n', startPos);
|
|
if (endPos == std::string::npos) break;
|
|
*m_logfp << prefix << text.substr(startPos, endPos - startPos) << '\n';
|
|
startPos = endPos + 1;
|
|
}
|
|
if (startPos < text.length()) *m_logfp << prefix << text.substr(startPos) << '\n';
|
|
}
|
|
};
|
|
|
|
static VlRProcess& getSolver() {
|
|
static VlRProcess s_solver;
|
|
static bool s_done = false;
|
|
if (s_done) return s_solver;
|
|
s_done = true;
|
|
|
|
static std::vector<const char*> s_argv;
|
|
static std::string s_program = Verilated::threadContextp()->solverProgram();
|
|
s_argv.emplace_back(&s_program[0]);
|
|
for (char* arg = &s_program[0]; *arg; ++arg) {
|
|
if (*arg == ' ') {
|
|
*arg = '\0';
|
|
s_argv.emplace_back(arg + 1);
|
|
}
|
|
}
|
|
s_argv.emplace_back(nullptr);
|
|
|
|
const char* const* const cmd = &s_argv[0];
|
|
s_solver.open(cmd);
|
|
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;
|
|
|
|
std::stringstream msg;
|
|
msg << "Unable to communicate with SAT solver, please check its installation or specify a "
|
|
"different one in VERILATOR_SOLVER environment variable.\n";
|
|
msg << " ... Tried: $";
|
|
for (const char* const* arg = cmd; *arg; ++arg) msg << ' ' << *arg;
|
|
msg << '\n';
|
|
const std::string str = msg.str();
|
|
VL_WARN_MT("", 0, "randomize", str.c_str());
|
|
|
|
while (getline(s_solver, s)) {}
|
|
return s_solver;
|
|
}
|
|
|
|
static std::string readUntilBalanced(std::istream& stream) {
|
|
std::string result;
|
|
std::string token;
|
|
int parenCount = 1;
|
|
while (stream >> token) {
|
|
for (const char c : token) {
|
|
if (c == '(') {
|
|
++parenCount;
|
|
} else if (c == ')') {
|
|
--parenCount;
|
|
}
|
|
}
|
|
result += token + " ";
|
|
if (parenCount == 0) break;
|
|
}
|
|
return result;
|
|
}
|
|
|
|
static std::string parseNestedSelect(const std::string& nested_select_expr,
|
|
std::vector<std::string>& indices) {
|
|
std::istringstream nestedStream(nested_select_expr);
|
|
std::string name;
|
|
std::string idx;
|
|
nestedStream >> name;
|
|
if (name == "(select") {
|
|
const std::string further_nested_expr = readUntilBalanced(nestedStream);
|
|
name = parseNestedSelect(further_nested_expr, indices);
|
|
}
|
|
std::getline(nestedStream, idx, ')');
|
|
indices.push_back(idx);
|
|
return name;
|
|
}
|
|
|
|
//======================================================================
|
|
// VlRandomizer:: Methods
|
|
|
|
void VlRandomVar::emitGetValue(std::ostream& s) const { s << ' ' << m_name; }
|
|
void VlRandomVar::emitExtract(std::ostream& s, int i) const {
|
|
s << " ((_ extract " << i << ' ' << i << ") " << m_name << ')';
|
|
}
|
|
void VlRandomVar::emitType(std::ostream& s) const { s << "(_ BitVec " << width() << ')'; }
|
|
// Serialize the current runtime value as an SMT-LIB binary literal. Used by
|
|
// randomize(null) to pin a var via `(assert (= var #b...))`. Binary (#b)
|
|
// rather than hex (#x) sidesteps SMT-LIB's hex-width-multiple-of-4 rule.
|
|
void VlRandomVar::emitConcreteValue(std::ostream& s) const {
|
|
const int w = width();
|
|
const void* const dp = datap(0);
|
|
s << "#b";
|
|
for (int i = w - 1; i >= 0; --i) {
|
|
int bit = 0;
|
|
if (w <= VL_BYTESIZE) {
|
|
bit = (*static_cast<const CData*>(dp) >> i) & 1;
|
|
} else if (w <= VL_SHORTSIZE) {
|
|
bit = (*static_cast<const SData*>(dp) >> i) & 1;
|
|
} else if (w <= VL_IDATASIZE) {
|
|
bit = (*static_cast<const IData*>(dp) >> i) & 1;
|
|
} else if (w <= VL_QUADSIZE) {
|
|
bit = (*static_cast<const QData*>(dp) >> i) & 1;
|
|
} else {
|
|
const WDataInP wp = WDataInP::external(static_cast<const EData*>(dp));
|
|
bit = (wp[VL_BITWORD_E(i)] >> VL_BITBIT_E(i)) & 1;
|
|
}
|
|
s << (bit ? '1' : '0');
|
|
}
|
|
}
|
|
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;
|
|
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 '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;
|
|
}
|
|
return true;
|
|
}
|
|
bool 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;
|
|
const int nidx = qiwp[0];
|
|
if (obits > VL_QUADSIZE) owp = WDataOutP::external(reinterpret_cast<EData*>(datap(nidx)));
|
|
if (!parseSMTNum(obits, owp, val)) return false;
|
|
|
|
if (obits <= VL_BYTESIZE) {
|
|
CData* const p = static_cast<CData*>(datap(nidx));
|
|
*p = VL_CLEAN_II(obits, obits, owp[0]);
|
|
} else if (obits <= VL_SHORTSIZE) {
|
|
SData* const p = static_cast<SData*>(datap(nidx));
|
|
*p = VL_CLEAN_II(obits, obits, owp[0]);
|
|
} else if (obits <= VL_IDATASIZE) {
|
|
IData* const p = static_cast<IData*>(datap(nidx));
|
|
*p = VL_CLEAN_II(obits, obits, owp[0]);
|
|
} else if (obits <= VL_QUADSIZE) {
|
|
QData* const p = static_cast<QData*>(datap(nidx));
|
|
*p = VL_CLEAN_QQ(obits, obits, VL_SET_QW(owp));
|
|
} else {
|
|
_vl_clean_inplace_w(obits, owp);
|
|
}
|
|
return true;
|
|
}
|
|
|
|
void VlRandomizer::randomConstraint(std::ostream& os, VlRNG& rngr, int bits) {
|
|
const IData hash = VL_RANDOM_RNG_I(rngr) & ((1 << bits) - 1);
|
|
int varBits = 0;
|
|
for (const auto& var : m_vars) varBits += var.second->totalWidth();
|
|
os << "(= #b";
|
|
for (int i = bits - 1; i >= 0; i--) os << (VL_BITISSET_I(hash, i) ? '1' : '0');
|
|
if (bits > 1) os << " (concat";
|
|
for (int i = 0; i < bits; ++i) {
|
|
IData varBitsLeft = varBits;
|
|
IData varBitsWant = (varBits + 1) / 2;
|
|
if (varBits > 2) os << " (bvxor";
|
|
for (const auto& var : m_vars) {
|
|
for (int j = 0; j < var.second->totalWidth(); j++, varBitsLeft--) {
|
|
const bool doEmit = (VL_RANDOM_RNG_I(rngr) % varBitsLeft) < varBitsWant;
|
|
if (doEmit) {
|
|
var.second->emitExtract(os, j);
|
|
if (--varBitsWant == 0) break;
|
|
}
|
|
}
|
|
if (varBitsWant == 0) break;
|
|
}
|
|
if (varBits > 2) os << ')';
|
|
}
|
|
if (bits > 1) os << ')';
|
|
os << ')';
|
|
}
|
|
|
|
size_t VlRandomizer::hashConstraints(const std::vector<std::string>& extras) const {
|
|
size_t h = 0;
|
|
for (const auto& c : m_constraints) {
|
|
h ^= std::hash<std::string>{}(c) + 0x9e3779b9 + (h << 6) + (h >> 2);
|
|
}
|
|
for (const auto& c : extras) {
|
|
h ^= std::hash<std::string>{}(c) + 0x9e3779b9 + (h << 6) + (h >> 2);
|
|
}
|
|
return h;
|
|
}
|
|
|
|
void VlRandomizer::emitRandcExclusions(std::ostream& os) const {
|
|
for (const auto& name : m_randcVarNames) {
|
|
const auto usedIt = m_randcUsedValues.find(name);
|
|
if (usedIt != m_randcUsedValues.end()) {
|
|
const int w = m_vars.at(name)->width();
|
|
for (const uint64_t val : usedIt->second) {
|
|
os << "(assert (not (= " << name << " (_ bv" << val << " " << w << "))))\n";
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
static uint64_t readVarValueU64(const void* datap, int width) {
|
|
if (width <= VL_BYTESIZE) return *static_cast<const CData*>(datap);
|
|
if (width <= VL_SHORTSIZE) return *static_cast<const SData*>(datap);
|
|
if (width <= VL_IDATASIZE) return *static_cast<const IData*>(datap);
|
|
if (width <= VL_QUADSIZE) return *static_cast<const QData*>(datap);
|
|
return 0;
|
|
}
|
|
|
|
void VlRandomizer::recordRandcValues() {
|
|
for (const auto& name : m_randcVarNames) {
|
|
const auto varIt = m_vars.find(name);
|
|
if (varIt == m_vars.end()) continue;
|
|
const VlRandomVar& var = *varIt->second;
|
|
m_randcUsedValues[name].insert(readVarValueU64(var.datap(0), var.width()));
|
|
}
|
|
}
|
|
|
|
bool VlRandomizer::next_check_only(VlRNG& rngr) { return nextRandomize(rngr, true); }
|
|
|
|
bool VlRandomizer::next(VlRNG& rngr) { return nextRandomize(rngr, false); }
|
|
|
|
bool VlRandomizer::nextRandomize(VlRNG& rngr, bool checkOnly) {
|
|
if (!checkOnly && m_vars.empty() && m_unique_arrays.empty()) return true;
|
|
if (checkOnly && m_vars.empty()) return true; // No rand members: trivially SAT
|
|
m_checkOnly = checkOnly;
|
|
const std::vector<std::string> uniqueExprs = buildUniqueExprs();
|
|
|
|
// Randc exclusion-based cycling: exclude previously used values per randc var.
|
|
// When solver returns unsat (all values exhausted), clear history for new cycle.
|
|
if (!m_randcVarNames.empty()) {
|
|
const size_t currentHash = hashConstraints(uniqueExprs);
|
|
// Invalidate history if constraints changed (e.g., constraint_mode toggled)
|
|
if (currentHash != m_randcConstraintHash) {
|
|
m_randcUsedValues.clear();
|
|
m_randcConstraintHash = currentHash;
|
|
}
|
|
}
|
|
|
|
// Pinned vars make phase ordering moot; skip phased path in check-only.
|
|
bool result;
|
|
if (!m_checkOnly && !m_solveBefore.empty()) {
|
|
result = nextPhased(rngr, uniqueExprs);
|
|
} else {
|
|
result = nextFlat(rngr, uniqueExprs);
|
|
}
|
|
m_checkOnly = false;
|
|
return result;
|
|
}
|
|
|
|
std::vector<std::string> VlRandomizer::buildUniqueExprs() const {
|
|
std::vector<std::string> exprs;
|
|
if (m_unique_arrays.empty()) return exprs;
|
|
const auto arrVarsp = std::make_shared<const ArrayInfoMap>(m_arr_vars);
|
|
for (const std::string& baseName : m_unique_arrays) {
|
|
const auto it = m_vars.find(baseName);
|
|
if (it == m_vars.end()) continue;
|
|
const VlRandomVar& var = *it->second;
|
|
// Select the elements the array actually holds now, by their own index
|
|
// or key, rather than by ordinal position
|
|
var.setArrayInfo(arrVarsp);
|
|
// 'distinct' needs at least two operands; fewer elements are trivially unique
|
|
if (var.countMatchingElements(*arrVarsp, baseName) < 2) continue;
|
|
std::ostringstream os;
|
|
os << "(__Vbv (distinct ";
|
|
var.emitGetValue(os);
|
|
os << "))";
|
|
exprs.push_back(os.str());
|
|
}
|
|
return exprs;
|
|
}
|
|
|
|
void VlRandomizer::emitDefines(std::ostream& os) const {
|
|
os << "(define-fun __Vbv ((b Bool)) (_ BitVec 1) (ite b #b1 #b0))\n";
|
|
os << "(define-fun __Vbool ((v (_ BitVec 1))) Bool (= #b1 v))\n";
|
|
}
|
|
|
|
void VlRandomizer::emitDeclares(std::ostream& os, bool pinCurrent) const {
|
|
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";
|
|
// Pin each var to its current value
|
|
if (pinCurrent) {
|
|
assert(var.second->dimension() == 0);
|
|
os << "(assert (= " << var.first << ' ';
|
|
var.second->emitConcreteValue(os);
|
|
os << "))\n";
|
|
}
|
|
}
|
|
}
|
|
|
|
void VlRandomizer::emitAsserts(std::ostream& os, const std::vector<std::string>& extras,
|
|
bool named) const {
|
|
int j = 0;
|
|
for (const std::string& constraint : m_constraints) {
|
|
if (named) {
|
|
os << "(assert (! (= #b1 " << constraint << ") :named cons" << j++ << "))\n";
|
|
} else {
|
|
os << "(assert (= #b1 " << constraint << "))\n";
|
|
}
|
|
}
|
|
for (const std::string& extra : extras) {
|
|
if (named) {
|
|
os << "(assert (! (= #b1 " << extra << ") :named cons" << j++ << "))\n";
|
|
} else {
|
|
os << "(assert (= #b1 " << extra << "))\n";
|
|
}
|
|
}
|
|
}
|
|
|
|
bool VlRandomizer::nextFlat(VlRNG& rngr, const std::vector<std::string>& uniqueExprs) {
|
|
// Randc retry: if unsat due to randc exhaustion, clear history and retry once
|
|
const bool hasRandc = !m_randcVarNames.empty();
|
|
for (int attempt = 0; attempt < (hasRandc ? 2 : 1); ++attempt) {
|
|
std::iostream& os = getSolver();
|
|
if (!os) return false;
|
|
|
|
os << "(set-option :produce-models true)\n";
|
|
// Lets the scalar pin path learn which free-bit assumptions conflict.
|
|
os << "(set-option :produce-unsat-assumptions true)\n";
|
|
os << "(set-logic QF_ABV)\n";
|
|
emitDefines(os);
|
|
emitDeclares(os, m_checkOnly);
|
|
emitAsserts(os, uniqueExprs, false);
|
|
|
|
// randc exclusions vs. a pinned current value would make every check
|
|
// trivially UNSAT after the first cycle.
|
|
if (!m_checkOnly) emitRandcExclusions(os);
|
|
|
|
relaxSoftConstraints(os);
|
|
os << "(check-sat)\n";
|
|
const bool sat = parseSolution(os);
|
|
|
|
if (!sat) {
|
|
os << "(reset)\n";
|
|
// 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.
|
|
if (m_checkOnly) return false;
|
|
// Genuine unsat: report via unsat-core
|
|
reportUnsatSetup(os, uniqueExprs);
|
|
os << "(reset)\n";
|
|
return false;
|
|
}
|
|
|
|
if (!m_checkOnly) {
|
|
solveDiversity(rngr, os);
|
|
// Check-only must not advance randc cycle state.
|
|
recordRandcValues();
|
|
}
|
|
|
|
os << "(reset)\n";
|
|
return true;
|
|
}
|
|
return false; // Should not reach here
|
|
}
|
|
|
|
void VlRandomizer::solveDiversity(VlRNG& rngr, std::iostream& os) {
|
|
bool hasArray = false;
|
|
for (const auto& var : m_vars) {
|
|
if (var.second->dimension() > 0) {
|
|
hasArray = true;
|
|
break;
|
|
}
|
|
}
|
|
if (hasArray) {
|
|
solveDiversityXor(rngr, os);
|
|
} else {
|
|
solveDiversityPins(rngr, os);
|
|
}
|
|
}
|
|
|
|
void VlRandomizer::solveDiversityPins(VlRNG& rngr, std::iostream& os) {
|
|
// Tie each free bit to a random target via an assumption literal;
|
|
// drop one conflicting literal per round until compatible
|
|
int npins = 0;
|
|
for (const auto& var : m_vars) {
|
|
const int w = var.second->totalWidth();
|
|
for (int b = 0; b < w; ++b) {
|
|
const bool target = (VL_RANDOM_RNG_I(rngr) & 1);
|
|
os << "(declare-fun a" << npins << " () Bool)\n";
|
|
os << "(assert (= a" << npins << " (=";
|
|
var.second->emitExtract(os, b);
|
|
os << " #b" << (target ? '1' : '0') << ")))\n";
|
|
++npins;
|
|
}
|
|
}
|
|
std::vector<bool> dropped(npins, false);
|
|
for (int round = 0; round <= npins; ++round) {
|
|
os << "(check-sat-assuming (";
|
|
for (int k = 0; k < npins; ++k) {
|
|
if (!dropped[k]) os << " a" << k;
|
|
}
|
|
os << "))\n";
|
|
if (parseSolution(os)) 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);
|
|
for (const int idx : core) {
|
|
if (idx < npins) {
|
|
dropped[idx] = true;
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
void VlRandomizer::solveDiversityXor(VlRNG& rngr, std::iostream& os) {
|
|
bool sat = true;
|
|
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);
|
|
}
|
|
}
|
|
|
|
bool VlRandomizer::checkSat(std::iostream& os) {
|
|
std::string result;
|
|
do { std::getline(os, result); } while (result.empty());
|
|
return result == "sat";
|
|
}
|
|
|
|
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;
|
|
os << "(push 1)\n";
|
|
for (const auto& s : m_softConstraints) os << "(assert (= #b1 " << s << "))\n";
|
|
os << "(check-sat)\n";
|
|
if (checkSat(os)) 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";
|
|
}
|
|
}
|
|
|
|
// 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 : reply) {
|
|
if (std::isdigit(static_cast<unsigned char>(c))) {
|
|
num += c;
|
|
} else if (!num.empty()) {
|
|
idxs.push_back(std::stoi(num));
|
|
num.clear();
|
|
}
|
|
}
|
|
if (!num.empty()) idxs.push_back(std::stoi(num));
|
|
return idxs;
|
|
}
|
|
|
|
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,
|
|
const std::vector<std::string>& uniqueExprs) {
|
|
os << "(set-option :produce-unsat-cores true)\n";
|
|
os << "(set-logic QF_ABV)\n";
|
|
emitDefines(os);
|
|
emitDeclares(os, false);
|
|
emitAsserts(os, uniqueExprs, true);
|
|
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") 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;
|
|
}
|
|
|
|
os << "(get-value (";
|
|
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);
|
|
}
|
|
var.second->emitGetValue(os);
|
|
}
|
|
os << "))\n";
|
|
// Quasi-parse S-expression of the form ((x #xVALUE) (y #bVALUE) (z #xVALUE))
|
|
char c;
|
|
os >> c;
|
|
if (c != '(') {
|
|
VL_WARN_MT(__FILE__, __LINE__, "randomize",
|
|
"Internal: Unable to parse solver's response: invalid S-expression");
|
|
return false;
|
|
}
|
|
while (true) {
|
|
os >> c;
|
|
if (c == ')') break;
|
|
if (c != '(') {
|
|
VL_WARN_MT(__FILE__, __LINE__, "randomize",
|
|
"Internal: Unable to parse solver's response: invalid S-expression");
|
|
return false;
|
|
}
|
|
std::string name;
|
|
std::string idx;
|
|
std::string value;
|
|
std::vector<std::string> indices;
|
|
os >> name;
|
|
indices.clear();
|
|
if (name == "(select") {
|
|
const std::string selectExpr = readUntilBalanced(os);
|
|
name = parseNestedSelect(selectExpr, indices);
|
|
}
|
|
std::getline(os, value, ')');
|
|
const auto it = m_vars.find(name);
|
|
if (it == m_vars.end()) continue;
|
|
const VlRandomVar& varr = *it->second;
|
|
if (!varr.randModeIdxNone()) {
|
|
// Static rand vars have their rand_mode in a class-package shared queue,
|
|
// not the per-instance one.
|
|
const VlQueue<CData>* const modep
|
|
= m_staticVars.count(name) ? m_static_randmodep : m_randmodep;
|
|
if (modep && !modep->at(varr.randModeIdx())) continue;
|
|
}
|
|
if (m_disabledVars.count(name)) continue;
|
|
if (!indices.empty()) {
|
|
std::ostringstream oss;
|
|
oss << varr.name();
|
|
for (const auto& hex_index : indices) {
|
|
const size_t start = hex_index.find_first_not_of(" ");
|
|
if (start == std::string::npos || hex_index.substr(start, 2) != "#x") {
|
|
VL_FATAL_MT(__FILE__, __LINE__, "randomize",
|
|
"hex_index contains invalid format");
|
|
continue;
|
|
}
|
|
std::string trimmed_hex = hex_index.substr(start + 2);
|
|
|
|
if (trimmed_hex.size() <= 8) { // Small numbers: <= 32 bits
|
|
// Convert to decimal and output directly
|
|
oss << "[" << std::to_string(std::stoll(trimmed_hex, nullptr, 16)) << "]";
|
|
} else { // Large numbers: > 32 bits
|
|
// Trim leading zeros and handle empty case
|
|
trimmed_hex.erase(0, trimmed_hex.find_first_not_of('0'));
|
|
oss << "[" << (trimmed_hex.empty() ? "0" : trimmed_hex) << "]";
|
|
}
|
|
}
|
|
const std::string indexed_name = oss.str();
|
|
|
|
const auto iti = std::find_if(m_arr_vars.begin(), m_arr_vars.end(),
|
|
[&indexed_name](const auto& entry) {
|
|
return entry.second->m_name == indexed_name;
|
|
});
|
|
if (iti != m_arr_vars.end()) {
|
|
std::ostringstream ss;
|
|
ss << "#x" << std::hex << std::setw(8) << std::setfill('0')
|
|
<< iti->second->m_index;
|
|
idx = ss.str();
|
|
} else {
|
|
VL_FATAL_MT(__FILE__, __LINE__, "randomize",
|
|
"indexed_name not found in m_arr_vars");
|
|
}
|
|
}
|
|
varr.set(idx, value);
|
|
}
|
|
return true;
|
|
}
|
|
|
|
void VlRandomizer::hard(std::string&& constraint, const char* filename, uint32_t linenum,
|
|
const char* source) {
|
|
m_constraints.emplace_back(std::move(constraint));
|
|
// Format constraint location: "filename:linenum source"
|
|
if (filename[0] != '\0' || source[0] != '\0') {
|
|
std::string line;
|
|
if (filename[0] != '\0') {
|
|
line = std::string(filename) + ":" + std::to_string(linenum);
|
|
if (source[0] != '\0') line += " " + std::string(source);
|
|
} else {
|
|
line = source;
|
|
}
|
|
m_constraints_line.emplace_back(std::move(line));
|
|
}
|
|
}
|
|
|
|
void VlRandomizer::soft(std::string&& constraint, const char* /*filename*/, uint32_t /*linenum*/,
|
|
const char* /*source*/) {
|
|
m_softConstraints.emplace_back(std::move(constraint));
|
|
}
|
|
|
|
void VlRandomizer::disable_soft(const std::string& varName) {
|
|
// IEEE 1800-2023 18.5.13: Remove all soft constraints referencing the variable
|
|
m_softConstraints.erase(
|
|
std::remove_if(m_softConstraints.begin(), m_softConstraints.end(),
|
|
[&](const std::string& c) { return c.find(varName) != std::string::npos; }),
|
|
m_softConstraints.end());
|
|
}
|
|
|
|
void VlRandomizer::clearConstraints() {
|
|
m_constraints.clear();
|
|
m_constraints_line.clear();
|
|
m_solveBefore.clear();
|
|
m_softConstraints.clear();
|
|
m_unique_arrays.clear(); // Re-registered by constraint setup
|
|
// Keep m_vars for class member randomization
|
|
}
|
|
|
|
void VlRandomizer::clearAll() {
|
|
m_constraints.clear();
|
|
m_softConstraints.clear();
|
|
m_vars.clear();
|
|
m_randcVarNames.clear();
|
|
m_randcUsedValues.clear();
|
|
m_randcConstraintHash = 0;
|
|
}
|
|
|
|
void VlRandomizer::markRandc(const char* name) { m_randcVarNames.insert(name); }
|
|
|
|
void VlRandomizer::solveBefore(const std::string& beforeName, const std::string& afterName) {
|
|
m_solveBefore.emplace_back(beforeName, afterName);
|
|
}
|
|
|
|
bool VlRandomizer::buildSolveLayers(std::vector<std::vector<std::string>>& layersr) {
|
|
std::map<std::string, std::set<std::string>> graph;
|
|
std::map<std::string, int> inDegree;
|
|
std::set<std::string> 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;
|
|
}
|
|
|
|
// "solve x before y": edge x -> y, in-degree of y increases
|
|
for (const auto& entry : graph) {
|
|
for (const auto& to : entry.second) { inDegree[to]++; }
|
|
}
|
|
|
|
std::set<std::string> remaining = solveBeforeVars;
|
|
while (!remaining.empty()) {
|
|
std::vector<std::string> 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]--; }
|
|
}
|
|
}
|
|
layersr.push_back(std::move(currentLayer));
|
|
}
|
|
return true;
|
|
}
|
|
|
|
const char* VlRandomizer::phasedLogic() const {
|
|
for (const auto& var : m_vars) {
|
|
if (var.second->dimension() == 0) continue;
|
|
if (!var.second->hasMatchingElements(m_arr_vars, var.second->name())) return "ALL";
|
|
}
|
|
return "QF_ABV";
|
|
}
|
|
|
|
bool VlRandomizer::nextPhased(VlRNG& rngr, const std::vector<std::string>& uniqueExprs) {
|
|
// Solve layer by layer with ALL constraints, pinning earlier layers
|
|
std::vector<std::vector<std::string>> layers;
|
|
if (!buildSolveLayers(layers)) return false;
|
|
|
|
// One layer: all solve_before vars are independent, no ordering required
|
|
if (layers.size() <= 1) return nextFlat(rngr, uniqueExprs);
|
|
|
|
return solvePhases(rngr, layers, uniqueExprs);
|
|
}
|
|
|
|
bool VlRandomizer::solvePhases(VlRNG& rngr, const std::vector<std::vector<std::string>>& layers,
|
|
const std::vector<std::string>& uniqueExprs) {
|
|
std::map<std::string, std::string> solvedValues; // varName -> SMT value literal
|
|
const char* const logicp = phasedLogic();
|
|
|
|
for (size_t phase = 0; phase < layers.size(); phase++) {
|
|
const bool isFinalPhase = (phase == layers.size() - 1);
|
|
|
|
std::iostream& os = getSolver();
|
|
if (!os) return false;
|
|
|
|
os << "(set-option :produce-models true)\n";
|
|
os << "(set-logic " << logicp << ")\n";
|
|
emitDefines(os);
|
|
emitDeclares(os, false);
|
|
|
|
for (const auto& entry : solvedValues) {
|
|
os << "(assert (= " << entry.first << " " << entry.second << "))\n";
|
|
}
|
|
emitAsserts(os, uniqueExprs, false);
|
|
|
|
// Randc: exclude previously used values
|
|
emitRandcExclusions(os);
|
|
|
|
// Soft constraints participate in every phase, priority-ordered.
|
|
relaxSoftConstraints(os);
|
|
|
|
// 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
|
|
const bool sat = parseSolution(os);
|
|
if (!sat) {
|
|
if (!m_randcVarNames.empty()) m_randcUsedValues.clear();
|
|
os << "(reset)\n";
|
|
return false;
|
|
}
|
|
// Record solved randc values for future exclusion
|
|
recordRandcValues();
|
|
solveDiversityXor(rngr, os);
|
|
os << "(reset)\n";
|
|
} else {
|
|
if (!checkSat(os)) {
|
|
os << "(reset)\n";
|
|
return false;
|
|
}
|
|
if (!solvePhaseValues(os, rngr, layers[phase], solvedValues)) {
|
|
os << "(reset)\n";
|
|
return false;
|
|
}
|
|
os << "(reset)\n";
|
|
}
|
|
}
|
|
|
|
return true;
|
|
}
|
|
|
|
// Intermediate phase: extract this layer's values, then try one diversity round
|
|
bool VlRandomizer::solvePhaseValues(std::iostream& os, VlRNG& rngr,
|
|
const std::vector<std::string>& layerVars,
|
|
std::map<std::string, std::string>& solvedValuesr) {
|
|
const auto emitGetValueCmd = [&]() {
|
|
os << "(get-value (";
|
|
for (const auto& varName : layerVars) {
|
|
const auto it = m_vars.find(varName);
|
|
if (it->second->dimension() > 0) {
|
|
auto arrVarsp = std::make_shared<const ArrayInfoMap>(m_arr_vars);
|
|
it->second->setArrayInfo(arrVarsp);
|
|
// Enumerable arrays: query each element for a QF_ABV-safe pin.
|
|
if (it->second->hasMatchingElements(m_arr_vars, it->second->name())) {
|
|
it->second->emitGetValue(os);
|
|
continue;
|
|
}
|
|
}
|
|
os << varName << " ";
|
|
}
|
|
os << "))\n";
|
|
};
|
|
// Get baseline values (deterministic, always valid)
|
|
emitGetValueCmd();
|
|
if (!parsePhaseValues(os, solvedValuesr)) 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";
|
|
if (checkSat(os)) {
|
|
emitGetValueCmd();
|
|
(void)parsePhaseValues(os, solvedValuesr);
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool VlRandomizer::parsePhaseValues(std::istream& is,
|
|
std::map<std::string, std::string>& solvedValuesr) {
|
|
// Parse ((name value) ...): one paren-depth counter drives every match.
|
|
char c = 0;
|
|
is >> c; // outer '('
|
|
if (c != '(') return false;
|
|
int depth = 1;
|
|
std::string tokens[2];
|
|
std::string cur;
|
|
int fields = 0;
|
|
const auto flush = [&]() {
|
|
if (cur.empty()) return;
|
|
if (fields < 2) tokens[fields] = cur;
|
|
++fields;
|
|
cur.clear();
|
|
};
|
|
while (depth > 0 && is.get(c)) {
|
|
if (c == '(') {
|
|
++depth;
|
|
if (depth >= 3) cur += c;
|
|
} else if (c == ')') {
|
|
--depth;
|
|
if (depth >= 2) {
|
|
cur += c;
|
|
} else if (depth == 1) {
|
|
flush();
|
|
if (fields == 2) solvedValuesr[tokens[0]] = tokens[1];
|
|
fields = 0;
|
|
}
|
|
} else if (c == ' ' || c == '\t' || c == '\n' || c == '\r') {
|
|
if (depth >= 3) {
|
|
cur += c;
|
|
} else {
|
|
flush();
|
|
}
|
|
} else {
|
|
cur += c;
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
|
|
#ifdef VL_DEBUG
|
|
void VlRandomizer::dump() const {
|
|
for (const auto& var : m_vars) {
|
|
VL_PRINTF("Variable (%d): %s\n", var.second->width(), var.second->name().c_str());
|
|
}
|
|
for (const std::string& c : m_constraints) VL_PRINTF("Constraint: %s\n", c.c_str());
|
|
}
|
|
#endif
|