New upstream version 0.9

15 files changed, 453 insertions, 72 deletions

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index dfe506c6..6863b40f 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -89,7 +89,8 @@ struct AigerWriter
 				aig_map[bit] = mkgate(a0, a1);
 			} else
 			if (alias_map.count(bit)) {
-				aig_map[bit] = bit2aig(alias_map.at(bit));
+                int a = bit2aig(alias_map.at(bit));
+				aig_map[bit] = a;
 			}
 
 			if (bit == State::Sx || bit == State::Sz)
@@ -776,6 +777,7 @@ struct AigerBackend : public Backend {
 		writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode);
 
 		if (!map_filename.empty()) {
+			rewrite_filename(filename);
 			std::ofstream mapf;
 			mapf.open(map_filename.c_str(), std::ofstream::trunc);
 			if (mapf.fail())
diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc
index 0db5ff27..a1761b66 100644
--- a/backends/blif/blif.cc
+++ b/backends/blif/blif.cc
@@ -140,7 +140,7 @@ struct BlifDumper
 			return "subckt";
 		if (!design->modules_.count(RTLIL::escape_id(cell_type)))
 			return "gate";
-		if (design->modules_.at(RTLIL::escape_id(cell_type))->get_bool_attribute("\\blackbox"))
+		if (design->modules_.at(RTLIL::escape_id(cell_type))->get_blackbox_attribute())
 			return "gate";
 		return "subckt";
 	}
@@ -196,7 +196,7 @@ struct BlifDumper
 		}
 		f << stringf("\n");
 
