Merge branch 'master' into xaig

9 files changed, 305 insertions, 62 deletions

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 53359bd7b..55c494996 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -615,6 +615,7 @@ struct BtorWorker
 		{
 			int abits = cell->getParam("\\ABITS").as_int();
 			int width = cell->getParam("\\WIDTH").as_int();
+			int nwords = cell->getParam("\\SIZE").as_int();
 			int rdports = cell->getParam("\\RD_PORTS").as_int();
 			int wrports = cell->getParam("\\WR_PORTS").as_int();
 
@@ -641,6 +642,52 @@ struct BtorWorker
 			int data_sid = get_bv_sid(width);
 			int bool_sid = get_bv_sid(1);
 			int sid = get_mem_sid(abits, width);
+
+			Const initdata = cell->getParam("\\INIT");
+			initdata.exts(nwords*width);
+			int nid_init_val = -1;
+
+			if (!initdata.is_fully_undef())
+			{
+				bool constword = true;
+				Const firstword = initdata.extract(0, width);
+
+				for (int i = 1; i < nwords; i++) {
+					Const thisword = initdata.extract(i*width, width);
+					if (thisword != firstword) {
+						constword = false;
+						break;
+					}
+				}
+
+				if (constword)
+				{
+					if (verbose)
+						btorf("; initval = %s\n", log_signal(firstword));
+					nid_init_val = get_sig_nid(firstword);
+				}
+				else
+				{
+					int nid_init_val = next_nid++;
+					btorf("%d state %d\n", nid_init_val, sid);
+
+					for (int i = 0; i < nwords; i++) {
+						Const thisword = initdata.extract(i*width, width);
+						if (thisword.is_fully_undef())
+							continue;
+						Const thisaddr(i, abits);
+						int nid_thisword = get_sig_nid(thisword);
+						int nid_thisaddr = get_sig_nid(thisaddr);
+						int last_nid_init_val = nid_init_val;
+						nid_init_val = next_nid++;
+						if (verbose)
+							btorf("; initval[%d] = %s\n", i, log_signal(thisword));
+						btorf("%d write %d %d %d %d\n", nid_init_val, sid, last_nid_init_val, nid_thisaddr, nid_thisword);
+					}
+				}
+			}
+
+
 			int nid = next_nid++;
 			int nid_head = nid;
 
@@ -649,6 +696,12 @@ struct BtorWorker
 			else
 				btorf("%d state %d %s\n", nid, sid, log_id(cell));
 
+			if (nid_init_val >= 0)
+			{
+				int nid_init = next_nid++;
+				btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val);
+			}
+
 			if (asyncwr)
 			{
 				for (int port = 0; port < wrports; port++)
@@ -932,9 +985,8 @@ struct BtorWorker
 
 			btorf_push(stringf("output %s", log_id(wire)));
 
-			int sid = get_bv_sid(GetSize(wire));
 			int nid = get_sig_nid(wire);
-			btorf("%d output %d %d %s\n", next_nid++, sid, nid, log_id(wire));
+			btorf("%d output %d %s\n", next_nid++, nid, log_id(wire));
 
 			btorf_pop(stringf("output %s", log_id(wire)));
 		}
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index 2d25f879d..7e30b67af 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -130,7 +130,7 @@ struct EdifBackend : public Backend {
 		bool port_rename = false;
 		bool attr_properties = false;
 		std::map<RTLIL::IdString, std::map<RTLIL::IdString, int>> lib_cell_ports;
-		bool nogndvcc = false, gndvccy = true;
+		bool nogndvcc = false, gndvccy = false;
 		CellTypes ct(design);
 		EdifNames edif_names;
 
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index 0917ecba6..ed6e9f8ee 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -106,6 +106,95 @@ struct FirrtlWorker
 	RTLIL::Design *design;
 	std::string indent;
 
+	// Define read/write ports and memories.
+	// We'll collect their definitions and emit the corresponding FIRRTL definitions at the appropriate point in module construction.
+	// For the moment, we don't handle $readmemh or $readmemb.
+	// These will be part of a subsequent PR.
+	struct read_port {
+		string name;
+		bool clk_enable;
+		bool clk_parity;
+		bool transparent;
+		RTLIL::SigSpec clk;
+		RTLIL::SigSpec ena;
+		RTLIL::SigSpec addr;
+		read_port(string name, bool clk_enable, bool clk_parity, bool transparent, RTLIL::SigSpec clk, RTLIL::SigSpec ena, RTLIL::SigSpec addr) : name(name), clk_enable(clk_enable), clk_parity(clk_parity), transparent(transparent), clk(clk), ena(ena), addr(addr) {
+			// Current (3/13/2019) conventions:
+			//  generate a constant 0 for clock and a constant 1 for enable if they are undefined.
+			if (!clk.is_fully_def())
+				this->clk = SigSpec(RTLIL::Const(0, 1));
+			if (!ena.is_fully_def())
+				this->ena = SigSpec(RTLIL::Const(1, 1));
+		}
+		string gen_read(const char * indent) {
+			string addr_expr = make_expr(addr);
+			string ena_expr = make_expr(ena);
+			string clk_expr = make_expr(clk);
+			string addr_str = stringf("%s%s.addr <= %s\n", indent, name.c_str(), addr_expr.c_str());
+			string ena_str = stringf("%s%s.en <= %s\n", indent, name.c_str(), ena_expr.c_str());
+			string clk_str = stringf("%s%s.clk <= asClock(%s)\n", indent, name.c_str(), clk_expr.c_str());
+			return addr_str + ena_str + clk_str;
+		}
+	};
+	struct write_port : read_port {
+		RTLIL::SigSpec mask;
+		write_port(string name, bool clk_enable, bool clk_parity, bool transparent, RTLIL::SigSpec clk, RTLIL::SigSpec ena, RTLIL::SigSpec addr, RTLIL::SigSpec mask) : read_port(name, clk_enable, clk_parity, transparent, clk, ena, addr), mask(mask) {
+			if (!clk.is_fully_def())
+				this->clk = SigSpec(RTLIL::Const(0));
+			if (!ena.is_fully_def())
+				this->ena = SigSpec(RTLIL::Const(0));
+			if (!mask.is_fully_def())
+				this->ena = SigSpec(RTLIL::Const(1));
+		}
+	  string gen_read(const char * /* indent */) {
+			log_error("gen_read called on write_port: %s\n", name.c_str());
+			return stringf("gen_read called on write_port: %s\n", name.c_str());
+		}
+		string gen_write(const char * indent) {
+			string addr_expr = make_expr(addr);
+			string ena_expr = make_expr(ena);
+			string clk_expr = make_expr(clk);
+			string mask_expr = make_expr(mask);
+			string mask_str = stringf("%s%s.mask <= %s\n", indent, name.c_str(), mask_expr.c_str());
+			string addr_str = stringf("%s%s.addr <= %s\n", indent, name.c_str(), addr_expr.c_str());
+			string ena_str = stringf("%s%s.en <= %s\n", indent, name.c_str(), ena_expr.c_str());
+			string clk_str = stringf("%s%s.clk <= asClock(%s)\n", indent, name.c_str(), clk_expr.c_str());
+			return addr_str + ena_str + clk_str + mask_str;
+		}
+	};
+	/* Memories defined within this module. */
+	 struct memory {
+		 string name;					// memory name
+		 int abits;						// number of address bits
+		 int size;						// size (in units) of the memory
+		 int width;						// size (in bits) of each element
+		 int read_latency;
+		 int write_latency;
+		 vector<read_port> read_ports;
+		 vector<write_port> write_ports;
+		 std::string init_file;
+		 std::string init_file_srcFileSpec;
+		 memory(string name, int abits, int size, int width) : name(name), abits(abits), size(size), width(width), read_latency(0), write_latency(1), init_file(""), init_file_srcFileSpec("") {}
+		 memory() : read_latency(0), write_latency(1), init_file(""), init_file_srcFileSpec(""){}
+		 void add_memory_read_port(read_port &rp) {
+			 read_ports.push_back(rp);
+		 }
+		 void add_memory_write_port(write_port &wp) {
+			 write_ports.push_back(wp);
+		 }
+		 void add_memory_file(std::string init_file, std::string init_file_srcFileSpec) {
+			 this->init_file = init_file;
+			 this->init_file_srcFileSpec = init_file_srcFileSpec;
+		 }
+
+	 };
+	dict<string, memory> memories;
+
+	void register_memory(memory &m)
+	{
+		memories[m.name] = m;
+	}
+
 	void register_reverse_wire_map(string id, SigSpec sig)
 	{
 		for (int i = 0; i < GetSize(sig); i++)
@@ -116,7 +205,7 @@ struct FirrtlWorker
 	{
 	}
 
-	string make_expr(const SigSpec &sig)
+	static string make_expr(const SigSpec &sig)
 	{
 		string expr;
 
@@ -165,11 +254,9 @@ struct FirrtlWorker
 
 	std::string fid(RTLIL::IdString internal_id)
 	{
-		const char *str = internal_id.c_str();
-		return *str == '\\' ? str + 1 : str;
+		return make_id(internal_id);
 	}
 
-
 	std::string cellname(RTLIL::Cell *cell)
 	{
 		return fid(cell->name).c_str();
@@ -219,29 +306,42 @@ struct FirrtlWorker
 			if (it->second.size() > 0) {
 				const SigSpec &secondSig = it->second;
 				const std::string firstName = cell_name + "." + make_id(it->first);
-				const std::string secondName = make_expr(secondSig);
+				const std::string secondExpr = make_expr(secondSig);
 				// Find the direction for this port.
 				FDirection dir = getPortFDirection(it->first, instModule);
-				std::string source, sink;
+				std::string sourceExpr, sinkExpr;
+				const SigSpec *sinkSig = nullptr;
 				switch (dir) {
 					case FD_INOUT:
 						log_warning("Instance port connection %s.%s is INOUT; treating as OUT\n", cell_type.c_str(), log_signal(it->second));
 					case FD_OUT:
-						source = firstName;
-						sink = secondName;
+						sourceExpr = firstName;
+						sinkExpr = secondExpr;
+						sinkSig = &secondSig;
 						break;
 					case FD_NODIRECTION:
 						log_warning("Instance port connection %s.%s is NODIRECTION; treating as IN\n", cell_type.c_str(), log_signal(it->second));
 						/* FALL_THROUGH */
 					case FD_IN:
-						source = secondName;
-						sink = firstName;
+						sourceExpr = secondExpr;
+						sinkExpr = firstName;
 						break;
 					default:
 						log_error("Instance port %s.%s unrecognized connection direction 0x%x !\n", cell_type.c_str(), log_signal(it->second), dir);
 						break;
 				}
-				wire_exprs.push_back(stringf("\n%s%s <= %s", indent.c_str(), sink.c_str(), source.c_str()));
+				// Check for subfield assignment.
+				std::string bitsString = "bits(";
+				if (sinkExpr.substr(0, bitsString.length()) == bitsString ) {
+					if (sinkSig == nullptr)
+						log_error("Unknown subfield %s.%s\n", cell_type.c_str(), sinkExpr.c_str());
+					// Don't generate the assignment here.
+					// Add the source and sink to the "reverse_wire_map" and we'll output the assignment
+					//  as part of the coalesced subfield assignments for this wire.
+					register_reverse_wire_map(sourceExpr, *sinkSig);
+				} else {
+					wire_exprs.push_back(stringf("\n%s%s <= %s", indent.c_str(), sinkExpr.c_str(), sourceExpr.c_str()));
+				}
 			}
 		}
 		wire_exprs.push_back(stringf("\n"));
@@ -504,6 +604,7 @@ struct FirrtlWorker
 				int abits = cell->parameters.at("\\ABITS").as_int();
 				int width = cell->parameters.at("\\WIDTH").as_int();
 				int size = cell->parameters.at("\\SIZE").as_int();
+				memory m(mem_id, abits, size, width);
 				int rd_ports = cell->parameters.at("\\RD_PORTS").as_int();
 				int wr_ports = cell->parameters.at("\\WR_PORTS").as_int();
 
@@ -520,33 +621,24 @@ struct FirrtlWorker
 				if (offset != 0)
 					log_error("Memory with nonzero offset: %s.%s\n", log_id(module), log_id(cell));
 
-				cell_exprs.push_back(stringf("    mem %s:\n", mem_id.c_str()));
-				cell_exprs.push_back(stringf("      data-type => UInt<%d>\n", width));
-				cell_exprs.push_back(stringf("      depth => %d\n", size));
-
-				for (int i = 0; i < rd_ports; i++)
-					cell_exprs.push_back(stringf("      reader => r%d\n", i));
-
-				for (int i = 0; i < wr_ports; i++)
-					cell_exprs.push_back(stringf("      writer => w%d\n", i));
-
-				cell_exprs.push_back(stringf("      read-latency => 0\n"));
-				cell_exprs.push_back(stringf("      write-latency => 1\n"));
-				cell_exprs.push_back(stringf("      read-under-write => undefined\n"));
-
 				for (int i = 0; i < rd_ports; i++)
 				{
 					if (rd_clk_enable[i] != State::S0)
 						log_error("Clocked read port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
 
+					SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(i*abits, abits);
 					SigSpec data_sig = cell->getPort("\\RD_DATA").extract(i*width, width);
-					string addr_expr = make_expr(cell->getPort("\\RD_ADDR").extract(i*abits, abits));
-
-					cell_exprs.push_back(stringf("    %s.r%d.addr <= %s\n", mem_id.c_str(), i, addr_expr.c_str()));
-					cell_exprs.push_back(stringf("    %s.r%d.en <= UInt<1>(1)\n", mem_id.c_str(), i));
-					cell_exprs.push_back(stringf("    %s.r%d.clk <= asClock(UInt<1>(0))\n", mem_id.c_str(), i));
-
-					register_reverse_wire_map(stringf("%s.r%d.data", mem_id.c_str(), i), data_sig);
+					string addr_expr = make_expr(addr_sig);
+					string name(stringf("%s.r%d", m.name.c_str(), i));
+					bool clk_enable = false;
+					bool clk_parity = true;
+					bool transparency = false;
+					SigSpec ena_sig = RTLIL::SigSpec(RTLIL::State::S1, 1);
+					SigSpec clk_sig = RTLIL::SigSpec(RTLIL::State::S0, 1);
+					read_port rp(name, clk_enable, clk_parity, transparency, clk_sig, ena_sig, addr_sig);
+					m.add_memory_read_port(rp);
+					cell_exprs.push_back(rp.gen_read(indent.c_str()));
+					register_reverse_wire_map(stringf("%s.data", name.c_str()), data_sig);
 				}
 
 				for (int i = 0; i < wr_ports; i++)
@@ -557,9 +649,16 @@ struct FirrtlWorker
 					if (wr_clk_polarity[i] != State::S1)
 						log_error("Negedge write port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
 
-					string addr_expr = make_expr(cell->getPort("\\WR_ADDR").extract(i*abits, abits));
-					string data_expr = make_expr(cell->getPort("\\WR_DATA").extract(i*width, width));
-					string clk_expr = make_expr(cell->getPort("\\WR_CLK").extract(i));
+					string name(stringf("%s.w%d", m.name.c_str(), i));
+					bool clk_enable = true;
+					bool clk_parity = true;
+					bool transparency = false;
+					SigSpec addr_sig =cell->getPort("\\WR_ADDR").extract(i*abits, abits);
+					string addr_expr = make_expr(addr_sig);
+					SigSpec data_sig =cell->getPort("\\WR_DATA").extract(i*width, width);
+					string data_expr = make_expr(data_sig);
+					SigSpec clk_sig = cell->getPort("\\WR_CLK").extract(i);
+					string clk_expr = make_expr(clk_sig);
 
 					SigSpec wen_sig = cell->getPort("\\WR_EN").extract(i*width, width);
 					string wen_expr = make_expr(wen_sig[0]);
@@ -568,13 +667,50 @@ struct FirrtlWorker
 						if (wen_sig[0] != wen_sig[i])
 							log_error("Complex write enable on port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
 
-					cell_exprs.push_back(stringf("    %s.w%d.addr <= %s\n", mem_id.c_str(), i, addr_expr.c_str()));
-					cell_exprs.push_back(stringf("    %s.w%d.data <= %s\n", mem_id.c_str(), i, data_expr.c_str()));
-					cell_exprs.push_back(stringf("    %s.w%d.en <= %s\n", mem_id.c_str(), i, wen_expr.c_str()));
-					cell_exprs.push_back(stringf("    %s.w%d.mask <= UInt<1>(1)\n", mem_id.c_str(), i));
-					cell_exprs.push_back(stringf("    %s.w%d.clk <= asClock(%s)\n", mem_id.c_str(), i, clk_expr.c_str()));
+					SigSpec mask_sig = RTLIL::SigSpec(RTLIL::State::S1, 1);
+					write_port wp(name, clk_enable, clk_parity, transparency, clk_sig, wen_sig[0], addr_sig, mask_sig);
+					m.add_memory_write_port(wp);
+					cell_exprs.push_back(stringf("%s%s.data <= %s\n", indent.c_str(), name.c_str(), data_expr.c_str()));
+					cell_exprs.push_back(wp.gen_write(indent.c_str()));
 				}
+				register_memory(m);
+				continue;
+			}
 
+			if (cell->type.in("$memwr", "$memrd", "$meminit"))
+			{
+				std::string cell_type = fid(cell->type);
+				std::string mem_id = make_id(cell->parameters["\\MEMID"].decode_string());
+				memory *mp = nullptr;
+				if (cell->type == "$meminit" ) {
+					log_error("$meminit (%s.%s.%s) currently unsupported\n", log_id(module), log_id(cell), mem_id.c_str());
+				} else {
+					// It's a $memwr or $memrd. Remember the read/write port parameters for the eventual FIRRTL memory definition.
+					auto addrSig = cell->getPort("\\ADDR");
+					auto dataSig = cell->getPort("\\DATA");
+					auto enableSig = cell->getPort("\\EN");
+					auto clockSig = cell->getPort("\\CLK");
+					Const clk_enable = cell->parameters.at("\\CLK_ENABLE");
+					Const clk_polarity = cell->parameters.at("\\CLK_POLARITY");
+
+					mp = &memories.at(mem_id);
+					int portNum = 0;
+					bool transparency = false;
+					string data_expr = make_expr(dataSig);
+					if (cell->type.in("$memwr")) {
+						portNum = (int) mp->write_ports.size();
+						write_port wp(stringf("%s.w%d", mem_id.c_str(), portNum), clk_enable.as_bool(), clk_polarity.as_bool(),  transparency, clockSig, enableSig, addrSig, dataSig);
+						mp->add_memory_write_port(wp);
+						cell_exprs.push_back(stringf("%s%s.data <= %s\n", indent.c_str(), wp.name.c_str(), data_expr.c_str()));
+						cell_exprs.push_back(wp.gen_write(indent.c_str()));
+					} else if (cell->type.in("$memrd")) {
+						portNum = (int) mp->read_ports.size();
+						read_port rp(stringf("%s.r%d", mem_id.c_str(), portNum), clk_enable.as_bool(), clk_polarity.as_bool(),  transparency, clockSig, enableSig, addrSig);
+						mp->add_memory_read_port(rp);
+						cell_exprs.push_back(rp.gen_read(indent.c_str()));
+						register_reverse_wire_map(stringf("%s.data", rp.name.c_str()), dataSig);
+					}
+				}
 				continue;
 			}
 
@@ -752,6 +888,24 @@ struct FirrtlWorker
 
 		f << stringf("\n");
 
+		// If we have any memory definitions, output them.
+		for (auto kv : memories) {
+			memory m = kv.second;
+			f << stringf("    mem %s:\n", m.name.c_str());
+			f << stringf("      data-type => UInt<%d>\n", m.width);
+			f << stringf("      depth => %d\n", m.size);
+			for (int i = 0; i < (int) m.read_ports.size(); i += 1) {
+				f << stringf("      reader => r%d\n", i);
+			}
+			for (int i = 0; i < (int) m.write_ports.size(); i += 1) {
+				f << stringf("      writer => w%d\n", i);
+			}
+			f << stringf("      read-latency => %d\n", m.read_latency);
+			f << stringf("      write-latency => %d\n", m.write_latency);
+			f << stringf("      read-under-write => undefined\n");
+		}
+		f << stringf("\n");
+
 		for (auto str : cell_exprs)
 			f << str;
 
diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index 4c58ea087..dc39e5e08 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -204,7 +204,7 @@ void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const
 		f << stringf("%s  case ", indent.c_str());
 		for (size_t i = 0; i < (*it)->compare.size(); i++) {
 			if (i > 0)
-				f << stringf(", ");
+				f << stringf(" , ");
 			dump_sigspec(f, (*it)->compare[i]);
 		}
 		f << stringf("\n");
diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc
index f56147cef..549fc73ae 100644
--- a/backends/protobuf/protobuf.cc
+++ b/backends/protobuf/protobuf.cc
@@ -48,7 +48,7 @@ struct ProtobufDesignSerializer
 
 	ProtobufDesignSerializer(bool use_selection, bool aig_mode) :
 			aig_mode_(aig_mode), use_selection_(use_selection) { }
-	
+
 	string get_name(IdString name)
 	{
 		return RTLIL::unescape_id(name);
@@ -60,7 +60,7 @@ struct ProtobufDesignSerializer
 	{
 		for (auto &param : parameters) {
 			std::string key = get_name(param.first);
-			
+
 
 			yosys::pb::Parameter pb_param;
 
@@ -207,7 +207,7 @@ struct ProtobufDesignSerializer
 			(*models)[aig.name] = pb_model;
 		}
 	}
-	
+
 	void serialize_design(yosys::pb::Design *pb, Design *design)
 	{
 		GOOGLE_PROTOBUF_VERIFY_VERSION;
diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index dce82f01a..92941d4cf 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -3,14 +3,30 @@ OBJS += backends/smt2/smt2.o
 
 ifneq ($(CONFIG),mxe)
 ifneq ($(CONFIG),emcc)
+
+# MSYS targets support yosys-smtbmc, but require a launcher script
+ifeq ($(CONFIG),$(filter $(CONFIG),msys2 msys2-64))
+TARGETS += yosys-smtbmc.exe yosys-smtbmc-script.py
+# Needed to find the Python interpreter for yosys-smtbmc scripts.
+# Override if necessary, it is only used for msys2 targets.
+PYTHON := $(shell cygpath -w -m $(PREFIX)/bin/python3)
+
+yosys-smtbmc-script.py: backends/smt2/smtbmc.py
+	$(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' \
+		-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
+
+yosys-smtbmc.exe: misc/launcher.c yosys-smtbmc-script.py
+	$(P) gcc -DGUI=0 -O -s -o $@ $<
+# Other targets
+else
 TARGETS += yosys-smtbmc
 
 yosys-smtbmc: backends/smt2/smtbmc.py
 	$(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new
 	$(Q) chmod +x $@.new
 	$(Q) mv $@.new $@
+endif
 
 $(eval $(call add_share_file,share/python3,backends/smt2/smtio.py))
 endif
 endif
-
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 418f8d766..688535f33 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -416,6 +416,7 @@ struct Smt2Worker
 		for (char ch : expr) {
 			if (ch == 'A') processed_expr += get_bv(sig_a);
 			else if (ch == 'B') processed_expr += get_bv(sig_b);
+			else if (ch == 'P') processed_expr += get_bv(cell->getPort("\\B"));
 			else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
 			else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
 			else processed_expr += ch;
@@ -554,7 +555,7 @@ struct Smt2Worker
 
 			if (cell->type.in("$shift", "$shiftx")) {
 				if (cell->getParam("\\B_SIGNED").as_bool()) {
-					return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) "
+					return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
 							"(bvlshr A B) (bvlshr A (bvneg B)))",
 							GetSize(cell->getPort("\\B")), 0), 's');
 				} else {
@@ -887,8 +888,8 @@ struct Smt2Worker
 
 				string name_a = get_bool(cell->getPort("\\A"));
 				string name_en = get_bool(cell->getPort("\\EN"));
-				decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id,
-						cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
+				string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\src").decode_string() : get_id(cell);
+				decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str()));
 
 				if (cell->type == "$cover")
 					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
@@ -1103,20 +1104,27 @@ struct Smt2Worker
 							break;
 
 						Const initword = init_data.extract(i*width, width, State::Sx);
+						Const initmask = initword;
 						bool gen_init_constr = false;
 
-						for (auto bit : initword.bits)
-							if (bit == State::S0 || bit == State::S1)
+						for (int k = 0; k < GetSize(initword); k++) {
+							if (initword[k] == State::S0 || initword[k] == State::S1) {
 								gen_init_constr = true;
+								initmask[k] = State::S1;
+							} else {
+								initmask[k] = State::S0;
+								initword[k] = State::S0;
+							}
+						}
 
 						if (gen_init_constr)
 						{
 							if (statebv)
 								/* FIXME */;
 							else
-								init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
+								init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]",
 										get_id(module), arrayid, Const(i, abits).as_string().c_str(),
-										initword.as_string().c_str(), get_id(cell), i));
+										initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i));
 						}
 					}
 				}
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 94a5e2da0..445a42e0d 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -1484,11 +1484,11 @@ else:  # not tempind, covermode
                             smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
                             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
                             smt_assert_consequent(get_constr_expr(constr_assumes, i))
