diff --git a/Changes b/Changes index 2ce61d1ea..c400489ba 100644 --- a/Changes +++ b/Changes @@ -49,6 +49,7 @@ Verilator 5.047 devel * Add VPI callback support to --main (#7145). * Add V3LiftExpr pass to lower impure expressions and calls (#7141) (#7164). [Geza Lore, Testorrent USA, Inc.] * Add --func-recursion-depth CLI option (#7175) (#7179). +* Add `+verilator+solver+file` (#7242). * Add MacOS support for address sanitizer memory limit (#7308). [Marco Bartoli] * Deprecate `--structs-packed` (#7222). * Improve assignment-compatibility type check (#2843) (#5666) (#7052). [Pawel Kojma, Antmicro Ltd.] diff --git a/bin/verilator b/bin/verilator index f85798ce0..8779c7344 100755 --- a/bin/verilator +++ b/bin/verilator @@ -585,6 +585,7 @@ description of these arguments. +verilator+quiet Minimize additional printing +verilator+rand+reset+ Set random reset technique +verilator+seed+ Set random seed + +verilator+solver+file+ Set random solver log filename +verilator+V Show verbose version and config +verilator+version Show version and exit +verilator+wno+unsatconstr+ Disable constraint warnings diff --git a/docs/guide/exe_sim.rst b/docs/guide/exe_sim.rst index fe916c089..7f696073e 100644 --- a/docs/guide/exe_sim.rst +++ b/docs/guide/exe_sim.rst @@ -116,6 +116,12 @@ Options: simulation runtime random seed value. If zero or not specified picks a value from the system random number generator. +.. option:: +verilator+solver+file+ + + If specified, when the randomization solver is used, open the given + filename for writing, and log all random solver commands and responses + to it. + .. option:: +verilator+V Shows the verbose version, including configuration information. diff --git a/include/verilated.cpp b/include/verilated.cpp index 922385126..16f8a6cee 100644 --- a/include/verilated.cpp +++ b/include/verilated.cpp @@ -3001,6 +3001,14 @@ std::string VerilatedContext::profVltFilename() const VL_MT_SAFE { const VerilatedLockGuard lock{m_mutex}; return m_ns.m_profVltFilename; } +void VerilatedContext::solverLogFilename(const std::string& flag) VL_MT_SAFE { + const VerilatedLockGuard lock{m_mutex}; + m_ns.m_solverLogFilename = flag; +} +std::string VerilatedContext::solverLogFilename() const VL_MT_SAFE { + const VerilatedLockGuard lock{m_mutex}; + return m_ns.m_solverLogFilename; +} void VerilatedContext::solverProgram(const std::string& flag) VL_MT_SAFE { const VerilatedLockGuard lock{m_mutex}; m_ns.m_solverProgram = flag; @@ -3017,6 +3025,12 @@ void VerilatedContext::randReset(int val) VL_MT_SAFE { const VerilatedLockGuard lock{m_mutex}; m_s.m_randReset = val; } + +std::string VerilatedContext::timeWithUnitString() const VL_MT_SAFE { + const double simtimeInUnits = VL_TIME_Q() * vl_time_multiplier(timeunit()) + * vl_time_multiplier(timeprecision() - timeunit()); + return vl_timescaled_double(simtimeInUnits); +} void VerilatedContext::timeunit(int value) VL_MT_SAFE { if (value < 0) value = -value; // Stored as 0..15 const VerilatedLockGuard lock{m_mutex}; @@ -3233,6 +3247,8 @@ void VerilatedContextImp::commandArgVl(const std::string& arg) { quiet(true); } else if (commandArgVlUint64(arg, "+verilator+rand+reset+", u64, 0, 2)) { randReset(static_cast(u64)); + } else if (commandArgVlString(arg, "+verilator+solver+file+", str)) { + solverLogFilename(str); } else if (commandArgVlUint64(arg, "+verilator+wno+unsatconstr+", u64, 0, 1)) { warnUnsatConstr(u64 == 0); // wno means disable, so invert } else if (commandArgVlUint64(arg, "+verilator+seed+", u64, 1, @@ -3326,7 +3342,7 @@ void VerilatedContext::statsPrintSummary() VL_MT_UNSAFE { const std::string endwhy = gotError() ? "$stop" : gotFinish() ? "$finish" : "end"; const double simtimeInUnits = VL_TIME_Q() * vl_time_multiplier(timeunit()) * vl_time_multiplier(timeprecision() - timeunit()); - const std::string simtime = vl_timescaled_double(simtimeInUnits); + const std::string simtime = timeWithUnitString(); const double walltime = statWallTimeSinceStart(); const double cputime = statCpuTimeSinceStart(); const std::string simtimePerf diff --git a/include/verilated.h b/include/verilated.h index b7f70bda7..b1c0bce15 100644 --- a/include/verilated.h +++ b/include/verilated.h @@ -415,6 +415,7 @@ protected: std::string m_coverageFilename; // +coverage+file filename std::string m_profExecFilename; // +prof+exec+file filename std::string m_profVltFilename; // +prof+vlt filename + std::string m_solverLogFilename; // SMT solver log filename std::string m_solverProgram; // SMT solver program bool m_warnUnsatConstr = true; // Warn on unsatisfied constraints VlOs::DeltaCpuTime m_cpuTimeStart{false}; // CPU time, starts when create first model @@ -586,6 +587,8 @@ public: void time(uint64_t value) VL_MT_SAFE { m_s.m_time = value; } /// Advance current simulation time. See time() for side effect details void timeInc(uint64_t add) VL_MT_UNSAFE { m_s.m_time += add; } + /// Return time as unit string + std::string timeWithUnitString() const VL_MT_SAFE; /// Return time units as power-of-ten int timeunit() const VL_MT_SAFE { return -m_s.m_timeunit; } /// Set time units as power-of-ten @@ -666,6 +669,9 @@ public: std::string profVltFilename() const VL_MT_SAFE; void profVltFilename(const std::string& flag) VL_MT_SAFE; + // Internal: Solver log filename + std::string solverLogFilename() const VL_MT_SAFE; + void solverLogFilename(const std::string& flag) VL_MT_SAFE; // Internal: SMT solver program std::string solverProgram() const VL_MT_SAFE; void solverProgram(const std::string& flag) VL_MT_SAFE; diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index 4aded2610..17d91877c 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -23,6 +23,7 @@ #include "verilated_random.h" +#include #include #include #include @@ -61,6 +62,9 @@ class VlRProcess final : private std::streambuf, public std::iostream { char m_readBuf[BUFFER_SIZE]; char m_writeBuf[BUFFER_SIZE]; + std::unique_ptr m_logfp; // Log file stream + uint64_t m_logLastTime = ~0ULL; // Last timestamp for logfile + public: typedef std::streambuf::traits_type traits_type; @@ -69,8 +73,8 @@ protected: const char c2 = static_cast(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); - // VL_PRINTF_MT("solver-write '%s'\n", std::string(pbase(), size).c_str()); if (VL_UNLIKELY(n == -1)) perror("write"); if (n <= 0) { wait_report(); @@ -91,6 +95,7 @@ protected: 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]); } @@ -104,6 +109,7 @@ public: : std::streambuf{} , std::iostream{this} , m_cmd{cmd} { + logOpen(); open(cmd); } @@ -175,6 +181,7 @@ public: return false; } + log("", "# Open: "s + cmd[0]); const pid_t pid = fork(); if (VL_UNLIKELY(pid < 0)) { perror("VlRProcess::open: fork"); @@ -212,6 +219,35 @@ public: return false; #endif } + +private: + void logOpen() { + const std::string filename = Verilated::threadContextp()->solverLogFilename(); + if (filename.empty()) return; + m_logfp = std::make_unique(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) VL_MT_SAFE_EXCLUDES(m_mutex) { + 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() { diff --git a/test_regress/t/t_constraint_solver_log.py b/test_regress/t/t_constraint_solver_log.py new file mode 100755 index 000000000..637c1e532 --- /dev/null +++ b/test_regress/t/t_constraint_solver_log.py @@ -0,0 +1,25 @@ +#!/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() + +solver_log = test.obj_dir + "/solver.log" + +test.execute(all_run_flags=['+verilator+solver+file+' + solver_log]) + +test.file_grep(solver_log, '# Verilator solver log') + +test.passes() diff --git a/test_regress/t/t_constraint_solver_log.v b/test_regress/t/t_constraint_solver_log.v new file mode 100644 index 000000000..f985b812a --- /dev/null +++ b/test_regress/t/t_constraint_solver_log.v @@ -0,0 +1,27 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Wilson Snyder +// SPDX-License-Identifier: CC0-1.0 + +class Packet; + rand int one; + constraint a {one > 0 && one < 2;} +endclass + +module t; + + Packet p; + + int v; + + initial begin + p = new; + v = p.randomize(); + if (v != 1) $stop; + if (p.one != 1) $stop; + + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule