diff --git a/Makefile.in b/Makefile.in index 80db572be..1e8f6181b 100644 --- a/Makefile.in +++ b/Makefile.in @@ -536,6 +536,7 @@ PY_PROGRAMS = \ src/vlcovgen \ test_regress/*.py \ test_regress/t/*.pf \ + test_regress/t/randomize_solver_tamper.py \ # Python files, subject to format but not lint PY_FILES = \ diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index 262e074bc..1903142d6 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -129,7 +129,7 @@ public: void wait_report() { if (m_pidExited) return; #ifdef _VL_SOLVER_PIPE - if (waitpid(m_pid, &m_pidStatus, 0) != m_pid) return; + if (waitpid(m_pid, &m_pidStatus, WNOHANG) != m_pid) m_pidStatus = 0; if (m_pidStatus) { std::stringstream msg; msg << "Subprocess command `" << m_cmd[0]; @@ -208,8 +208,10 @@ public: // Child close(fd_stdin[P_WR]); dup2(fd_stdin[P_RD], STDIN_FILENO); + close(fd_stdin[P_RD]); close(fd_stdout[P_RD]); dup2(fd_stdout[P_WR], STDOUT_FILENO); + close(fd_stdout[P_WR]); execvp(cmd[0], const_cast(cmd)); std::stringstream msg; msg << "VlRProcess::open: execvp(" << cmd[0] << ")"; @@ -691,9 +693,17 @@ void VlRandomizer::solveDiversityXor(VlRNG& rngr, std::iostream& os) { } } +// False once the solver is gone, so no reply loop can spin forever +static bool readNonBlankLine(std::istream& is, std::string& liner) { + do { + if (!std::getline(is, liner)) return false; + } while (liner.empty()); + return true; +} + bool VlRandomizer::checkSat(std::iostream& os) { std::string result; - do { std::getline(os, result); } while (result.empty()); + if (!readNonBlankLine(os, result)) return false; return result == "sat"; } @@ -733,7 +743,7 @@ static std::vector scanIntRuns(const std::string& reply) { std::vector VlRandomizer::readUnsatAssumptions(std::iostream& os) { os << "(get-unsat-assumptions)\n"; std::string line; - do { std::getline(os, line); } while (line.empty()); + if (!readNonBlankLine(os, line)) return {}; // The response lists only "a" literals; collect each full integer run. return scanIntRuns(line); } @@ -748,7 +758,7 @@ void VlRandomizer::reportUnsatSetup(std::iostream& os, emitAsserts(os, uniqueExprs, true); os << "(check-sat)\n"; std::string status; - do { std::getline(os, status); } while (status.empty()); + if (!readNonBlankLine(os, status)) return; if (status == "unsat") reportUnsatCore(os); } @@ -788,7 +798,7 @@ void VlRandomizer::reportUnsatCore(std::iostream& os) { bool VlRandomizer::parseSolution(std::iostream& os) { std::string sat; - do { std::getline(os, sat); } while (sat == ""); + if (!readNonBlankLine(os, sat)) return false; if (sat == "unsat") return false; if (sat != "sat") { std::stringstream msg; @@ -809,14 +819,13 @@ bool VlRandomizer::parseSolution(std::iostream& os) { os << "))\n"; // Quasi-parse S-expression of the form ((x #xVALUE) (y #bVALUE) (z #xVALUE)) char c; - os >> c; - if (c != '(') { + if (!(os >> c) || c != '(') { VL_WARN_MT(__FILE__, __LINE__, "randomize", "Internal: Unable to parse solver's response: invalid S-expression"); return false; } while (true) { - os >> c; + if (!(os >> c)) return false; if (c == ')') break; if (c != '(') { VL_WARN_MT(__FILE__, __LINE__, "randomize", diff --git a/test_regress/t/randomize_solver_tamper.py b/test_regress/t/randomize_solver_tamper.py new file mode 100755 index 000000000..1f3fb5398 --- /dev/null +++ b/test_regress/t/randomize_solver_tamper.py @@ -0,0 +1,71 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: fake SMT solver wrapper for solver resilience tests +# +# This program is free software; you can redistribute it and/or modify it +# under the terms of either the GNU Lesser General Public License Version 3, +# or the Perl Artistic License Version 2.0. +# SPDX-FileCopyrightText: 2026 Wilson Snyder +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 +# +# Forwards the SMT-LIB conversation to a real solver, then kills it. +# +# Input arguments from environment variables: +# TAMPER: none | die_at | die_status_at | mute_at | garbage_at +# die_at - kill the solver and exit, closing every pipe end +# die_status_at - same, counting sat/unsat status lines instead of models +# mute_at - close the reply pipe but keep this wrapper running +# garbage_at - replace every Nth model reply with a non-S-expression line +# TAMPER_AT: reply index to act on (default 3) + +# pylint: disable=C0103,C0114,consider-using-with + +import os +import shutil +import subprocess +import sys +import time + +mode = os.environ.get("TAMPER", "none") +at = int(os.environ.get("TAMPER_AT", "3")) + + +def real_solver(): + """Return argv for the first SMT solver found in PATH""" + for cmd in (["z3", "-in"], ["cvc5", "--incremental"], ["cvc4", "--lang=smt2", + "--incremental"]): + if shutil.which(cmd[0]): + return cmd + sys.exit("randomize_solver_tamper.py: no SMT solver found") + + +proc = subprocess.Popen(real_solver(), stdin=sys.stdin, stdout=subprocess.PIPE, text=True) + +replies = 0 +acting = False + +for line in proc.stdout: + line = line.rstrip("\n") + counted = line in ("sat", "unsat", + "unknown") if mode == "die_status_at" else line.startswith("((") + if counted: + replies += 1 + acting = counted and replies >= at + if acting and mode == "garbage_at": + line = "junk" + replies = 0 + sys.stdout.write(line + "\n") + sys.stdout.flush() + if not acting: + continue + if mode in ("die_at", "die_status_at"): + proc.kill() + proc.wait() + sys.exit(0) + if mode == "mute_at": + os.close(1) + proc.kill() + proc.wait() + parent = os.getppid() + while os.getppid() == parent: + time.sleep(0.05) + sys.exit(0) diff --git a/test_regress/t/t_randomize_solver_fault.v b/test_regress/t/t_randomize_solver_fault.v new file mode 100644 index 000000000..0103a00d8 --- /dev/null +++ b/test_regress/t/t_randomize_solver_fault.v @@ -0,0 +1,63 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`define stop $stop +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + +// Model and diversity assumption replies +class Packet; + rand bit [7:0] a; + rand bit [7:0] b; + constraint c { + a > 8'd10; + b < 8'd200; + a != b; + } +endclass + +// Soft constraint relaxation replies +class Softy; + rand bit [7:0] s; + constraint sc { + soft s == 8'd42; + s > 8'd100; + } +endclass + +// Phased solve...before replies +class Phased; + rand bit [3:0] x; + rand bit [3:0] y; + constraint order_c {solve x before y;} + constraint rel_c {y > x;} +endclass + +module t; + initial begin + automatic Packet p = new; + automatic Softy s = new; + automatic Phased ph = new; + automatic int npass = 0; + automatic int rc; + for (int i = 0; i < 4; ++i) begin + // Below the constraint, so any model the runtime applies overwrites it + p.a = 8'd5; + rc = p.randomize(); + if (rc != 0) npass++; + rc = s.randomize(); + if (rc != 0) npass++; + rc = ph.randomize(); + if (rc != 0) npass++; + end + $write("NPASS=%0d\n", npass); + // A randomize that failed must leave the variable alone + `checkd(p.a, 8'd5); + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule diff --git a/test_regress/t/t_randomize_solver_pipe.py b/test_regress/t/t_randomize_solver_pipe.py new file mode 100755 index 000000000..25d42eee6 --- /dev/null +++ b/test_regress/t/t_randomize_solver_pipe.py @@ -0,0 +1,36 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# This program is free software; you can redistribute it and/or modify it +# under the terms of either the GNU Lesser General Public License Version 3 +# or the Perl Artistic License Version 2.0. +# SPDX-FileCopyrightText: 2026 Wilson Snyder +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +import vltest_bootstrap + +test.scenarios('vlt') +test.top_filename = "t/t_randomize_solver_fault.v" + +if not test.have_solver: + test.skip("No constraint solver installed") + +test.compile() + +# Reply index picks which reply the runtime is waiting on when the solver goes +runs = [ + ('die_at', 10, 3), # solver exits with a model reply pending + ('die_status_at', 4, 1), # solver exits with a soft constraint status pending + ('die_status_at', 7, 2), # solver exits between the status and the model read + ('mute_at', 3, 2), # solver stays running but stops answering + ('garbage_at', 2, 1), # solver answers, but not with an S-expression +] + +for mode, at, npass in runs: + logfile = test.obj_dir + '/sim_' + mode + '_' + str(at) + '.log' + test.execute(logfile=logfile, + run_env='VERILATOR_SOLVER="' + test.t_dir + '/randomize_solver_tamper.py" ' + + 'TAMPER=' + mode + ' TAMPER_AT=' + str(at)) + test.file_grep(logfile, r'NPASS=' + str(npass) + r'\n') + +test.passes()