-                    print_msg("Re-solving with appended steps..")
-                    if smt_check_sat() == "unsat":
-                        print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
-                        retstatus = False
-                        break
+                        print_msg("Re-solving with appended steps..")
+                        if smt_check_sat() == "unsat":
+                            print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
+                            retstatus = False
+                            break
                     print_anyconsts(step)
                     for i in range(step, last_check_step+1):
                         print_failed_asserts(i)
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index d351a6266..83d83f488 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -33,7 +33,7 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
-bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, defparam, decimal;
+bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, defparam, decimal, siminit;
 int auto_name_counter, auto_name_offset, auto_name_digits;
 std::map<RTLIL::IdString, int> auto_name_map;
 std::set<RTLIL::IdString> reg_wires, reg_ct;
@@ -1310,7 +1310,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		}
 	}
 
-	if (reg_ct.count(cell->type) && cell->hasPort("\\Q")) {
+	if (siminit && reg_ct.count(cell->type) && cell->hasPort("\\Q")) {
 		std::stringstream ss;
 		dump_reg_init(ss, cell->getPort("\\Q"));
 		if (!ss.str().empty()) {
@@ -1607,6 +1607,10 @@ struct VerilogBackend : public Backend {
 		log("        without this option all internal cells are converted to Verilog\n");
 		log("        expressions.\n");
 		log("\n");
+		log("    -siminit\n");
+		log("        add initial statements with hierarchical refs to initialize FFs when\n");
+		log("        in -noexpr mode.\n");
+		log("\n");
 		log("    -nodec\n");
 		log("        32-bit constant values are by default dumped as decimal numbers,\n");
 		log("        not bit pattern. This option deactivates this feature and instead\n");
@@ -1663,11 +1667,14 @@ struct VerilogBackend : public Backend {
 		nostr = false;
 		defparam = false;
 		decimal = false;
+		siminit = false;
 		auto_prefix = "";
 
 		bool blackboxes = false;
 		bool selected = false;
 
+		auto_name_map.clear();
+		reg_wires.clear();
 		reg_ct.clear();
 
 		reg_ct.insert("$dff");
@@ -1739,6 +1746,10 @@ struct VerilogBackend : public Backend {
 				decimal = true;
 				continue;
 			}
+			if (arg == "-siminit") {
+				siminit = true;
+				continue;
+			}
 			if (arg == "-blackboxes") {
 				blackboxes = true;
 				continue;
@@ -1770,6 +1781,8 @@ struct VerilogBackend : public Backend {
 			dump_module(*f, "", it->second);
 		}
 
+		auto_name_map.clear();
+		reg_wires.clear();
 		reg_ct.clear();
 	}
 } VerilogBackend;