diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index 59548dc0a..354eabd92 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -53,6 +53,7 @@ #ifdef _VL_SOLVER_PIPE # include +# include # include #endif @@ -76,6 +77,7 @@ class VlRProcess final : private std::streambuf, public std::iostream { char m_readBuf[BUFFER_SIZE]; char m_writeBuf[BUFFER_SIZE]; + bool m_logTried = false; // Log file name looked up, at the first start std::unique_ptr m_logfp; // Log file stream uint64_t m_logLastTime = ~0ULL; // Last timestamp for logfile @@ -123,14 +125,29 @@ public: : std::streambuf{} , std::iostream{this} , m_cmd{cmd} { - logOpen(); open(cmd); } + // Kill and reap a solver that is still running, so no child is left behind + void terminate() { +#ifdef _VL_SOLVER_PIPE + if (!m_pidExited) { + ::kill(m_pid, SIGKILL); + waitpid(m_pid, &m_pidStatus, 0); + } +#endif + m_pidExited = true; + m_pid = 0; + closeFds(); + } + void wait_report() { if (m_pidExited) return; + bool reaped = true; #ifdef _VL_SOLVER_PIPE - if (waitpid(m_pid, &m_pidStatus, WNOHANG) != m_pid) m_pidStatus = 0; + const pid_t rc = waitpid(m_pid, &m_pidStatus, WNOHANG); + if (rc != m_pid) m_pidStatus = 0; + reaped = rc != 0; // Zero means still running, so terminate() reaps it if (m_pidStatus) { std::stringstream msg; msg << "Subprocess command `" << m_cmd[0]; @@ -145,8 +162,10 @@ public: VL_WARN_MT("", 0, "VlRProcess", str.c_str()); } #endif - m_pidExited = true; - m_pid = 0; + if (reaped) { + m_pidExited = true; + m_pid = 0; + } closeFds(); } @@ -162,11 +181,16 @@ public: } bool open(const char* const* const cmd) { + clear(); 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; + if (!m_logTried) { + m_logTried = true; + logOpen(); + } int fd_stdin[2]; // Can't use std::array int fd_stdout[2]; // Can't use std::array constexpr int P_RD = 0; @@ -385,40 +409,133 @@ static bool readSExpr(std::istream& is, std::string& outr) { return false; } -static VlRProcess& getSolver() { - static VlRProcess s_solver; - static bool s_done = false; - if (s_done) return s_solver; - s_done = true; +//====================================================================== +// Solver session lifecycle - static std::vector 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); - } +// Owns the solver process; serializes transactions and replaces a solver that +// died or was left out of step with the reply stream +class VlSolverSession final { + friend class VlRandomizer; + friend class VlSolverTxn; + enum class State : uint8_t { UNSTARTED, LIVE, BROKEN, DISABLED }; + static constexpr int MAX_CONSEC_FAILS = 3; + + VerilatedMutex m_mutex; // Serializes whole solver transactions + VlRProcess m_proc VL_GUARDED_BY(m_mutex); // Solver subprocess and its pipes + State m_state VL_GUARDED_BY(m_mutex) = State::UNSTARTED; + int m_consecFails VL_GUARDED_BY(m_mutex) = 0; // Failed transactions in a row + bool m_dirty VL_GUARDED_BY(m_mutex) = false; // Transaction left the pipe out of step + std::string m_program VL_GUARDED_BY(m_mutex); // Storage backing m_argv + std::vector m_argv VL_GUARDED_BY(m_mutex); // Solver argv + bool m_warnedRestart VL_GUARDED_BY(m_mutex) = false; + +public: + std::iostream& os() VL_REQUIRES(m_mutex) { return m_proc; } + // The pipe may hold bytes of an abandoned reply, so replace the solver + void abandon() VL_REQUIRES(m_mutex) { m_dirty = true; } + + // A status the runtime cannot use fails the call, but the reply itself was + // complete, so the solver is left alone + VlSolverStatus readStatus() VL_REQUIRES(m_mutex) { return ::readStatus(m_proc); } + // An unreadable reply means text of it may still be queued, so it is not + // safe to read anything more from this solver + bool readSExpr(std::string& outr) VL_REQUIRES(m_mutex) { + if (::readSExpr(m_proc, outr)) return true; + abandon(); + return false; } - 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"; - if (readStatus(s_solver) == VlSolverStatus::SAT) return s_solver; + // Start a transaction, spawning or respawning the solver as needed + bool begin() VL_REQUIRES(m_mutex) { + m_dirty = false; + if (m_state == State::BROKEN) { + if (m_consecFails >= MAX_CONSEC_FAILS) { + m_state = State::DISABLED; + VL_WARN_MT(__FILE__, __LINE__, "randomize", + "Solver failed repeatedly, so randomize() returns 0 from now on"); + } else if (!m_warnedRestart) { + m_warnedRestart = true; + VL_WARN_MT(__FILE__, __LINE__, "randomize", + "Solver died or replied unreadably, so this randomize() returned 0; " + "restarting it, warned once"); + } + } + if (m_state == State::UNSTARTED || m_state == State::BROKEN) spawn(); + return m_state == State::LIVE; + } - 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()); - return s_solver; -} + // End a transaction; a solver left out of step or dead is replaced next time + void end() VL_REQUIRES(m_mutex) { + bool healthy = !m_dirty && !m_proc.fail(); + if (healthy) { + m_proc << "(reset)\n"; + m_proc.flush(); + healthy = !m_proc.fail(); + } + if (healthy) { + m_consecFails = 0; + } else { + m_proc.terminate(); + m_state = State::BROKEN; + ++m_consecFails; + } + m_dirty = false; + } + +private: + // A solver that will not start is not started again + void spawn() VL_REQUIRES(m_mutex) { + if (m_argv.empty()) { + m_program = Verilated::threadContextp()->solverProgram(); + m_argv.emplace_back(&m_program[0]); + for (char* argp = &m_program[0]; *argp; ++argp) { + if (*argp == ' ') { + *argp = '\0'; + m_argv.emplace_back(argp + 1); + } + } + m_argv.emplace_back(nullptr); + } + m_proc.open(m_argv.data()); + m_proc << "(set-logic QF_ABV)\n"; + m_proc << "(check-sat)\n"; + m_proc << "(reset)\n"; + if (readStatus() == VlSolverStatus::SAT) { + m_state = State::LIVE; + m_dirty = false; + return; + } + m_proc.terminate(); + m_state = State::DISABLED; + 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* argp = m_argv.data(); *argp; ++argp) msg << ' ' << *argp; + msg << '\n'; + const std::string str = msg.str(); + VL_WARN_MT("", 0, "randomize", str.c_str()); + } +}; + +// Constructed before main(), so nothing here may touch the thread context +static VlSolverSession s_solverSession; + +// One solver transaction; the caller holds the session mutex +class VlSolverTxn final { + VlSolverSession& m_sess; + const bool m_ok; + +public: + explicit VlSolverTxn(VlSolverSession& sess) VL_REQUIRES(sess.m_mutex) + : m_sess{sess} + , m_ok{sess.begin()} {} + // Analysis cannot see through the reference member back to the caller's lock + ~VlSolverTxn() VL_NO_THREAD_SAFETY_ANALYSIS { + if (m_ok) m_sess.end(); + } + bool ok() const { return m_ok; } +}; static std::string readUntilBalanced(std::istream& stream) { std::string result; @@ -629,6 +746,8 @@ 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 + VlSolverSession& sess = s_solverSession; + const VerilatedLockGuard lock{sess.m_mutex}; m_checkOnly = checkOnly; const std::vector uniqueExprs = buildUniqueExprs(); @@ -646,9 +765,9 @@ bool VlRandomizer::nextRandomize(VlRNG& rngr, bool checkOnly) { // Pinned vars make phase ordering moot; skip phased path in check-only. bool result; if (!m_checkOnly && !m_solveBefore.empty()) { - result = nextPhased(rngr, uniqueExprs); + result = nextPhased(rngr, sess, uniqueExprs); } else { - result = nextFlat(rngr, uniqueExprs); + result = nextFlat(rngr, sess, uniqueExprs); } m_checkOnly = false; return result; @@ -719,13 +838,15 @@ void VlRandomizer::emitAsserts(std::ostream& os, const std::vector& } } -bool VlRandomizer::nextFlat(VlRNG& rngr, const std::vector& uniqueExprs) { +bool VlRandomizer::nextFlat(VlRNG& rngr, VlSolverSession& sess, + const std::vector& uniqueExprs) + VL_REQUIRES(sess.m_mutex) { + VlSolverTxn txn{sess}; + if (!txn.ok()) return false; + std::iostream& os = sess.os(); // 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"; @@ -738,13 +859,13 @@ bool VlRandomizer::nextFlat(VlRNG& rngr, const std::vector& uniqueE // trivially UNSAT after the first cycle. if (!m_checkOnly) emitRandcExclusions(os); - relaxSoftConstraints(os); + relaxSoftConstraints(sess); os << "(check-sat)\n"; - const VlSolverStatus status = readStatus(os); + const VlSolverStatus status = sess.readStatus(); if (status != VlSolverStatus::SAT) { - os << "(reset)\n"; if (status != VlSolverStatus::UNSAT) return false; + 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(); @@ -755,28 +876,22 @@ bool VlRandomizer::nextFlat(VlRNG& rngr, const std::vector& uniqueE // 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"; + reportUnsatSetup(sess, uniqueExprs); return false; } + if (!applyModel(sess)) return false; if (!m_checkOnly) { - solveDiversity(rngr, os); + solveDiversity(rngr, sess); // 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) { +void VlRandomizer::solveDiversity(VlRNG& rngr, VlSolverSession& sess) VL_REQUIRES(sess.m_mutex) { bool hasArray = false; for (const auto& var : m_vars) { if (var.second->dimension() > 0) { @@ -785,13 +900,15 @@ void VlRandomizer::solveDiversity(VlRNG& rngr, std::iostream& os) { } } if (hasArray) { - solveDiversityXor(rngr, os); + solveDiversityXor(rngr, sess); } else { - solveDiversityPins(rngr, os); + solveDiversityPins(rngr, sess); } } -void VlRandomizer::solveDiversityPins(VlRNG& rngr, std::iostream& os) { +void VlRandomizer::solveDiversityPins(VlRNG& rngr, VlSolverSession& sess) + VL_REQUIRES(sess.m_mutex) { + std::iostream& os = sess.os(); // Tie each free bit to a random target via an assumption literal; // drop one conflicting literal per round until compatible int npins = 0; @@ -813,16 +930,16 @@ void VlRandomizer::solveDiversityPins(VlRNG& rngr, std::iostream& os) { if (!dropped[k]) os << " a" << k; } os << "))\n"; - const VlSolverStatus status = readStatus(os); + const VlSolverStatus status = sess.readStatus(); if (status == VlSolverStatus::SAT) { - applyModel(os); + applyModel(sess); 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 core = readUnsatAssumptions(os); + const std::vector core = readUnsatAssumptions(sess); bool droppedOne = false; for (const int idx : core) { if (idx < npins) { @@ -835,31 +952,34 @@ void VlRandomizer::solveDiversityPins(VlRNG& rngr, std::iostream& os) { } } -void VlRandomizer::solveDiversityXor(VlRNG& rngr, std::iostream& os) { +void VlRandomizer::solveDiversityXor(VlRNG& rngr, VlSolverSession& sess) + VL_REQUIRES(sess.m_mutex) { + std::iostream& os = sess.os(); 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"; - if (readStatus(os) != VlSolverStatus::SAT) break; - if (!applyModel(os)) break; + if (sess.readStatus() != VlSolverStatus::SAT) break; + if (!applyModel(sess)) break; } } // Re-add softs highest-priority first, dropping incompatible ones. -void VlRandomizer::relaxSoftConstraints(std::iostream& os) { +void VlRandomizer::relaxSoftConstraints(VlSolverSession& sess) VL_REQUIRES(sess.m_mutex) { if (m_softConstraints.empty()) return; + std::iostream& os = sess.os(); os << "(push 1)\n"; for (const auto& s : m_softConstraints) os << "(assert (= #b1 " << s << "))\n"; os << "(check-sat)\n"; - const VlSolverStatus status = readStatus(os); + const VlSolverStatus status = sess.readStatus(); 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"; - const VlSolverStatus probe = readStatus(os); + const VlSolverStatus probe = sess.readStatus(); if (probe == VlSolverStatus::FAIL) return; if (probe != VlSolverStatus::SAT) os << "(pop 1)\n"; } @@ -882,10 +1002,11 @@ static std::vector scanIntRuns(const std::string& reply) { return idxs; } -std::vector VlRandomizer::readUnsatAssumptions(std::iostream& os) { - os << "(get-unsat-assumptions)\n"; +std::vector VlRandomizer::readUnsatAssumptions(VlSolverSession& sess) + VL_REQUIRES(sess.m_mutex) { + sess.os() << "(get-unsat-assumptions)\n"; std::string reply; - if (!readSExpr(os, reply)) return {}; + if (!sess.readSExpr(reply)) return {}; if (isSolverError(reply)) { warnSolverReply(reply); return {}; @@ -895,21 +1016,23 @@ std::vector VlRandomizer::readUnsatAssumptions(std::iostream& os) { } // Re-solve with named asserts so an unsat core can name the failing constraints -void VlRandomizer::reportUnsatSetup(std::iostream& os, - const std::vector& uniqueExprs) { +void VlRandomizer::reportUnsatSetup(VlSolverSession& sess, + const std::vector& uniqueExprs) + VL_REQUIRES(sess.m_mutex) { + std::iostream& os = sess.os(); 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"; - if (readStatus(os) == VlSolverStatus::UNSAT) reportUnsatCore(os); + if (sess.readStatus() == VlSolverStatus::UNSAT) reportUnsatCore(sess); } -void VlRandomizer::reportUnsatCore(std::iostream& os) { - os << "(get-unsat-core)\n"; +void VlRandomizer::reportUnsatCore(VlSolverSession& sess) VL_REQUIRES(sess.m_mutex) { + sess.os() << "(get-unsat-core)\n"; std::string reply; - if (!readSExpr(os, reply)) return; + if (!sess.readSExpr(reply)) return; if (isSolverError(reply)) { warnSolverReply(reply); return; @@ -944,7 +1067,8 @@ void VlRandomizer::reportUnsatCore(std::iostream& os) { } } -bool VlRandomizer::applyModel(std::iostream& os) { +bool VlRandomizer::applyModel(VlSolverSession& sess) VL_REQUIRES(sess.m_mutex) { + std::iostream& os = sess.os(); size_t requested = 0; std::stringstream getValueStr; for (const auto& var : m_vars) { @@ -964,7 +1088,7 @@ bool VlRandomizer::applyModel(std::iostream& os) { } os << "(get-value (" << getValueStr.str() << "))\n"; std::string reply; - if (!readSExpr(os, reply)) return false; + if (!sess.readSExpr(reply)) return false; if (isSolverError(reply)) { warnSolverReply(reply); return false; @@ -1188,32 +1312,38 @@ const char* VlRandomizer::phasedLogic() const { return "QF_ABV"; } -bool VlRandomizer::nextPhased(VlRNG& rngr, const std::vector& uniqueExprs) { +bool VlRandomizer::nextPhased(VlRNG& rngr, VlSolverSession& sess, + const std::vector& uniqueExprs) + VL_REQUIRES(sess.m_mutex) { // Solve layer by layer with ALL constraints, pinning earlier layers std::vector> 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); + if (layers.size() <= 1) return nextFlat(rngr, sess, uniqueExprs); - if (solvePhases(rngr, layers, uniqueExprs)) return true; + VlSolverTxn txn{sess}; + if (!txn.ok()) return false; // Retry once with the randc cycle cleared, as nextFlat does - if (m_randcUsedValues.empty()) return false; + bool exhausted = false; + if (solvePhases(rngr, sess, layers, uniqueExprs, exhausted)) return true; + if (!exhausted) return false; m_randcUsedValues.clear(); - return solvePhases(rngr, layers, uniqueExprs); + sess.os() << "(reset)\n"; + return solvePhases(rngr, sess, layers, uniqueExprs, exhausted); } -bool VlRandomizer::solvePhases(VlRNG& rngr, const std::vector>& layers, - const std::vector& uniqueExprs) { +bool VlRandomizer::solvePhases(VlRNG& rngr, VlSolverSession& sess, + const std::vector>& layers, + const std::vector& uniqueExprs, bool& exhaustedr) + VL_REQUIRES(sess.m_mutex) { + std::iostream& os = sess.os(); std::map 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); @@ -1228,29 +1358,24 @@ bool VlRandomizer::solvePhases(VlRNG& rngr, const std::vector& layerVars, - std::map& solvedValuesr) { + std::map& solvedValuesr) + VL_REQUIRES(sess.m_mutex) { + std::iostream& os = sess.os(); const auto emitGetValueCmd = [&]() { os << "(get-value ("; for (const auto& varName : layerVars) { @@ -1281,7 +1408,7 @@ bool VlRandomizer::solvePhaseValues(std::iostream& os, VlRNG& rngr, }; // Get baseline values (deterministic, always valid) emitGetValueCmd(); - if (!readPhaseValues(os, solvedValuesr)) return false; + if (!readPhaseValues(sess, solvedValuesr)) return false; // Try diversity: add random constraint, re-check. If sat, get // updated (more diverse) values. If unsat, keep baseline values. @@ -1289,17 +1416,18 @@ bool VlRandomizer::solvePhaseValues(std::iostream& os, VlRNG& rngr, randomConstraint(os, rngr, _VL_SOLVER_HASH_LEN); os << ")\n"; os << "(check-sat)\n"; - if (readStatus(os) == VlSolverStatus::SAT) { + if (sess.readStatus() == VlSolverStatus::SAT) { emitGetValueCmd(); - (void)readPhaseValues(os, solvedValuesr); + (void)readPhaseValues(sess, solvedValuesr); } return true; } -bool VlRandomizer::readPhaseValues(std::iostream& os, - std::map& solvedValuesr) { +bool VlRandomizer::readPhaseValues(VlSolverSession& sess, + std::map& solvedValuesr) + VL_REQUIRES(sess.m_mutex) { std::string reply; - if (!readSExpr(os, reply)) return false; + if (!sess.readSExpr(reply)) return false; if (isSolverError(reply)) { warnSolverReply(reply); return false; diff --git a/include/verilated_random.h b/include/verilated_random.h index 54abb2d0e..bd68f9dec 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -230,6 +230,8 @@ public: } }; +class VlSolverSession; + //============================================================================= // Object holding constraints and variable references. class VlRandomizer VL_NOT_FINAL { @@ -258,14 +260,14 @@ class VlRandomizer VL_NOT_FINAL { // PRIVATE METHODS void randomConstraint(std::ostream& os, VlRNG& rngr, int bits); // Fetch the model and write it into the registered variables. - bool applyModel(std::iostream& os); + bool applyModel(VlSolverSession& sess); bool parseModel(std::istream& is, size_t requested); // Assert the maximal compatible soft-constraint set onto the open session. - void relaxSoftConstraints(std::iostream& os); + void relaxSoftConstraints(VlSolverSession& sess); // Indices of the "a" literals named by (get-unsat-assumptions). - std::vector readUnsatAssumptions(std::iostream& os); - void reportUnsatSetup(std::iostream& os, const std::vector& uniqueExprs); - void reportUnsatCore(std::iostream& os); + std::vector readUnsatAssumptions(VlSolverSession& sess); + void reportUnsatSetup(VlSolverSession& sess, const std::vector& uniqueExprs); + void reportUnsatCore(VlSolverSession& sess); void emitRandcExclusions(std::ostream& os) const; // Emit randc exclusion constraints void recordRandcValues(); // Record solved randc values for future exclusion size_t hashConstraints(const std::vector& extras) const; @@ -275,20 +277,22 @@ class VlRandomizer VL_NOT_FINAL { void emitDefines(std::ostream& os) const; void emitDeclares(std::ostream& os, bool pinCurrent) const; void emitAsserts(std::ostream& os, const std::vector& extras, bool named) const; - bool nextFlat(VlRNG& rngr, const std::vector& uniqueExprs); - void solveDiversity(VlRNG& rngr, std::iostream& os); - void solveDiversityPins(VlRNG& rngr, std::iostream& os); - void solveDiversityXor(VlRNG& rngr, std::iostream& os); + bool nextFlat(VlRNG& rngr, VlSolverSession& sess, const std::vector& uniqueExprs); + void solveDiversity(VlRNG& rngr, VlSolverSession& sess); + void solveDiversityPins(VlRNG& rngr, VlSolverSession& sess); + void solveDiversityXor(VlRNG& rngr, VlSolverSession& sess); // Layers of solve...before variables in dependency order bool buildSolveLayers(std::vector>& layersr); const char* phasedLogic() const; - bool nextPhased(VlRNG& rngr, const std::vector& uniqueExprs); - bool solvePhases(VlRNG& rngr, const std::vector>& layers, - const std::vector& uniqueExprs); - bool solvePhaseValues(std::iostream& os, VlRNG& rngr, + bool nextPhased(VlRNG& rngr, VlSolverSession& sess, + const std::vector& uniqueExprs); + bool solvePhases(VlRNG& rngr, VlSolverSession& sess, + const std::vector>& layers, + const std::vector& uniqueExprs, bool& exhaustedr); + bool solvePhaseValues(VlSolverSession& sess, VlRNG& rngr, const std::vector& layerVars, std::map& solvedValuesr); - bool readPhaseValues(std::iostream& os, std::map& solvedValuesr); + bool readPhaseValues(VlSolverSession& sess, std::map& solvedValuesr); bool parsePhaseValues(std::istream& is, std::map& solvedValuesr); public: diff --git a/test_regress/t/randomize_solver_tamper.py b/test_regress/t/randomize_solver_tamper.py index 6db7fc7e3..8ea7facba 100755 --- a/test_regress/t/randomize_solver_tamper.py +++ b/test_regress/t/randomize_solver_tamper.py @@ -11,14 +11,14 @@ # # Input arguments from environment variables: # 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 +# | core_junk | crlf | die_at | die_status_at | diversity_model +# | 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 +# | unsat_recheck | 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 @@ -29,6 +29,7 @@ # 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 +# diversity_model - replace the Nth array model reply with one holding an unusable value # 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 ...) @@ -60,9 +61,13 @@ # 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 +# unsat_recheck - answer the status that follows an unsat with sat # 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) +# TAMPER_ONCE: file marking that the tamper already acted. The runtime restarts +# a solver that died, which starts this wrapper again, so without the file a +# mode acts once per solver rather than once per simulation. # pylint: disable=C0103,C0114,consider-using-with @@ -75,6 +80,7 @@ import time mode = os.environ.get("TAMPER", "none") at = int(os.environ.get("TAMPER_AT", "3")) +once = os.environ.get("TAMPER_ONCE", "") # 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", @@ -82,8 +88,10 @@ STATUS_MODES = ("die_status_at", "err_multiline", "err_once", "err_trunc", "err_ "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", ) +# Modes acting on an array model reply, which arrives as (select ...) terms +SELECT_MODES = ("bad_index", "diversity_model") +# Modes acting on the status the solver sends after answering unsat +RECHECK_MODES = ("unsat_recheck", ) # 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 literals @@ -159,7 +167,8 @@ def swallow(first): replies = 0 -done = False +seen_unsat = False +done = bool(once) and os.path.exists(once) 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 @@ -175,6 +184,8 @@ for line in proc.stdout: counted = at_reply_start and line.startswith("(") elif mode in SELECT_MODES: counted = at_reply_start and line.startswith("(((select") + elif mode in RECHECK_MODES: + counted = is_status and seen_unsat elif mode in PHASE_MODES: counted = at_reply_start and line.startswith("((x") elif mode in ASSUME_MODES: @@ -183,12 +194,17 @@ for line in proc.stdout: counted = at_reply_start and line.startswith("(cons") else: counted = at_reply_start and line.startswith("((") + if line == "unsat": + seen_unsat = True if counted: replies += 1 acting = counted and replies >= at and not done and mode not in STREAM_MODES if not acting: forward(line, at_reply_start) continue + if once: + with open(once, "w", encoding="utf-8"): + pass done = True @@ -224,6 +240,11 @@ for line in proc.stdout: proc.kill() proc.wait() sys.exit(0) + # The base model comes first, so a later one belongs to a diversity round + if mode == "diversity_model": + emit("(((select q #x00000000) bogus))") + swallow(line) + continue if mode == "dup_model": emit("((a #x0b) (a #x0c) (b #x05))") swallow(line) @@ -337,6 +358,13 @@ for line in proc.stdout: emit("((zzz #x01) (b #x12))") swallow(line) continue + # Every re-solve answers the same way, so this re-arms instead of latching + if mode == "unsat_recheck": + replies = 0 + seen_unsat = False + done = False + emit("sat") + continue if mode == "unsupported_once": emit("unsupported") continue diff --git a/test_regress/t/t_randomize_solver_core.py b/test_regress/t/t_randomize_solver_core.py new file mode 100755 index 000000000..4e930f79e --- /dev/null +++ b/test_regress/t/t_randomize_solver_core.py @@ -0,0 +1,33 @@ +#!/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() + +# The core is read from a second solve of the same constraints, so the only +# statuses here are that solve's and the one it repeats +test.execute() +test.file_grep(test.run_log_filename, r'NFAIL=(\d+)', 3) +test.file_grep(test.run_log_filename, r'Unsatisfied constraint') + +# A solver that does not repeat its unsat leaves the constraints unnamed +logfile = test.obj_dir + '/sim_unsat_recheck.log' +test.execute(logfile=logfile, + run_env='VERILATOR_SOLVER="' + test.t_dir + '/randomize_solver_tamper.py" ' + + 'TAMPER=unsat_recheck TAMPER_AT=1') +test.file_grep(logfile, r'NFAIL=(\d+)', 3) +test.file_grep_not(logfile, r'Unsatisfied constraint') + +test.passes() diff --git a/test_regress/t/t_randomize_solver_core.v b/test_regress/t/t_randomize_solver_core.v new file mode 100644 index 000000000..d97a8ff44 --- /dev/null +++ b/test_regress/t/t_randomize_solver_core.v @@ -0,0 +1,36 @@ +// 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 + +// Only unsatisfiable, so every solver status this test produces belongs to the +// unsat core report +class Unsat; + rand bit [7:0] u; + constraint uc { + u > 8'd200; + u < 8'd100; + } +endclass + +module t; + initial begin + automatic Unsat un = new; + automatic int nfail = 0; + for (int i = 0; i < 3; ++i) begin + un.u = 8'd7; + if (un.randomize() == 0) nfail++; + // An unsatisfiable randomize leaves the variable alone + `checkd(un.u, 8'd7); + end + $write("NFAIL=%0d\n", nfail); + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule diff --git a/test_regress/t/t_randomize_solver_fault.v b/test_regress/t/t_randomize_solver_fault.v index 0103a00d8..551537284 100644 --- a/test_regress/t/t_randomize_solver_fault.v +++ b/test_regress/t/t_randomize_solver_fault.v @@ -48,15 +48,15 @@ module t; // 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++; end $write("NPASS=%0d\n", npass); - // A randomize that failed must leave the variable alone - `checkd(p.a, 8'd5); $write("*-* All Finished *-*\n"); $finish; end diff --git a/test_regress/t/t_randomize_solver_mt.py b/test_regress/t/t_randomize_solver_mt.py new file mode 100755 index 000000000..baec04b92 --- /dev/null +++ b/test_regress/t/t_randomize_solver_mt.py @@ -0,0 +1,23 @@ +#!/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('vltmt') + +if not test.have_solver: + test.skip("No constraint solver installed") + +test.compile() + +test.execute() + +test.file_grep(test.run_log_filename, r'NLO=99 NHI=50') + +test.passes() diff --git a/test_regress/t/t_randomize_solver_mt.v b/test_regress/t/t_randomize_solver_mt.v new file mode 100644 index 000000000..a294f04f5 --- /dev/null +++ b/test_regress/t/t_randomize_solver_mt.v @@ -0,0 +1,91 @@ +// 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 + +// Each class pins one value, so a reply delivered to the wrong transaction +// shows up as a wrong value rather than as a rare miscount +class PktLo; + rand bit [7:0] a; + constraint c {a == 8'd25;} +endclass + +class PktHi; + rand bit [7:0] b; + constraint c {b == 8'd105;} +endclass + +// Two modules randomize on the same edge, so the runtime has to serialize the +// solver transactions of the threads running them +module sub_lo ( + input logic clk, + output int npass +); + PktLo p; + initial begin + p = new; + npass = 0; + end + always @(posedge clk) begin + automatic int rc = p.randomize(); + `checkd(rc, 1); + `checkd(p.a, 8'd25); + npass <= npass + 1; + end +endmodule + +module sub_hi ( + input logic clk, + output int npass +); + PktHi p; + int phase; + initial begin + p = new; + npass = 0; + phase = 0; + end + // Randomizes every other edge, so the two modules also collide unevenly + always @(posedge clk) begin + phase <= phase + 1; + if (phase[0] == 1'b0) begin + automatic int rc = p.randomize(); + `checkd(rc, 1); + `checkd(p.b, 8'd105); + npass <= npass + 1; + end + end +endmodule + +module t ( /*AUTOARG*/ + // Inputs + clk +); + input clk; + int nlo, nhi; + int cyc = 0; + sub_lo u_lo ( + .clk(clk), + .npass(nlo) + ); + sub_hi u_hi ( + .clk(clk), + .npass(nhi) + ); + always @(posedge clk) begin + cyc <= cyc + 1; + if (cyc == 99) begin + $display("NLO=%0d NHI=%0d", nlo, nhi); + `checkd(nlo, 99); + `checkd(nhi, 50); + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule diff --git a/test_regress/t/t_randomize_solver_pipe.py b/test_regress/t/t_randomize_solver_pipe.py index 25d42eee6..a884a1c77 100755 --- a/test_regress/t/t_randomize_solver_pipe.py +++ b/test_regress/t/t_randomize_solver_pipe.py @@ -7,6 +7,8 @@ # SPDX-FileCopyrightText: 2026 Wilson Snyder # SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 +import os + import vltest_bootstrap test.scenarios('vlt') @@ -17,20 +19,52 @@ if not test.have_solver: test.compile() -# Reply index picks which reply the runtime is waiting on when the solver goes +# Every scenario acts on the first reply of its kind, so the counts do not +# depend on how many replies a particular solver sends per randomize() call. +# once=True acts one time in the whole run; the restarted solver then serves +# every later call. once=False acts again in every solver, so the runtime gives +# up and disables randomization. runs = [ - ('die_at', 10, 3), # solver exits with a model reply pending - ('die_status_at', 4, 1), # solver exits with a soft constraint status pending - ('die_status_at', 7, 2), # solver exits between the status and the model read - ('mute_at', 3, 2), # solver stays running but stops answering - ('garbage_at', 2, 1), # solver answers, but not with an S-expression + ('die_at', True, 11), # solver exits with a model reply pending + ('die_status_at', True, 11), # solver exits with a status pending + ('mute_at', True, 11), # solver stays running but stops answering + ('garbage_at', True, 11), # solver answers, but not with an S-expression + ('garbage_at', False, 0), # every solver answers the same way ] -for mode, at, npass in runs: - logfile = test.obj_dir + '/sim_' + mode + '_' + str(at) + '.log' +for mode, once, npass in runs: + tag = mode + ('_once' if once else '_always') + logfile = test.obj_dir + '/sim_' + tag + '.log' + latch = test.obj_dir + '/' + tag + '.latch' + if os.path.exists(latch): + os.unlink(latch) 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=' + str(npass) + r'\n') + 'TAMPER=' + mode + ' TAMPER_AT=1 ' + + ('TAMPER_ONCE="' + latch + '" ' if once else '')) + test.file_grep(logfile, r'NPASS=(\d+)', npass) + test.file_grep(logfile, r'Solver died or replied unreadably') + +test.file_grep(test.obj_dir + '/sim_garbage_at_always.log', r'Solver failed repeatedly') + +# A solver that never starts is not restarted, so it is never reported as dead +logfile = test.obj_dir + '/sim_nosolver.log' +test.execute(logfile=logfile, run_env='VERILATOR_SOLVER=someimaginarysolver ') +test.file_grep(logfile, r'NPASS=(\d+)', 0) +test.file_grep(logfile, r'Unable to communicate with SAT solver') +test.file_grep_not(logfile, r'Solver died') + +# One rejected command must not count against the solver: the reply was +# complete, so the session stays and later calls keep working +logfile = test.obj_dir + '/sim_err_once.log' +latch = test.obj_dir + '/err_once.latch' +if os.path.exists(latch): + os.unlink(latch) +test.execute(logfile=logfile, + run_env='VERILATOR_SOLVER="' + test.t_dir + '/randomize_solver_tamper.py" ' + + 'TAMPER=err_once TAMPER_AT=2 TAMPER_ONCE="' + latch + '" ') +test.file_grep(logfile, r'NPASS=(\d+)', 11) +test.file_grep_not(logfile, r'Solver failed repeatedly') +test.file_grep_not(logfile, r'Solver died') test.passes() diff --git a/test_regress/t/t_randomize_solver_reply.py b/test_regress/t/t_randomize_solver_reply.py index 20de56971..f83e6a1a6 100755 --- a/test_regress/t/t_randomize_solver_reply.py +++ b/test_regress/t/t_randomize_solver_reply.py @@ -24,8 +24,9 @@ runs = [ ('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 + ('core_junk', 1, 16), # garbage opens the core reply, then the pipe closes ('crlf', 1, 16), # CRLF line endings + ('diversity_model', 2, 16), # a diversity round answers with an unusable value ('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 @@ -49,7 +50,7 @@ runs = [ ('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 + ('phase_trunc', 1, 12), # 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