Support constrained randomization with external solvers (#4947)

Makefile.in

@@ -91,6 +91,7 @@ datarootdir = @datarootdir@
 CFG_WITH_CCWARN = @CFG_WITH_CCWARN@
 CFG_WITH_DEFENV = @CFG_WITH_DEFENV@
 CFG_WITH_LONGTESTS = @CFG_WITH_LONGTESTS@
+CFG_WITH_SOLVER = @CFG_WITH_SOLVER@
 PACKAGE_VERSION = @PACKAGE_VERSION@
 
 #### End of system configuration section. ####

ci/ci-install.bash

@@ -92,8 +92,8 @@ elif [ "$CI_BUILD_STAGE_NAME" = "test" ]; then
     sudo apt-get update ||
     sudo apt-get update
     # libfl-dev needed for internal coverage's test runs
-    sudo apt-get install gdb gtkwave lcov libfl-dev ccache jq ||
+    sudo apt-get install gdb gtkwave lcov libfl-dev ccache jq z3 ||
-    sudo apt-get install gdb gtkwave lcov libfl-dev ccache jq
+    sudo apt-get install gdb gtkwave lcov libfl-dev ccache jq z3
     # Required for test_regress/t/t_dist_attributes.pl
     if [ "$CI_RUNS_ON" = "ubuntu-22.04" ]; then
       sudo apt-get install python3-clang mold ||
@@ -106,10 +106,10 @@ elif [ "$CI_BUILD_STAGE_NAME" = "test" ]; then
   elif [ "$CI_OS_NAME" = "osx" ]; then
     brew update
     # brew cask install gtkwave # fst2vcd hangs at launch, so don't bother
-    brew install ccache perl jq
+    brew install ccache perl jq z3
   elif [ "$CI_OS_NAME" = "freebsd" ]; then
     # fst2vcd fails with "Could not open '<input file>', exiting."
-    sudo pkg install -y ccache gmake perl5 python3 jq
+    sudo pkg install -y ccache gmake perl5 python3 jq z3
   else
     fatal "Unknown os: '$CI_OS_NAME'"
   fi

ci/docker/buildenv/Dockerfile

@@ -43,6 +43,7 @@ RUN apt-get update \
                         perl \
                         python3 \
                         wget \
+                        z3 \
                         zlib1g \
                         zlib1g-dev \
     && apt-get clean \

configure.ac

@@ -134,6 +134,28 @@ AC_ARG_ENABLE([longtests],
 AC_SUBST(CFG_WITH_LONGTESTS)
 AC_MSG_RESULT($CFG_WITH_LONGTESTS)
 
+AC_CHECK_PROG(HAVE_Z3,z3,yes)
+AC_CHECK_PROG(HAVE_CVC5,cvc5,yes)
+AC_CHECK_PROG(HAVE_CVC4,cvc4,yes)
+
+# Special Substitutions - CFG_WITH_SOLVER
+AC_MSG_CHECKING(for SMT solver)
+AC_ARG_WITH([solver],
+              [AS_HELP_STRING([--with-solver='z3 --in'],
+                              [set default SMT solver for constrained randomization])],
+              [CFG_WITH_SOLVER="${withval}"],
+              [CFG_WITH_SOLVER=no
+               if test "x$HAVE_Z3" = "xyes"; then
+                CFG_WITH_SOLVER="z3 --in"
+               elif test "x$HAVE_CVC5" = "xyes"; then
+                CFG_WITH_SOLVER="cvc5 --incremental"
+               elif test "x$HAVE_CVC4" = "xyes"; then
+                CFG_WITH_SOLVER="cvc4 --lang=smt2 --incremental"
+               fi]
+              )
+AC_SUBST(CFG_WITH_SOLVER)
+AC_MSG_RESULT($CFG_WITH_SOLVER)
+
 # Compiler flags (ensure they are not empty to avoid configure defaults)
 CFLAGS="$CFLAGS "
 CPPFLAGS="$CPPFLAGS "

docs/guide/environment.rst

@@ -118,6 +118,12 @@ associated programs.
 
    See :ref:`Installation` for more details.
 
+.. option:: VERILATOR_SOLVER
+
+   If set, the command to run as a constrained randomization backend, such
+   as :command:`cvc4 --lang=smt2 --incremental`.  If not specified, it will use
+   the one supplied or found during configure, or :command:`z3 --in` if empty.
+
 .. option:: VERILATOR_VALGRIND
 
    If set, the command to run when using the :vlopt:`--valgrind` option, such as

docs/guide/install.rst

@@ -152,6 +152,17 @@ To make use of Verilator FST tracing you will want `GTKwave
 required at Verilator build time.
 
 
+Install Z3
+^^^^^^^^^^
+
+In order to use constrained randomization the `Z3 Theorem Prover
+<https://github.com/z3prover/z3#readme>`__ must be installed, however this is
+not required at Verilator build time. There are other compatible SMT solvers,
+like CVC5/CVC4, but they are not guaranteed to work. Since different solvers are
+faster for different scenarios, the solver to use at run-time can be specified
+by the environment variable :option:`VERILATOR_SOLVER`.
+
+
 .. _Obtain Sources:
 
 Obtain Sources
@@ -193,8 +204,9 @@ Eventual Installation Options
 Before configuring the build, you must decide how you're going to
 eventually install Verilator onto your system. Verilator will be compiling
 the current value of the environment variables :option:`VERILATOR_ROOT`,
-:option:`SYSTEMC_INCLUDE`, and :option:`SYSTEMC_LIBDIR` as defaults into
+:option:`VERILATOR_SOLVER`, :option:`SYSTEMC_INCLUDE`, and
-the executable, so they must be correct before configuring.
+:option:`SYSTEMC_LIBDIR` as defaults into the executable, so they must be
+correct before configuring.
 
 These are the installation options:
 

docs/internals.rst

@@ -1031,6 +1031,91 @@ the evaluation process records a bitmask of variables that might have
 changed; if clear, checking those signals for changes may be skipped.
 
 
+Constrained randomization
+-------------------------
+
+Because general constrained randomization is a co-NP-hard problem, not all
+cases are implemented in Verilator, and an external specialized SMT solver is
+used for any non-obvious ones.
+
+The ``randomize()`` method spawns an SMT solver in a sub-process. Then the
+solver gets a setup query, then the definition of variables, then all the
+constraints (SMT assertions) about the variables. Since the solver has no
+information about the class' PRNG state, if the problem is satisfiable,
+the solution space is further constrained by adding extra random constraints,
+and querying the values satisfying the problem statement.
+The constraint is currently constructed as fixing a simple xor of randomly
+chosen bits of the variables being randomized.
+
+The runtime classes used for handling the randomization are  defined in
+``verilated_random.h`` and ``verilated_random.cpp``.
+
+
+``VlSubprocess``
+~~~~~~~~~~~~~~~~
+
+Subprocess handle, responsible for keeping track of the resources like child
+PID, read and write file descriptors, and presenting them as a C++ iostream.
+
+
+``VlRandomizer``
+~~~~~~~~~~~~~~~~
+
+Randomizer class, responsible for keeping track of variables and constraints,
+and communicating with the solver subprocess.
+
+The solver gets the constraints in `SMT-LIB2
+<https://smtlib.cs.uiowa.edu/>`__ textual format in the following syntax:
+
+::
+
+    (set-info :smt-lib-version 2.0)
+    (set-option :produce-models true)
+    (set-logic QF_BV)
+
+    (declare-fun v () (_ BitVec 16))
+    (declare-fun w () (_ BitVec 64))
+    (declare-fun x () (_ BitVec 48))
+    (declare-fun z () (_ BitVec 24))
+    (declare-fun t () (_ BitVec 23))
+    (assert (or (= v #x0003) (= v #x0008)))
+    (assert (= w #x0000000000000009))
+    (assert (or (or (= x #x000000000001) (= x #x000000000002)) (or (= x #x000000000004) (= x #x000000000009))))
+    (assert (bvult ((_ zero_extend 8) z) #x00000015))
+    (assert (bvugt ((_ zero_extend 8) z) #x0000000d))
+
+    (check-sat)
+
+The solver responds with either ``sat`` or ``unsat``. Then the initial solution
+is queried with:
+
+::
+
+    (get-value (v w x z t ))
+
+The solver then responds with e.g.:
+
+::
+
+    ((v #x0008)
+     (w #x0000000000000005)
+     (x #x000000000002)
+     (z #x000010)
+     (t #b00000000000000000000000))
+
+And then a follow-up query (or a series thereof) is asked, and the solver gets
+reset, so that it can be reused by subsequent randomization attempts:
+
+::
+
+    (assert (= (bvxor (bvxor <...> (bvxor ((_ extract 21 21) z) ((_ extract 39 39) x)) ((_ extract 5 5) w)) <...> ((_ extract 10 10) w)) #b0))
+    (check-sat)
+    (get-value)
+    ...
+    (reset)
+
+
+
 Coding Conventions
 ==================
 
@@ -2125,6 +2210,10 @@ VERILATOR_ROOT
   Standard path to Verilator distribution root; see primary Verilator
   documentation.
 
+VERILATOR_SOLVER
+  SMT solver command for constrained randomization; see primary Verilator
+  documentation.
+
 VERILATOR_TESTS_SITE
   Used with ``--site``, a colon-separated list of directories with tests to
   be added to testlist.

include/verilated.cpp

@@ -82,6 +82,12 @@
 
 #include "verilated_trace.h"
 
+#ifdef VM_SOLVER_DEFAULT
+#define VL_SOLVER_DEFAULT VM_SOLVER_DEFAULT
+#else
+#define VL_SOLVER_DEFAULT "z3 --in"
+#endif
+
 // Max characters in static char string for VL_VALUE_STRING
 constexpr unsigned VL_VALUE_STRING_MAX_WIDTH = 8192;
 
@@ -1171,8 +1177,8 @@ static char* _vl_vsss_read_bin(FILE* fp, int& floc, const WDataInP fromp, const
 static void _vl_vsss_setbit(WDataOutP iowp, int obits, int lsb, int nbits, IData ld) VL_MT_SAFE {
     for (; nbits && lsb < obits; nbits--, lsb++, ld >>= 1) VL_ASSIGNBIT_WI(lsb, iowp, ld & 1);
 }
-static void _vl_vsss_based(WDataOutP owp, int obits, int baseLog2, const char* strp,
+void _vl_vsss_based(WDataOutP owp, int obits, int baseLog2, const char* strp, size_t posstart,
-                           size_t posstart, size_t posend) VL_MT_SAFE {
+                    size_t posend) VL_MT_SAFE {
     // Read in base "2^^baseLog2" digits from strp[posstart..posend-1] into owp of size obits.
     VL_ZERO_W(obits, owp);
     int lsb = 0;
@@ -2460,6 +2466,7 @@ VerilatedContext::VerilatedContext()
     m_ns.m_coverageFilename = "coverage.dat";
     m_ns.m_profExecFilename = "profile_exec.dat";
     m_ns.m_profVltFilename = "profile.vlt";
+    m_ns.m_solverProgram = VlOs::getenvStr("VERILATOR_SOLVER", VL_SOLVER_DEFAULT);
     m_fdps.resize(31);
     std::fill(m_fdps.begin(), m_fdps.end(), static_cast<FILE*>(nullptr));
     m_fdFreeMct.resize(30);
@@ -2570,6 +2577,14 @@ std::string VerilatedContext::profVltFilename() const VL_MT_SAFE {
     const VerilatedLockGuard lock{m_mutex};
     return m_ns.m_profVltFilename;
 }
+void VerilatedContext::solverProgram(const std::string& flag) VL_MT_SAFE {
+    const VerilatedLockGuard lock{m_mutex};
+    m_ns.m_solverProgram = flag;
+}
+std::string VerilatedContext::solverProgram() const VL_MT_SAFE {
+    const VerilatedLockGuard lock{m_mutex};
+    return m_ns.m_solverProgram;
+}
 void VerilatedContext::quiet(bool flag) VL_MT_SAFE {
     const VerilatedLockGuard lock{m_mutex};
     m_s.m_quiet = flag;

include/verilated.h

@@ -396,6 +396,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_solverProgram;  // SMT solver program
         VlOs::DeltaCpuTime m_cpuTimeStart{false};  // CPU time, starts when create first model
         VlOs::DeltaWallTime m_wallTimeStart{false};  // Wall time, starts when create first model
         std::vector<traceBaseModelCb_t> m_traceBaseModelCbs;  // Callbacks to traceRegisterModel
@@ -624,6 +625,10 @@ public:
     void profVltFilename(const std::string& flag) VL_MT_SAFE;
     std::string profVltFilename() const VL_MT_SAFE;
 
+    // Internal: SMT solver program
+    void solverProgram(const std::string& flag) VL_MT_SAFE;
+    std::string solverProgram() const VL_MT_SAFE;
+
     // Internal: Find scope
     const VerilatedScope* scopeFind(const char* namep) const VL_MT_SAFE;
     const VerilatedScopeNameMap* scopeNameMap() VL_MT_SAFE;

include/verilated_funcs.h

@@ -115,6 +115,9 @@ extern void VL_PRINTTIMESCALE(const char* namep, const char* timeunitp,
 extern WDataOutP _vl_moddiv_w(int lbits, WDataOutP owp, WDataInP const lwp, WDataInP const rwp,
                               bool is_modulus) VL_MT_SAFE;
 
+extern void _vl_vsss_based(WDataOutP owp, int obits, int baseLog2, const char* strp,
+                           size_t posstart, size_t posend) VL_MT_SAFE;
+
 extern IData VL_FGETS_IXI(int obits, void* destp, IData fpi) VL_MT_SAFE;
 
 extern void VL_FFLUSH_I(IData fdi) VL_MT_SAFE;

include/verilated_random.cpp

@@ -0,0 +1,424 @@
+// -*- mode: C++; c-file-style: "cc-mode" -*-
+//*************************************************************************
+//
+// Code available from: https://verilator.org
+//
+// Copyright 2024 by Wilson Snyder.  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-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 <iostream>
+#include <sstream>
+#include <streambuf>
+
+#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 Process 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];
+
+public:
+    typedef std::streambuf::traits_type traits_type;
+
+protected:
+    int overflow(int c = traits_type::eof()) override {
+        char c2 = static_cast<char>(c);
+        if (pbase() == pptr()) return 0;
+        size_t size = pptr() - pbase();
+        ssize_t n = ::write(m_writeFd, pbase(), size);
+        if (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();
+        ssize_t n = ::read(m_readFd, m_readBuf, sizeof(m_readBuf));
+        if (n == -1) perror("read");
+        if (n <= 0) {
+            wait_report();
+            return traits_type::eof();
+        }
+        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 Process(const char* const* const cmd = nullptr)
+        : std::streambuf{}
+        , std::iostream{this}
+        , m_cmd{cmd} {
+        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, "Process", 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 (pipe(fd_stdin) != 0) {
+            perror("Process::open: pipe");
+            return false;
+        }
+        if (pipe(fd_stdout) != 0) {
+            perror("Process::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;
+        }
+
+        const pid_t pid = fork();
+        if (pid < 0) {
+            perror("Process::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 << "Process::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
+    }
+};
+
+static Process& getSolver() {
+    static Process 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_BV)\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;
+}
+
+//======================================================================
+// VlRandomizer:: Methods
+
+void VlRandomVar::emit(std::ostream& s) const { s << m_name; }
+void VlRandomConst::emit(std::ostream& s) const {
+    s << "#b";
+    for (int i = 0; i < m_width; i++) s << (VL_BITISSET_Q(m_val, m_width - i - 1) ? '1' : '0');
+}
+void VlRandomBinOp::emit(std::ostream& s) const {
+    s << '(' << m_op << ' ';
+    m_lhs->emit(s);
+    s << ' ';
+    m_rhs->emit(s);
+    s << ')';
+}
+void VlRandomExtract::emit(std::ostream& s) const {
+    s << "((_ extract " << m_idx << ' ' << m_idx << ") ";
+    m_expr->emit(s);
+    s << ')';
+}
+bool VlRandomVar::set(std::string&& val) const {
+    VlWide<VL_WQ_WORDS_E> qowp;
+    VL_SET_WQ(qowp, 0ULL);
+    WDataOutP owp = qowp;
+    int obits = width();
+    if (obits > VL_QUADSIZE) owp = reinterpret_cast<WDataOutP>(datap());
+    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;
+    }
+    if (obits <= VL_BYTESIZE) {
+        CData* const p = static_cast<CData*>(datap());
+        *p = VL_CLEAN_II(obits, obits, owp[0]);
+    } else if (obits <= VL_SHORTSIZE) {
+        SData* const p = static_cast<SData*>(datap());
+        *p = VL_CLEAN_II(obits, obits, owp[0]);
+    } else if (obits <= VL_IDATASIZE) {
+        IData* const p = static_cast<IData*>(datap());
+        *p = VL_CLEAN_II(obits, obits, owp[0]);
+    } else if (obits <= VL_QUADSIZE) {
+        QData* const p = static_cast<QData*>(datap());
+        *p = VL_CLEAN_QQ(obits, obits, VL_SET_QW(owp));
+    } else {
+        _vl_clean_inplace_w(obits, owp);
+    }
+    return true;
+}
+
+std::shared_ptr<const VlRandomExpr> VlRandomizer::randomConstraint(VlRNG& rngr, int bits) {
+    unsigned long long hash = VL_RANDOM_RNG_I(rngr) & ((1 << bits) - 1);
+    std::shared_ptr<const VlRandomExpr> concat = nullptr;
+    std::vector<std::shared_ptr<const VlRandomExpr>> varbits;
+    for (const auto& var : m_vars) {
+        for (int i = 0; i < var.second->width(); i++)
+            varbits.emplace_back(std::make_shared<const VlRandomExtract>(var.second, i));
+    }
+    for (int i = 0; i < bits; i++) {
+        std::shared_ptr<const VlRandomExpr> bit = nullptr;
+        for (unsigned j = 0; j * 2 < varbits.size(); j++) {
+            unsigned idx = j + VL_RANDOM_RNG_I(rngr) % (varbits.size() - j);
+            auto sel = varbits[idx];
+            std::swap(varbits[idx], varbits[j]);
+            bit = bit == nullptr ? sel : std::make_shared<const VlRandomBinOp>("bvxor", bit, sel);
+        }
+        concat = concat == nullptr ? bit
+                                   : std::make_shared<const VlRandomBinOp>("concat", concat, bit);
+    }
+    return std::make_shared<const VlRandomBinOp>(
+        "=", concat, std::make_shared<const VlRandomConst>(hash, bits));
+}
+
+bool VlRandomizer::next(VlRNG& rngr) {
+    if (m_vars.empty()) return true;
+    std::iostream& f = getSolver();
+    if (!f) return false;
+
+    f << "(set-option :produce-models true)\n";
+    f << "(set-logic QF_BV)\n";
+    for (const auto& var : m_vars) {
+        f << "(declare-fun " << var.second->name() << " () (_ BitVec " << var.second->width()
+          << "))\n";
+    }
+    for (const std::string& constraint : m_constraints) { f << "(assert " << constraint << ")\n"; }
+    f << "(check-sat)\n";
+
+    bool sat = parseSolution(f);
+    if (!sat) {
+        f << "(reset)\n";
+        return false;
+    }
+
+    for (int i = 0; i < _VL_SOLVER_HASH_LEN_TOTAL && sat; i++) {
+        f << "(assert ";
+        randomConstraint(rngr, _VL_SOLVER_HASH_LEN)->emit(f);
+        f << ")\n";
+        f << "\n(check-sat)\n";
+        sat = parseSolution(f);
+    }
+
+    f << "(reset)\n";
+    return true;
+}
+
+bool VlRandomizer::parseSolution(std::iostream& f) {
+    std::string sat;
+    do { std::getline(f, 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;
+    }
+
+    f << "(get-value (";
+    for (const auto& var : m_vars) f << var.second->name() << ' ';
+    f << "))\n";
+
+    // Quasi-parse S-expression of the form ((x #xVALUE) (y #bVALUE) (z #xVALUE))
+    char c;
+    f >> c;
+    if (c != '(') {
+        VL_WARN_MT(__FILE__, __LINE__, "randomize",
+                   "Internal: Unable to parse solver's response: invalid S-expression");
+        return false;
+    }
+
+    while (true) {
+        f >> 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, value;
+        f >> name;
+        std::getline(f, value, ')');
+
+        auto it = m_vars.find(name);
+        if (it == m_vars.end()) continue;
+
+        it->second->set(std::move(value));
+    }
+
+    return true;
+}
+
+void VlRandomizer::hard(std::string&& constraint) {
+    m_constraints.emplace_back(std::move(constraint));
+}
+
+#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());
+    }
+    for (const std::string& c : m_constraints) VL_PRINTF("Constraint: %s\n", c.c_str());
+}
+#endif

include/verilated_random.h

@@ -0,0 +1,120 @@
+// -*- mode: C++; c-file-style: "cc-mode" -*-
+//*************************************************************************
+//
+// Code available from: https://verilator.org
+//
+// Copyright 2024 by Wilson Snyder.  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-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+//
+//*************************************************************************
+///
+/// \file
+/// \brief Verilated randomization header
+///
+/// This file is included automatically by Verilator in some of the C++ files
+/// it generates if randomization features are used.
+///
+/// This file is not part of the Verilated public-facing API.
+/// It is only for internal use.
+///
+/// See the internals documentation docs/internals.rst for details.
+///
+//*************************************************************************
+#ifndef VERILATOR_VERILATED_RANDOM_H_
+#define VERILATOR_VERILATED_RANDOM_H_
+
+#include "verilated.h"
+
+//=============================================================================
+// VlRandomExpr and subclasses represent expressions for the constraint solver.
+
+class VlRandomExpr VL_NOT_FINAL {
+public:
+    virtual void emit(std::ostream& s) const = 0;
+};
+class VlRandomVar final : public VlRandomExpr {
+    const char* const m_name;  // Variable name
+    void* const m_datap;  // Reference to variable data
+    const int m_width;  // Variable width in bits
+
+public:
+    VlRandomVar(const char* name, int width, void* datap)
+        : m_name{name}
+        , m_datap{datap}
+        , m_width{width} {}
+    const char* name() const { return m_name; }
+    int width() const { return m_width; }
+    void* datap() const { return m_datap; }
+    bool set(std::string&&) const;
+    void emit(std::ostream& s) const;
+};
+
+class VlRandomConst final : public VlRandomExpr {
+    const QData m_val;  // Constant value
+    const int m_width;  // Constant width in bits
+
+public:
+    VlRandomConst(QData val, int width)
+        : m_val{val}
+        , m_width{width} {
+        assert(width <= sizeof(m_val) * 8);
+    }
+    void emit(std::ostream& s) const;
+};
+
+class VlRandomExtract final : public VlRandomExpr {
+    const std::shared_ptr<const VlRandomExpr> m_expr;  // Sub-expression
+    const unsigned m_idx;  // Extracted index
+
+public:
+    VlRandomExtract(std::shared_ptr<const VlRandomExpr> expr, unsigned idx)
+        : m_expr{expr}
+        , m_idx{idx} {}
+    void emit(std::ostream& s) const;
+};
+
+class VlRandomBinOp final : public VlRandomExpr {
+    const char* const m_op;  // Binary operation identifier
+    const std::shared_ptr<const VlRandomExpr> m_lhs, m_rhs;  // Sub-expressions
+
+public:
+    VlRandomBinOp(const char* op, std::shared_ptr<const VlRandomExpr> lhs,
+                  std::shared_ptr<const VlRandomExpr> rhs)
+        : m_op{op}
+        , m_lhs{lhs}
+        , m_rhs{rhs} {}
+    void emit(std::ostream& s) const;
+};
+
+//=============================================================================
+// VlRandomizer is the object holding constraints and variable references.
+
+class VlRandomizer final {
+    // MEMBERS
+    std::vector<std::string> m_constraints;  // Solver-dependent constraints
+    std::map<std::string, std::shared_ptr<const VlRandomVar>>
+        m_vars;  // Solver-dependent variables
+
+    // PRIVATE METHODS
+    std::shared_ptr<const VlRandomExpr> randomConstraint(VlRNG& rngr, int bits);
+    bool parseSolution(std::iostream& file);
+
+public:
+    // METHODS
+    // Finds the next solution satisfying the constraints
+    bool next(VlRNG& rngr);
+    template <typename T>
+    void write_var(T& var, int width, const char* name) {
+        auto it = m_vars.find(name);
+        if (it != m_vars.end()) return;
+        m_vars[name] = std::make_shared<const VlRandomVar>(name, width, &var);
+    }
+    void hard(std::string&& constraint);
+#ifdef VL_DEBUG
+    void dump() const;
+#endif
+};
+
+#endif  // Guard

src/Makefile_obj.in

@@ -56,6 +56,7 @@ pkgdatadir = @pkgdatadir@
 # Compile options
 CFG_WITH_CCWARN = @CFG_WITH_CCWARN@
 CFG_WITH_DEFENV = @CFG_WITH_DEFENV@
+CFG_WITH_SOLVER = @CFG_WITH_SOLVER@
 CPPFLAGS += @CPPFLAGS@
 CFLAGS += @CFLAGS@
 CXXFLAGS += @CXXFLAGS@
@@ -125,6 +126,13 @@ ifeq ($(CFG_WITH_DEFENV),yes)
  else
   CPPFLAGS += -DDEFENV_VERILATOR_ROOT=\"$(VERILATOR_ROOT)\"
  endif
+ ifneq ($(CFG_WITH_SOLVER),no)
+  CPPFLAGS += -DDEFENV_VERILATOR_SOLVER='"$(CFG_WITH_SOLVER)"'
+ else
+  ifneq ($(VERILATOR_SOLVER),)
+   CPPFLAGS += -DDEFENV_VERILATOR_SOLVER='"$(VERILATOR_SOLVER)"'
+  endif
+ endif
 endif
 
 HEADERS = $(wildcard V*.h v*.h)

src/V3Ast.h

@@ -559,6 +559,7 @@ public:
         DYNAMIC_TRIGGER_SCHEDULER,
         FORK_SYNC,
         PROCESS_REFERENCE,
+        RANDOM_GENERATOR,
         // Unsigned and two state; fundamental types
         UINT32,
         UINT64,
@@ -592,6 +593,7 @@ public:
                                             "VlDynamicTriggerScheduler",
                                             "VlFork",
                                             "VlProcessRef",
+                                            "VlRandomizer",
                                             "IData",
                                             "QData",
                                             "LOGIC_IMPLICIT",
@@ -599,20 +601,13 @@ public:
         return names[m_e];
     }
     const char* dpiType() const {
-        static const char* const names[] = {"%E-unk",        "svBit",
+        static const char* const names[]
-                                            "char",          "void*",
+            = {"%E-unk",       "svBit",           "char",          "void*",        "char",
-                                            "char",          "int",
+               "int",          "%E-integer",      "svLogic",       "long long",    "double",
-                                            "%E-integer",    "svLogic",
+               "short",        "%E-time",         "const char*",   "%E-untyped",   "dpiScope",
-                                            "long long",     "double",
+               "const char*",  "%E-mtaskstate",   "%E-triggervec", "%E-dly-sched", "%E-trig-sched",
-                                            "short",         "%E-time",
+               "%E-dyn-sched", "%E-fork",         "%E-proc-ref",   "%E-rand-gen",  "IData",
-                                            "const char*",   "%E-untyped",
+               "QData",        "%E-logic-implct", " MAX"};
-                                            "dpiScope",      "const char*",
-                                            "%E-mtaskstate", "%E-triggervec",
-                                            "%E-dly-sched",  "%E-trig-sched",
-                                            "%E-dyn-sched",  "%E-fork",
-                                            "%E-proc-ref",   "IData",
-                                            "QData",         "%E-logic-implct",
-                                            " MAX"};
         return names[m_e];
     }
     static void selfTest() {
@@ -652,6 +647,7 @@ public:
         case DYNAMIC_TRIGGER_SCHEDULER: return 0;  // opaque
         case FORK_SYNC: return 0;  // opaque
         case PROCESS_REFERENCE: return 0;  // opaque
+        case RANDOM_GENERATOR: return 0;  // opaque
         case UINT32: return 32;
         case UINT64: return 64;
         default: return 0;
@@ -691,7 +687,8 @@ public:
         return (m_e == EVENT || m_e == STRING || m_e == SCOPEPTR || m_e == CHARPTR
                 || m_e == MTASKSTATE || m_e == TRIGGERVEC || m_e == DELAY_SCHEDULER
                 || m_e == TRIGGER_SCHEDULER || m_e == DYNAMIC_TRIGGER_SCHEDULER || m_e == FORK_SYNC
-                || m_e == PROCESS_REFERENCE || m_e == DOUBLE || m_e == UNTYPED);
+                || m_e == PROCESS_REFERENCE || m_e == RANDOM_GENERATOR || m_e == DOUBLE
+                || m_e == UNTYPED);
     }
     bool isDouble() const VL_MT_SAFE { return m_e == DOUBLE; }
     bool isEvent() const { return m_e == EVENT; }

src/V3AstNodeDType.h

@@ -428,6 +428,9 @@ public:
     bool isDynamicTriggerScheduler() const VL_MT_SAFE {
         return keyword() == VBasicDTypeKwd::DYNAMIC_TRIGGER_SCHEDULER;
     }
+    bool isRandomGenerator() const VL_MT_SAFE {
+        return keyword() == VBasicDTypeKwd::RANDOM_GENERATOR;
+    }
     bool isOpaque() const VL_MT_SAFE { return keyword().isOpaque(); }
     bool isString() const VL_MT_SAFE { return keyword().isString(); }
     bool isZeroInit() const { return keyword().isZeroInit(); }

src/V3AstNodeExpr.h

@@ -56,6 +56,7 @@ public:
     virtual string emitVerilog() = 0;  /// Format string for verilog writing; see V3EmitV
     // For documentation on emitC format see EmitCFunc::emitOpName
     virtual string emitC() = 0;
+    virtual string emitSMT() const { V3ERROR_NA_RETURN(""); };
     virtual string emitSimpleOperator() { return ""; }  // "" means not ok to use
     virtual bool emitCheckMaxWords() { return false; }  // Check VL_MULS_MAX_WORDS
     virtual bool cleanOut() const = 0;  // True if output has extra upper bits zero
@@ -2401,6 +2402,7 @@ public:
         out.opConcat(lhs, rhs);
     }
     string emitC() override { return "VL_CONCAT_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(concat %l %r)"; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
     bool cleanRhs() const override { return true; }
@@ -2447,6 +2449,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f/ %r)"; }
     string emitC() override { return "VL_DIV_%nq%lq%rq(%lw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvudiv %l %r)"; }
     bool cleanOut() const override { return false; }
     bool cleanLhs() const override { return true; }
     bool cleanRhs() const override { return true; }
@@ -2493,6 +2496,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f/ %r)"; }
     string emitC() override { return "VL_DIVS_%nq%lq%rq(%lw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvsdiv %l %r)"; }
     bool cleanOut() const override { return false; }
     bool cleanLhs() const override { return true; }
     bool cleanRhs() const override { return true; }
@@ -2519,6 +2523,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f==? %r)"; }
     string emitC() override { return "VL_EQ_%lq(%lW, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(= %l %r)"; }
     string emitSimpleOperator() override { return "=="; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -2641,6 +2646,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f> %r)"; }
     string emitC() override { return "VL_GT_%lq(%lW, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvugt %l %r)"; }
     string emitSimpleOperator() override { return ">"; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -2711,6 +2717,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f> %r)"; }
     string emitC() override { return "VL_GTS_%nq%lq%rq(%lw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvsgt %l %r)"; }
     string emitSimpleOperator() override { return ""; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -2734,6 +2741,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f>= %r)"; }
     string emitC() override { return "VL_GTE_%lq(%lW, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvuge %l %r)"; }
     string emitSimpleOperator() override { return ">="; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -2804,6 +2812,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f>= %r)"; }
     string emitC() override { return "VL_GTES_%nq%lq%rq(%lw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvsge %l %r)"; }
     string emitSimpleOperator() override { return ""; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -2827,6 +2836,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f&& %r)"; }
     string emitC() override { return "VL_LOGAND_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(and %l %r)"; }
     string emitSimpleOperator() override { return "&&"; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -2850,6 +2860,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f-> %r)"; }
     string emitC() override { return "VL_LOGIF_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(=> %l %r)"; }
     string emitSimpleOperator() override { return "->"; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -2873,6 +2884,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f|| %r)"; }
     string emitC() override { return "VL_LOGOR_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(or %l %r)"; }
     string emitSimpleOperator() override { return "||"; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -2896,6 +2908,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f< %r)"; }
     string emitC() override { return "VL_LT_%lq(%lW, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvult %l %r)"; }
     string emitSimpleOperator() override { return "<"; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -2966,6 +2979,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f< %r)"; }
     string emitC() override { return "VL_LTS_%nq%lq%rq(%lw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvslt %l %r)"; }
     string emitSimpleOperator() override { return ""; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -2989,6 +3003,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f<= %r)"; }
     string emitC() override { return "VL_LTE_%lq(%lW, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvule %l %r)"; }
     string emitSimpleOperator() override { return "<="; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -3059,6 +3074,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f<= %r)"; }
     string emitC() override { return "VL_LTES_%nq%lq%rq(%lw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvsle %l %r)"; }
     string emitSimpleOperator() override { return ""; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -3082,6 +3098,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f%% %r)"; }
     string emitC() override { return "VL_MODDIV_%nq%lq%rq(%lw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvurem %l %r)"; }
     bool cleanOut() const override { return false; }
     bool cleanLhs() const override { return true; }
     bool cleanRhs() const override { return true; }
@@ -3104,6 +3121,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f%% %r)"; }
     string emitC() override { return "VL_MODDIVS_%nq%lq%rq(%lw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvsmod %l %r)"; }
     bool cleanOut() const override { return false; }
     bool cleanLhs() const override { return true; }
     bool cleanRhs() const override { return true; }
@@ -3277,6 +3295,9 @@ public:
     }
     string emitVerilog() override { return "%f{%r{%k%l}}"; }
     string emitC() override { return "VL_REPLICATE_%nq%lq%rq(%lw, %P, %li, %ri)"; }
+    string emitSMT() const override {
+        return "((_ repeat " + cvtToStr(width() / lhsp()->width()) + ") %l)";
+    }
     bool cleanOut() const override { return false; }
     bool cleanLhs() const override { return true; }
     bool cleanRhs() const override { return true; }
@@ -3325,6 +3346,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f<< %r)"; }
     string emitC() override { return "VL_SHIFTL_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvshl %l %r)"; }
     string emitSimpleOperator() override {
         return (rhsp()->isWide() || rhsp()->isQuad()) ? "" : "<<";
     }
@@ -3373,6 +3395,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f>> %r)"; }
     string emitC() override { return "VL_SHIFTR_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvlshr %l %r)"; }
     string emitSimpleOperator() override {
         return (rhsp()->isWide() || rhsp()->isQuad()) ? "" : ">>";
     }
@@ -3425,6 +3448,7 @@ public:
         out.opShiftRS(lhs, rhs, lhsp()->widthMinV());
     }
     string emitVerilog() override { return "%k(%l %f>>> %r)"; }
+    string emitSMT() const override { return "(bvashr %l %r)"; }
     string emitC() override { return "VL_SHIFTRS_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; }
     string emitSimpleOperator() override { return ""; }
     bool cleanOut() const override { return false; }
@@ -3476,6 +3500,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f- %r)"; }
     string emitC() override { return "VL_SUB_%lq(%lW, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvsub %l %r)"; }
     string emitSimpleOperator() override { return "-"; }
     bool cleanOut() const override { return false; }
     bool cleanLhs() const override { return false; }
@@ -3552,6 +3577,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f== %r)"; }
     string emitC() override { return "VL_EQ_%lq(%lW, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(= %l %r)"; }
     string emitSimpleOperator() override { return "=="; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -3668,6 +3694,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f<-> %r)"; }
     string emitC() override { return "VL_LOGEQ_%nq%lq%rq(%nw,%lw,%rw, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvxnor %l %r)"; }
     string emitSimpleOperator() override { return "<->"; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -3692,6 +3719,7 @@ public:
     string emitVerilog() override { return "%k(%l %f!= %r)"; }
     string emitC() override { return "VL_NEQ_%lq(%lW, %P, %li, %ri)"; }
     string emitSimpleOperator() override { return "!="; }
+    string emitSMT() const override { return "(not (= %l %r))"; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
     bool cleanRhs() const override { return true; }
@@ -3809,6 +3837,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f+ %r)"; }
     string emitC() override { return "VL_ADD_%lq(%lW, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvadd %l %r)"; }
     string emitSimpleOperator() override { return "+"; }
     bool cleanOut() const override { return false; }
     bool cleanLhs() const override { return false; }
@@ -3855,6 +3884,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f& %r)"; }
     string emitC() override { return "VL_AND_%lq(%lW, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvand %l %r)"; }
     string emitSimpleOperator() override { return "&"; }
     bool cleanOut() const override { V3ERROR_NA_RETURN(false); }
     bool cleanLhs() const override { return false; }
@@ -3878,6 +3908,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f* %r)"; }
     string emitC() override { return "VL_MUL_%lq(%lW, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvmul %l %r)"; }
     string emitSimpleOperator() override { return "*"; }
     bool cleanOut() const override { return false; }
     bool cleanLhs() const override { return true; }
@@ -3950,6 +3981,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f| %r)"; }
     string emitC() override { return "VL_OR_%lq(%lW, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvor %l %r)"; }
     string emitSimpleOperator() override { return "|"; }
     bool cleanOut() const override { V3ERROR_NA_RETURN(false); }
     bool cleanLhs() const override { return false; }
@@ -3973,6 +4005,7 @@ public:
     }
     string emitVerilog() override { return "%k(%l %f^ %r)"; }
     string emitC() override { return "VL_XOR_%lq(%lW, %P, %li, %ri)"; }
+    string emitSMT() const override { return "(bvxor %l %r)"; }
     string emitSimpleOperator() override { return "^"; }
     bool cleanOut() const override { return false; }  // Lclean && Rclean
     bool cleanLhs() const override { return false; }
@@ -4895,6 +4928,9 @@ public:
     void numberOperate(V3Number& out, const V3Number& lhs) override { out.opAssign(lhs); }
     string emitVerilog() override { return "%l"; }
     string emitC() override { return "VL_EXTEND_%nq%lq(%nw,%lw, %P, %li)"; }
+    string emitSMT() const override {
+        return "((_ zero_extend " + cvtToStr(width() - lhsp()->width()) + ") %l)";
+    }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
     bool sizeMattersLhs() const override {
@@ -4918,6 +4954,9 @@ public:
     }
     string emitVerilog() override { return "%l"; }
     string emitC() override { return "VL_EXTENDS_%nq%lq(%nw,%lw, %P, %li)"; }
+    string emitSMT() const override {
+        return "((_ sign_extend " + cvtToStr(width() - lhsp()->width()) + ") %l)";
+    }
     bool cleanOut() const override { return false; }
     bool cleanLhs() const override { return true; }
     bool sizeMattersLhs() const override {
@@ -5050,6 +5089,7 @@ public:
     void numberOperate(V3Number& out, const V3Number& lhs) override { out.opLogNot(lhs); }
     string emitVerilog() override { return "%f(! %l)"; }
     string emitC() override { return "VL_LOGNOT_%nq%lq(%nw,%lw, %P, %li)"; }
+    string emitSMT() const override { return "(not %l)"; }
     string emitSimpleOperator() override { return "!"; }
     bool cleanOut() const override { return true; }
     bool cleanLhs() const override { return true; }
@@ -5080,6 +5120,7 @@ public:
     void numberOperate(V3Number& out, const V3Number& lhs) override { out.opNegate(lhs); }
     string emitVerilog() override { return "%f(- %l)"; }
     string emitC() override { return "VL_NEGATE_%lq(%lW, %P, %li)"; }
+    string emitSMT() const override { return "(bvneg %l)"; }
     string emitSimpleOperator() override { return "-"; }
     bool cleanOut() const override { return false; }
     bool cleanLhs() const override { return false; }
@@ -5112,6 +5153,7 @@ public:
     void numberOperate(V3Number& out, const V3Number& lhs) override { out.opNot(lhs); }
     string emitVerilog() override { return "%f(~ %l)"; }
     string emitC() override { return "VL_NOT_%lq(%lW, %P, %li)"; }
+    string emitSMT() const override { return "(bvnot %l)"; }
     string emitSimpleOperator() override { return "~"; }
     bool cleanOut() const override { return false; }
     bool cleanLhs() const override { return false; }

src/V3AstNodes.cpp

@@ -843,6 +843,8 @@ AstNodeDType::CTypeRecursed AstNodeDType::cTypeRecurse(bool compound, bool packe
             info.m_type = "VlForkSync";
         } else if (bdtypep->isProcessRef()) {
             info.m_type = "VlProcessRef";
+        } else if (bdtypep->isRandomGenerator()) {
+            info.m_type = "VlRandomizer";
         } else if (bdtypep->isEvent()) {
             info.m_type = v3Global.assignsEvents() ? "VlAssignableEvent" : "VlEvent";
         } else if (dtypep->widthMin() <= 8) {  // Handle unpacked arrays; not bdtypep->width
@@ -2737,6 +2739,7 @@ void AstCMethodHard::setPurity() {
                                                           {"find_last_index", true},
                                                           {"fire", false},
                                                           {"first", false},
+                                                          {"hard", false},
                                                           {"init", false},
                                                           {"insert", false},
                                                           {"inside", true},
@@ -2776,7 +2779,8 @@ void AstCMethodHard::setPurity() {
                                                           {"trigger", false},
                                                           {"unique", true},
                                                           {"unique_index", true},
-                                                          {"word", true}};
+                                                          {"word", true},
+                                                          {"write_var", false}};
 
     auto isPureIt = isPureMethod.find(name());
     UASSERT_OBJ(isPureIt != isPureMethod.end(), this, "Unknown purity of method " + name());

src/V3Common.cpp

@@ -113,7 +113,9 @@ static void makeToStringMiddle(AstClass* nodep) {
     std::string comma;
     for (AstNode* itemp = nodep->membersp(); itemp; itemp = itemp->nextp()) {
         if (const auto* const varp = VN_CAST(itemp, Var)) {
-            if (!varp->isParam() && !varp->isInternal()) {
+            if (!varp->isParam() && !varp->isInternal()
+                && !(varp->dtypeSkipRefp()->basicp()
+                     && varp->dtypeSkipRefp()->basicp()->isRandomGenerator())) {
                 string stmt = "out += \"";
                 stmt += comma;
                 comma = ", ";

src/V3EmitCFunc.cpp

@@ -722,6 +722,8 @@ string EmitCFunc::emitVarResetRecurse(const AstVar* varp, const string& varNameP
         return "";
     } else if (basicp && basicp->isDynamicTriggerScheduler()) {
         return "";
+    } else if (basicp && basicp->isRandomGenerator()) {
+        return "";
     } else if (basicp) {
         const bool zeroit
             = (varp->attrFileDescr()  // Zero so we don't do file IO if never $fopen

src/V3EmitCHeaders.cpp

@@ -515,6 +515,7 @@ class EmitCHeader final : public EmitCConstInit {
         if (v3Global.opt.savable()) puts("#include \"verilated_save.h\"\n");
         if (v3Global.opt.coverage()) puts("#include \"verilated_cov.h\"\n");
         if (v3Global.usesTiming()) puts("#include \"verilated_timing.h\"\n");
+        if (v3Global.useRandomizeMethods()) puts("#include \"verilated_random.h\"\n");
 
         std::set<string> cuse_set;
         auto add_to_cuse_set = [&](string s) { cuse_set.insert(s); };

src/V3EmitCMake.cpp

@@ -85,6 +85,9 @@ class CMakeEmitter final {
         cmake_set(*of, "VERILATOR_ROOT",
                   V3OutFormatter::quoteNameControls(V3Options::getenvVERILATOR_ROOT()), "PATH",
                   "Path to Verilator kit (from $VERILATOR_ROOT)");
+        cmake_set(*of, "VERILATOR_SOLVER",
+                  V3OutFormatter::quoteNameControls(V3Options::getenvVERILATOR_SOLVER()), "STRING",
+                  "Default SMT solver for constrained randomization (from $VERILATOR_SOLVER)");
 
         *of << "\n### Compiler flags...\n";
 
@@ -160,6 +163,9 @@ class CMakeEmitter final {
         if (v3Global.usesTiming()) {
             global.emplace_back("${VERILATOR_ROOT}/include/verilated_timing.cpp");
         }
+        if (v3Global.useRandomizeMethods()) {
+            global.emplace_back("${VERILATOR_ROOT}/include/verilated_random.cpp");
+        }
         global.emplace_back("${VERILATOR_ROOT}/include/verilated_threads.cpp");
         if (v3Global.opt.usesProfiler()) {
             global.emplace_back("${VERILATOR_ROOT}/include/verilated_profiler.cpp");

src/V3EmitMk.cpp

@@ -106,6 +106,8 @@ public:
                     }
                     if (v3Global.usesProbDist()) putMakeClassEntry(of, "verilated_probdist.cpp");
                     if (v3Global.usesTiming()) putMakeClassEntry(of, "verilated_timing.cpp");
+                    if (v3Global.useRandomizeMethods())
+                        putMakeClassEntry(of, "verilated_random.cpp");
                     putMakeClassEntry(of, "verilated_threads.cpp");
                     if (v3Global.opt.usesProfiler()) {
                         putMakeClassEntry(of, "verilated_profiler.cpp");
@@ -187,6 +189,10 @@ public:
 
         of.puts("# User CFLAGS (from -CFLAGS on Verilator command line)\n");
         of.puts("VM_USER_CFLAGS = \\\n");
+        const std::string solver = V3Options::getenvVERILATOR_SOLVER();
+        if (v3Global.useRandomizeMethods() && solver != "")
+            of.puts("\t-DVM_SOLVER_DEFAULT='\"" + V3OutFormatter::quoteNameControls(solver)
+                    + "\"' \\\n");
         if (!v3Global.opt.libCreate().empty()) of.puts("\t-fPIC \\\n");
         const V3StringList& cFlags = v3Global.opt.cFlags();
         for (const string& i : cFlags) of.puts("\t" + i + " \\\n");

src/V3Options.cpp

@@ -750,6 +750,18 @@ string V3Options::getenvVERILATOR_ROOT() {
     return V3Os::filenameCleanup(var);
 }
 
+string V3Options::getenvVERILATOR_SOLVER() {
+    string var = V3Os::getenvStr("VERILATOR_SOLVER", "");
+    // Treat compiled-in DEFENV string literals as C-strings to enable
+    // binary patching for relocatable installs (e.g. conda)
+    string defenv = string{DEFENV_VERILATOR_SOLVER}.c_str();
+    if (var == "" && defenv != "") {
+        var = defenv;
+        V3Os::setenvStr("VERILATOR_SOLVER", var, "Hardcoded at build time");
+    }
+    return var;
+}
+
 string V3Options::getStdPackagePath() {
     return V3Os::filenameJoin(getenvVERILATOR_ROOT(), "include", "verilated_std.sv");
 }

src/V3Options.h

@@ -717,6 +717,7 @@ public:
     static string getenvSYSTEMC_INCLUDE();
     static string getenvSYSTEMC_LIBDIR();
     static string getenvVERILATOR_ROOT();
+    static string getenvVERILATOR_SOLVER();
     static string getStdPackagePath();
     static string getSupported(const string& var);
     static bool systemCSystemWide();

src/V3Randomize.cpp

@@ -39,24 +39,28 @@ class RandomizeMarkVisitor final : public VNVisitorConst {
     // NODE STATE
     // Cleared on Netlist
     //  AstClass::user1()       -> bool.  Set true to indicate needs randomize processing
+    //  AstConstraintExpr::user1() -> bool.  Set true to indicate state-dependent
+    //  AstNodeExpr::user1()    -> bool.  Set true to indicate constraint expression depending on a
+    //                                    randomized variable
     const VNUser1InUse m_inuser1;
 
     using DerivedSet = std::unordered_set<AstClass*>;
-    using BaseToDerivedMap = std::unordered_map<AstClass*, DerivedSet>;
+    using BaseToDerivedMap = std::unordered_map<const AstClass*, DerivedSet>;
 
     BaseToDerivedMap m_baseToDerivedMap;  // Mapping from base classes to classes that extend them
     AstClass* m_classp = nullptr;  // Current class
+    AstConstraintExpr* m_constraintExprp = nullptr;  // Current constraint expression
 
     // METHODS
-    void markMembers(AstClass* nodep) {
+    void markMembers(const AstClass* nodep) {
-        for (auto* classp = nodep; classp;
+        for (const AstClass* classp = nodep; classp;
              classp = classp->extendsp() ? classp->extendsp()->classp() : nullptr) {
-            for (auto* memberp = classp->stmtsp(); memberp; memberp = memberp->nextp()) {
+            for (const AstNode* memberp = classp->stmtsp(); memberp; memberp = memberp->nextp()) {
                 // If member is rand and of class type, mark its class
                 if (VN_IS(memberp, Var) && VN_AS(memberp, Var)->isRand()) {
-                    if (const auto* const classRefp
+                    if (const AstClassRefDType* const classRefp
                         = VN_CAST(memberp->dtypep()->skipRefp(), ClassRefDType)) {
-                        auto* const rclassp = classRefp->classp();
+                        AstClass* const rclassp = classRefp->classp();
                         if (!rclassp->user1()) {
                             rclassp->user1(true);
                             markMembers(rclassp);
@@ -67,11 +71,11 @@ class RandomizeMarkVisitor final : public VNVisitorConst {
             }
         }
     }
-    void markDerived(AstClass* nodep) {
+    void markDerived(const AstClass* nodep) {
         const auto it = m_baseToDerivedMap.find(nodep);
         if (it != m_baseToDerivedMap.end()) {
             for (auto* classp : it->second) {
-                if (!classp->user1p()) {
+                if (!classp->user1()) {
                     classp->user1(true);
                     markMembers(classp);
                     markDerived(classp);
@@ -92,7 +96,7 @@ class RandomizeMarkVisitor final : public VNVisitorConst {
         iterateChildrenConst(nodep);
         if (nodep->extendsp()) {
             // Save pointer to derived class
-            AstClass* const basep = nodep->extendsp()->classp();
+            const AstClass* const basep = nodep->extendsp()->classp();
             m_baseToDerivedMap[basep].insert(nodep);
         }
     }
@@ -111,6 +115,22 @@ class RandomizeMarkVisitor final : public VNVisitorConst {
         if (nodep->name() != "randomize") return;
         if (m_classp) m_classp->user1(true);
     }
+    void visit(AstConstraintExpr* nodep) override {
+        VL_RESTORER(m_constraintExprp);
+        m_constraintExprp = nodep;
+        iterateChildrenConst(nodep);
+    }
+    void visit(AstNodeVarRef* nodep) override {
+        if (!m_constraintExprp) return;
+        if (!nodep->varp()->isRand()) {
+            m_constraintExprp->user1(true);
+            nodep->v3warn(CONSTRAINTIGN, "State-dependent constraint ignored (unsupported)");
+            return;
+        }
+        for (AstNode* backp = nodep; backp != m_constraintExprp && !backp->user1();
+             backp = backp->backp())
+            backp->user1(true);
+    }
 
     void visit(AstNode* nodep) override { iterateChildrenConst(nodep); }
 
@@ -123,6 +143,143 @@ public:
     ~RandomizeMarkVisitor() override = default;
 };
 
+//######################################################################
+// Visitor that turns constraints into template strings for solvers
+
+class ConstraintExprVisitor final : public VNVisitor {
+    // NODE STATE
+    //  AstVar::user4()         -> bool. Handled in constraints
+    //  AstNodeExpr::user1()    -> bool. Depending on a randomized variable
+    // VNUser4InUse    m_inuser4;      (Allocated for use in RandomizeVisitor)
+
+    AstTask* const m_taskp;  // X_setup_constraint() method of the constraint
+    AstVar* const m_genp;  // VlRandomizer variable of the class
+
+    bool editFormat(AstNodeExpr* nodep) {
+        if (nodep->user1()) return false;
+        // Replace computable expression with SMT constant
+        VNRelinker handle;
+        nodep->unlinkFrBack(&handle);
+        AstSFormatF* const newp = new AstSFormatF{
+            nodep->fileline(), (nodep->width() & 3) ? "#b%b" : "#x%x", false, nodep};
+        handle.relink(newp);
+        return true;
+    }
+    void editSMT(AstNodeExpr* nodep, AstNodeExpr* lhsp = nullptr, AstNodeExpr* rhsp = nullptr) {
+        // Replace incomputable (result-dependent) expression with SMT expression
+        std::string smtExpr = nodep->emitSMT();  // Might need child width (AstExtend)
+        UASSERT_OBJ(smtExpr != "", nodep,
+                    "Node needs randomization constraint, but no emitSMT: " << nodep);
+
+        if (lhsp) lhsp = VN_AS(iterateSubtreeReturnEdits(lhsp->unlinkFrBack()), NodeExpr);
+        if (rhsp) rhsp = VN_AS(iterateSubtreeReturnEdits(rhsp->unlinkFrBack()), NodeExpr);
+
+        AstNodeExpr* argsp = nullptr;
+        for (string::iterator pos = smtExpr.begin(); pos != smtExpr.end(); ++pos) {
+            if (pos[0] == '%') {
+                ++pos;
+                switch (pos[0]) {
+                case '%': break;
+                case 'l':
+                    pos[0] = '@';
+                    UASSERT_OBJ(lhsp, nodep, "emitSMT() references undef node");
+                    argsp = AstNode::addNext(argsp, lhsp);
+                    lhsp = nullptr;
+                    break;
+                case 'r':
+                    pos[0] = '@';
+                    UASSERT_OBJ(rhsp, nodep, "emitSMT() references undef node");
+                    argsp = AstNode::addNext(argsp, rhsp);
+                    rhsp = nullptr;
+                    break;
+                default: nodep->v3fatalSrc("Unknown emitSMT format code: %" << pos[0]); break;
+                }
+            }
+        }
+        UASSERT_OBJ(!lhsp, nodep, "Missing emitSMT %l for " << lhsp);
+        UASSERT_OBJ(!rhsp, nodep, "Missing emitSMT %r for " << rhsp);
+        AstSFormatF* const newp = new AstSFormatF{nodep->fileline(), smtExpr, false, argsp};
+        nodep->replaceWith(newp);
+        VL_DO_DANGLING(pushDeletep(nodep), nodep);
+    }
+
+    // VISITORS
+    void visit(AstNodeVarRef* nodep) override {
+        if (editFormat(nodep)) return;
+        // In SMT just variable name, but we also ensure write_var for the variable
+        const std::string smtName = nodep->name();  // Can be anything unique
+        nodep->replaceWith(new AstSFormatF{nodep->fileline(), smtName, false, nullptr});
+
+        AstVar* const varp = nodep->varp();
+
+        VL_DO_DANGLING(pushDeletep(nodep), nodep);
+
+        if (!varp->user4()) {
+            varp->user4(true);
+            AstCMethodHard* const methodp = new AstCMethodHard{
+                varp->fileline(), new AstVarRef{varp->fileline(), m_genp, VAccess::READWRITE},
+                "write_var"};
+            methodp->dtypeSetVoid();
+            methodp->addPinsp(new AstVarRef{varp->fileline(), varp, VAccess::WRITE});
+            methodp->addPinsp(new AstConst{varp->dtypep()->fileline(), AstConst::Unsized64{},
+                                           (size_t)varp->width()});
+            AstNodeExpr* const varnamep
+                = new AstCExpr{varp->fileline(), "\"" + smtName + "\"", varp->width()};
+            varnamep->dtypep(varp->dtypep());
+            methodp->addPinsp(varnamep);
+            m_taskp->addStmtsp(new AstStmtExpr{varp->fileline(), methodp});
+        }
+    }
+    void visit(AstNodeBiop* nodep) override {
+        if (editFormat(nodep)) return;
+        editSMT(nodep, nodep->lhsp(), nodep->rhsp());
+    }
+    void visit(AstNodeUniop* nodep) override {
+        if (editFormat(nodep)) return;
+        editSMT(nodep, nodep->lhsp());
+    }
+    void visit(AstReplicate* nodep) override {
+        // Biop, but RHS is harmful
+        if (editFormat(nodep)) return;
+        editSMT(nodep, nodep->srcp());
+    }
+    void visit(AstSFormatF* nodep) override {}
+    void visit(AstConstraintExpr* nodep) override { iterateChildren(nodep); }
+    void visit(AstCMethodHard* nodep) override {
+        if (editFormat(nodep)) return;
+
+        UASSERT_OBJ(nodep->name() == "size", nodep, "Non-size method call in constraints");
+
+        AstNode* fromp = nodep->fromp();
+        // Warn early while the dtype is still there
+        fromp->v3warn(E_UNSUPPORTED, "Unsupported: random member variable with type "
+                                         << fromp->dtypep()->prettyDTypeNameQ());
+
+        iterateChildren(nodep);  // Might change fromp
+        fromp = nodep->fromp()->unlinkFrBack();
+        fromp->dtypep(nodep->dtypep());
+        nodep->replaceWith(fromp);
+        VL_DO_DANGLING(pushDeletep(nodep), nodep);
+    }
+    void visit(AstNodeExpr* nodep) override {
+        if (editFormat(nodep)) return;
+        nodep->v3fatalSrc(
+            "Visit function missing? Constraint function missing for math node: " << nodep);
+    }
+    void visit(AstNode* nodep) override {
+        nodep->v3fatalSrc(
+            "Visit function missing? Constraint function missing for node: " << nodep);
+    }
+
+public:
+    // CONSTRUCTORS
+    explicit ConstraintExprVisitor(AstConstraintExpr* nodep, AstTask* taskp, AstVar* genp)
+        : m_taskp(taskp)
+        , m_genp(genp) {
+        iterate(nodep);
+    }
+};
+
 //######################################################################
 // Visitor that defines a randomize method where needed
 
@@ -130,10 +287,15 @@ class RandomizeVisitor final : public VNVisitor {
     // NODE STATE
     // Cleared on Netlist
     //  AstClass::user1()       -> bool.  Set true to indicate needs randomize processing
+    //  AstConstraintExpr::user1() -> bool.  Set true to indicate state-dependent
     //  AstEnumDType::user2()   -> AstVar*.  Pointer to table with enum values
     //  AstClass::user3()       -> AstFunc*. Pointer to randomize() method of a class
+    //  AstVar::user4()         -> bool. Handled in constraints
+    //  AstClass::user4()       -> AstVar*.  Constrained randomizer variable
     // VNUser1InUse    m_inuser1;      (Allocated for use in RandomizeMarkVisitor)
     const VNUser2InUse m_inuser2;
+    const VNUser3InUse m_inuser3;
+    const VNUser4InUse m_inuser4;
 
     // STATE
     VMemberMap m_memberMap;  // Member names cached for fast lookup
@@ -274,6 +436,12 @@ class RandomizeVisitor final : public VNVisitor {
             funcp->addStmtsp(callp->makeStmt());
         }
     }
+    AstTask* newSetupConstraintTask(AstClass* nodep, const std::string& name) {
+        AstTask* const taskp = new AstTask{nodep->fileline(), name + "_setup_constraint", nullptr};
+        taskp->classMethod(true);
+        nodep->addMembersp(taskp);
+        return taskp;
+    }
 
     // VISITORS
     void visit(AstNodeModule* nodep) override {
@@ -315,20 +483,28 @@ class RandomizeVisitor final : public VNVisitor {
                 beginValp = baseRandCallp;
             }
         }
+        if (m_modp->user4p()) {
+            AstNode* const argsp = new AstVarRef{nodep->fileline(), VN_AS(m_modp->user4p(), Var),
+                                                 VAccess::READWRITE};
+            argsp->addNext(new AstText{fl, ".next(__Vm_rng)"});
+            AstNodeExpr* const solverCallp = new AstCExpr{fl, argsp};
+            solverCallp->dtypeSetBit();
+            beginValp = beginValp ? new AstAnd{fl, beginValp, solverCallp} : solverCallp;
+        }
         if (!beginValp) beginValp = new AstConst{fl, AstConst::WidthedValue{}, 32, 1};
 
         funcp->addStmtsp(new AstAssign{fl, new AstVarRef{fl, fvarp, VAccess::WRITE}, beginValp});
 
-        for (auto* memberp = nodep->stmtsp(); memberp; memberp = memberp->nextp()) {
+        for (AstNode* memberp = nodep->stmtsp(); memberp; memberp = memberp->nextp()) {
             AstVar* const memberVarp = VN_CAST(memberp, Var);
-            if (!memberVarp || !memberVarp->isRand()) continue;
+            if (!memberVarp || !memberVarp->isRand() || memberVarp->user4()) continue;
             const AstNodeDType* const dtypep = memberp->dtypep()->skipRefp();
             if (VN_IS(dtypep, BasicDType) || VN_IS(dtypep, StructDType)) {
                 AstVar* const randcVarp = newRandcVarsp(memberVarp);
                 AstVarRef* const refp = new AstVarRef{fl, memberVarp, VAccess::WRITE};
                 AstNodeStmt* const stmtp = newRandStmtsp(fl, refp, randcVarp);
                 funcp->addStmtsp(stmtp);
-            } else if (const auto* const classRefp = VN_CAST(dtypep, ClassRefDType)) {
+            } else if (const AstClassRefDType* const classRefp = VN_CAST(dtypep, ClassRefDType)) {
                 if (classRefp->classp() == nodep) {
                     memberp->v3warn(
                         E_UNSUPPORTED,
@@ -358,8 +534,40 @@ class RandomizeVisitor final : public VNVisitor {
         nodep->user1(false);
     }
     void visit(AstConstraint* nodep) override {
-        nodep->v3warn(CONSTRAINTIGN, "Constraint ignored (unsupported)");
+        AstNodeFTask* const newp = VN_AS(m_memberMap.findMember(m_modp, "new"), NodeFTask);
-        if (!v3Global.opt.xmlOnly()) VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
+        UASSERT_OBJ(newp, m_modp, "No new() in class");
+        AstTask* const taskp = newSetupConstraintTask(VN_AS(m_modp, Class), nodep->name());
+        AstTaskRef* const setupTaskRefp
+            = new AstTaskRef{nodep->fileline(), taskp->name(), nullptr};
+        setupTaskRefp->taskp(taskp);
+        newp->addStmtsp(new AstStmtExpr{nodep->fileline(), setupTaskRefp});
+
+        AstVar* genp = VN_AS(m_modp->user4p(), Var);
+        if (!genp) {
+            genp = new AstVar(nodep->fileline(), VVarType::MEMBER, "constraint",
+                              m_modp->findBasicDType(VBasicDTypeKwd::RANDOM_GENERATOR));
+            VN_AS(m_modp, Class)->addMembersp(genp);
+            m_modp->user4p(genp);
+        }
+
+        while (nodep->itemsp()) {
+            AstConstraintExpr* const condsp = VN_CAST(nodep->itemsp(), ConstraintExpr);
+            if (!condsp || condsp->user1()) {
+                nodep->itemsp()->v3warn(CONSTRAINTIGN,
+                                        "Constraint expression ignored (unsupported)");
+                pushDeletep(nodep->itemsp()->unlinkFrBack());
+                continue;
+            }
+            { ConstraintExprVisitor{condsp->unlinkFrBack(), taskp, genp}; }
+            // Only hard constraints are now supported
+            AstCMethodHard* const methodp = new AstCMethodHard{
+                condsp->fileline(), new AstVarRef{condsp->fileline(), genp, VAccess::READWRITE},
+                "hard", condsp->exprp()->unlinkFrBack()};
+            methodp->dtypeSetVoid();
+            taskp->addStmtsp(new AstStmtExpr{condsp->fileline(), methodp});
+            VL_DO_DANGLING(condsp->deleteTree(), condsp);
+        }
+        VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
     }
     void visit(AstRandCase* nodep) override {
         // RANDCASE

src/config_build.h

@@ -50,6 +50,9 @@
 #ifndef DEFENV_VERILATOR_ROOT
 # define DEFENV_VERILATOR_ROOT ""
 #endif
+#ifndef DEFENV_VERILATOR_SOLVER
+# define DEFENV_VERILATOR_SOLVER ""
+#endif
 // clang-format on
 
 //**********************************************************************

test_regress/t/t_constraint.v

@@ -21,9 +21,7 @@ module t (/*AUTOARG*/);
       p = new;
       v = p.randomize();
       if (v != 1) $stop;
-`ifndef VERILATOR
       if (p.one != 1) $stop;
-`endif
 
       $write("*-* All Finished *-*\n");
       $finish;

test_regress/t/t_constraint_json_only.out

@@ -48,7 +48,164 @@
           {"type":"VARREF","name":"strings_equal","addr":"(JB)","loc":"d,60:7,60:13","dtypep":"(U)","access":"WR","varp":"(BB)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"}
         ],"timingControlp": []}
       ],"scopeNamep": []},
-      {"type":"FUNC","name":"new","addr":"(KB)","loc":"d,7:1,7:6","dtypep":"(LB)","method":true,"dpiExport":false,"dpiImport":false,"dpiOpenChild":false,"dpiOpenParent":false,"prototype":false,"recursive":false,"taskPublic":false,"cname":"new","fvarp": [],"classOrPackagep": [],"stmtsp": [],"scopeNamep": []}
+      {"type":"FUNC","name":"new","addr":"(KB)","loc":"d,7:1,7:6","dtypep":"(LB)","method":true,"dpiExport":false,"dpiImport":false,"dpiOpenChild":false,"dpiOpenParent":false,"prototype":false,"recursive":false,"taskPublic":false,"cname":"new","fvarp": [],"classOrPackagep": [],
+       "stmtsp": [
+        {"type":"STMTEXPR","name":"","addr":"(MB)","loc":"d,19:15,19:20",
+         "exprp": [
+          {"type":"TASKREF","name":"empty_setup_constraint","addr":"(NB)","loc":"d,19:15,19:20","dtypep":"(LB)","dotted":"","taskp":"(OB)","classOrPackagep":"UNLINKED","namep": [],"pinsp": [],"scopeNamep": []}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(PB)","loc":"d,21:15,21:19",
+         "exprp": [
+          {"type":"TASKREF","name":"size_setup_constraint","addr":"(QB)","loc":"d,21:15,21:19","dtypep":"(LB)","dotted":"","taskp":"(RB)","classOrPackagep":"UNLINKED","namep": [],"pinsp": [],"scopeNamep": []}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(SB)","loc":"d,28:15,28:18",
+         "exprp": [
+          {"type":"TASKREF","name":"ifs_setup_constraint","addr":"(TB)","loc":"d,28:15,28:18","dtypep":"(LB)","dotted":"","taskp":"(UB)","classOrPackagep":"UNLINKED","namep": [],"pinsp": [],"scopeNamep": []}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(VB)","loc":"d,39:15,39:23",
+         "exprp": [
+          {"type":"TASKREF","name":"arr_uniq_setup_constraint","addr":"(WB)","loc":"d,39:15,39:23","dtypep":"(LB)","dotted":"","taskp":"(XB)","classOrPackagep":"UNLINKED","namep": [],"pinsp": [],"scopeNamep": []}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(YB)","loc":"d,46:15,46:20",
+         "exprp": [
+          {"type":"TASKREF","name":"order_setup_constraint","addr":"(ZB)","loc":"d,46:15,46:20","dtypep":"(LB)","dotted":"","taskp":"(AC)","classOrPackagep":"UNLINKED","namep": [],"pinsp": [],"scopeNamep": []}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(BC)","loc":"d,48:15,48:18",
+         "exprp": [
+          {"type":"TASKREF","name":"dis_setup_constraint","addr":"(CC)","loc":"d,48:15,48:18","dtypep":"(LB)","dotted":"","taskp":"(DC)","classOrPackagep":"UNLINKED","namep": [],"pinsp": [],"scopeNamep": []}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(EC)","loc":"d,54:15,54:19",
+         "exprp": [
+          {"type":"TASKREF","name":"meth_setup_constraint","addr":"(FC)","loc":"d,54:15,54:19","dtypep":"(LB)","dotted":"","taskp":"(GC)","classOrPackagep":"UNLINKED","namep": [],"pinsp": [],"scopeNamep": []}
+        ]}
+      ],"scopeNamep": []},
+      {"type":"TASK","name":"empty_setup_constraint","addr":"(OB)","loc":"d,7:1,7:6","method":true,"dpiExport":false,"dpiImport":false,"dpiOpenChild":false,"dpiOpenParent":false,"prototype":false,"recursive":false,"taskPublic":false,"cname":"empty_setup_constraint","fvarp": [],"classOrPackagep": [],"stmtsp": [],"scopeNamep": []},
+      {"type":"VAR","name":"constraint","addr":"(HC)","loc":"d,19:15,19:20","dtypep":"(IC)","origName":"constraint","isSc":false,"isPrimaryIO":false,"direction":"NONE","isConst":false,"isPullup":false,"isPulldown":false,"isUsedClock":false,"isSigPublic":false,"isLatched":false,"isUsedLoopIdx":false,"noReset":false,"attrIsolateAssign":false,"attrFileDescr":false,"isDpiOpenArray":false,"isFuncReturn":false,"isFuncLocal":false,"attrClocker":"UNKNOWN","lifetime":"NONE","varType":"MEMBER","dtypeName":"VlRandomizer","isSigUserRdPublic":false,"isSigUserRWPublic":false,"isGParam":false,"isParam":false,"attrScBv":false,"attrSFormat":false,"sensIfacep":"UNLINKED","childDTypep": [],"delayp": [],"valuep": [],"attrsp": []},
+      {"type":"TASK","name":"size_setup_constraint","addr":"(RB)","loc":"d,7:1,7:6","method":true,"dpiExport":false,"dpiImport":false,"dpiOpenChild":false,"dpiOpenParent":false,"prototype":false,"recursive":false,"taskPublic":false,"cname":"size_setup_constraint","fvarp": [],"classOrPackagep": [],
+       "stmtsp": [
+        {"type":"STMTEXPR","name":"","addr":"(JC)","loc":"d,8:13,8:19",
+         "exprp": [
+          {"type":"CMETHODHARD","name":"write_var","addr":"(KC)","loc":"d,8:13,8:19","dtypep":"(LB)",
+           "fromp": [
+            {"type":"VARREF","name":"constraint","addr":"(LC)","loc":"d,8:13,8:19","dtypep":"(IC)","access":"RW","varp":"(HC)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"}
+          ],
+           "pinsp": [
+            {"type":"VARREF","name":"header","addr":"(MC)","loc":"d,8:13,8:19","dtypep":"(Q)","access":"WR","varp":"(P)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"},
+            {"type":"CONST","name":"64'h20","addr":"(NC)","loc":"d,8:9,8:12","dtypep":"(OC)"},
+            {"type":"CEXPR","name":"","addr":"(PC)","loc":"d,8:13,8:19","dtypep":"(Q)",
+             "exprsp": [
+              {"type":"TEXT","name":"","addr":"(QC)","loc":"d,8:13,8:19","shortText":"\"header\""}
+            ]}
+          ]}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(RC)","loc":"d,22:18,22:20",
+         "exprp": [
+          {"type":"CMETHODHARD","name":"hard","addr":"(SC)","loc":"d,22:18,22:20","dtypep":"(LB)",
+           "fromp": [
+            {"type":"VARREF","name":"constraint","addr":"(TC)","loc":"d,22:18,22:20","dtypep":"(IC)","access":"RW","varp":"(HC)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"}
+          ],
+           "pinsp": [
+            {"type":"CONST","name":"\\\"(and (bvsgt header #x00000000) (bvsle header #x00000007))\\\"","addr":"(UC)","loc":"d,22:18,22:20","dtypep":"(M)"}
+          ]}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(VC)","loc":"d,9:13,9:19",
+         "exprp": [
+          {"type":"CMETHODHARD","name":"write_var","addr":"(WC)","loc":"d,9:13,9:19","dtypep":"(LB)",
+           "fromp": [
+            {"type":"VARREF","name":"constraint","addr":"(XC)","loc":"d,9:13,9:19","dtypep":"(IC)","access":"RW","varp":"(HC)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"}
+          ],
+           "pinsp": [
+            {"type":"VARREF","name":"length","addr":"(YC)","loc":"d,9:13,9:19","dtypep":"(Q)","access":"WR","varp":"(R)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"},
+            {"type":"CONST","name":"64'h20","addr":"(ZC)","loc":"d,8:9,8:12","dtypep":"(OC)"},
+            {"type":"CEXPR","name":"","addr":"(AD)","loc":"d,9:13,9:19","dtypep":"(Q)",
+             "exprsp": [
+              {"type":"TEXT","name":"","addr":"(BD)","loc":"d,9:13,9:19","shortText":"\"length\""}
+            ]}
+          ]}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(CD)","loc":"d,23:14,23:16",
+         "exprp": [
+          {"type":"CMETHODHARD","name":"hard","addr":"(DD)","loc":"d,23:14,23:16","dtypep":"(LB)",
+           "fromp": [
+            {"type":"VARREF","name":"constraint","addr":"(ED)","loc":"d,23:14,23:16","dtypep":"(IC)","access":"RW","varp":"(HC)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"}
+          ],
+           "pinsp": [
+            {"type":"CONST","name":"\\\"(bvsle length #x0000000f)\\\"","addr":"(FD)","loc":"d,23:14,23:16","dtypep":"(M)"}
+          ]}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(GD)","loc":"d,24:14,24:16",
+         "exprp": [
+          {"type":"CMETHODHARD","name":"hard","addr":"(HD)","loc":"d,24:14,24:16","dtypep":"(LB)",
+           "fromp": [
+            {"type":"VARREF","name":"constraint","addr":"(ID)","loc":"d,24:14,24:16","dtypep":"(IC)","access":"RW","varp":"(HC)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"}
+          ],
+           "pinsp": [
+            {"type":"CONST","name":"\\\"(bvsge length header)\\\"","addr":"(JD)","loc":"d,24:14,24:16","dtypep":"(M)"}
+          ]}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(KD)","loc":"d,25:7,25:13",
+         "exprp": [
+          {"type":"CMETHODHARD","name":"hard","addr":"(LD)","loc":"d,25:7,25:13","dtypep":"(LB)",
+           "fromp": [
+            {"type":"VARREF","name":"constraint","addr":"(MD)","loc":"d,25:7,25:13","dtypep":"(IC)","access":"RW","varp":"(HC)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"}
+          ],
+           "pinsp": [
+            {"type":"CONST","name":"\\\"length\\\"","addr":"(ND)","loc":"d,25:7,25:13","dtypep":"(M)"}
+          ]}
+        ]}
+      ],"scopeNamep": []},
+      {"type":"TASK","name":"ifs_setup_constraint","addr":"(UB)","loc":"d,7:1,7:6","method":true,"dpiExport":false,"dpiImport":false,"dpiOpenChild":false,"dpiOpenParent":false,"prototype":false,"recursive":false,"taskPublic":false,"cname":"ifs_setup_constraint","fvarp": [],"classOrPackagep": [],"stmtsp": [],"scopeNamep": []},
+      {"type":"TASK","name":"arr_uniq_setup_constraint","addr":"(XB)","loc":"d,7:1,7:6","method":true,"dpiExport":false,"dpiImport":false,"dpiOpenChild":false,"dpiOpenParent":false,"prototype":false,"recursive":false,"taskPublic":false,"cname":"arr_uniq_setup_constraint","fvarp": [],"classOrPackagep": [],"stmtsp": [],"scopeNamep": []},
+      {"type":"TASK","name":"order_setup_constraint","addr":"(AC)","loc":"d,7:1,7:6","method":true,"dpiExport":false,"dpiImport":false,"dpiOpenChild":false,"dpiOpenParent":false,"prototype":false,"recursive":false,"taskPublic":false,"cname":"order_setup_constraint","fvarp": [],"classOrPackagep": [],"stmtsp": [],"scopeNamep": []},
+      {"type":"TASK","name":"dis_setup_constraint","addr":"(DC)","loc":"d,7:1,7:6","method":true,"dpiExport":false,"dpiImport":false,"dpiOpenChild":false,"dpiOpenParent":false,"prototype":false,"recursive":false,"taskPublic":false,"cname":"dis_setup_constraint","fvarp": [],"classOrPackagep": [],
+       "stmtsp": [
+        {"type":"STMTEXPR","name":"","addr":"(OD)","loc":"d,10:13,10:22",
+         "exprp": [
+          {"type":"CMETHODHARD","name":"write_var","addr":"(PD)","loc":"d,10:13,10:22","dtypep":"(LB)",
+           "fromp": [
+            {"type":"VARREF","name":"constraint","addr":"(QD)","loc":"d,10:13,10:22","dtypep":"(IC)","access":"RW","varp":"(HC)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"}
+          ],
+           "pinsp": [
+            {"type":"VARREF","name":"sublength","addr":"(RD)","loc":"d,10:13,10:22","dtypep":"(Q)","access":"WR","varp":"(S)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"},
+            {"type":"CONST","name":"64'h20","addr":"(SD)","loc":"d,8:9,8:12","dtypep":"(OC)"},
+            {"type":"CEXPR","name":"","addr":"(TD)","loc":"d,10:13,10:22","dtypep":"(Q)",
+             "exprsp": [
+              {"type":"TEXT","name":"","addr":"(UD)","loc":"d,10:13,10:22","shortText":"\"sublength\""}
+            ]}
+          ]}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(VD)","loc":"d,49:7,49:11",
+         "exprp": [
+          {"type":"CMETHODHARD","name":"hard","addr":"(WD)","loc":"d,49:7,49:11","dtypep":"(LB)",
+           "fromp": [
+            {"type":"VARREF","name":"constraint","addr":"(XD)","loc":"d,49:7,49:11","dtypep":"(IC)","access":"RW","varp":"(HC)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"}
+          ],
+           "pinsp": [
+            {"type":"CONST","name":"\\\"sublength\\\"","addr":"(YD)","loc":"d,49:12,49:21","dtypep":"(M)"}
+          ]}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(ZD)","loc":"d,50:7,50:14",
+         "exprp": [
+          {"type":"CMETHODHARD","name":"hard","addr":"(AE)","loc":"d,50:7,50:14","dtypep":"(LB)",
+           "fromp": [
+            {"type":"VARREF","name":"constraint","addr":"(BE)","loc":"d,50:7,50:14","dtypep":"(IC)","access":"RW","varp":"(HC)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"}
+          ],
+           "pinsp": [
+            {"type":"CONST","name":"\\\"sublength\\\"","addr":"(CE)","loc":"d,50:20,50:29","dtypep":"(M)"}
+          ]}
+        ]},
+        {"type":"STMTEXPR","name":"","addr":"(DE)","loc":"d,51:17,51:19",
+         "exprp": [
+          {"type":"CMETHODHARD","name":"hard","addr":"(EE)","loc":"d,51:17,51:19","dtypep":"(LB)",
+           "fromp": [
+            {"type":"VARREF","name":"constraint","addr":"(FE)","loc":"d,51:17,51:19","dtypep":"(IC)","access":"RW","varp":"(HC)","varScopep":"UNLINKED","classOrPackagep":"UNLINKED"}
+          ],
+           "pinsp": [
+            {"type":"CONST","name":"\\\"(bvsle sublength length)\\\"","addr":"(GE)","loc":"d,51:17,51:19","dtypep":"(M)"}
+          ]}
+        ]}
+      ],"scopeNamep": []},
+      {"type":"TASK","name":"meth_setup_constraint","addr":"(GC)","loc":"d,7:1,7:6","method":true,"dpiExport":false,"dpiImport":false,"dpiOpenChild":false,"dpiOpenParent":false,"prototype":false,"recursive":false,"taskPublic":false,"cname":"meth_setup_constraint","fvarp": [],"classOrPackagep": [],"stmtsp": [],"scopeNamep": []}
     ],"activesp": [],"extendsp": []}
   ],"activesp": []}
 ],"filesp": [],
@@ -56,28 +213,30 @@
   {"type":"TYPETABLE","name":"","addr":"(C)","loc":"a,0:0,0:0","constraintRefp":"UNLINKED","emptyQueuep":"UNLINKED","queueIndexp":"UNLINKED","streamp":"UNLINKED","voidp":"(LB)",
    "typesp": [
     {"type":"BASICDTYPE","name":"logic","addr":"(GB)","loc":"d,22:14,22:15","dtypep":"(GB)","keyword":"logic","generic":true,"rangep": []},
-    {"type":"BASICDTYPE","name":"logic","addr":"(MB)","loc":"d,25:21,25:22","dtypep":"(MB)","keyword":"logic","range":"31:0","generic":true,"rangep": []},
+    {"type":"BASICDTYPE","name":"logic","addr":"(HE)","loc":"d,25:21,25:22","dtypep":"(HE)","keyword":"logic","range":"31:0","generic":true,"rangep": []},
     {"type":"BASICDTYPE","name":"string","addr":"(M)","loc":"d,71:7,71:13","dtypep":"(M)","keyword":"string","generic":true,"rangep": []},
     {"type":"BASICDTYPE","name":"int","addr":"(Q)","loc":"d,8:9,8:12","dtypep":"(Q)","keyword":"int","range":"31:0","generic":true,"rangep": []},
     {"type":"BASICDTYPE","name":"bit","addr":"(U)","loc":"d,11:9,11:12","dtypep":"(U)","keyword":"bit","generic":true,"rangep": []},
     {"type":"UNPACKARRAYDTYPE","name":"","addr":"(Y)","loc":"d,15:18,15:19","dtypep":"(Y)","isCompound":false,"declRange":"[0:1]","generic":false,"refDTypep":"(Q)","childDTypep": [],
      "rangep": [
-      {"type":"RANGE","name":"","addr":"(NB)","loc":"d,15:18,15:19","ascending":true,
+      {"type":"RANGE","name":"","addr":"(IE)","loc":"d,15:18,15:19","ascending":true,
        "leftp": [
-        {"type":"CONST","name":"32'h0","addr":"(OB)","loc":"d,15:19,15:20","dtypep":"(MB)"}
+        {"type":"CONST","name":"32'h0","addr":"(JE)","loc":"d,15:19,15:20","dtypep":"(HE)"}
       ],
        "rightp": [
-        {"type":"CONST","name":"32'h1","addr":"(PB)","loc":"d,15:19,15:20","dtypep":"(MB)"}
+        {"type":"CONST","name":"32'h1","addr":"(KE)","loc":"d,15:19,15:20","dtypep":"(HE)"}
       ]}
     ]},
     {"type":"VOIDDTYPE","name":"","addr":"(LB)","loc":"d,7:1,7:6","dtypep":"(LB)","generic":false},
-    {"type":"CLASSREFDTYPE","name":"Packet","addr":"(H)","loc":"d,67:4,67:10","dtypep":"(H)","generic":false,"classp":"(O)","classOrPackagep":"(O)","paramsp": []}
+    {"type":"CLASSREFDTYPE","name":"Packet","addr":"(H)","loc":"d,67:4,67:10","dtypep":"(H)","generic":false,"classp":"(O)","classOrPackagep":"(O)","paramsp": []},
+    {"type":"BASICDTYPE","name":"VlRandomizer","addr":"(IC)","loc":"d,7:1,7:6","dtypep":"(IC)","keyword":"VlRandomizer","generic":true,"rangep": []},
+    {"type":"BASICDTYPE","name":"logic","addr":"(OC)","loc":"d,8:9,8:12","dtypep":"(OC)","keyword":"logic","range":"63:0","generic":true,"rangep": []}
   ]},
   {"type":"CONSTPOOL","name":"","addr":"(D)","loc":"a,0:0,0:0",
    "modulep": [
-    {"type":"MODULE","name":"@CONST-POOL@","addr":"(QB)","loc":"a,0:0,0:0","origName":"@CONST-POOL@","level":0,"modPublic":false,"inLibrary":false,"dead":false,"recursiveClone":false,"recursive":false,"timeunit":"NONE","inlinesp": [],
+    {"type":"MODULE","name":"@CONST-POOL@","addr":"(LE)","loc":"a,0:0,0:0","origName":"@CONST-POOL@","level":0,"modPublic":false,"inLibrary":false,"dead":false,"recursiveClone":false,"recursive":false,"timeunit":"NONE","inlinesp": [],
      "stmtsp": [
-      {"type":"SCOPE","name":"@CONST-POOL@","addr":"(RB)","loc":"a,0:0,0:0","aboveScopep":"UNLINKED","aboveCellp":"UNLINKED","modp":"(QB)","varsp": [],"blocksp": [],"inlinesp": []}
+      {"type":"SCOPE","name":"@CONST-POOL@","addr":"(ME)","loc":"a,0:0,0:0","aboveScopep":"UNLINKED","aboveCellp":"UNLINKED","modp":"(LE)","varsp": [],"blocksp": [],"inlinesp": []}
     ],"activesp": []}
   ]}
 ]}

test_regress/t/t_constraint_mode.v

@@ -30,9 +30,7 @@ module t (/*AUTOARG*/);
       p = new;
       v = p.randomize();
       if (v != 1) $stop;
-`ifndef VERILATOR
       if (p.m_one != 1) $stop;
-`endif
 
       // IEEE: function void object[.constraint_identifier].constraint_mode(bit on_off);
       // IEEE: function int object.constraint_identifier.constraint_mode();

test_regress/t/t_constraint_mode_warn_bad.out

@@ -12,40 +12,36 @@
                                                    : ... note: In instance 't'
    18 |       if (cons.constraint_mode() != 0) $stop;
       |                ^~~~~~~~~~~~~~~
-%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:42:9: Unsupported: 'constraint_mode' called on object
+%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:40:9: Unsupported: 'constraint_mode' called on object
                                                   : ... note: In instance 't'
-   42 |       p.constraint_mode(0);
+   40 |       p.constraint_mode(0);
       |         ^~~~~~~~~~~~~~~
-%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:43:9: Unsupported: 'constraint_mode' called on object
+%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:41:9: Unsupported: 'constraint_mode' called on object
                                                   : ... note: In instance 't'
-   43 |       p.constraint_mode(1);
+   41 |       p.constraint_mode(1);
       |         ^~~~~~~~~~~~~~~
-%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:48:14: constraint_mode ignored (unsupported)
+%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:46:14: constraint_mode ignored (unsupported)
                                                    : ... note: In instance 't'
-   48 |       p.cons.constraint_mode(1);
+   46 |       p.cons.constraint_mode(1);
       |              ^~~~~~~~~~~~~~~
-%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:49:14: constraint_mode ignored (unsupported)
+%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:47:14: constraint_mode ignored (unsupported)
                                                    : ... note: In instance 't'
-   49 |       p.cons.constraint_mode(0);
+   47 |       p.cons.constraint_mode(0);
       |              ^~~~~~~~~~~~~~~
-%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:50:18: constraint_mode ignored (unsupported)
+%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:48:18: constraint_mode ignored (unsupported)
                                                    : ... note: In instance 't'
-   50 |       if (p.cons.constraint_mode() != 0) $stop;
+   48 |       if (p.cons.constraint_mode() != 0) $stop;
       |                  ^~~~~~~~~~~~~~~
-%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:55:20: constraint_mode ignored (unsupported)
+%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:53:20: constraint_mode ignored (unsupported)
                                                    : ... note: In instance 't'
-   55 |       p.other.cons.constraint_mode(1);
+   53 |       p.other.cons.constraint_mode(1);
       |                    ^~~~~~~~~~~~~~~
-%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:56:20: constraint_mode ignored (unsupported)
+%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:54:20: constraint_mode ignored (unsupported)
                                                    : ... note: In instance 't'
-   56 |       p.other.cons.constraint_mode(0);
+   54 |       p.other.cons.constraint_mode(0);
       |                    ^~~~~~~~~~~~~~~
-%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:57:24: constraint_mode ignored (unsupported)
+%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:55:24: constraint_mode ignored (unsupported)
                                                    : ... note: In instance 't'
-   57 |       if (p.other.cons.constraint_mode() != 0) $stop;
+   55 |       if (p.other.cons.constraint_mode() != 0) $stop;
       |                        ^~~~~~~~~~~~~~~
-%Warning-CONSTRAINTIGN: t/t_constraint_mode.v:10:15: Constraint ignored (unsupported)
-                                                   : ... note: In instance 't'
-   10 |    constraint cons { m_one > 0 && m_one < 2; }
-      |               ^~~~
 %Error: Exiting due to

test_regress/t/t_constraint_nosolver_bad.out

@@ -0,0 +1,8 @@
+Process::open: execvp(someimaginarysolver): No such file or directory
+%Warning: Subprocess command `someimaginarysolver' failed: exit status 127
+%Warning: Unable to communicate with SAT solver, please check its installation or specify a different one in VERILATOR_SOLVER environment variable.
+ ... Tried: $ someimaginarysolver
+
+%Error: t/t_constraint.v:23: Verilog $stop
+Aborting...
+Aborted (core dumped)

test_regress/t/t_constraint_nosolver_bad.pl

@@ -0,0 +1,27 @@
+#!/usr/bin/env perl
+if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# Copyright 2024 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+scenarios(vlt => 1);
+
+top_filename("t/t_constraint.v");
+
+compile(
+    );
+
+execute(
+    run_env => 'VERILATOR_SOLVER=someimaginarysolver',
+    fails => 1,
+    check_finished => 0,
+    expect_filename => $Self->{golden_filename},
+    );
+
+ok(1);
+
+1;

test_regress/t/t_constraint_operators.pl

@@ -0,0 +1,22 @@
+#!/usr/bin/env perl
+if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# Copyright 2019 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+scenarios(simulator => 1);
+
+compile(
+    );
+
+execute(
+    check_finished => 1,
+    );
+
+
+ok(1);
+1;

test_regress/t/t_constraint_operators.v

@@ -0,0 +1,50 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain, for
+// any use, without warranty, 2023 by Wilson Snyder.
+// SPDX-License-Identifier: CC0-1.0
+
+class Packet;
+   rand int x;
+   rand bit [31:0] b;
+   rand bit [31:0] c;
+   rand bit tiny;
+
+   typedef bit signed [63:0] s64;
+   typedef bit [63:0] u64;
+
+   constraint arith { x + x - x == x; }
+   constraint divmod { int'((x % 5) / 2) != (b % 99) / 7; }
+   constraint mul { x * 9 != b * 3; }
+   constraint impl { tiny == 1 -> x != 10; }
+   constraint concat { {c, b} != 'h1111; }
+   constraint unary { !(-~c == 'h22); }
+   constraint log { ((b ^ c) & (b >>> c | b >> c | b << c)) > 0; }
+   constraint cmps { x < x || x <= x || x > x || x >= x; }
+   constraint cmpu { b < b || b <= b || b > b || b >= b; }
+   constraint ext { s64'(x) != u64'(tiny); }
+
+endclass
+
+module t (/*AUTOARG*/);
+
+   Packet p;
+
+   int v;
+
+   initial begin
+      p = new;
+      v = p.randomize();
+      if (v != 1) $stop;
+      if ((p.x % 5) / 2 == (p.b % 99) / 7) $stop;
+      if (p.x * 9 == p.b * 3) $stop;
+      if (p.tiny && p.x == 10) $stop;
+      if ({p.c, p.b} == 'h1111) $stop;
+      if (-~p.c == 'h22) $stop;
+      if (((p.b ^ p.c) & (p.b >>> p.c | p.b >> p.c | p.b << p.c)) <= 0) $stop;
+      if (p.x == int'(p.tiny)) $stop;
+
+      $write("*-* All Finished *-*\n");
+      $finish;
+   end
+endmodule

test_regress/t/t_constraint_xml.out

@@ -35,167 +35,6 @@
         <var loc="d,13,13,13,24" name="if_state_ok" dtype_id="4" vartype="bit" origName="if_state_ok"/>
         <var loc="d,15,13,15,18" name="array" dtype_id="5" vartype="" origName="array"/>
         <var loc="d,17,11,17,16" name="state" dtype_id="2" vartype="string" origName="state"/>
-        <constraint loc="d,19,15,19,20" name="empty"/>
-        <constraint loc="d,21,15,21,19" name="size">
-          <constraintexpr loc="d,22,18,22,20">
-            <and loc="d,22,18,22,20" dtype_id="6">
-              <lts loc="d,22,14,22,15" dtype_id="6">
-                <const loc="d,22,16,22,17" name="32&apos;sh0" dtype_id="7"/>
-                <varref loc="d,22,7,22,13" name="header" dtype_id="3"/>
-              </lts>
-              <gtes loc="d,22,28,22,30" dtype_id="6">
-                <const loc="d,22,31,22,32" name="32&apos;sh7" dtype_id="7"/>
-                <varref loc="d,22,21,22,27" name="header" dtype_id="3"/>
-              </gtes>
-            </and>
-          </constraintexpr>
-          <constraintexpr loc="d,23,14,23,16">
-            <gtes loc="d,23,14,23,16" dtype_id="6">
-              <const loc="d,23,17,23,19" name="32&apos;shf" dtype_id="7"/>
-              <varref loc="d,23,7,23,13" name="length" dtype_id="3"/>
-            </gtes>
-          </constraintexpr>
-          <constraintexpr loc="d,24,14,24,16">
-            <gtes loc="d,24,14,24,16" dtype_id="6">
-              <varref loc="d,24,7,24,13" name="length" dtype_id="3"/>
-              <varref loc="d,24,17,24,23" name="header" dtype_id="3"/>
-            </gtes>
-          </constraintexpr>
-          <constraintexpr loc="d,25,7,25,13">
-            <varref loc="d,25,7,25,13" name="length" dtype_id="3"/>
-          </constraintexpr>
-        </constraint>
-        <constraint loc="d,28,15,28,18" name="ifs">
-          <if loc="d,29,7,29,9">
-            <lts loc="d,29,18,29,19" dtype_id="6">
-              <const loc="d,29,20,29,21" name="32&apos;sh4" dtype_id="7"/>
-              <varref loc="d,29,11,29,17" name="header" dtype_id="3"/>
-            </lts>
-            <begin>
-              <constraintexpr loc="d,30,15,30,17">
-                <varref loc="d,30,10,30,14" name="if_4" dtype_id="6"/>
-              </constraintexpr>
-            </begin>
-          </if>
-          <if loc="d,32,7,32,9">
-            <or loc="d,32,23,32,25" dtype_id="6">
-              <eq loc="d,32,18,32,20" dtype_id="6">
-                <const loc="d,32,21,32,22" name="32&apos;sh5" dtype_id="7"/>
-                <varref loc="d,32,11,32,17" name="header" dtype_id="3"/>
-              </eq>
-              <eq loc="d,32,33,32,35" dtype_id="6">
-                <const loc="d,32,36,32,37" name="32&apos;sh6" dtype_id="7"/>
-                <varref loc="d,32,26,32,32" name="header" dtype_id="3"/>
-              </eq>
-            </or>
-            <begin>
-              <constraintexpr loc="d,33,18,33,20">
-                <varref loc="d,33,10,33,17" name="iff_5_6" dtype_id="6"/>
-              </constraintexpr>
-            </begin>
-            <begin>
-              <constraintexpr loc="d,35,18,35,20">
-                <not loc="d,35,18,35,20" dtype_id="4">
-                  <varref loc="d,35,10,35,17" name="iff_5_6" dtype_id="4"/>
-                </not>
-              </constraintexpr>
-            </begin>
-          </if>
-        </constraint>
-        <constraint loc="d,39,15,39,23" name="arr_uniq">
-          <constraintforeach loc="d,40,7,40,14">
-            <selloopvars loc="d,40,21,40,22">
-              <varref loc="d,40,16,40,21" name="array" dtype_id="5"/>
-              <var loc="d,40,22,40,23" name="i" dtype_id="8" vartype="integer" origName="i"/>
-            </selloopvars>
-            <constraintexpr loc="d,41,19,41,25">
-              <or loc="d,41,19,41,25" dtype_id="6">
-                <or loc="d,41,19,41,25" dtype_id="6">
-                  <eqwild loc="d,41,27,41,28" dtype_id="6">
-                    <arraysel loc="d,41,15,41,16" dtype_id="3">
-                      <varref loc="d,41,10,41,15" name="array" dtype_id="5"/>
-                      <sel loc="d,41,16,41,17" dtype_id="9">
-                        <varref loc="d,41,16,41,17" name="i" dtype_id="8"/>
-                        <const loc="d,41,16,41,17" name="32&apos;h0" dtype_id="10"/>
-                        <const loc="d,41,16,41,17" name="32&apos;h1" dtype_id="10"/>
-                      </sel>
-                    </arraysel>
-                    <const loc="d,41,27,41,28" name="32&apos;sh2" dtype_id="7"/>
-                  </eqwild>
-                  <eqwild loc="d,41,30,41,31" dtype_id="6">
-                    <arraysel loc="d,41,15,41,16" dtype_id="3">
-                      <varref loc="d,41,10,41,15" name="array" dtype_id="5"/>
-                      <sel loc="d,41,16,41,17" dtype_id="9">
-                        <varref loc="d,41,16,41,17" name="i" dtype_id="8"/>
-                        <const loc="d,41,16,41,17" name="32&apos;h0" dtype_id="10"/>
-                        <const loc="d,41,16,41,17" name="32&apos;h1" dtype_id="10"/>
-                      </sel>
-                    </arraysel>
-                    <const loc="d,41,30,41,31" name="32&apos;sh4" dtype_id="7"/>
-                  </eqwild>
-                </or>
-                <eqwild loc="d,41,33,41,34" dtype_id="6">
-                  <arraysel loc="d,41,15,41,16" dtype_id="3">
-                    <varref loc="d,41,10,41,15" name="array" dtype_id="5"/>
-                    <sel loc="d,41,16,41,17" dtype_id="9">
-                      <varref loc="d,41,16,41,17" name="i" dtype_id="8"/>
-                      <const loc="d,41,16,41,17" name="32&apos;h0" dtype_id="10"/>
-                      <const loc="d,41,16,41,17" name="32&apos;h1" dtype_id="10"/>
-                    </sel>
-                  </arraysel>
-                  <const loc="d,41,33,41,34" name="32&apos;sh6" dtype_id="7"/>
-                </eqwild>
-              </or>
-            </constraintexpr>
-          </constraintforeach>
-          <constraintunique loc="d,43,7,43,13">
-            <arraysel loc="d,43,21,43,22" dtype_id="3">
-              <varref loc="d,43,16,43,21" name="array" dtype_id="5"/>
-              <const loc="d,43,22,43,23" name="1&apos;h0" dtype_id="9"/>
-            </arraysel>
-            <arraysel loc="d,43,31,43,32" dtype_id="3">
-              <varref loc="d,43,26,43,31" name="array" dtype_id="5"/>
-              <const loc="d,43,32,43,33" name="1&apos;h1" dtype_id="9"/>
-            </arraysel>
-          </constraintunique>
-        </constraint>
-        <constraint loc="d,46,15,46,20" name="order">
-          <constraintbefore loc="d,46,23,46,28">
-            <varref loc="d,46,29,46,35" name="length" dtype_id="3"/>
-            <varref loc="d,46,43,46,49" name="header" dtype_id="3"/>
-          </constraintbefore>
-        </constraint>
-        <constraint loc="d,48,15,48,18" name="dis">
-          <constraintexpr loc="d,49,7,49,11">
-            <varref loc="d,49,12,49,21" name="sublength" dtype_id="3"/>
-          </constraintexpr>
-          <constraintexpr loc="d,50,7,50,14">
-            <varref loc="d,50,20,50,29" name="sublength" dtype_id="3"/>
-          </constraintexpr>
-          <constraintexpr loc="d,51,17,51,19">
-            <ltes loc="d,51,17,51,19" dtype_id="6">
-              <varref loc="d,51,7,51,16" name="sublength" dtype_id="3"/>
-              <varref loc="d,51,20,51,26" name="length" dtype_id="3"/>
-            </ltes>
-          </constraintexpr>
-        </constraint>
-        <constraint loc="d,54,15,54,19" name="meth">
-          <if loc="d,55,7,55,9">
-            <funcref loc="d,55,11,55,24" name="strings_equal" dtype_id="4">
-              <arg loc="d,55,25,55,30">
-                <varref loc="d,55,25,55,30" name="state" dtype_id="2"/>
-              </arg>
-              <arg loc="d,55,32,55,36">
-                <const loc="d,55,32,55,36" name="&quot;ok&quot;" dtype_id="2"/>
-              </arg>
-            </funcref>
-            <begin>
-              <constraintexpr loc="d,56,22,56,24">
-                <varref loc="d,56,10,56,21" name="if_state_ok" dtype_id="6"/>
-              </constraintexpr>
-            </begin>
-          </if>
-        </constraint>
         <func loc="d,59,17,59,30" name="strings_equal" dtype_id="4">
           <var loc="d,59,17,59,30" name="strings_equal" dtype_id="4" dir="output" vartype="bit" origName="strings_equal"/>
           <var loc="d,59,38,59,39" name="a" dtype_id="2" dir="input" vartype="string" origName="a"/>
@@ -208,14 +47,117 @@
             <varref loc="d,60,7,60,13" name="strings_equal" dtype_id="4"/>
           </assign>
         </func>
-        <func loc="d,7,1,7,6" name="new" dtype_id="11"/>
+        <func loc="d,7,1,7,6" name="new" dtype_id="7">
+          <stmtexpr loc="d,19,15,19,20">
+            <taskref loc="d,19,15,19,20" name="empty_setup_constraint" dtype_id="7"/>
+          </stmtexpr>
+          <stmtexpr loc="d,21,15,21,19">
+            <taskref loc="d,21,15,21,19" name="size_setup_constraint" dtype_id="7"/>
+          </stmtexpr>
+          <stmtexpr loc="d,28,15,28,18">
+            <taskref loc="d,28,15,28,18" name="ifs_setup_constraint" dtype_id="7"/>
+          </stmtexpr>
+          <stmtexpr loc="d,39,15,39,23">
+            <taskref loc="d,39,15,39,23" name="arr_uniq_setup_constraint" dtype_id="7"/>
+          </stmtexpr>
+          <stmtexpr loc="d,46,15,46,20">
+            <taskref loc="d,46,15,46,20" name="order_setup_constraint" dtype_id="7"/>
+          </stmtexpr>
+          <stmtexpr loc="d,48,15,48,18">
+            <taskref loc="d,48,15,48,18" name="dis_setup_constraint" dtype_id="7"/>
+          </stmtexpr>
+          <stmtexpr loc="d,54,15,54,19">
+            <taskref loc="d,54,15,54,19" name="meth_setup_constraint" dtype_id="7"/>
+          </stmtexpr>
+        </func>
+        <task loc="d,7,1,7,6" name="empty_setup_constraint"/>
+        <var loc="d,19,15,19,20" name="constraint" dtype_id="8" vartype="VlRandomizer" origName="constraint"/>
+        <task loc="d,7,1,7,6" name="size_setup_constraint">
+          <stmtexpr loc="d,8,13,8,19">
+            <cmethodhard loc="d,8,13,8,19" name="write_var" dtype_id="7">
+              <varref loc="d,8,13,8,19" name="constraint" dtype_id="8"/>
+              <varref loc="d,8,13,8,19" name="header" dtype_id="3"/>
+              <const loc="d,8,9,8,12" name="64&apos;h20" dtype_id="9"/>
+              <cexpr loc="d,8,13,8,19" dtype_id="3">
+                <text loc="d,8,13,8,19"/>
+              </cexpr>
+            </cmethodhard>
+          </stmtexpr>
+          <stmtexpr loc="d,22,18,22,20">
+            <cmethodhard loc="d,22,18,22,20" name="hard" dtype_id="7">
+              <varref loc="d,22,18,22,20" name="constraint" dtype_id="8"/>
+              <const loc="d,22,18,22,20" name="&quot;(and (bvsgt header #x00000000) (bvsle header #x00000007))&quot;" dtype_id="2"/>
+            </cmethodhard>
+          </stmtexpr>
+          <stmtexpr loc="d,9,13,9,19">
+            <cmethodhard loc="d,9,13,9,19" name="write_var" dtype_id="7">
+              <varref loc="d,9,13,9,19" name="constraint" dtype_id="8"/>
+              <varref loc="d,9,13,9,19" name="length" dtype_id="3"/>
+              <const loc="d,8,9,8,12" name="64&apos;h20" dtype_id="9"/>
+              <cexpr loc="d,9,13,9,19" dtype_id="3">
+                <text loc="d,9,13,9,19"/>
+              </cexpr>
+            </cmethodhard>
+          </stmtexpr>
+          <stmtexpr loc="d,23,14,23,16">
+            <cmethodhard loc="d,23,14,23,16" name="hard" dtype_id="7">
+              <varref loc="d,23,14,23,16" name="constraint" dtype_id="8"/>
+              <const loc="d,23,14,23,16" name="&quot;(bvsle length #x0000000f)&quot;" dtype_id="2"/>
+            </cmethodhard>
+          </stmtexpr>
+          <stmtexpr loc="d,24,14,24,16">
+            <cmethodhard loc="d,24,14,24,16" name="hard" dtype_id="7">
+              <varref loc="d,24,14,24,16" name="constraint" dtype_id="8"/>
+              <const loc="d,24,14,24,16" name="&quot;(bvsge length header)&quot;" dtype_id="2"/>
+            </cmethodhard>
+          </stmtexpr>
+          <stmtexpr loc="d,25,7,25,13">
+            <cmethodhard loc="d,25,7,25,13" name="hard" dtype_id="7">
+              <varref loc="d,25,7,25,13" name="constraint" dtype_id="8"/>
+              <const loc="d,25,7,25,13" name="&quot;length&quot;" dtype_id="2"/>
+            </cmethodhard>
+          </stmtexpr>
+        </task>
+        <task loc="d,7,1,7,6" name="ifs_setup_constraint"/>
+        <task loc="d,7,1,7,6" name="arr_uniq_setup_constraint"/>
+        <task loc="d,7,1,7,6" name="order_setup_constraint"/>
+        <task loc="d,7,1,7,6" name="dis_setup_constraint">
+          <stmtexpr loc="d,10,13,10,22">
+            <cmethodhard loc="d,10,13,10,22" name="write_var" dtype_id="7">
+              <varref loc="d,10,13,10,22" name="constraint" dtype_id="8"/>
+              <varref loc="d,10,13,10,22" name="sublength" dtype_id="3"/>
+              <const loc="d,8,9,8,12" name="64&apos;h20" dtype_id="9"/>
+              <cexpr loc="d,10,13,10,22" dtype_id="3">
+                <text loc="d,10,13,10,22"/>
+              </cexpr>
+            </cmethodhard>
+          </stmtexpr>
+          <stmtexpr loc="d,49,7,49,11">
+            <cmethodhard loc="d,49,7,49,11" name="hard" dtype_id="7">
+              <varref loc="d,49,7,49,11" name="constraint" dtype_id="8"/>
+              <const loc="d,49,12,49,21" name="&quot;sublength&quot;" dtype_id="2"/>
+            </cmethodhard>
+          </stmtexpr>
+          <stmtexpr loc="d,50,7,50,14">
+            <cmethodhard loc="d,50,7,50,14" name="hard" dtype_id="7">
+              <varref loc="d,50,7,50,14" name="constraint" dtype_id="8"/>
+              <const loc="d,50,20,50,29" name="&quot;sublength&quot;" dtype_id="2"/>
+            </cmethodhard>
+          </stmtexpr>
+          <stmtexpr loc="d,51,17,51,19">
+            <cmethodhard loc="d,51,17,51,19" name="hard" dtype_id="7">
+              <varref loc="d,51,17,51,19" name="constraint" dtype_id="8"/>
+              <const loc="d,51,17,51,19" name="&quot;(bvsle sublength length)&quot;" dtype_id="2"/>
+            </cmethodhard>
+          </stmtexpr>
+        </task>
+        <task loc="d,7,1,7,6" name="meth_setup_constraint"/>
       </class>
     </package>
     <typetable loc="a,0,0,0,0">
       <basicdtype loc="d,22,14,22,15" id="6" name="logic"/>
       <basicdtype loc="d,25,21,25,22" id="10" name="logic" left="31" right="0"/>
       <basicdtype loc="d,71,7,71,13" id="2" name="string"/>
-      <basicdtype loc="d,40,22,40,23" id="8" name="integer" left="31" right="0" signed="true"/>
       <basicdtype loc="d,8,9,8,12" id="3" name="int" left="31" right="0" signed="true"/>
       <basicdtype loc="d,11,9,11,12" id="4" name="bit"/>
       <unpackarraydtype loc="d,15,18,15,19" id="5" sub_dtype_id="3">
@@ -224,10 +166,10 @@
           <const loc="d,15,19,15,20" name="32&apos;h1" dtype_id="10"/>
         </range>
       </unpackarraydtype>
-      <basicdtype loc="d,32,18,32,20" id="9" name="logic" signed="true"/>
+      <voiddtype loc="d,7,1,7,6" id="7"/>
-      <voiddtype loc="d,7,1,7,6" id="11"/>
       <classrefdtype loc="d,67,4,67,10" id="1" name="Packet"/>
-      <basicdtype loc="d,22,16,22,17" id="7" name="logic" left="31" right="0" signed="true"/>
+      <basicdtype loc="d,7,1,7,6" id="8" name="VlRandomizer"/>
+      <basicdtype loc="d,8,9,8,12" id="9" name="logic" left="63" right="0"/>
     </typetable>
   </netlist>
 </verilator_xml>

test_regress/t/t_randomize.out

@@ -1,29 +1,29 @@
-%Warning-CONSTRAINTIGN: t/t_randomize.v:16:15: Constraint ignored (unsupported)
+%Warning-CONSTRAINTIGN: t/t_randomize.v:38:16: State-dependent constraint ignored (unsupported)
                                              : ... note: In instance 't'
-   16 |    constraint empty {}
+   38 |          array[i] inside {2, 4, 6};
-      |               ^~~~~
+      |                ^
                         ... For warning description see https://verilator.org/warn/CONSTRAINTIGN?v=latest
                         ... Use "/* verilator lint_off CONSTRAINTIGN */" and lint_on around source to disable this message.
-%Warning-CONSTRAINTIGN: t/t_randomize.v:18:15: Constraint ignored (unsupported)
+%Warning-CONSTRAINTIGN: t/t_randomize.v:26:7: Constraint expression ignored (unsupported)
                                             : ... note: In instance 't'
-   18 |    constraint size {
+   26 |       if (header > 4) {
-      |               ^~~~
+      |       ^~
-%Warning-CONSTRAINTIGN: t/t_randomize.v:25:15: Constraint ignored (unsupported)
+%Warning-CONSTRAINTIGN: t/t_randomize.v:29:7: Constraint expression ignored (unsupported)
                                             : ... note: In instance 't'
-   25 |    constraint ifs {
+   29 |       if (header == 5 || header == 6) {
-      |               ^~~
+      |       ^~
-%Warning-CONSTRAINTIGN: t/t_randomize.v:36:15: Constraint ignored (unsupported)
+%Warning-CONSTRAINTIGN: t/t_randomize.v:37:7: Constraint expression ignored (unsupported)
                                             : ... note: In instance 't'
-   36 |    constraint arr_uniq {
+   37 |       foreach (array[i]) {
-      |               ^~~~~~~~
+      |       ^~~~~~~
-%Warning-CONSTRAINTIGN: t/t_randomize.v:43:15: Constraint ignored (unsupported)
+%Warning-CONSTRAINTIGN: t/t_randomize.v:40:7: Constraint expression ignored (unsupported)
+                                            : ... note: In instance 't'
+   40 |       unique { array[0], array[1] };
+      |       ^~~~~~
+%Warning-CONSTRAINTIGN: t/t_randomize.v:43:23: Constraint expression ignored (unsupported)
                                              : ... note: In instance 't'
    43 |    constraint order { solve length before header; }
       |                       ^~~~~
-%Warning-CONSTRAINTIGN: t/t_randomize.v:45:15: Constraint ignored (unsupported)
-                                             : ... note: In instance 't'
-   45 |    constraint dis {
-      |               ^~~
 %Error-UNSUPPORTED: t/t_randomize.v:14:13: Unsupported: random member variable with type 'int$[0:1]'
                                          : ... note: In instance 't'
    14 |    rand int array[2];   

test_regress/t/t_randomize_method_constraints.pl

@@ -0,0 +1,21 @@
+#!/usr/bin/env perl
+if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# Copyright 2020 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+scenarios(simulator => 1);
+
+compile(
+    );
+
+execute(
+    check_finished => 1,
+    );
+
+ok(1);
+1;

test_regress/t/t_randomize_method_constraints.v

@@ -0,0 +1,69 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain, for
+// any use, without warranty, 2024 by Antmicro Ltd.
+// SPDX-License-Identifier: CC0-1.0
+
+typedef enum bit[15:0] {
+   ONE   = 3,
+   TWO   = 5,
+   THREE = 8,
+   FOUR  = 13
+} Enum;
+
+class Cls;
+   constraint A { v inside {ONE, THREE}; }
+   constraint B { w == 5; x inside {1,2} || x inside {4,5}; }
+   constraint C { z < 3 * 7; z > 5 + 8; u > 0; }
+
+   rand logic[79:0] u;
+   rand Enum v;
+   rand logic[63:0] w;
+   rand logic[47:0] x;
+   rand logic[31:0] y;
+   rand logic[22:0] z;
+
+   function new;
+      u = 0;
+      v = ONE;
+      w = 0;
+      x = 0;
+      y = 0;
+      z = 0;
+   endfunction
+
+endclass
+
+module t (/*AUTOARG*/);
+   Cls obj;
+
+   initial begin
+      int rand_result;
+      longint prev_checksum;
+      $display("===================\nSatisfiable constraints:");
+      for (int i = 0; i < 25; i++) begin
+         obj = new;
+         rand_result = obj.randomize();
+         $display("obj.u == %0d", obj.u);
+         $display("obj.v == %0d", obj.v);
+         $display("obj.w == %0d", obj.w);
+         $display("obj.x == %0d", obj.x);
+         $display("obj.y == %0d", obj.y);
+         $display("obj.z == %0d", obj.z);
+         $display("rand_result == %0d", rand_result);
+         $display("-------------------");
+         if (!(obj.v inside {ONE, THREE})) $stop;
+         if (obj.w != 5) $stop;
+         if (!(obj.x inside {1,2,4,5})) $stop;
+         if (obj.z <= 13 || obj.z >= 21) $stop;
+      end
+      //$display("===================\nUnsatisfiable constraints for obj.y:");
+      //rand_result = obj.randomize() with { 256 < y && y < 256; };
+      //$display("obj.y == %0d", obj.y);
+      //$display("rand_result == %0d", rand_result);
+      //if (rand_result != 0) $stop;
+      //rand_result = obj.randomize() with { 16 <= z && z <= 32; };
+      $write("*-* All Finished *-*\n");
+      $finish;
+   end
+endmodule

test_regress/t/t_randomize_method_types_unsup.out

@@ -1,12 +1,20 @@
+%Warning-CONSTRAINTIGN: t/t_randomize_method_types_unsup.v:20:30: State-dependent constraint ignored (unsupported)
+                                                                : ... note: In instance 't'
+   20 |    constraint statedep { i < st + 2; }
+      |                              ^~
+                        ... For warning description see https://verilator.org/warn/CONSTRAINTIGN?v=latest
+                        ... Use "/* verilator lint_off CONSTRAINTIGN */" and lint_on around source to disable this message.
+%Error-UNSUPPORTED: t/t_randomize_method_types_unsup.v:19:25: Unsupported: random member variable with type 'int[]'
+   19 |    constraint dynsize { dynarr.size < 20; }
+      |                         ^~~~~~
+%Warning-CONSTRAINTIGN: t/t_randomize_method_types_unsup.v:20:28: Constraint expression ignored (unsupported)
+                                                                : ... note: In instance 't'
+   20 |    constraint statedep { i < st + 2; }
+      |                            ^
 %Error-UNSUPPORTED: t/t_randomize_method_types_unsup.v:12:13: Unsupported: random member variable with type 'int[string]'
                                                             : ... note: In instance 't'
    12 |    rand int assocarr[string];
       |             ^~~~~~~~
-                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
-%Error-UNSUPPORTED: t/t_randomize_method_types_unsup.v:13:13: Unsupported: random member variable with type 'int[]'
-                                                            : ... note: In instance 't'
-   13 |    rand int dynarr[];
-      |             ^~~~~~
 %Error-UNSUPPORTED: t/t_randomize_method_types_unsup.v:14:13: Unsupported: random member variable with type 'int$[0:4]'
                                                             : ... note: In instance 't'
    14 |    rand int unpackarr[5];

test_regress/t/t_randomize_method_types_unsup.v

@@ -14,6 +14,10 @@ class Cls;
    rand int unpackarr[5];
    rand Union uni;
    rand Cls cls;
+   rand int i;
+   int st;
+   constraint dynsize { dynarr.size < 20; }
+   constraint statedep { i < st + 2; }
 endclass
 
 module t (/*AUTOARG*/);

test_regress/t/t_randomize_method_with_unsup.out

@@ -0,0 +1,11 @@
+%Error-UNSUPPORTED: t/t_randomize_method_with_unsup.v:47:40: Unsupported: randomize() 'with' constraint
+   47 |          rand_result = obj.randomize() with { lb <= y && y <= ub; };
+      |                                        ^~~~
+                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
+%Error-UNSUPPORTED: t/t_randomize_method_with_unsup.v:63:37: Unsupported: randomize() 'with' constraint
+   63 |       rand_result = obj.randomize() with { 256 < y && y < 256; };
+      |                                     ^~~~
+%Error-UNSUPPORTED: t/t_randomize_method_with_unsup.v:67:37: Unsupported: randomize() 'with' constraint
+   67 |       rand_result = obj.randomize() with { 16 <= z && z <= 32; };
+      |                                     ^~~~
+%Error: Exiting due to

test_regress/t/t_randomize_method_with_unsup.pl

@@ -0,0 +1,19 @@
+#!/usr/bin/env perl
+if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# Copyright 2023 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+scenarios(linter => 1);
+
+compile(
+    expect_filename => $Self->{golden_filename},
+    fails => 1,
+    );
+
+ok(1);
+1;

test_regress/t/t_randomize_method_with_unsup.v

@@ -0,0 +1,71 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain, for
+// any use, without warranty, 2024 by Antmicro Ltd.
+// SPDX-License-Identifier: CC0-1.0
+
+typedef enum bit[15:0] {
+   ONE   = 3,
+   TWO   = 5,
+   THREE = 8,
+   FOUR  = 13
+} Enum;
+
+class Cls;
+   constraint A { v inside {ONE, THREE}; }
+   constraint B { w == 5; x inside {1,2} || x inside {4,5}; }
+   constraint C { z < 3 * 7; z > 5 + 8; }
+
+   rand Enum v;
+   rand logic[63:0] w;
+   rand logic[47:0] x;
+   rand logic[31:0] y;
+   rand logic[23:0] z;
+
+   function new;
+      v = ONE;
+      w = 0;
+      x = 0;
+      y = 0;
+      z = 0;
+   endfunction
+
+endclass
+
+module t (/*AUTOARG*/);
+   Cls obj;
+
+   initial begin
+      int rand_result;
+      int lb, ub;
+      longint prev_checksum;
+      $display("===================\nSatisfiable constraints:");
+      for (int i = 0; i < 25; i++) begin
+         obj = new;
+         lb = 16;
+         ub = 32;
+         rand_result = obj.randomize() with { lb <= y && y <= ub; };
+         $display("obj.v == %0d", obj.v);
+         $display("obj.w == %0d", obj.w);
+         $display("obj.x == %0d", obj.x);
+         $display("obj.y == %0d", obj.y);
+         $display("obj.z == %0d", obj.z);
+         $display("rand_result == %0d", rand_result);
+         $display("-------------------");
+         if (!(obj.v inside {ONE, THREE})) $stop;
+         if (obj.w != 5) $stop;
+         if (!(obj.x inside {1,2,4,5})) $stop;
+         if (obj.y < 16 || obj.y > 32) $stop;
+         if (obj.z <= 13 || obj.z >= 21) $stop;
+         if (lb != 16 || ub != 32) $stop;
+      end
+      $display("===================\nUnsatisfiable constraints for obj.y:");
+      rand_result = obj.randomize() with { 256 < y && y < 256; };
+      $display("obj.y == %0d", obj.y);
+      $display("rand_result == %0d", rand_result);
+      if (rand_result != 0) $stop;
+      rand_result = obj.randomize() with { 16 <= z && z <= 32; };
+      $write("*-* All Finished *-*\n");
+      $finish;
+   end
+endmodule

test_regress/t/t_verilated_all.v

@@ -4,14 +4,20 @@
 // any use, without warranty, 2017 by Wilson Snyder.
 // SPDX-License-Identifier: CC0-1.0
 
+class Rnd;
+   rand bit x;
+endclass
+
 module t (/*AUTOARG*/
    // Inputs
    clk
    );
+   Rnd c;
 
    input clk;
 
    integer cyc;
+   integer rand_result;
    integer seed = 123;
 
    always @ (posedge clk) begin
@@ -20,6 +26,9 @@ module t (/*AUTOARG*/
          if (cyc == 10) begin
             #5;
             $display("dist: %f ", $dist_poisson(seed, 12));  // Get verilated_probdist.cpp
+            c = new;
+            rand_result = c.randomize();
+            $display("rand: %x x: %x ", rand_result, c.x);  // Get verilated_random.cpp
             $write("*-* All Finished *-*\n");
             $finish;
          end