From cdc728b6f009ba9faa9829e26332f428896a0b77 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Fri, 20 Feb 2026 09:33:51 -0800 Subject: [PATCH 1/4] Suggest use of YW when possible --- passes/sat/sim.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 27d6d12c1..5392cd9e5 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -2624,6 +2624,7 @@ struct SimPass : public Pass { log(" -r \n"); log(" read simulation or formal results file\n"); log(" File formats supported: FST, VCD, AIW, WIT and .yw\n"); + log(" Yosys witness (.yw) replay is preferred when possible.\n"); log(" VCD support requires vcd2fst external tool to be present\n"); log("\n"); log(" -width \n"); From b454582f540753343524d33e7d2e3ad8ca95972b Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Fri, 20 Feb 2026 11:00:59 -0800 Subject: [PATCH 2/4] Detect undriven and error/warn --- passes/sat/sim.cc | 81 ++++++++++++++++++++++++++++++++--- tests/sim/undriven_replay.v | 7 +++ tests/sim/undriven_replay.vcd | 15 +++++++ tests/sim/undriven_replay.ys | 10 +++++ 4 files changed, 108 insertions(+), 5 deletions(-) create mode 100644 tests/sim/undriven_replay.v create mode 100644 tests/sim/undriven_replay.vcd create mode 100644 tests/sim/undriven_replay.ys diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 5392cd9e5..bd723f5f1 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -26,6 +26,7 @@ #include "kernel/yw.h" #include "kernel/json.h" #include "kernel/fmt.h" +#include "kernel/drivertools.h" #include @@ -125,6 +126,8 @@ struct SimShared bool serious_asserts = false; bool fst_noinit = false; bool initstate = true; + bool undriven_check = true; + bool undriven_warning = false; }; void zinit(Const &v) @@ -426,7 +429,7 @@ struct SimInstance Const value = builder.build(); if (shared->debug) - log("[%s] get %s: %s\n", hiername(), log_signal(sig), log_signal(value)); + log("[%s] get %s: %s\n", hiername(), log_signal(sig, true), log_signal(value, true)); return value; } @@ -445,7 +448,7 @@ struct SimInstance } if (shared->debug) - log("[%s] set %s: %s\n", hiername(), log_signal(sig), log_signal(value)); + log("[%s] set %s: %s\n", hiername(), log_signal(sig, true), log_signal(value, true)); return did_something; } @@ -1192,6 +1195,54 @@ struct SimInstance child.second->addAdditionalInputs(); } + // Preconditions / assumptions: + // 1) fst_handles is populated for this instance (0 handle means not in trace). + // 2) fst_inputs is finalized (top-level inputs + addAdditionalInputs() for $anyseq). + // 3) module has no processes (sim enforces proc-lowered input before this point). + // 4) sigmap is valid for per-bit queries on this instance. + // 5) shared->fst is active, i.e. this is called from FST/VCD replay flow. + int checkUndrivenReplaySignals() + { + int issue_count = 0; + bool has_replay_candidates = false; + + for (auto &item : fst_handles) + if (item.second != 0 && !fst_inputs.count(item.first)) { + has_replay_candidates = true; + break; + } + + if (has_replay_candidates) { + DriverMap drivermap(module->design); + drivermap.add(module); + + for (auto &item : fst_handles) { + Wire *wire = item.first; + if (item.second == 0 || fst_inputs.count(wire)) + continue; + + SigSpec undriven; + for (auto bit : sigmap(wire)) + if (bit.wire != nullptr && drivermap(DriveBit(bit)).is_none()) + undriven.append(bit); + + undriven.sort_and_unify(); + if (undriven.empty()) + continue; + + issue_count++; + std::string wire_name = scope + "." + RTLIL::unescape_id(wire->name); + log_warning("Input trace contains undriven signal `%s` (%s); values for this signal are not replayed from FST/VCD input.\n", + wire_name.c_str(), log_signal(undriven, true)); + } + } + + for (auto child : children) + issue_count += child.second->checkUndrivenReplaySignals(); + + return issue_count; + } + bool setInputs() { bool did_something = false; @@ -1248,7 +1299,7 @@ struct SimInstance } else if (shared->sim_mode == SimulationMode::gate && !fst_val.is_fully_def()) { // FST data contains X for(int i=0;isim_mode == SimulationMode::gold && !sim_val.is_fully_def()) { // sim data contains X for(int i=0;iaddAdditionalInputs(); + if (undriven_check) { + int issue_count = top->checkUndrivenReplaySignals(); + if (issue_count > 0 && !undriven_warning) + log_cmd_error("Found %d undriven signal%s in the replay trace. Use -undriven-warn to continue or -no-undriven-check to disable this check.\n", + issue_count, issue_count == 1 ? "" : "s"); + } uint64_t startCount = 0; uint64_t stopCount = 0; @@ -2627,6 +2684,12 @@ struct SimPass : public Pass { log(" Yosys witness (.yw) replay is preferred when possible.\n"); log(" VCD support requires vcd2fst external tool to be present\n"); log("\n"); + log(" -no-undriven-check\n"); + log(" skip undriven-signal checks for FST/VCD replay\n"); + log("\n"); + log(" -undriven-warn\n"); + log(" downgrade undriven-signal replay errors to warnings\n"); + log("\n"); log(" -width \n"); log(" cycle width in generated simulation output (must be divisible by 2).\n"); log("\n"); @@ -2844,6 +2907,14 @@ struct SimPass : public Pass { worker.fst_noinit = true; continue; } + if (args[argidx] == "-no-undriven-check") { + worker.undriven_check = false; + continue; + } + if (args[argidx] == "-undriven-warn") { + worker.undriven_warning = true; + continue; + } if (args[argidx] == "-x") { worker.ignore_x = true; continue; diff --git a/tests/sim/undriven_replay.v b/tests/sim/undriven_replay.v new file mode 100644 index 000000000..501f438a1 --- /dev/null +++ b/tests/sim/undriven_replay.v @@ -0,0 +1,7 @@ +module undriven_replay ( + input wire in, + output wire out, + output wire undrv +); + assign out = in; +endmodule diff --git a/tests/sim/undriven_replay.vcd b/tests/sim/undriven_replay.vcd new file mode 100644 index 000000000..e9cc35ae5 --- /dev/null +++ b/tests/sim/undriven_replay.vcd @@ -0,0 +1,15 @@ +$version Yosys $end +$scope module undriven_replay $end +$var wire 1 ! in $end +$var wire 1 " out $end +$var wire 1 # undrv $end +$upscope $end +$enddefinitions $end +#0 +b0 ! +b0 " +b1 # +#10 +b1 ! +b1 " +b0 # diff --git a/tests/sim/undriven_replay.ys b/tests/sim/undriven_replay.ys new file mode 100644 index 000000000..9766a8d60 --- /dev/null +++ b/tests/sim/undriven_replay.ys @@ -0,0 +1,10 @@ +read_verilog undriven_replay.v +prep -top undriven_replay + +logger -expect error "Found 1 undriven signal in the replay trace" 1 +sim -r undriven_replay.vcd -scope undriven_replay -q + +logger -expect warning "Input trace contains undriven signal" 1 +sim -r undriven_replay.vcd -scope undriven_replay -q -undriven-warn + +sim -r undriven_replay.vcd -scope undriven_replay -q -no-undriven-check From c0f1654028736cd88d2fa7cae5b0335371e8e866 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 23 Feb 2026 10:27:36 -0800 Subject: [PATCH 3/4] Expand test into three tests for three cases (1) no check, (2) check with warning, (3) check with error. Previously the single test was not testing all cases, as it was exiting after the first error. --- tests/sim/undriven_replay.ys | 5 ----- tests/sim/undriven_replay_nocheck.ys | 4 ++++ tests/sim/undriven_replay_warn.ys | 5 +++++ 3 files changed, 9 insertions(+), 5 deletions(-) create mode 100644 tests/sim/undriven_replay_nocheck.ys create mode 100644 tests/sim/undriven_replay_warn.ys diff --git a/tests/sim/undriven_replay.ys b/tests/sim/undriven_replay.ys index 9766a8d60..854a40049 100644 --- a/tests/sim/undriven_replay.ys +++ b/tests/sim/undriven_replay.ys @@ -3,8 +3,3 @@ prep -top undriven_replay logger -expect error "Found 1 undriven signal in the replay trace" 1 sim -r undriven_replay.vcd -scope undriven_replay -q - -logger -expect warning "Input trace contains undriven signal" 1 -sim -r undriven_replay.vcd -scope undriven_replay -q -undriven-warn - -sim -r undriven_replay.vcd -scope undriven_replay -q -no-undriven-check diff --git a/tests/sim/undriven_replay_nocheck.ys b/tests/sim/undriven_replay_nocheck.ys new file mode 100644 index 000000000..dcb1cfc92 --- /dev/null +++ b/tests/sim/undriven_replay_nocheck.ys @@ -0,0 +1,4 @@ +read_verilog undriven_replay.v +prep -top undriven_replay + +sim -r undriven_replay.vcd -scope undriven_replay -q -no-undriven-check diff --git a/tests/sim/undriven_replay_warn.ys b/tests/sim/undriven_replay_warn.ys new file mode 100644 index 000000000..ca3b1937c --- /dev/null +++ b/tests/sim/undriven_replay_warn.ys @@ -0,0 +1,5 @@ +read_verilog undriven_replay.v +prep -top undriven_replay + +logger -expect warning "Input trace contains undriven signal" 1 +sim -r undriven_replay.vcd -scope undriven_replay -q -undriven-warn From 366f98ae25bf45be94a6ea8118abe431eb676bdf Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 23 Feb 2026 11:51:54 -0800 Subject: [PATCH 4/4] ADd clarification --- passes/sat/sim.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index bd723f5f1..ddc256384 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -2685,7 +2685,7 @@ struct SimPass : public Pass { log(" VCD support requires vcd2fst external tool to be present\n"); log("\n"); log(" -no-undriven-check\n"); - log(" skip undriven-signal checks for FST/VCD replay\n"); + log(" skip undriven-signal checks for FST/VCD replay (can be expensive for large designs)\n"); log("\n"); log(" -undriven-warn\n"); log(" downgrade undriven-signal replay errors to warnings\n");