-		if (module->get_bool_attribute("\\blackbox")) {
+		if (module->get_blackbox_attribute()) {
 			f << stringf(".blackbox\n");
 			f << stringf(".end\n");
 			return;
@@ -409,12 +409,26 @@ struct BlifDumper
 
 			f << stringf(".%s %s", subckt_or_gate(cell->type.str()), cstr(cell->type));
 			for (auto &conn : cell->connections())
-			for (int i = 0; i < conn.second.size(); i++) {
-				if (conn.second.size() == 1)
-					f << stringf(" %s", cstr(conn.first));
-				else
-					f << stringf(" %s[%d]", cstr(conn.first), i);
-				f << stringf("=%s", cstr(conn.second.extract(i, 1)));
+			{
+				if (conn.second.size() == 1) {
+					f << stringf(" %s=%s", cstr(conn.first), cstr(conn.second[0]));
+					continue;
+				}
+
+				Module *m = design->module(cell->type);
+				Wire *w = m ? m->wire(conn.first) : nullptr;
+
+				if (w == nullptr) {
+					for (int i = 0; i < GetSize(conn.second); i++)
+						f << stringf(" %s[%d]=%s", cstr(conn.first), i, cstr(conn.second[i]));
+				} else {
+					for (int i = 0; i < std::min(GetSize(conn.second), GetSize(w)); i++) {
+						SigBit sig(w, i);
+						f << stringf(" %s[%d]=%s", cstr(conn.first), sig.wire->upto ?
+								sig.wire->start_offset+sig.wire->width-sig.offset-1 :
+								sig.wire->start_offset+sig.offset, cstr(conn.second[i]));
+					}
+				}
 			}
 			f << stringf("\n");
 
@@ -640,7 +654,7 @@ struct BlifBackend : public Backend {
 		for (auto module_it : design->modules_)
 		{
 			RTLIL::Module *module = module_it.second;
-			if (module->get_bool_attribute("\\blackbox") && !config.blackbox_mode)
+			if (module->get_blackbox_attribute() && !config.blackbox_mode)
 				continue;
 
 			if (module->processes.size() != 0)
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 55c49499..a507b120 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -17,6 +17,11 @@
  *
  */
 
+// [[CITE]] Btor2 , BtorMC and Boolector 3.0
+// Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
+// Computer Aided Verification - 30th International Conference, CAV 2018
+// https://cs.stanford.edu/people/niemetz/publication/2018/niemetzpreinerwolfbiere-cav18/
+
 #include "kernel/rtlil.h"
 #include "kernel/register.h"
 #include "kernel/sigtools.h"
@@ -129,7 +134,13 @@ struct BtorWorker
 
 	void export_cell(Cell *cell)
 	{
-		log_assert(cell_recursion_guard.count(cell) == 0);
+		if (cell_recursion_guard.count(cell)) {
+			string cell_list;
+			for (auto c : cell_recursion_guard)
+				cell_list += stringf("\n    %s", log_id(c));
+			log_error("Found topological loop while processing cell %s. Active cells:%s\n", log_id(cell), cell_list.c_str());
+		}
+
 		cell_recursion_guard.insert(cell);
 		btorf_push(log_id(cell));
 
@@ -340,7 +351,7 @@ struct BtorWorker
 			if (cell->type == "$lt") btor_op = "lt";
 			if (cell->type == "$le") btor_op = "lte";
 			if (cell->type.in("$eq", "$eqx")) btor_op = "eq";
-			if (cell->type.in("$ne", "$nex")) btor_op = "ne";
+			if (cell->type.in("$ne", "$nex")) btor_op = "neq";
 			if (cell->type == "$ge") btor_op = "gte";
 			if (cell->type == "$gt") btor_op = "gt";
 			log_assert(!btor_op.empty());
@@ -869,9 +880,28 @@ struct BtorWorker
 					else
 					{
 						if (bit_cell.count(bit) == 0)
-							log_error("No driver for signal bit %s.\n", log_signal(bit));
-						export_cell(bit_cell.at(bit));
-						log_assert(bit_nid.count(bit));
+						{
+							SigSpec s = bit;
+
+							while (i+GetSize(s) < GetSize(sig) && sig[i+GetSize(s)].wire != nullptr &&
+									bit_cell.count(sig[i+GetSize(s)]) == 0)
+								s.append(sig[i+GetSize(s)]);
+
+							log_warning("No driver for signal %s.\n", log_signal(s));
+
+							int sid = get_bv_sid(GetSize(s));
+							int nid = next_nid++;
+							btorf("%d input %d %s\n", nid, sid);
+							nid_width[nid] = GetSize(s);
+
+							i += GetSize(s)-1;
+							continue;
+						}
+						else
+						{
+							export_cell(bit_cell.at(bit));
+							log_assert(bit_nid.count(bit));
+						}
 					}
 				}
 
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index 7e30b67a..6d946953 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -178,7 +178,7 @@ struct EdifBackend : public Backend {
 		for (auto module_it : design->modules_)
 		{
 			RTLIL::Module *module = module_it.second;
-			if (module->get_bool_attribute("\\blackbox"))
+			if (module->get_blackbox_attribute())
 				continue;
 
 			if (top_module_name.empty())
@@ -192,7 +192,7 @@ struct EdifBackend : public Backend {
 			for (auto cell_it : module->cells_)
 			{
 				RTLIL::Cell *cell = cell_it.second;
-				if (!design->modules_.count(cell->type) || design->modules_.at(cell->type)->get_bool_attribute("\\blackbox")) {
+				if (!design->modules_.count(cell->type) || design->modules_.at(cell->type)->get_blackbox_attribute()) {
 					lib_cell_ports[cell->type];
 					for (auto p : cell->connections())
 						lib_cell_ports[cell->type][p.first] = GetSize(p.second);
@@ -302,7 +302,7 @@ struct EdifBackend : public Backend {
 		*f << stringf("    (technology (numberDefinition))\n");
 		for (auto module : sorted_modules)
 		{
-			if (module->get_bool_attribute("\\blackbox"))
+			if (module->get_blackbox_attribute())
 				continue;
 
 			SigMap sigmap(module);
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index eef6401b..1c7a7351 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -106,6 +106,125 @@ 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 {
+		Cell *pCell;					// for error reporting
+		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;
+		string srcLine;
+		memory(Cell *pCell, string name, int abits, int size, int width) : pCell(pCell), name(name), abits(abits), size(size), width(width), read_latency(0), write_latency(1), init_file(""), init_file_srcFileSpec("") {
+			// Provide defaults for abits or size if one (but not the other) is specified.
+			if (this->abits == 0 && this->size != 0) {
+				this->abits = ceil_log2(this->size);
+			} else if (this->abits != 0 && this->size == 0) {
+				this->size = 1 << this->abits;
+			}
+			// Sanity-check this construction.
+			if (this->name == "") {
+				log_error("Nameless memory%s\n", this->atLine());
+			}
+			if (this->abits == 0 && this->size == 0) {
+				log_error("Memory %s has zero address bits and size%s\n", this->name.c_str(), this->atLine());
+			}
+			if (this->width == 0) {
+				log_error("Memory %s has zero width%s\n", this->name.c_str(), this->atLine());
+			}
+		 }
+		// We need a default constructor for the dict insert.
+	   memory() : pCell(0), read_latency(0), write_latency(1), init_file(""), init_file_srcFileSpec(""){}
+
+		const char *atLine() {
+			if (srcLine == "") {
+				if (pCell) {
+					auto p = pCell->attributes.find("\\src");
+					srcLine = " at " + p->second.decode_string();
+				}
+			}
+			return srcLine.c_str();
+		}
+		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 +235,7 @@ struct FirrtlWorker
 	{
 	}
 
-	string make_expr(const SigSpec &sig)
+	static string make_expr(const SigSpec &sig)
 	{
 		string expr;
 
@@ -225,6 +344,7 @@ struct FirrtlWorker
 				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));
+						/* FALLTHRU */
 					case FD_OUT:
 						sourceExpr = firstName;
 						sinkExpr = secondExpr;
@@ -232,7 +352,7 @@ struct FirrtlWorker
 						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 */
+						/* FALLTHRU */
 					case FD_IN:
 						sourceExpr = secondExpr;
 						sinkExpr = firstName;
@@ -329,8 +449,10 @@ struct FirrtlWorker
 				string primop;
 				bool always_uint = false;
 				if (cell->type == "$not") primop = "not";
-				else if (cell->type == "$neg") primop = "neg";
-				else if (cell->type == "$logic_not") {
+				else if (cell->type == "$neg") {
+					primop = "neg";
+					is_signed = true;	// Result of "neg" is signed (an SInt).
+				} else if (cell->type == "$logic_not") {
                                         primop = "eq";
                                         a_expr = stringf("%s, UInt(0)", a_expr.c_str());
                                 }
@@ -442,6 +564,7 @@ struct FirrtlWorker
 					auto b_sig = cell->getPort("\\B");
 					if (b_sig.is_fully_const()) {
 						primop = "shl";
+						b_expr = std::to_string(b_sig.as_int());
 					} else {
 						primop = "dshl";
 						// Convert from FIRRTL left shift semantics.
@@ -455,6 +578,7 @@ struct FirrtlWorker
 					auto b_sig = cell->getPort("\\B");
 					if (b_sig.is_fully_const()) {
 						primop = "shr";
+						b_expr = std::to_string(b_sig.as_int());
 					} else {
 						primop = "dshr";
 					}
@@ -515,6 +639,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(cell, 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();
 
@@ -531,33 +656,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++)
@@ -568,9 +684,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]);
@@ -579,13 +702,57 @@ 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());
+				int abits = cell->parameters.at("\\ABITS").as_int();
+				int width = cell->parameters.at("\\WIDTH").as_int();
+				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");
+
+					// Do we already have an entry for this memory?
+					if (memories.count(mem_id) == 0) {
+						memory m(cell, mem_id, abits, 0, width);
+						register_memory(m);
+					}
+					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;
 			}
 
@@ -763,6 +930,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 dc39e5e0..313af7d5 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -160,7 +160,10 @@ void ILANG_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL::
 	}
 	f << stringf("%s" "cell %s %s\n", indent.c_str(), cell->type.c_str(), cell->name.c_str());
 	for (auto &it : cell->parameters) {
-		f << stringf("%s  parameter%s %s ", indent.c_str(), (it.second.flags & RTLIL::CONST_FLAG_SIGNED) != 0 ? " signed" : "", it.first.c_str());
+		f << stringf("%s  parameter%s%s %s ", indent.c_str(),
+				(it.second.flags & RTLIL::CONST_FLAG_SIGNED) != 0 ? " signed" : "",
+				(it.second.flags & RTLIL::CONST_FLAG_REAL) != 0 ? " real" : "",
+				it.first.c_str());
 		dump_const(f, it.second);
 		f << stringf("\n");
 	}
@@ -201,6 +204,11 @@ void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const
 
 	for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it)
 	{
+		for (auto ait = (*it)->attributes.begin(); ait != (*it)->attributes.end(); ++ait) {
+			f << stringf("%s  attribute %s ", indent.c_str(), ait->first.c_str());
+			dump_const(f, ait->second);
+			f << stringf("\n");
+		}
 		f << stringf("%s  case ", indent.c_str());
 		for (size_t i = 0; i < (*it)->compare.size(); i++) {
 			if (i > 0)
@@ -480,6 +488,7 @@ struct DumpPass : public Pass {
 		std::stringstream buf;
 
 		if (!filename.empty()) {
+			rewrite_filename(filename);
 			std::ofstream *ff = new std::ofstream;
 			ff->open(filename.c_str(), append ? std::ofstream::app : std::ofstream::trunc);
 			if (ff->fail()) {
diff --git a/backends/intersynth/intersynth.cc b/backends/intersynth/intersynth.cc
index 2eb08dbe..b0e3cd25 100644
--- a/backends/intersynth/intersynth.cc
+++ b/backends/intersynth/intersynth.cc
@@ -127,7 +127,7 @@ struct IntersynthBackend : public Backend {
 			RTLIL::Module *module = module_it.second;
 			SigMap sigmap(module);
 
-			if (module->get_bool_attribute("\\blackbox"))
+			if (module->get_blackbox_attribute())
 				continue;
 			if (module->memories.size() == 0 && module->processes.size() == 0 && module->cells_.size() == 0)
 				continue;
diff --git a/backends/json/json.cc b/backends/json/json.cc
index f5c68798..dda4dfed 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -126,6 +126,10 @@ struct JsonWriter
 			f << stringf("%s\n", first ? "" : ",");
 			f << stringf("        %s: {\n", get_name(n).c_str());
 			f << stringf("          \"direction\": \"%s\",\n", w->port_input ? w->port_output ? "inout" : "input" : "output");
+			if (w->start_offset)
+				f << stringf("          \"offset\": %d,\n", w->start_offset);
+			if (w->upto)
+				f << stringf("          \"upto\": 1,\n");
 			f << stringf("          \"bits\": %s\n", get_bits(w).c_str());
 			f << stringf("        }");
 			first = false;
@@ -189,6 +193,10 @@ struct JsonWriter
 			f << stringf("        %s: {\n", get_name(w->name).c_str());
 			f << stringf("          \"hide_name\": %s,\n", w->name[0] == '$' ? "1" : "0");
 			f << stringf("          \"bits\": %s,\n", get_bits(w).c_str());
+			if (w->start_offset)
+				f << stringf("          \"offset\": %d,\n", w->start_offset);
+			if (w->upto)
+				f << stringf("          \"upto\": 1,\n");
 			f << stringf("          \"attributes\": {");
 			write_parameters(w->attributes);
 			f << stringf("\n          }\n");
@@ -525,6 +533,7 @@ struct JsonPass : public Pass {
 		std::stringstream buf;
 
 		if (!filename.empty()) {
+			rewrite_filename(filename);
 			std::ofstream *ff = new std::ofstream;
 			ff->open(filename.c_str(), std::ofstream::trunc);
 			if (ff->fail()) {
diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc
index 549fc73a..fff110bb 100644
--- a/backends/protobuf/protobuf.cc
+++ b/backends/protobuf/protobuf.cc
@@ -336,6 +336,7 @@ struct ProtobufPass : public Pass {
 		std::stringstream buf;
 
 		if (!filename.empty()) {
+			rewrite_filename(filename);
 			std::ofstream *ff = new std::ofstream;
 			ff->open(filename.c_str(), std::ofstream::trunc);
 			if (ff->fail()) {
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 688535f3..e318a405 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -1543,7 +1543,7 @@ struct Smt2Backend : public Backend {
 
 		for (auto module : sorted_modules)
 		{
-			if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn())
+			if (module->get_blackbox_attribute() || module->has_memories_warn() || module->has_processes_warn())
 				continue;
 
 			log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index ab20a4af..ae7968a1 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -1023,6 +1023,8 @@ class MkVcd:
         assert t >= self.t
         if t != self.t:
             if self.t == -1:
+                print("$version Generated by Yosys-SMTBMC $end", file=self.f)
+                print("$timescale 1ns $end", file=self.f)
                 print("$var integer 32 t smt_step $end", file=self.f)
                 print("$var event 1 ! smt_clock $end", file=self.f)
 
@@ -1041,7 +1043,10 @@ class MkVcd:
                         scope = scope[:-1]
 
                     while uipath[:-1] != scope:
-                        print("$scope module %s $end" % uipath[len(scope)], file=self.f)
+                        scopename = uipath[len(scope)]
+                        if scopename.startswith("$"):
+                            scopename = "\\" + scopename
+                        print("$scope module %s $end" % scopename, file=self.f)
                         scope.append(uipath[len(scope)])
 
                     if path in self.clocks and self.clocks[path][1] == "event":
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index f379c9c4..d75456c1 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -739,7 +739,7 @@ struct SmvBackend : public Backend {
 		pool<Module*> modules;
 
 		for (auto module : design->modules())
-			if (!module->get_bool_attribute("\\blackbox") && !module->has_memories_warn() && !module->has_processes_warn())
+			if (!module->get_blackbox_attribute() && !module->has_memories_warn() && !module->has_processes_warn())
 				modules.insert(module);
 
 		if (template_f.is_open())
diff --git a/backends/spice/spice.cc b/backends/spice/spice.cc
index b6a3f1e7..6738a4bb 100644
--- a/backends/spice/spice.cc
+++ b/backends/spice/spice.cc
@@ -212,7 +212,7 @@ struct SpiceBackend : public Backend {
 		for (auto module_it : design->modules_)
 		{
 			RTLIL::Module *module = module_it.second;
-			if (module->get_bool_attribute("\\blackbox"))
+			if (module->get_blackbox_attribute())
 				continue;
 
 			if (module->processes.size() != 0)
diff --git a/backends/table/table.cc b/backends/table/table.cc
index b75169ea..796f1805 100644
--- a/backends/table/table.cc
+++ b/backends/table/table.cc
@@ -67,7 +67,7 @@ struct TableBackend : public Backend {
 
 		for (auto module : design->modules())
 		{
-			if (module->get_bool_attribute("\\blackbox"))
+			if (module->get_blackbox_attribute())
 				continue;
 
 			SigMap sigmap(module);
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 83d83f48..087c6fec 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -183,10 +183,15 @@ bool is_reg_wire(RTLIL::SigSpec sig, std::string &reg_name)
 	return true;
 }
 
-void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool no_decimal = false, bool set_signed = false, bool escape_comment = false)
+void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool no_decimal = false, bool escape_comment = false)
 {
+	bool set_signed = (data.flags & RTLIL::CONST_FLAG_SIGNED) != 0;
 	if (width < 0)
 		width = data.bits.size() - offset;
+	if (width == 0) {
+		f << "\"\"";
+		return;
+	}
 	if (nostr)
 		goto dump_hex;
 	if ((data.flags & RTLIL::CONST_FLAG_STRING) == 0 || width != (int)data.bits.size()) {
@@ -271,7 +276,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
 			}
 		}
 	} else {
-		f << stringf("\"");
+		if ((data.flags & RTLIL::CONST_FLAG_REAL) == 0)
+			f << stringf("\"");
 		std::string str = data.decode_string();
 		for (size_t i = 0; i < str.size(); i++) {
 			if (str[i] == '\n')
@@ -289,7 +295,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
 			else
 				f << str[i];
 		}
-		f << stringf("\"");
+		if ((data.flags & RTLIL::CONST_FLAG_REAL) == 0)
+			f << stringf("\"");
 	}
 }
 
@@ -340,6 +347,10 @@ void dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, bool no_decima
 
 void dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig)
 {
+	if (GetSize(sig) == 0) {
+		f << "\"\"";
+		return;
+	}
 	if (sig.is_chunk()) {
 		dump_sigchunk(f, sig.as_chunk());
 	} else {
@@ -353,20 +364,22 @@ void dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig)
 	}
 }
 
-void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString, RTLIL::Const> &attributes, char term = '\n', bool modattr = false)
+void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString, RTLIL::Const> &attributes, char term = '\n', bool modattr = false, bool as_comment = false)
 {
 	if (noattr)
 		return;
+	if (attr2comment)
+		as_comment = true;
 	for (auto it = attributes.begin(); it != attributes.end(); ++it) {
-		f << stringf("%s" "%s %s", indent.c_str(), attr2comment ? "/*" : "(*", id(it->first).c_str());
+		f << stringf("%s" "%s %s", indent.c_str(), as_comment ? "/*" : "(*", id(it->first).c_str());
 		f << stringf(" = ");
 		if (modattr && (it->second == Const(0, 1) || it->second == Const(0)))
 			f << stringf(" 0 ");
 		else if (modattr && (it->second == Const(1, 1) || it->second == Const(1)))
 			f << stringf(" 1 ");
 		else
-			dump_const(f, it->second, -1, 0, false, false, attr2comment);
-		f << stringf(" %s%c", attr2comment ? "*/" : "*)", term);
+			dump_const(f, it->second, -1, 0, false, as_comment);
+		f << stringf(" %s%c", as_comment ? "*/" : "*)", term);
 	}
 }
 
@@ -1234,6 +1247,118 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
+	if (cell->type.in("$assert", "$assume", "$cover"))
+	{
+		f << stringf("%s" "always @* if (", indent.c_str());
+		dump_sigspec(f, cell->getPort("\\EN"));
+		f << stringf(") %s(", cell->type.c_str()+1);
+		dump_sigspec(f, cell->getPort("\\A"));
+		f << stringf(");\n");
+		return true;
+	}
+
+	if (cell->type.in("$specify2", "$specify3"))
+	{
+		f << stringf("%s" "specify\n%s  ", indent.c_str(), indent.c_str());
+
+		SigSpec en = cell->getPort("\\EN");
+		if (en != State::S1) {
+			f << stringf("if (");
+			dump_sigspec(f, cell->getPort("\\EN"));
+			f << stringf(") ");
+		}
+
+		f << "(";
+		if (cell->type == "$specify3" && cell->getParam("\\EDGE_EN").as_bool())
+			f << (cell->getParam("\\EDGE_POL").as_bool() ? "posedge ": "negedge ");
+
+		dump_sigspec(f, cell->getPort("\\SRC"));
+
+		f << " ";
+		if (cell->getParam("\\SRC_DST_PEN").as_bool())
+			f << (cell->getParam("\\SRC_DST_POL").as_bool() ? "+": "-");
+		f << (cell->getParam("\\FULL").as_bool() ? "*> ": "=> ");
+
+		if (cell->type == "$specify3") {
+			f << "(";
+			dump_sigspec(f, cell->getPort("\\DST"));
+			f << " ";
+			if (cell->getParam("\\DAT_DST_PEN").as_bool())
+				f << (cell->getParam("\\DAT_DST_POL").as_bool() ? "+": "-");
+			f << ": ";
+			dump_sigspec(f, cell->getPort("\\DAT"));
+			f << ")";
+		} else {
+			dump_sigspec(f, cell->getPort("\\DST"));
+		}
+
+		bool bak_decimal = decimal;
+		decimal = 1;
+
+		f << ") = (";
+		dump_const(f, cell->getParam("\\T_RISE_MIN"));
+		f << ":";
+		dump_const(f, cell->getParam("\\T_RISE_TYP"));
+		f << ":";
+		dump_const(f, cell->getParam("\\T_RISE_MAX"));
+		f << ", ";
+		dump_const(f, cell->getParam("\\T_FALL_MIN"));
+		f << ":";
+		dump_const(f, cell->getParam("\\T_FALL_TYP"));
+		f << ":";
+		dump_const(f, cell->getParam("\\T_FALL_MAX"));
+		f << ");\n";
+
+		decimal = bak_decimal;
+
+		f << stringf("%s" "endspecify\n", indent.c_str());
+		return true;
+	}
+
+	if (cell->type == "$specrule")
+	{
+		f << stringf("%s" "specify\n%s  ", indent.c_str(), indent.c_str());
+
+		string spec_type = cell->getParam("\\TYPE").decode_string();
+		f << stringf("%s(", spec_type.c_str());
+
+		if (cell->getParam("\\SRC_PEN").as_bool())
+			f << (cell->getParam("\\SRC_POL").as_bool() ? "posedge ": "negedge ");
+		dump_sigspec(f, cell->getPort("\\SRC"));
+
+		if (cell->getPort("\\SRC_EN") != State::S1) {
+			f << " &&& ";
+			dump_sigspec(f, cell->getPort("\\SRC_EN"));
+		}
+
+		f << ", ";
+		if (cell->getParam("\\DST_PEN").as_bool())
+			f << (cell->getParam("\\DST_POL").as_bool() ? "posedge ": "negedge ");
+		dump_sigspec(f, cell->getPort("\\DST"));
+
+		if (cell->getPort("\\DST_EN") != State::S1) {
+			f << " &&& ";
+			dump_sigspec(f, cell->getPort("\\DST_EN"));
+		}
+
+		bool bak_decimal = decimal;
+		decimal = 1;
+
+		f << ", ";
+		dump_const(f, cell->getParam("\\T_LIMIT"));
+
+		if (spec_type == "$setuphold" || spec_type == "$recrem" || spec_type == "$fullskew") {
+			f << ", ";
+			dump_const(f, cell->getParam("\\T_LIMIT2"));
+		}
+
+		f << ");\n";
+		decimal = bak_decimal;
+
+		f << stringf("%s" "endspecify\n", indent.c_str());
+		return true;
+	}
+
 	// FIXME: $_SR_[PN][PN]_, $_DLATCH_[PN]_, $_DLATCHSR_[PN][PN][PN]_
 	// FIXME: $sr, $dlatch, $memrd, $memwr, $fsm
 
@@ -1256,8 +1381,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 			if (it != cell->parameters.begin())
 				f << stringf(",");
 			f << stringf("\n%s  .%s(", indent.c_str(), id(it->first).c_str());
-			bool is_signed = (it->second.flags & RTLIL::CONST_FLAG_SIGNED) != 0;
-			dump_const(f, it->second, -1, 0, false, is_signed);
+			dump_const(f, it->second);
 			f << stringf(")");
 		}
 		f << stringf("\n%s" ")", indent.c_str());
@@ -1304,8 +1428,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 	if (defparam && cell->parameters.size() > 0) {
 		for (auto it = cell->parameters.begin(); it != cell->parameters.end(); ++it) {
 			f << stringf("%sdefparam %s.%s = ", indent.c_str(), cell_name.c_str(), id(it->first).c_str());
-			bool is_signed = (it->second.flags & RTLIL::CONST_FLAG_SIGNED) != 0;
-			dump_const(f, it->second, -1, 0, false, is_signed);
+			dump_const(f, it->second);
 			f << stringf(";\n");
 		}
 	}
@@ -1371,12 +1494,14 @@ void dump_proc_switch(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw
 		return;
 	}
 
+	dump_attributes(f, indent, sw->attributes);
 	f << stringf("%s" "casez (", indent.c_str());
 	dump_sigspec(f, sw->signal);
 	f << stringf(")\n");
 
 	bool got_default = false;
 	for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it) {
+		dump_attributes(f, indent + "  ", (*it)->attributes, '\n', /*modattr=*/false, /*as_comment=*/true);
 		if ((*it)->compare.size() == 0) {
 			if (got_default)
 				continue;
@@ -1497,7 +1622,8 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 			SigSpec sig = active_sigmap(wire);
 			Const val = wire->attributes.at("\\init");
 			for (int i = 0; i < GetSize(sig) && i < GetSize(val); i++)
-				active_initdata[sig[i]] = val.bits.at(i);
+				if (val[i] == State::S0 || val[i] == State::S1)
+					active_initdata[sig[i]] = val[i];
 		}
 
 	if (!module->processes.empty())
@@ -1540,7 +1666,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 		}
 	}
 
-	dump_attributes(f, indent, module->attributes, '\n', true);
+	dump_attributes(f, indent, module->attributes, '\n', /*attr2comment=*/true);
 	f << stringf("%s" "module %s(", indent.c_str(), id(module->name, false).c_str());
 	bool keep_running = true;
 	for (int port_id = 1; keep_running; port_id++) {
@@ -1770,7 +1896,7 @@ struct VerilogBackend : public Backend {
 
 		*f << stringf("/* Generated by %s */\n", yosys_version_str);
 		for (auto it = design->modules_.begin(); it != design->modules_.end(); ++it) {
-			if (it->second->get_bool_attribute("\\blackbox") != blackboxes)
+			if (it->second->get_blackbox_attribute() != blackboxes)
 				continue;
 			if (selected && !design->selected_whole_module(it->first)) {
 				if (design->selected_module(it->first))