Add `+verilator+solver+file` (#7242).

Fixes #7242.

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.]

bin/verilator

@@ -585,6 +585,7 @@ description of these arguments.
      +verilator+quiet                      Minimize additional printing
      +verilator+rand+reset+<value>         Set random reset technique
      +verilator+seed+<value>               Set random seed
+     +verilator+solver+file+<filename>     Set random solver log filename
      +verilator+V                          Show verbose version and config
      +verilator+version                    Show version and exit
      +verilator+wno+unsatconstr+<value>    Disable constraint warnings

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+<filename>
+
+   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.

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<int>(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

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;

include/verilated_random.cpp

@@ -23,6 +23,7 @@
 
 #include "verilated_random.h"
 
+#include <fstream>
 #include <iomanip>
 #include <iostream>
 #include <sstream>
@@ -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<std::ofstream> 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<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);
-        // 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<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) 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() {

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

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