Merge 366f98ae25 into 8d1d5a25e5

passes/sat/sim.cc

@@ -27,6 +27,7 @@
 #include "kernel/yw.h"
 #include "kernel/json.h"
 #include "kernel/fmt.h"
+#include "kernel/drivertools.h"
 
 #include <ctime>
 
@@ -126,6 +127,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)
@@ -427,7 +430,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;
 	}
 
@@ -446,7 +449,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;
 	}
 
@@ -1193,6 +1196,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;
@@ -1249,7 +1300,7 @@ 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;
 					}
@@ -1257,14 +1308,14 @@ struct SimInstance
 			} 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;
 				}
 			}
@@ -1499,6 +1550,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;
@@ -2625,8 +2682,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");
@@ -2844,6 +2908,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;

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

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 #

tests/sim/undriven_replay.ys

@@ -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

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

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