Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
82 changes: 77 additions & 5 deletions passes/sat/sim.cc
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@
#include "kernel/yw.h"
#include "kernel/json.h"
#include "kernel/fmt.h"
#include "kernel/drivertools.h"

#include <ctime>

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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;
}

Expand All @@ -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;
}

Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -1248,22 +1299,22 @@ struct SimInstance
} else if (shared->sim_mode == SimulationMode::gate && !fst_val.is_fully_def()) { // FST data contains X
for(int i=0;i<fst_val.size();i++) {
if (fst_val[i]!=State::Sx && fst_val[i]!=sim_val[i]) {
log_warning("Signal '%s.%s' in file %s in simulation %s\n", scope, log_id(item.first), log_signal(fst_val), log_signal(sim_val));
log_warning("Signal '%s.%s' in file %s in simulation %s\n", scope, log_id(item.first), log_signal(fst_val, true), log_signal(sim_val, true));
retVal = true;
break;
}
}
} else if (shared->sim_mode == SimulationMode::gold && !sim_val.is_fully_def()) { // sim data contains X
for(int i=0;i<sim_val.size();i++) {
if (sim_val[i]!=State::Sx && fst_val[i]!=sim_val[i]) {
log_warning("Signal '%s.%s' in file %s in simulation %s\n", scope, log_id(item.first), log_signal(fst_val), log_signal(sim_val));
log_warning("Signal '%s.%s' in file %s in simulation %s\n", scope, log_id(item.first), log_signal(fst_val, true), log_signal(sim_val, true));
retVal = true;
break;
}
}
} else {
if (fst_val!=sim_val) {
log_warning("Signal '%s.%s' in file %s in simulation '%s'\n", scope, log_id(item.first), log_signal(fst_val), log_signal(sim_val));
log_warning("Signal '%s.%s' in file %s in simulation '%s'\n", scope, log_id(item.first), log_signal(fst_val, true), log_signal(sim_val, true));
retVal = true;
}
}
Expand Down Expand Up @@ -1498,6 +1549,12 @@ struct SimWorker : SimShared
}

top->addAdditionalInputs();
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;
Expand Down Expand Up @@ -2624,8 +2681,15 @@ struct SimPass : public Pass {
log(" -r <filename>\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(" -no-undriven-check\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");
log("\n");
log(" -width <integer>\n");
log(" cycle width in generated simulation output (must be divisible by 2).\n");
log("\n");
Expand Down Expand Up @@ -2843,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;
Expand Down
7 changes: 7 additions & 0 deletions tests/sim/undriven_replay.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
module undriven_replay (
input wire in,
output wire out,
output wire undrv
);
assign out = in;
endmodule
15 changes: 15 additions & 0 deletions tests/sim/undriven_replay.vcd
Original file line number Diff line number Diff line change
@@ -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 #
5 changes: 5 additions & 0 deletions tests/sim/undriven_replay.ys
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
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
4 changes: 4 additions & 0 deletions tests/sim/undriven_replay_nocheck.ys
Original file line number Diff line number Diff line change
@@ -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
5 changes: 5 additions & 0 deletions tests/sim/undriven_replay_warn.ys
Original file line number Diff line number Diff line change
@@ -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
Loading