From 7eaa4bcb4605d6c1d30d4daf96a94cea3b423df3 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Thu, 28 Sep 2023 17:29:24 +0200
Subject: [PATCH] sim: Add -noinitstate option and handle non-cosim initstate

This adds the -noinitstate option which is required to simulate
counterexamples to induction with yw-cosim. Also add handling for
$initstate cells for non-co-simulation.
---
 passes/sat/sim.cc | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 1e6645303b5..963c6481b16 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -111,6 +111,7 @@ struct SimShared
 	int step = 0;
 	std::vector<TriggeredAssertion> triggered_assertions;
 	bool serious_asserts = false;
+	bool initstate = true;
 };
 
 void zinit(State &v)
@@ -1356,6 +1357,8 @@ struct SimWorker : SimShared
 		set_inports(clock, State::Sx);
 		set_inports(clockn, State::Sx);
 
+		top->set_initstate_outputs(initstate ? State::S1 : State::S0);
+
 		update(false);
 
 		register_output_step(0);
@@ -1372,6 +1375,9 @@ struct SimWorker : SimShared
 			update(true);
 			register_output_step(10*cycle + 5);
 
+			if (cycle == 0)
+				top->set_initstate_outputs(State::S0);
+
 			if (debug)
 				log("\n===== %d =====\n", 10*cycle + 10);
 			else if (verbose)
@@ -1953,7 +1959,7 @@ struct SimWorker : SimShared
 		if (yw.steps.empty()) {
 			log_warning("Yosys witness file `%s` contains no time steps\n", yw.filename.c_str());
 		} else {
-			top->set_initstate_outputs(State::S1);
+			top->set_initstate_outputs(initstate ? State::S1 : State::S0);
 			set_yw_state(yw, hierarchy, 0);
 			set_yw_clocks(yw, hierarchy, true);
 			initialize_stable_past();
@@ -2546,6 +2552,9 @@ struct SimPass : public Pass {
 		log("    -n <integer>\n");
 		log("        number of clock cycles to simulate (default: 20)\n");
 		log("\n");
+		log("    -noinitstate\n");
+		log("        do not activate $initstate cells during the first cycle\n");
+		log("\n");
 		log("    -a\n");
 		log("        use all nets in VCD/FST operations, not just those with public names\n");
 		log("\n");
@@ -2646,6 +2655,10 @@ struct SimPass : public Pass {
 				worker.cycles_set = true;
 				continue;
 			}
+			if (args[argidx] == "-noinitstate") {
+				worker.initstate = false;
+				continue;
+			}
 			if (args[argidx] == "-rstlen" && argidx+1 < args.size()) {
 				worker.rstlen = atoi(args[++argidx].c_str());
 				continue;