From 739be2f78242b51e84fe6ba4360659ac8cac867f Mon Sep 17 00:00:00 2001 From: Arkadiusz Kozdra Date: Fri, 17 May 2024 16:38:34 +0200 Subject: [PATCH] Support constrained randomization with external solvers (#4947) --- Makefile.in | 1 + ci/ci-install.bash | 8 +- ci/docker/buildenv/Dockerfile | 1 + configure.ac | 22 + docs/guide/environment.rst | 6 + docs/guide/install.rst | 16 +- docs/internals.rst | 89 ++++ include/verilated.cpp | 19 +- include/verilated.h | 5 + include/verilated_funcs.h | 3 + include/verilated_random.cpp | 424 ++++++++++++++++++ include/verilated_random.h | 120 +++++ src/Makefile_obj.in | 8 + src/V3Ast.h | 27 +- src/V3AstNodeDType.h | 3 + src/V3AstNodeExpr.h | 42 ++ src/V3AstNodes.cpp | 6 +- src/V3Common.cpp | 4 +- src/V3EmitCFunc.cpp | 2 + src/V3EmitCHeaders.cpp | 1 + src/V3EmitCMake.cpp | 6 + src/V3EmitMk.cpp | 6 + src/V3Options.cpp | 12 + src/V3Options.h | 1 + src/V3Randomize.cpp | 236 +++++++++- src/config_build.h | 3 + test_regress/t/t_constraint.v | 2 - test_regress/t/t_constraint_json_only.out | 175 +++++++- test_regress/t/t_constraint_mode.v | 2 - test_regress/t/t_constraint_mode_warn_bad.out | 36 +- test_regress/t/t_constraint_nosolver_bad.out | 8 + test_regress/t/t_constraint_nosolver_bad.pl | 27 ++ test_regress/t/t_constraint_operators.pl | 22 + test_regress/t/t_constraint_operators.v | 50 +++ test_regress/t/t_constraint_xml.out | 274 +++++------ test_regress/t/t_randomize.out | 42 +- .../t/t_randomize_method_constraints.pl | 21 + .../t/t_randomize_method_constraints.v | 69 +++ .../t/t_randomize_method_types_unsup.out | 18 +- .../t/t_randomize_method_types_unsup.v | 4 + .../t/t_randomize_method_with_unsup.out | 11 + .../t/t_randomize_method_with_unsup.pl | 19 + .../t/t_randomize_method_with_unsup.v | 71 +++ test_regress/t/t_verilated_all.v | 9 + 44 files changed, 1668 insertions(+), 263 deletions(-) create mode 100644 include/verilated_random.cpp create mode 100644 include/verilated_random.h create mode 100644 test_regress/t/t_constraint_nosolver_bad.out create mode 100755 test_regress/t/t_constraint_nosolver_bad.pl create mode 100755 test_regress/t/t_constraint_operators.pl create mode 100644 test_regress/t/t_constraint_operators.v create mode 100755 test_regress/t/t_randomize_method_constraints.pl create mode 100644 test_regress/t/t_randomize_method_constraints.v create mode 100644 test_regress/t/t_randomize_method_with_unsup.out create mode 100755 test_regress/t/t_randomize_method_with_unsup.pl create mode 100644 test_regress/t/t_randomize_method_with_unsup.v diff --git a/Makefile.in b/Makefile.in index 9d2ce218f..88de77fda 100644 --- a/Makefile.in +++ b/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. #### diff --git a/ci/ci-install.bash b/ci/ci-install.bash index 0907d081e..723dcb586 100755 --- a/ci/ci-install.bash +++ b/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 + sudo apt-get install gdb gtkwave lcov libfl-dev ccache jq z3 || + 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 '', 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 diff --git a/ci/docker/buildenv/Dockerfile b/ci/docker/buildenv/Dockerfile index 385e0b088..88e39b85f 100644 --- a/ci/docker/buildenv/Dockerfile +++ b/ci/docker/buildenv/Dockerfile @@ -43,6 +43,7 @@ RUN apt-get update \ perl \ python3 \ wget \ + z3 \ zlib1g \ zlib1g-dev \ && apt-get clean \ diff --git a/configure.ac b/configure.ac index 8dc34f73a..c55dd2ec9 100644 --- a/configure.ac +++ b/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 " diff --git a/docs/guide/environment.rst b/docs/guide/environment.rst index 8629c741e..d099acea3 100644 --- a/docs/guide/environment.rst +++ b/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 diff --git a/docs/guide/install.rst b/docs/guide/install.rst index 8ae132f9c..ecc06bc48 100644 --- a/docs/guide/install.rst +++ b/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 +`__ 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 -the executable, so they must be correct before configuring. +:option:`VERILATOR_SOLVER`, :option:`SYSTEMC_INCLUDE`, and +:option:`SYSTEMC_LIBDIR` as defaults into the executable, so they must be +correct before configuring. These are the installation options: diff --git a/docs/internals.rst b/docs/internals.rst index 72a0f3b3a..89502b1d9 100644 --- a/docs/internals.rst +++ b/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 +`__ 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. diff --git a/include/verilated.cpp b/include/verilated.cpp index 1a0377f11..fc1bcd26c 100644 --- a/include/verilated.cpp +++ b/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, - size_t posstart, size_t posend) VL_MT_SAFE { +void _vl_vsss_based(WDataOutP owp, int obits, int baseLog2, const char* strp, size_t posstart, + 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(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; diff --git a/include/verilated.h b/include/verilated.h index 808df79ce..90836de85 100644 --- a/include/verilated.h +++ b/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 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; diff --git a/include/verilated_funcs.h b/include/verilated_funcs.h index 02ac6911f..dcabf1855 100644 --- a/include/verilated_funcs.h +++ b/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; diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp new file mode 100644 index 000000000..4eec944db --- /dev/null +++ b/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 +#include +#include + +#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 +# include +#endif + +#if defined(_WIN32) || defined(__MINGW32__) +# include // 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(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(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 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 qowp; + VL_SET_WQ(qowp, 0ULL); + WDataOutP owp = qowp; + int obits = width(); + if (obits > VL_QUADSIZE) owp = reinterpret_cast(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(datap()); + *p = VL_CLEAN_II(obits, obits, owp[0]); + } else if (obits <= VL_SHORTSIZE) { + SData* const p = static_cast(datap()); + *p = VL_CLEAN_II(obits, obits, owp[0]); + } else if (obits <= VL_IDATASIZE) { + IData* const p = static_cast(datap()); + *p = VL_CLEAN_II(obits, obits, owp[0]); + } else if (obits <= VL_QUADSIZE) { + QData* const p = static_cast(datap()); + *p = VL_CLEAN_QQ(obits, obits, VL_SET_QW(owp)); + } else { + _vl_clean_inplace_w(obits, owp); + } + return true; +} + +std::shared_ptr VlRandomizer::randomConstraint(VlRNG& rngr, int bits) { + unsigned long long hash = VL_RANDOM_RNG_I(rngr) & ((1 << bits) - 1); + std::shared_ptr concat = nullptr; + std::vector> varbits; + for (const auto& var : m_vars) { + for (int i = 0; i < var.second->width(); i++) + varbits.emplace_back(std::make_shared(var.second, i)); + } + for (int i = 0; i < bits; i++) { + std::shared_ptr 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("bvxor", bit, sel); + } + concat = concat == nullptr ? bit + : std::make_shared("concat", concat, bit); + } + return std::make_shared( + "=", concat, std::make_shared(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 diff --git a/include/verilated_random.h b/include/verilated_random.h new file mode 100644 index 000000000..e1e77f3b1 --- /dev/null +++ b/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 m_expr; // Sub-expression + const unsigned m_idx; // Extracted index + +public: + VlRandomExtract(std::shared_ptr 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 m_lhs, m_rhs; // Sub-expressions + +public: + VlRandomBinOp(const char* op, std::shared_ptr lhs, + std::shared_ptr 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 m_constraints; // Solver-dependent constraints + std::map> + m_vars; // Solver-dependent variables + + // PRIVATE METHODS + std::shared_ptr randomConstraint(VlRNG& rngr, int bits); + bool parseSolution(std::iostream& file); + +public: + // METHODS + // Finds the next solution satisfying the constraints + bool next(VlRNG& rngr); + template + 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(name, width, &var); + } + void hard(std::string&& constraint); +#ifdef VL_DEBUG + void dump() const; +#endif +}; + +#endif // Guard diff --git a/src/Makefile_obj.in b/src/Makefile_obj.in index 232ff7b15..30dd7dad1 100644 --- a/src/Makefile_obj.in +++ b/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) diff --git a/src/V3Ast.h b/src/V3Ast.h index c910bc4c7..6366bb630 100644 --- a/src/V3Ast.h +++ b/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", - "char", "void*", - "char", "int", - "%E-integer", "svLogic", - "long long", "double", - "short", "%E-time", - "const char*", "%E-untyped", - "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"}; + static const char* const names[] + = {"%E-unk", "svBit", "char", "void*", "char", + "int", "%E-integer", "svLogic", "long long", "double", + "short", "%E-time", "const char*", "%E-untyped", "dpiScope", + "const char*", "%E-mtaskstate", "%E-triggervec", "%E-dly-sched", "%E-trig-sched", + "%E-dyn-sched", "%E-fork", "%E-proc-ref", "%E-rand-gen", "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; } diff --git a/src/V3AstNodeDType.h b/src/V3AstNodeDType.h index 6fe3d4eef..0ecd3a791 100644 --- a/src/V3AstNodeDType.h +++ b/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(); } diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 0146f6b70..7f66a8bfc 100644 --- a/src/V3AstNodeExpr.h +++ b/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; } diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp index 35202d35b..b39ad25ea 100644 --- a/src/V3AstNodes.cpp +++ b/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()); diff --git a/src/V3Common.cpp b/src/V3Common.cpp index 57a489487..04e44b88e 100644 --- a/src/V3Common.cpp +++ b/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 = ", "; diff --git a/src/V3EmitCFunc.cpp b/src/V3EmitCFunc.cpp index 943b84d95..3c934aac9 100644 --- a/src/V3EmitCFunc.cpp +++ b/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 diff --git a/src/V3EmitCHeaders.cpp b/src/V3EmitCHeaders.cpp index eb9ef230c..36126ada1 100644 --- a/src/V3EmitCHeaders.cpp +++ b/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 cuse_set; auto add_to_cuse_set = [&](string s) { cuse_set.insert(s); }; diff --git a/src/V3EmitCMake.cpp b/src/V3EmitCMake.cpp index 14ab4fd6e..bc24a53aa 100644 --- a/src/V3EmitCMake.cpp +++ b/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"); diff --git a/src/V3EmitMk.cpp b/src/V3EmitMk.cpp index 12b049d10..c9666b4ef 100644 --- a/src/V3EmitMk.cpp +++ b/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"); diff --git a/src/V3Options.cpp b/src/V3Options.cpp index 3b828c712..0611b2035 100644 --- a/src/V3Options.cpp +++ b/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"); } diff --git a/src/V3Options.h b/src/V3Options.h index 4907b8534..de515ce0d 100644 --- a/src/V3Options.h +++ b/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(); diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index c00800689..69cedc7a5 100644 --- a/src/V3Randomize.cpp +++ b/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; - using BaseToDerivedMap = std::unordered_map; + using BaseToDerivedMap = std::unordered_map; 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) { - for (auto* classp = nodep; classp; + void markMembers(const AstClass* nodep) { + 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)"); - if (!v3Global.opt.xmlOnly()) VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep); + AstNodeFTask* const newp = VN_AS(m_memberMap.findMember(m_modp, "new"), NodeFTask); + 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 diff --git a/src/config_build.h b/src/config_build.h index 770ad2c95..e842f0444 100644 --- a/src/config_build.h +++ b/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 //********************************************************************** diff --git a/test_regress/t/t_constraint.v b/test_regress/t/t_constraint.v index 59dea5195..dd700f2d9 100644 --- a/test_regress/t/t_constraint.v +++ b/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; diff --git a/test_regress/t/t_constraint_json_only.out b/test_regress/t/t_constraint_json_only.out index 7d2621e8b..75fc08e22 100644 --- a/test_regress/t/t_constraint_json_only.out +++ b/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": []} ]} ]} diff --git a/test_regress/t/t_constraint_mode.v b/test_regress/t/t_constraint_mode.v index cdf87c283..2add26c45 100644 --- a/test_regress/t/t_constraint_mode.v +++ b/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(); diff --git a/test_regress/t/t_constraint_mode_warn_bad.out b/test_regress/t/t_constraint_mode_warn_bad.out index 261aaab42..c2b2fa931 100644 --- a/test_regress/t/t_constraint_mode_warn_bad.out +++ b/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 diff --git a/test_regress/t/t_constraint_nosolver_bad.out b/test_regress/t/t_constraint_nosolver_bad.out new file mode 100644 index 000000000..fbc57de11 --- /dev/null +++ b/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) diff --git a/test_regress/t/t_constraint_nosolver_bad.pl b/test_regress/t/t_constraint_nosolver_bad.pl new file mode 100755 index 000000000..5f489c0d1 --- /dev/null +++ b/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; diff --git a/test_regress/t/t_constraint_operators.pl b/test_regress/t/t_constraint_operators.pl new file mode 100755 index 000000000..e45199a00 --- /dev/null +++ b/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; diff --git a/test_regress/t/t_constraint_operators.v b/test_regress/t/t_constraint_operators.v new file mode 100644 index 000000000..159f6cc52 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_constraint_xml.out b/test_regress/t/t_constraint_xml.out index 647a7ef3d..8c1255b93 100644 --- a/test_regress/t/t_constraint_xml.out +++ b/test_regress/t/t_constraint_xml.out @@ -35,167 +35,6 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -208,14 +47,117 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - @@ -224,10 +166,10 @@ - - + - + + diff --git a/test_regress/t/t_randomize.out b/test_regress/t/t_randomize.out index 03a8a5ecf..69f59261b 100644 --- a/test_regress/t/t_randomize.out +++ b/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) - : ... note: In instance 't' - 18 | constraint size { - | ^~~~ -%Warning-CONSTRAINTIGN: t/t_randomize.v:25:15: Constraint ignored (unsupported) - : ... note: In instance 't' - 25 | constraint ifs { - | ^~~ -%Warning-CONSTRAINTIGN: t/t_randomize.v:36:15: Constraint ignored (unsupported) - : ... note: In instance 't' - 36 | constraint arr_uniq { - | ^~~~~~~~ -%Warning-CONSTRAINTIGN: t/t_randomize.v:43:15: Constraint ignored (unsupported) +%Warning-CONSTRAINTIGN: t/t_randomize.v:26:7: Constraint expression ignored (unsupported) + : ... note: In instance 't' + 26 | if (header > 4) { + | ^~ +%Warning-CONSTRAINTIGN: t/t_randomize.v:29:7: Constraint expression ignored (unsupported) + : ... note: In instance 't' + 29 | if (header == 5 || header == 6) { + | ^~ +%Warning-CONSTRAINTIGN: t/t_randomize.v:37:7: Constraint expression ignored (unsupported) + : ... note: In instance 't' + 37 | foreach (array[i]) { + | ^~~~~~~ +%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]; diff --git a/test_regress/t/t_randomize_method_constraints.pl b/test_regress/t/t_randomize_method_constraints.pl new file mode 100755 index 000000000..aabcde63e --- /dev/null +++ b/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; diff --git a/test_regress/t/t_randomize_method_constraints.v b/test_regress/t/t_randomize_method_constraints.v new file mode 100644 index 000000000..23a1f7b05 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_randomize_method_types_unsup.out b/test_regress/t/t_randomize_method_types_unsup.out index d75313662..6f41402bb 100644 --- a/test_regress/t/t_randomize_method_types_unsup.out +++ b/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]; diff --git a/test_regress/t/t_randomize_method_types_unsup.v b/test_regress/t/t_randomize_method_types_unsup.v index fb3fd938d..4e24716bc 100644 --- a/test_regress/t/t_randomize_method_types_unsup.v +++ b/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*/); diff --git a/test_regress/t/t_randomize_method_with_unsup.out b/test_regress/t/t_randomize_method_with_unsup.out new file mode 100644 index 000000000..d979ce6ea --- /dev/null +++ b/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 diff --git a/test_regress/t/t_randomize_method_with_unsup.pl b/test_regress/t/t_randomize_method_with_unsup.pl new file mode 100755 index 000000000..882bc2418 --- /dev/null +++ b/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; diff --git a/test_regress/t/t_randomize_method_with_unsup.v b/test_regress/t/t_randomize_method_with_unsup.v new file mode 100644 index 000000000..fb070ce1b --- /dev/null +++ b/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 diff --git a/test_regress/t/t_verilated_all.v b/test_regress/t/t_verilated_all.v index 14b2fab87..c34cb4d11 100644 --- a/test_regress/t/t_verilated_all.v +++ b/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