Added satgen initstate support

1 files changed, 27 insertions, 0 deletions

diff --git a/kernel/satgen.h b/kernel/satgen.h
index eb1c6fe36..31b7a3e5a 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -71,6 +71,7 @@ struct SatGen
 	std::map<std::string, RTLIL::SigSpec> assumes_a, assumes_en;
 	std::map<std::string, RTLIL::SigSpec> predict_a, predict_en;
 	std::map<std::string, std::map<RTLIL::SigBit, int>> imported_signals;
+	std::map<std::pair<std::string, int>, bool> initstates;
 	bool ignore_div_by_zero;
 	bool model_undef;
 
@@ -267,6 +268,13 @@ struct SatGen
 		ez->assume(ez->OR(undef, ez->IFF(y, yy)));
 	}
 
+	void setInitState(int timestep)
+	{
+		auto key = make_pair(prefix, timestep);
+		log_assert(initstates.count(key) == 0 || initstates.at(key) == true);
+		initstates[key] = true;
+	}
+
 	bool importCell(RTLIL::Cell *cell, int timestep = -1)
 	{
 		bool arith_undef_handled = false;
@@ -1331,6 +1339,25 @@ struct SatGen
 			return true;
 		}
 
+		if (cell->type == "$initstate")
+		{
+			auto key = make_pair(prefix, timestep);
+			if (initstates.count(key) == 0)
+				initstates[key] = false;
+
+			std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
+			log_assert(GetSize(y) == 1);
+			ez->SET(y[0], initstates[key] ? ez->CONST_TRUE : ez->CONST_FALSE);
+
+			if (model_undef) {
+				std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
+				log_assert(GetSize(undef_y) == 1);
+				ez->SET(undef_y[0], ez->CONST_FALSE);
+			}
+
+			return true;
+		}
+
 		if (cell->type == "$assert")
 		{
 			std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));