This commit is contained in:
parent
a3553e7bee
commit
ace84ef2b3
|
|
@ -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 = \
|
||||
|
|
|
|||
|
|
@ -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<char* const*>(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<int> scanIntRuns(const std::string& reply) {
|
|||
std::vector<int> 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<N>" 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",
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
@ -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
|
||||
|
|
@ -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()
|
||||
Loading…
Reference in New Issue