14 files changed, 1085 insertions, 222 deletions
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 35935b847..547d131ee 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -606,7 +606,7 @@ struct AigerWriter
 		f << stringf("c\nGenerated by %s\n", yosys_version_str);
 	}
 
-	void write_map(std::ostream &f, bool verbose_map)
+	void write_map(std::ostream &f, bool verbose_map, bool no_startoffset)
 	{
 		dict<int, string> input_lines;
 		dict<int, string> init_lines;
@@ -627,32 +627,33 @@ struct AigerWriter
 					continue;
 
 				int a = aig_map.at(sig[i]);
+				int index = no_startoffset ? i : (wire->start_offset+i);
 
 				if (verbose_map)
-					wire_lines[a] += stringf("wire %d %d %s\n", a, wire->start_offset+i, log_id(wire));
+					wire_lines[a] += stringf("wire %d %d %s\n", a, index, log_id(wire));
 
 				if (wire->port_input) {
 					log_assert((a & 1) == 0);
-					input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, wire->start_offset+i, log_id(wire));
+					input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, index, log_id(wire));
 				}
 
 				if (wire->port_output) {
 					int o = ordered_outputs.at(sig[i]);
-					output_lines[o] += stringf("output %d %d %s\n", o, wire->start_offset+i, log_id(wire));
+					output_lines[o] += stringf("output %d %d %s\n", o, index, log_id(wire));
 				}
 
 				if (init_inputs.count(sig[i])) {
 					int a = init_inputs.at(sig[i]);
 					log_assert((a & 1) == 0);
-					init_lines[a] += stringf("init %d %d %s\n", (a >> 1)-1, wire->start_offset+i, log_id(wire));
+					init_lines[a] += stringf("init %d %d %s\n", (a >> 1)-1, index, log_id(wire));
 				}
 
 				if (ordered_latches.count(sig[i])) {
 					int l = ordered_latches.at(sig[i]);
 					if (zinit_mode && (aig_latchinit.at(l) == 1))
-						latch_lines[l] += stringf("invlatch %d %d %s\n", l, wire->start_offset+i, log_id(wire));
+						latch_lines[l] += stringf("invlatch %d %d %s\n", l, index, log_id(wire));
 					else
-						latch_lines[l] += stringf("latch %d %d %s\n", l, wire->start_offset+i, log_id(wire));
+						latch_lines[l] += stringf("latch %d %d %s\n", l, index, log_id(wire));
 				}
 			}
 		}
@@ -713,6 +714,9 @@ struct AigerBackend : public Backend {
 		log("    -vmap <filename>\n");
 		log("        like -map, but more verbose\n");
 		log("\n");
+		log("    -no-startoffset\n");
+		log("        make indexes zero based, enable using map files with smt solvers.\n");
+		log("\n");
 		log("    -I, -O, -B, -L\n");
 		log("        If the design contains no input/output/assert/flip-flop then create one\n");
 		log("        dummy input/output/bad_state-pin or latch to make the tools reading the\n");
@@ -730,6 +734,7 @@ struct AigerBackend : public Backend {
 		bool omode = false;
 		bool bmode = false;
 		bool lmode = false;
+		bool no_startoffset = false;
 		std::string map_filename;
 
 		log_header(design, "Executing AIGER backend.\n");
@@ -762,6 +767,10 @@ struct AigerBackend : public Backend {
 				verbose_map = true;
 				continue;
 			}
+			if (args[argidx] == "-no-startoffset") {
+				no_startoffset = true;
+				continue;
+			}
 			if (args[argidx] == "-I") {
 				imode = true;
 				continue;
@@ -804,7 +813,7 @@ struct AigerBackend : public Backend {
 			mapf.open(map_filename.c_str(), std::ofstream::trunc);
 			if (mapf.fail())
 				log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
-			writer.write_map(mapf, verbose_map);
+			writer.write_map(mapf, verbose_map, no_startoffset);
 		}
 	}
 } AigerBackend;
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 96df54a2c..831a3ada2 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -446,25 +446,28 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in(ID($not), ID($neg), ID($_NOT_)))
+		if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos)))
 		{
 			string btor_op;
 			if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not";
 			if (cell->type == ID($neg)) btor_op = "neg";
-			log_assert(!btor_op.empty());
 
 			int width = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y)));
 
 			bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
-
-			int sid = get_bv_sid(width);
 			int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
-
-			int nid = next_nid++;
-			btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
-
 			SigSpec sig = sigmap(cell->getPort(ID::Y));
 
+			// the $pos cell just passes through, all other cells need an actual operation applied
+			int nid = nid_a;
+			if (cell->type != ID($pos))
+			{
+				log_assert(!btor_op.empty());
+				int sid = get_bv_sid(width);
+				nid = next_nid++;
+				btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
+			}
+
 			if (GetSize(sig) < width) {
 				int sid = get_bv_sid(GetSize(sig));
 				int nid2 = next_nid++;
@@ -678,7 +681,7 @@ struct BtorWorker
 			int sid = get_bv_sid(GetSize(sig_y));
 			int nid = next_nid++;
 
-			btorf("%d state %d\n", nid, sid);
+			btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str());
 
 			if (cell->type == ID($anyconst)) {
 				int nid2 = next_nid++;
@@ -699,7 +702,7 @@ struct BtorWorker
 				int one_nid = get_sig_nid(State::S1);
 				int zero_nid = get_sig_nid(State::S0);
 				initstate_nid = next_nid++;
-				btorf("%d state %d\n", initstate_nid, sid);
+				btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str());
 				btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
 				btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
 			}
@@ -1220,6 +1223,8 @@ struct BtorWorker
 
 			int this_nid = next_nid++;
 			btorf("%d uext %d %d %d%s\n", this_nid, sid, nid, 0, getinfo(wire).c_str());
+			if (info_clocks.count(nid))
+				info_clocks[this_nid] |= info_clocks[nid];
 
 			btorf_pop(stringf("wire %s", log_id(wire)));
 			continue;
@@ -1399,6 +1404,11 @@ struct BtorBackend : public Backend {
 
 		log_header(design, "Executing BTOR backend.\n");
 
+		log_push();
+		Pass::call(design, "bmuxmap");
+		Pass::call(design, "demuxmap");
+		log_pop();
+
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
 		{
diff --git a/backends/cxxrtl/cxxrtl.h b/backends/cxxrtl/cxxrtl.h
index 4552a0125..073921cc4 100644
--- a/backends/cxxrtl/cxxrtl.h
+++ b/backends/cxxrtl/cxxrtl.h
@@ -457,6 +457,42 @@ struct value : public expr_base<value<Bits>> {
 		return shr<AmountBits, /*Signed=*/true>(amount);
 	}
 
+	template<size_t ResultBits, size_t SelBits>
+	value<ResultBits> bmux(const value<SelBits> &sel) const {
+		static_assert(ResultBits << SelBits == Bits, "invalid sizes used in bmux()");
+		size_t amount = sel.data[0] * ResultBits;
+		size_t shift_chunks = amount / chunk::bits;
+		size_t shift_bits   = amount % chunk::bits;
+		value<ResultBits> result;
+		chunk::type carry = 0;
+		if (ResultBits % chunk::bits + shift_bits > chunk::bits)
+			carry = data[result.chunks + shift_chunks] << (chunk::bits - shift_bits);
+		for (size_t n = 0; n < result.chunks; n++) {
+			result.data[result.chunks - 1 - n] = carry | (data[result.chunks + shift_chunks - 1 - n] >> shift_bits);
+			carry = (shift_bits == 0) ? 0
+				: data[result.chunks + shift_chunks - 1 - n] << (chunk::bits - shift_bits);
+		}
+		return result;
+	}
+
+	template<size_t ResultBits, size_t SelBits>
+	value<ResultBits> demux(const value<SelBits> &sel) const {
+		static_assert(Bits << SelBits == ResultBits, "invalid sizes used in demux()");
+		size_t amount = sel.data[0] * Bits;
+		size_t shift_chunks = amount / chunk::bits;
+		size_t shift_bits   = amount % chunk::bits;
+		value<ResultBits> result;
+		chunk::type carry = 0;
+		for (size_t n = 0; n < chunks; n++) {
+			result.data[shift_chunks + n] = (data[n] << shift_bits) | carry;
+			carry = (shift_bits == 0) ? 0
+				: data[n] >> (chunk::bits - shift_bits);
+		}
+		if (Bits % chunk::bits + shift_bits > chunk::bits)
+			result.data[shift_chunks + chunks] = carry;
+		return result;
+	}
+
 	size_t ctpop() const {
 		size_t count = 0;
 		for (size_t n = 0; n < chunks; n++) {
@@ -722,50 +758,32 @@ std::ostream &operator<<(std::ostream &os, const wire<Bits> &val) {
 
 template<size_t Width>
 struct memory {
-	std::vector<value<Width>> data;
+	const size_t depth;
+	std::unique_ptr<value<Width>[]> data;
 
-	size_t depth() const {
-		return data.size();
-	}
-
-	memory() = delete;
-	explicit memory(size_t depth) : data(depth) {}
+	explicit memory(size_t depth) : depth(depth), data(new value<Width>[depth]) {}
 
 	memory(const memory<Width> &) = delete;
 	memory<Width> &operator=(const memory<Width> &) = delete;
 
 	memory(memory<Width> &&) = default;
-	memory<Width> &operator=(memory<Width> &&) = default;
-
-	// The only way to get the compiler to put the initializer in .rodata and do not copy it on stack is to stuff it
-	// into a plain array. You'd think an std::initializer_list would work here, but it doesn't, because you can't
-	// construct an initializer_list in a constexpr (or something) and so if you try to do that the whole thing is
-	// first copied on the stack (probably overflowing it) and then again into `data`.
-	template<size_t Size>
-	struct init {
-		size_t offset;
-		value<Width> data[Size];
-	};
-
-	template<size_t... InitSize>
-	explicit memory(size_t depth, const init<InitSize> &...init) : data(depth) {
-		data.resize(depth);
-		// This utterly reprehensible construct is the most reasonable way to apply a function to every element
-		// of a parameter pack, if the elements all have different types and so cannot be cast to an initializer list.
-		auto _ = {std::move(std::begin(init.data), std::end(init.data), data.begin() + init.offset)...};
-		(void)_;
+	memory<Width> &operator=(memory<Width> &&other) {
+		assert(depth == other.depth);
+		data = std::move(other.data);
+		write_queue = std::move(other.write_queue);
+		return *this;
 	}
 
 	// An operator for direct memory reads. May be used at any time during the simulation.
 	const value<Width> &operator [](size_t index) const {
-		assert(index < data.size());
+		assert(index < depth);
 		return data[index];
 	}
 
 	// An operator for direct memory writes. May only be used before the simulation is started. If used
 	// after the simulation is started, the design may malfunction.
 	value<Width> &operator [](size_t index) {
-		assert(index < data.size());
+		assert(index < depth);
 		return data[index];
 	}
 
@@ -790,7 +808,7 @@ struct memory {
 	std::vector<write> write_queue;
 
 	void update(size_t index, const value<Width> &val, const value<Width> &mask, int priority = 0) {
-		assert(index < data.size());
+		assert(index < depth);
 		// Queue up the write while keeping the queue sorted by priority.
 		write_queue.insert(
 			std::upper_bound(write_queue.begin(), write_queue.end(), priority,
@@ -947,9 +965,9 @@ struct debug_item : ::cxxrtl_object {
 		flags   = 0;
 		width   = Width;
 		lsb_at  = 0;
-		depth   = item.data.size();
+		depth   = item.depth;
 		zero_at = zero_offset;
-		curr    = item.data.empty() ? nullptr : item.data[0].data;
+		curr    = item.data ? item.data[0].data : nullptr;
 		next    = nullptr;
 		outline = nullptr;
 	}
@@ -1051,9 +1069,9 @@ struct debug_items {
 	}
 };
 
-// Tag class to disambiguate module move constructor and module constructor that takes black boxes
-// out of another instance of the module.
-struct adopt {};
+// Tag class to disambiguate the default constructor used by the toplevel module that calls reset(),
+// and the constructor of interior modules that should not call it.
+struct interior {};
 
 struct module {
 	module() {}
@@ -1557,6 +1575,27 @@ value<BitsY> mod_ss(const value<BitsA> &a, const value<BitsB> &b) {
 	return divmod_ss<BitsY>(a, b).second;
 }
 
+template<size_t BitsY, size_t BitsA, size_t BitsB>
+CXXRTL_ALWAYS_INLINE
+value<BitsY> modfloor_uu(const value<BitsA> &a, const value<BitsB> &b) {
+	return divmod_uu<BitsY>(a, b).second;
+}
+
+// GHDL Modfloor operator. Returns r=a mod b, such that r has the same sign as b and
+// a=b*N+r where N is some integer
+// In practical terms, when a and b have different signs and the remainder returned by divmod_ss is not 0
+// then return the remainder + b
+template<size_t BitsY, size_t BitsA, size_t BitsB>
+CXXRTL_ALWAYS_INLINE
+value<BitsY> modfloor_ss(const value<BitsA> &a, const value<BitsB> &b) {
+	value<BitsY> r;
+	r = divmod_ss<BitsY>(a, b).second;
+	if((b.is_neg() != a.is_neg()) && !r.is_zero())
+		return add_ss<BitsY>(b, r);
+	return r;
+}
+
+
 // Memory helper
 struct memory_index {
 	bool valid;
diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc
index ff28c20b3..62768bd33 100644
--- a/backends/cxxrtl/cxxrtl_backend.cc
+++ b/backends/cxxrtl/cxxrtl_backend.cc
@@ -185,7 +185,7 @@ bool is_binary_cell(RTLIL::IdString type)
 		ID($and), ID($or), ID($xor), ID($xnor), ID($logic_and), ID($logic_or),
 		ID($shl), ID($sshl), ID($shr), ID($sshr), ID($shift), ID($shiftx),
 		ID($eq), ID($ne), ID($eqx), ID($nex), ID($gt), ID($ge), ID($lt), ID($le),
-		ID($add), ID($sub), ID($mul), ID($div), ID($mod));
+		ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($modfloor));
 }
 
 bool is_extending_cell(RTLIL::IdString type)
@@ -198,7 +198,7 @@ bool is_extending_cell(RTLIL::IdString type)
 bool is_inlinable_cell(RTLIL::IdString type)
 {
 	return is_unary_cell(type) || is_binary_cell(type) || type.in(
-		ID($mux), ID($concat), ID($slice), ID($pmux));
+		ID($mux), ID($concat), ID($slice), ID($pmux), ID($bmux), ID($demux));
 }
 
 bool is_ff_cell(RTLIL::IdString type)
@@ -934,11 +934,6 @@ struct CxxrtlWorker {
 		f << "}";
 	}
 
-	void dump_const_init(const RTLIL::Const &data)
-	{
-		dump_const_init(data, data.size());
-	}
-
 	void dump_const(const RTLIL::Const &data, int width, int offset = 0, bool fixed_width = false)
 	{
 		f << "value<" << width << ">";
@@ -1159,6 +1154,22 @@ struct CxxrtlWorker {
 			for (int part = 0; part < s_width; part++) {
 				f << ")";
 			}
+		// Big muxes
+		} else if (cell->type == ID($bmux)) {
+			dump_sigspec_rhs(cell->getPort(ID::A), for_debug);
+			f << ".bmux<";
+			f << cell->getParam(ID::WIDTH).as_int();
+			f << ">(";
+			dump_sigspec_rhs(cell->getPort(ID::S), for_debug);
+			f << ").val()";
+		// Demuxes
+		} else if (cell->type == ID($demux)) {
+			dump_sigspec_rhs(cell->getPort(ID::A), for_debug);
+			f << ".demux<";
+			f << GetSize(cell->getPort(ID::Y));
+			f << ">(";
+			dump_sigspec_rhs(cell->getPort(ID::S), for_debug);
+			f << ").val()";
 		// Concats
 		} else if (cell->type == ID($concat)) {
 			dump_sigspec_rhs(cell->getPort(ID::B), for_debug);
@@ -1785,20 +1796,10 @@ struct CxxrtlWorker {
 		} else {
 			f << "<" << wire->width << ">";
 		}
-		f << " " << mangle(wire);
-		if (wire_init.count(wire)) {
-			f << " ";
-			dump_const_init(wire_init.at(wire));
-		}
-		f << ";\n";
+		f << " " << mangle(wire) << ";\n";
 		if (edge_wires[wire]) {
 			if (!wire_type.is_buffered()) {
-				f << indent << "value<" << wire->width << "> prev_" << mangle(wire);
-				if (wire_init.count(wire)) {
-					f << " ";
-					dump_const_init(wire_init.at(wire));
-				}
-				f << ";\n";
+				f << indent << "value<" << wire->width << "> prev_" << mangle(wire) << ";\n";
 			}
 			for (auto edge_type : edge_types) {
 				if (edge_type.first.wire == wire) {
@@ -1848,38 +1849,67 @@ struct CxxrtlWorker {
 		f << "value<" << wire->width << "> " << mangle(wire) << ";\n";
 	}
 
-	void dump_memory(Mem *mem)
+	void dump_reset_method(RTLIL::Module *module)
 	{
-		dump_attrs(mem);
-		f << indent << "memory<" << mem->width << "> " << mangle(mem)
-		            << " { " << mem->size << "u";
-		if (!GetSize(mem->inits)) {
-			f << " };\n";
-		} else {
-			f << ",\n";
-			inc_indent();
-				for (auto &init : mem->inits) {
+		int mem_init_idx = 0;
+		inc_indent();
+			for (auto wire : module->wires()) {
+				const auto &wire_type = wire_types[wire];
+				if (!wire_type.is_named() || wire_type.is_local()) continue;
+				if (!wire_init.count(wire)) continue;
+
+				f << indent << mangle(wire) << " = ";
+				if (wire_types[wire].is_buffered()) {
+					f << "wire<" << wire->width << ">";
+				} else {
+					f << "value<" << wire->width << ">";
+				}
+				dump_const_init(wire_init.at(wire), wire->width);
+				f << ";\n";
+
+				if (edge_wires[wire] && !wire_types[wire].is_buffered()) {
+					f << indent << "prev_" << mangle(wire) << " = ";
+					dump_const(wire_init.at(wire), wire->width);
+					f << ";\n";
+				}
+			}
+			for (auto &mem : mod_memories[module]) {
+				for (auto &init : mem.inits) {
 					if (init.removed)
 						continue;
 					dump_attrs(&init);
-					int words = GetSize(init.data) / mem->width;
-					f << indent << "memory<" << mem->width << ">::init<" << words << "> { "
-						    << stringf("%#x", init.addr.as_int()) << ", {";
+					int words = GetSize(init.data) / mem.width;
+					f << indent << "static const value<" << mem.width << "> ";
+					f << "mem_init_" << ++mem_init_idx << "[" << words << "] {";
 					inc_indent();
 						for (int n = 0; n < words; n++) {
 							if (n % 4 == 0)
 								f << "\n" << indent;
 							else
 								f << " ";
-							dump_const(init.data, mem->width, n * mem->width, /*fixed_width=*/true);
+							dump_const(init.data, mem.width, n * mem.width, /*fixed_width=*/true);
 							f << ",";
 						}
 					dec_indent();
-					f << "\n" << indent << "}},\n";
+					f << "\n";
+					f << indent << "};\n";
+					f << indent << "std::copy(std::begin(mem_init_" << mem_init_idx << "), ";
+					f << "std::end(mem_init_" << mem_init_idx << "), ";
+					f << "&" << mangle(&mem) << ".data[" << stringf("%#x", init.addr.as_int()) << "]);\n";
 				}
-			dec_indent();
-			f << indent << "};\n";
-		}
+			}
+			for (auto cell : module->cells()) {
+				if (is_internal_cell(cell->type))
+					continue;
+				f << indent << mangle(cell);
+				RTLIL::Module *cell_module = module->design->module(cell->type);
+				if (cell_module->get_bool_attribute(ID(cxxrtl_blackbox))) {
+					f << "->reset();\n";
+				} else {
+					f << ".reset();\n";
+				}
+			}
+		dec_indent();
 	}
 
 	void dump_eval_method(RTLIL::Module *module)
@@ -2200,6 +2230,10 @@ struct CxxrtlWorker {
 						dump_wire(wire, /*is_local=*/false);
 				}
 				f << "\n";
+				f << indent << "void reset() override {\n";
+				dump_reset_method(module);
+				f << indent << "}\n";
+				f << "\n";
 				f << indent << "bool eval() override {\n";
 				dump_eval_method(module);
 				f << indent << "}\n";
@@ -2248,7 +2282,9 @@ struct CxxrtlWorker {
 					dump_debug_wire(wire, /*is_local=*/false);
 				bool has_memories = false;
 				for (auto &mem : mod_memories[module]) {
-					dump_memory(&mem);
+					dump_attrs(&mem);
+					f << indent << "memory<" << mem.width << "> " << mangle(&mem)
+					            << " { " << mem.size << "u };\n";
 					has_memories = true;
 				}
 				if (has_memories)
@@ -2269,52 +2305,20 @@ struct CxxrtlWorker {
 						dump_metadata_map(cell->attributes);
 						f << ");\n";
 					} else {
-						f << indent << mangle(cell_module) << " " << mangle(cell) << ";\n";
+						f << indent << mangle(cell_module) << " " << mangle(cell) << " {interior()};\n";
 					}
 					has_cells = true;
 				}
 				if (has_cells)
 					f << "\n";
-				f << indent << mangle(module) << "() {}\n";
-				if (has_cells) {
-					f << indent << mangle(module) << "(adopt, " << mangle(module) << " other) :\n";
-					bool first = true;
-					for (auto cell : module->cells()) {
-						if (is_internal_cell(cell->type))
-							continue;
-						if (first) {
-							first = false;
-						} else {
-							f << ",\n";
-						}
-						RTLIL::Module *cell_module = module->design->module(cell->type);
-						if (cell_module->get_bool_attribute(ID(cxxrtl_blackbox))) {
-							f << indent << "  " << mangle(cell) << "(std::move(other." << mangle(cell) << "))";
-						} else {
-							f << indent << "  " << mangle(cell) << "(adopt {}, std::move(other." << mangle(cell) << "))";
-						}
-					}
-					f << " {\n";
-					inc_indent();
-						for (auto cell : module->cells()) {
-							if (is_internal_cell(cell->type))
-								continue;
-							RTLIL::Module *cell_module = module->design->module(cell->type);
-							if (cell_module->get_bool_attribute(ID(cxxrtl_blackbox)))
-								f << indent << mangle(cell) << "->reset();\n";
-						}
-					dec_indent();
-					f << indent << "}\n";
-				} else {
-					f << indent << mangle(module) << "(adopt, " << mangle(module) << " other) {}\n";
-				}
-				f << "\n";
-				f << indent << "void reset() override {\n";
+				f << indent << mangle(module) << "(interior) {}\n";
+				f << indent << mangle(module) << "() {\n";
 				inc_indent();
-					f << indent << "*this = " << mangle(module) << "(adopt {}, std::move(*this));\n";
+					f << indent << "reset();\n";
 				dec_indent();
-				f << indent << "}\n";
+				f << indent << "};\n";
 				f << "\n";
+				f << indent << "void reset() override;\n";
 				f << indent << "bool eval() override;\n";
 				f << indent << "bool commit() override;\n";
 				if (debug_info) {
@@ -2341,6 +2345,10 @@ struct CxxrtlWorker {
 	{
 		if (module->get_bool_attribute(ID(cxxrtl_blackbox)))
 			return;
+		f << indent << "void " << mangle(module) << "::reset() {\n";
+		dump_reset_method(module);
+		f << indent << "}\n";
+		f << "\n";
 		f << indent << "bool " << mangle(module) << "::eval() {\n";
 		dump_eval_method(module);
 		f << indent << "}\n";
@@ -2898,15 +2906,16 @@ struct CxxrtlWorker {
 								debug_wire_type = {WireType::INLINE, node->cell}; // wire replaced with cell
 								break;
 							case FlowGraph::Node::Type::CONNECT:
-							  debug_wire_type = {WireType::INLINE, node->connect.second}; // wire replaced with sig
+								debug_wire_type = {WireType::INLINE, node->connect.second}; // wire replaced with sig
 								break;
 							default: continue;
 						}
 						debug_live_nodes.erase(node);
-					} else if (wire_type.is_member() || wire_type.is_local()) {
+					} else if (wire_type.is_member() || wire_type.type == WireType::LOCAL) {
 						debug_wire_type = wire_type; // wire not inlinable
 					} else {
-						log_assert(wire_type.type == WireType::UNUSED);
+						log_assert(wire_type.type == WireType::INLINE ||
+						           wire_type.type == WireType::UNUSED);
 						if (flow.wire_comb_defs[wire].size() == 0) {
 							if (wire_init.count(wire)) { // wire never modified
 								debug_wire_type = {WireType::CONST, wire_init.at(wire)};
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index 7abe584c9..76ba77abb 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -729,12 +729,12 @@ struct FirrtlWorker
 					always_uint = true;
 					firrtl_width = max(a_width, b_width);
 				}
-				else if ((cell->type == ID($eq)) | (cell->type == ID($eqx))) {
+				else if ((cell->type == ID($eq)) || (cell->type == ID($eqx))) {
 					primop = "eq";
 					always_uint = true;
 					firrtl_width = 1;
 				}
-				else if ((cell->type == ID($ne)) | (cell->type == ID($nex))) {
+				else if ((cell->type == ID($ne)) || (cell->type == ID($nex))) {
 					primop = "neq";
 					always_uint = true;
 					firrtl_width = 1;
@@ -759,7 +759,7 @@ struct FirrtlWorker
 					always_uint = true;
 					firrtl_width = 1;
 				}
-				else if ((cell->type == ID($shl)) | (cell->type == ID($sshl))) {
+				else if ((cell->type == ID($shl)) || (cell->type == ID($sshl))) {
 					// FIRRTL will widen the result (y) by the amount of the shift.
 					// We'll need to offset this by extracting the un-widened portion as Verilog would do.
 					extract_y_bits = true;
@@ -777,7 +777,7 @@ struct FirrtlWorker
 						firrtl_width = a_width + (1 << b_width) - 1;
 					}
 				}
-				else if ((cell->type == ID($shr)) | (cell->type == ID($sshr))) {
+				else if ((cell->type == ID($shr)) || (cell->type == ID($sshr))) {
 					// We don't need to extract a specific range of bits.
 					extract_y_bits = false;
 					// Is the shift amount constant?
@@ -1188,6 +1188,8 @@ struct FirrtlBackend : public Backend {
 		log("Write a FIRRTL netlist of the current design.\n");
 		log("The following commands are executed by this command:\n");
 		log("        pmuxtree\n");
+		log("        bmuxmap\n");
+		log("        demuxmap\n");
 		log("\n");
 	}
 	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
@@ -1210,7 +1212,9 @@ struct FirrtlBackend : public Backend {
 		log_header(design, "Executing FIRRTL backend.\n");
 		log_push();
 
-		Pass::call(design, stringf("pmuxtree"));
+		Pass::call(design, "pmuxtree");
+		Pass::call(design, "bmuxmap");
+		Pass::call(design, "demuxmap");
 
 		namecache.clear();
 		autoid_counter = 0;
diff --git a/backends/jny/Makefile.inc b/backends/jny/Makefile.inc
new file mode 100644
index 000000000..5e417128e
--- /dev/null
+++ b/backends/jny/Makefile.inc
@@ -0,0 +1,2 @@
+
+OBJS += backends/jny/jny.o
diff --git a/backends/jny/jny.cc b/backends/jny/jny.cc
new file mode 100644
index 000000000..d801b144c
--- /dev/null
+++ b/backends/jny/jny.cc
@@ -0,0 +1,554 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Aki "lethalbit" Van Ness <aki@yosyshq.com> <aki@lethalbit.net>
+ *
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/rtlil.h"
+#include "kernel/register.h"
+#include "kernel/sigtools.h"
+#include "kernel/celltypes.h"
+#include "kernel/cellaigs.h"
+#include "kernel/log.h"
+#include <string>
+#include <algorithm>
+#include <unordered_map>
+#include <vector>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+
+struct JnyWriter
+{
+    private:
+        std::ostream &f;
+        bool _use_selection;
+
+        // XXX(aki): TODO: this needs to be updated to us
+        // dict<T, V> and then coalesce_cells needs to be updated
+        // but for now for the PoC this looks to be sufficient
+        std::unordered_map<std::string, std::vector<Cell*>> _cells{};
+
+        bool _include_connections;
+        bool _include_attributes;
+        bool _include_properties;
+
+        string escape_string(string str) {
+            std::string newstr;
+
+            auto itr = str.begin();
+
+            for(; itr != str.end(); ++itr) {
+                switch (*itr) {
+                    case '\\': {
+                        newstr += "\\\\";
+                        break;
+                    } case '\n': {
+                        newstr += "\\n";
+                        break;
+                    } case '\f': {
+                        newstr += "\\f";
+                        break;
+                    } case '\t': {
+                        newstr += "\\t";
+                        break;
+                    } case '\r': {
+                        newstr += "\\r";
+                        break;
+                    } case '\"': {
+                        newstr += "\\\"";
+                        break;
+                    } case '\b': {
+                        newstr += "\\b";
+                        break;
+                    } default: {
+                        newstr += *itr;
+                    }
+                }
+            }
+
+            return newstr;
+        }
+
+        // XXX(aki): I know this is far from ideal but i'm out of spoons and cant focus so
+        // it'll have to do for now,
+        void coalesce_cells(Module* mod)
+        {
+            _cells.clear();
+            for (auto cell : mod->cells()) {
+                const auto cell_type = escape_string(RTLIL::unescape_id(cell->type));
+
+                if (_cells.find(cell_type) == _cells.end())
+                    _cells.emplace(cell_type, std::vector<Cell*>());
+
+                _cells.at(cell_type).push_back(cell);
+            }
+        }
+
+        // XXX(aki): this is a lazy way to do this i know,,,
+        std::string gen_indent(const uint16_t level)
+        {
+            std::stringstream s;
+            for (uint16_t i = 0; i <= level; ++i)
+            {
+                s << "  ";
+            }
+            return s.str();
+        }
+
+    public:
+    JnyWriter(std::ostream &f, bool use_selection, bool connections, bool attributes, bool properties) noexcept:
+        f(f), _use_selection(use_selection),
+        _include_connections(connections), _include_attributes(attributes), _include_properties(properties)
+         { }
+
+    void write_metadata(Design *design, uint16_t indent_level = 0)
+    {
+        log_assert(design != nullptr);
+
+        design->sort();
+
+        f << "{\n";
+        f << stringf("  \"generator\": \"%s\",\n", escape_string(yosys_version_str).c_str());
+        // XXX(aki): Replace this with a proper version info eventually:tm:
+        f << "  \"version\": \"0.0.0\",\n";
+
+        f << "  \"features\": [";
+
+        size_t fnum{0};
+        if (_include_connections) {
+            ++fnum;
+            f << "\"connections\"";
+        }
+
+        if (_include_attributes) {
+            if (fnum > 0)
+                f << ", ";
+            ++fnum;
+            f << "\"attributes\"";
+        }
+
+        if (_include_properties) {
+            if (fnum > 0)
+                f << ", ";
+            ++fnum;
+            f << "\"properties\"";
+        }
+
+        f << "],\n";
+
+        f << "  \"modules\": [\n";
+
+        bool first{true};
+        for (auto mod : _use_selection ? design->selected_modules() : design->modules()) {
+            if (!first)
+                f << ",\n";
+            write_module(mod, indent_level + 2);
+            first = false;
+        }
+
+        f << "\n";
+        f << "  ]\n";
+        f << "}\n";
+    }
+
+    void write_sigspec(const RTLIL::SigSpec& sig, uint16_t indent_level = 0) {
+        const auto _indent = gen_indent(indent_level);
+
+        f << _indent << "  {\n";
+        f << _indent << "    \"width\": \"" << sig.size() << "\",\n";
+        f << _indent << "    \"type\": \"";
+
+        if (sig.is_wire()) {
+            f << "wire";
+        } else if (sig.is_chunk()) {
+            f << "chunk";
+        } else if (sig.is_bit()) {
+            f << "bit";
+        } else {
+            f << "unknown";
+        }
+        f << "\",\n";
+
+        f << _indent << "    \"const\": ";
+        if (sig.has_const()) {
+            f << "true";
+        } else {
+            f << "false";
+        }
+
+        f << "\n";
+
+        f << _indent << "  }";
+    }
+
+    void write_mod_conn(const std::pair<RTLIL::SigSpec, RTLIL::SigSpec>& conn, uint16_t indent_level = 0) {
+        const auto _indent = gen_indent(indent_level);
+        f << _indent << "  {\n";
+        f << _indent << "    \"signals\": [\n";
+
+        write_sigspec(conn.first, indent_level + 2);
+        f << ",\n";
+        write_sigspec(conn.second, indent_level + 2);
+        f << "\n";
+
+        f << _indent << "     ]\n";
+        f << _indent << "  }";
+    }
+
+    void write_cell_conn(const std::pair<RTLIL::IdString, RTLIL::SigSpec>& sig, uint16_t indent_level = 0) {
+        const auto _indent = gen_indent(indent_level);
+        f << _indent << "  {\n";
+        f << _indent << "    \"name\": \"" << escape_string(RTLIL::unescape_id(sig.first)) << "\",\n";
+        f << _indent << "    \"signals\": [\n";
+
+        write_sigspec(sig.second, indent_level + 2);
+        f << "\n";
+
+        f << _indent << "     ]\n";
+        f << _indent << "  }";
+    }
+
+    void write_module(Module* mod, uint16_t indent_level = 0) {
+        log_assert(mod != nullptr);
+
+        coalesce_cells(mod);
+
+        const auto _indent = gen_indent(indent_level);
+
+        f << _indent << "{\n";
+        f << stringf("  %s\"name\": \"%s\",\n", _indent.c_str(), escape_string(RTLIL::unescape_id(mod->name)).c_str());
+        f << _indent << "  \"cell_sorts\": [\n";
+
+        bool first_sort{true};
+        for (auto& sort : _cells) {
+            if (!first_sort)
+                f << ",\n";
+            write_cell_sort(sort, indent_level + 2);
+            first_sort = false;
+        }
+        f << "\n";
+
+        f << _indent << "  ]";
+        if (_include_connections) {
+            f << ",\n" << _indent << "  \"connections\": [\n";
+
+            bool first_conn{true};
+            for (const auto& conn : mod->connections()) {
+                if (!first_conn)
+                    f << ",\n";
+
+                write_mod_conn(conn, indent_level + 2);
+
+                first_conn = false;
+            }
+
+            f << _indent << "  ]";
+        }
+        if (_include_attributes) {
+            f << ",\n" << _indent << "  \"attributes\": {\n";
+
+            write_prams(mod->attributes, indent_level + 2);
+
+            f << "\n";
+            f << _indent << "  }";
+        }
+        f << "\n" << _indent << "}";
+    }
+
+    void write_cell_ports(RTLIL::Cell* port_cell, uint64_t indent_level = 0) {
+        const auto _indent = gen_indent(indent_level);
+
+        bool first_port{true};
+        for (auto con : port_cell->connections()) {
+            if (!first_port)
+                f << ",\n";
+
+            f << _indent << "  {\n";
+            f << stringf("    %s\"name\": \"%s\",\n", _indent.c_str(), escape_string(RTLIL::unescape_id(con.first)).c_str());
+            f << _indent << "    \"direction\": \"";
+            if (port_cell->input(con.first))
+                f << "i";
+            if (port_cell->input(con.first))
+                f << "o";
+            f << "\",\n";
+            if (con.second.size() == 1)
+                f << _indent << "    \"range\": [0, 0]\n";
+            else
+                f << stringf("    %s\"range\": [%d, %d]\n", _indent.c_str(), con.second.size(), 0);
+            f << _indent << "  }";
+
+            first_port = false;
+        }
+        f << "\n";
+    }
+
+
+    void write_cell_sort(std::pair<const std::string, std::vector<Cell*>>& sort, uint16_t indent_level = 0) {
+        const auto port_cell = sort.second.front();
+        const auto _indent = gen_indent(indent_level);
+
+        f << _indent << "{\n";
+        f << stringf("  %s\"type\": \"%s\",\n", _indent.c_str(), sort.first.c_str());
+        f << _indent << "  \"ports\": [\n";
+
+        write_cell_ports(port_cell, indent_level + 2);
+
+        f << _indent << "  ],\n" << _indent << "  \"cells\": [\n";
+
+        bool first_cell{true};
+        for (auto& cell : sort.second) {
+            if (!first_cell)
+                f << ",\n";
+
+            write_cell(cell, indent_level + 2);
+
+            first_cell = false;
+        }
+
+        f << "\n";
+        f << _indent << "  ]\n";
+        f << _indent << "}";
+    }
+
+    void write_param_val(const Const& v) {
+        if ((v.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) == RTLIL::ConstFlags::CONST_FLAG_STRING) {
+            const auto str = v.decode_string();
+
+            // XXX(aki): TODO, uh, yeah
+
+            f << "\"" << escape_string(str) << "\"";
+        } else if ((v.flags & RTLIL::ConstFlags::CONST_FLAG_SIGNED) == RTLIL::ConstFlags::CONST_FLAG_SIGNED) {
+            f << stringf("\"%dsd %d\"", v.size(), v.as_int(true));
+        } else if ((v.flags & RTLIL::ConstFlags::CONST_FLAG_REAL) == RTLIL::ConstFlags::CONST_FLAG_REAL) {
+
+        } else {
+            f << "\"" << escape_string(v.as_string()) << "\"";
+        }
+    }
+
+    void write_prams(dict<RTLIL::IdString, RTLIL::Const>& params, uint16_t indent_level = 0) {
+        const auto _indent = gen_indent(indent_level);
+
+        bool first_param{true};
+        for (auto& param : params) {
+            if (!first_param)
+                f << stringf(",\n");
+            const auto param_val = param.second;
+            if (!param_val.empty()) {
+                f << stringf("  %s\"%s\": ", _indent.c_str(), escape_string(RTLIL::unescape_id(param.first)).c_str());
+                write_param_val(param_val);
+            } else {
+                f << stringf("  %s\"%s\": true", _indent.c_str(), escape_string(RTLIL::unescape_id(param.first)).c_str());
+            }
+
+            first_param = false;
+        }
+    }
+
+    void write_cell(Cell* cell, uint16_t indent_level = 0) {
+        const auto _indent = gen_indent(indent_level);
+        log_assert(cell != nullptr);
+
+        f << _indent << "  {\n";
+        f << stringf("    %s\"name\": \"%s\"", _indent.c_str(), escape_string(RTLIL::unescape_id(cell->name)).c_str());
+
+        if (_include_connections) {
+            f << ",\n" << _indent << "    \"connections\": [\n";
+
+            bool first_conn{true};
+            for (const auto& conn : cell->connections()) {
+                if (!first_conn)
+                    f << ",\n";
+
+                write_cell_conn(conn, indent_level + 2);
+
+                first_conn = false;
+            }
+
+            f << "\n";
+            f << _indent << "    ]";
+        }
+
+        if (_include_attributes) {
+            f << ",\n" << _indent << "    \"attributes\": {\n";
+
+            write_prams(cell->attributes, indent_level + 2);
+
+            f << "\n";
+            f << _indent << "    }";
+        }
+
+        if (_include_properties) {
+            f << ",\n" << _indent << "    \"parameters\": {\n";
+
+            write_prams(cell->parameters, indent_level + 2);
+
+            f << "\n";
+            f << _indent << "    }";
+        }
+
+        f << "\n" << _indent << "  }";
+    }
+};
+
+struct JnyBackend : public Backend {
+    JnyBackend() : Backend("jny", "generate design metadata") { }
+    void help() override {
+        // XXX(aki): TODO: explicitly document the JSON schema
+        //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+        log("\n");
+        log("    jny [options] [selection]\n");
+        log("\n");
+        log("    -no-connections\n");
+        log("        Don't include connection information in the netlist output.\n");
+        log("\n");
+        log("    -no-attributes\n");
+        log("        Don't include attributed information in the netlist output.\n");
+        log("\n");
+        log("    -no-properties\n");
+        log("        Don't include property information in the netlist output.\n");
+        log("\n");
+        log("Write a JSON metadata for the current design\n");
+        log("\n");
+        log("\n");
+    }
+
+    void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override {
+
+        bool connections{true};
+        bool attributes{true};
+        bool properties{true};
+
+        size_t argidx{1};
+        for (; argidx < args.size(); argidx++) {
+            if (args[argidx] == "-no-connections") {
+                connections = false;
+                continue;
+            }
+
+            if (args[argidx] == "-no-attributes") {
+                attributes = false;
+                continue;
+            }
+
+            if (args[argidx] == "-no-properties") {
+                properties = false;
+                continue;
+            }
+
+            break;
+        }
+        extra_args(f, filename, args, argidx);
+
+        log_header(design, "Executing jny backend.\n");
+
+        JnyWriter jny_writer(*f, false, connections, attributes, properties);
+        jny_writer.write_metadata(design);
+    }
+
+} JnyBackend;
+
+
+struct JnyPass : public Pass {
+    JnyPass() : Pass("jny", "write design and metadata") { }
+
+    void help() override {
+        //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+        log("\n");
+        log("    jny [options] [selection]\n");
+        log("\n");
+        log("Write a JSON netlist metadata for the current design\n");
+        log("\n");
+        log("    -o <filename>\n");
+        log("        write to the specified file.\n");
+        log("\n");
+        log("    -no-connections\n");
+        log("        Don't include connection information in the netlist output.\n");
+        log("\n");
+        log("    -no-attributes\n");
+        log("        Don't include attributed information in the netlist output.\n");
+        log("\n");
+        log("    -no-properties\n");
+        log("        Don't include property information in the netlist output.\n");
+        log("\n");
+        log("See 'help write_jny' for a description of the JSON format used.\n");
+        log("\n");
+    }
+    void execute(std::vector<std::string> args, RTLIL::Design *design) override {
+        std::string filename{};
+
+        bool connections{true};
+        bool attributes{true};
+        bool properties{true};
+
+        size_t argidx{1};
+        for (; argidx < args.size(); argidx++) {
+            if (args[argidx] == "-o" && argidx+1 < args.size()) {
+                filename = args[++argidx];
+                continue;
+            }
+
+            if (args[argidx] == "-no-connections") {
+                connections = false;
+                continue;
+            }
+
+            if (args[argidx] == "-no-attributes") {
+                attributes = false;
+                continue;
+            }
+
+            if (args[argidx] == "-no-properties") {
+                properties = false;
+                continue;
+            }
+
+            break;
+        }
+        extra_args(args, argidx, design);
+
+        std::ostream *f;
+        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()) {
+                delete ff;
+                log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
+            }
+            f = ff;
+        } else {
+            f = &buf;
+        }
+
+
+        JnyWriter jny_writer(*f, false, connections, attributes, properties);
+        jny_writer.write_metadata(design);
+
+        if (!filename.empty()) {
+            delete f;
+        } else {
+            log("%s", buf.str().c_str());
+        }
+    }
+
+} JnyPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/backends/json/json.cc b/backends/json/json.cc
index 4aa8046d6..270d762ee 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -52,8 +52,23 @@ struct JsonWriter
 		string newstr = "\"";
 		for (char c : str) {
 			if (c == '\\')
+				newstr += "\\\\";
+			else if (c == '"')
+				newstr += "\\\"";
+			else if (c == '\b')
+				newstr += "\\b";
+			else if (c == '\f')
+				newstr += "\\f";
+			else if (c == '\n')
+				newstr += "\\n";
+			else if (c == '\r')
+				newstr += "\\r";
+			else if (c == '\t')
+				newstr += "\\t";
+			else if (c < 0x20)
+				newstr += stringf("\\u%04X", c);
+			else
 				newstr += c;
-			newstr += c;
 		}
 		return newstr + "\"";
 	}
@@ -379,6 +394,7 @@ struct JsonBackend : public Backend {
 		log("      \"bits\": <bit_vector>\n");
 		log("      \"offset\": <the lowest bit index in use, if non-0>\n");
 		log("      \"upto\": <1 if the port bit indexing is MSB-first>\n");
+		log("      \"signed\": <1 if the port is signed>\n");
 		log("    }\n");
 		log("\n");
 		log("The \"offset\" and \"upto\" fields are skipped if their value would be 0.");
@@ -428,6 +444,7 @@ struct JsonBackend : public Backend {
 		log("      \"bits\": <bit_vector>\n");
 		log("      \"offset\": <the lowest bit index in use, if non-0>\n");
 		log("      \"upto\": <1 if the port bit indexing is MSB-first>\n");
+		log("      \"signed\": <1 if the port is signed>\n");
 		log("    }\n");
 		log("\n");
 		log("The \"hide_name\" fields are set to 1 when the name of this cell or net is\n");
diff --git a/backends/rtlil/rtlil_backend.cc b/backends/rtlil/rtlil_backend.cc
index 68521d52d..1b11de5ec 100644
--- a/backends/rtlil/rtlil_backend.cc
+++ b/backends/rtlil/rtlil_backend.cc
@@ -358,8 +358,8 @@ void RTLIL_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Modu
 
 		bool first_conn_line = true;
 		for (auto it = module->connections().begin(); it != module->connections().end(); ++it) {
-			bool show_conn = !only_selected;
-			if (only_selected) {
+			bool show_conn = !only_selected || design->selected_whole_module(module->name);
+			if (!show_conn) {
 				RTLIL::SigSpec sigs = it->first;
 				sigs.append(it->second);
 				for (auto &c : sigs.chunks()) {
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index f2fa003bc..7481e0510 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -53,6 +53,8 @@ struct Smt2Worker
 	std::map<int, int> bvsizes;
 	dict<IdString, char*> ids;
 
+	bool is_smtlib2_module;
+
 	const char *get_id(IdString n)
 	{
 		if (ids.count(n) == 0) {
@@ -112,9 +114,10 @@ struct Smt2Worker
 	}
 
 	Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, bool forallmode,
-			dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache) :
-			ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
-			verbose(verbose), statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width)
+		   dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache)
+	    : ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode), verbose(verbose),
+	      statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width),
+	      is_smtlib2_module(module->has_attribute(ID::smtlib2_module))
 	{
 		pool<SigBit> noclock;
 
@@ -124,6 +127,9 @@ struct Smt2Worker
 		memories = Mem::get_all_memories(module);
 		for (auto &mem : memories)
 		{
+			if (is_smtlib2_module)
+				log_error("Memory %s.%s not allowed in module with smtlib2_module attribute", get_id(module), mem.memid.c_str());
+
 			mem.narrow();
 			mem_dict[mem.memid] = &mem;
 			for (auto &port : mem.wr_ports)
@@ -649,6 +655,27 @@ struct Smt2Worker
 					return export_bvop(cell, "(bvurem A B)", 'd');
 				}
 			}
+			// "div" = flooring division
+			if (cell->type == ID($divfloor)) {
+				if (cell->getParam(ID::A_SIGNED).as_bool()) {
+					// bvsdiv is truncating division, so we can't use it here.
+					int width = max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::B)));
+					width = max(width, GetSize(cell->getPort(ID::Y)));
+					auto expr = stringf("(let ("
+							    "(a_neg (bvslt A #b%0*d)) "
+							    "(b_neg (bvslt B #b%0*d))) "
+							    "(let ((abs_a (ite a_neg (bvneg A) A)) "
+							    "(abs_b (ite b_neg (bvneg B) B))) "
+							    "(let ((u (bvudiv abs_a abs_b)) "
+							    "(adj (ite (= #b%0*d (bvurem abs_a abs_b)) #b%0*d #b%0*d))) "
+							    "(ite (= a_neg b_neg) u "
+							    "(bvneg (bvadd u adj))))))",
+							    width, 0, width, 0, width, 0, width, 0, width, 1);
+					return export_bvop(cell, expr, 'd');
+				} else {
+					return export_bvop(cell, "(bvudiv A B)", 'd');
+				}
+			}
 
 			if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)) &&
 					2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) {
@@ -872,10 +899,25 @@ struct Smt2Worker
 				log_id(cell->type), log_id(module), log_id(cell));
 	}
 
+	void verify_smtlib2_module()
+	{
+		if (!module->get_blackbox_attribute())
+			log_error("Module %s with smtlib2_module attribute must also have blackbox attribute.\n", log_id(module));
+		if (module->cells().size() > 0)
+			log_error("Module %s with smtlib2_module attribute must not have any cells inside it.\n", log_id(module));
+		for (auto wire : module->wires())
+			if (!wire->port_id)
+				log_error("Wire %s.%s must be input or output since module has smtlib2_module attribute.\n", log_id(module),
+					  log_id(wire));
+	}
+
 	void run()
 	{
 		if (verbose) log("=> export logic driving outputs\n");
 
+		if (is_smtlib2_module)
+			verify_smtlib2_module();
+
 		pool<SigBit> reg_bits;
 		for (auto cell : module->cells())
 			if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) {
@@ -884,11 +926,25 @@ struct Smt2Worker
 					reg_bits.insert(bit);
 			}
 
+		std::string smtlib2_inputs;
+		std::vector<std::string> smtlib2_decls;
+		if (is_smtlib2_module) {
+			for (auto wire : module->wires()) {
+				if (!wire->port_input)
+					continue;
+				smtlib2_inputs += stringf("(|%s| (|%s_n %s| state))\n", get_id(wire), get_id(module), get_id(wire));
+			}
+		}
+
 		for (auto wire : module->wires()) {
 			bool is_register = false;
 			for (auto bit : SigSpec(wire))
 				if (reg_bits.count(bit))
 					is_register = true;
+			bool is_smtlib2_comb_expr = wire->has_attribute(ID::smtlib2_comb_expr);
+			if (is_smtlib2_comb_expr && !is_smtlib2_module)
+				log_error("smtlib2_comb_expr is only valid in a module with the smtlib2_module attribute: wire %s.%s", log_id(module),
+					  log_id(wire));
 			if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
 				RTLIL::SigSpec sig = sigmap(wire);
 				std::vector<std::string> comments;
@@ -903,11 +959,22 @@ struct Smt2Worker
 				if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
 					comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
 							clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
+				std::string smtlib2_comb_expr;
+				if (is_smtlib2_comb_expr) {
+					smtlib2_comb_expr =
+					  "(let (\n" + smtlib2_inputs + ")\n" + wire->get_string_attribute(ID::smtlib2_comb_expr) + "\n)";
+					if (wire->port_input || !wire->port_output)
+						log_error("smtlib2_comb_expr is only valid on output: wire %s.%s", log_id(module), log_id(wire));
+					if (!bvmode && GetSize(sig) > 1)
+						log_error("smtlib2_comb_expr is unsupported on multi-bit wires when -nobv is specified: wire %s.%s",
+							  log_id(module), log_id(wire));
+				}
+				auto &out_decls = is_smtlib2_comb_expr ? smtlib2_decls : decls;
 				if (bvmode && GetSize(sig) > 1) {
-					std::string sig_bv = get_bv(sig);
+					std::string sig_bv = is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bv(sig);
 					if (!comments.empty())
-						decls.insert(decls.end(), comments.begin(), comments.end());
-					decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
+						out_decls.insert(out_decls.end(), comments.begin(), comments.end());
+					out_decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
 							get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str()));
 					if (wire->port_input)
 						ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
@@ -915,19 +982,19 @@ struct Smt2Worker
 				} else {
 					std::vector<std::string> sig_bool;
 					for (int i = 0; i < GetSize(sig); i++) {
-						sig_bool.push_back(get_bool(sig[i]));
+						sig_bool.push_back(is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bool(sig[i]));
 					}
 					if (!comments.empty())
-						decls.insert(decls.end(), comments.begin(), comments.end());
+						out_decls.insert(out_decls.end(), comments.begin(), comments.end());
 					for (int i = 0; i < GetSize(sig); i++) {
 						if (GetSize(sig) > 1) {
-							decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
+							out_decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
 									get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str()));
 							if (wire->port_input)
 								ex_input_eq.push_back(stringf("  (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))",
 										get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
 						} else {
-							decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
+							out_decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
 									get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str()));
 							if (wire->port_input)
 								ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
@@ -938,11 +1005,17 @@ struct Smt2Worker
 			}
 		}
 
+		decls.insert(decls.end(), smtlib2_decls.begin(), smtlib2_decls.end());
+
 		if (verbose) log("=> export logic associated with the initial state\n");
 
 		vector<string> init_list;
 		for (auto wire : module->wires())
 			if (wire->attributes.count(ID::init)) {
+				if (is_smtlib2_module)
+					log_error("init attribute not allowed on wires in module with smtlib2_module attribute: wire %s.%s",
+						  log_id(module), log_id(wire));
+
 				RTLIL::SigSpec sig = sigmap(wire);
 				Const val = wire->attributes.at(ID::init);
 				val.bits.resize(GetSize(sig), State::Sx);
@@ -985,8 +1058,10 @@ struct Smt2Worker
 
 				string name_a = get_bool(cell->getPort(ID::A));
 				string name_en = get_bool(cell->getPort(ID::EN));
-				string infostr = (cell->name[0] == '$' && cell->attributes.count(ID::src)) ? cell->attributes.at(ID::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->name[0] == '$' && cell->attributes.count(ID::src))
+					decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string().c_str()));
+				else
+					decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, get_id(cell)));
 
 				if (cell->type == ID($cover))
 					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
@@ -1183,10 +1258,12 @@ struct Smt2Worker
 						data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
 								data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());
 
+						string empty_mask(mem->width, '0');
+
 						decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
-								"(store (|%s#%d#%d| state) %s %s)) ; %s\n",
+								"(ite (= %s #b%s) (|%s#%d#%d| state) (store (|%s#%d#%d| state) %s %s))) ; %s\n",
 								get_id(module), arrayid, i+1, get_id(module), abits, mem->width,
-								get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid)));
+								mask.c_str(), empty_mask.c_str(), get_id(module), arrayid, i, get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid)));
 					}
 				}
 
@@ -1531,6 +1608,11 @@ struct Smt2Backend : public Backend {
 
 		log_header(design, "Executing SMT2 backend.\n");
 
+		log_push();
+		Pass::call(design, "bmuxmap");
+		Pass::call(design, "demuxmap");
+		log_pop();
+
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
 		{
@@ -1657,7 +1739,10 @@ struct Smt2Backend : public Backend {
 
 		for (auto module : sorted_modules)
 		{
-			if (module->get_blackbox_attribute() || module->has_processes_warn())
+			if (module->get_blackbox_attribute() && !module->has_attribute(ID::smtlib2_module))
+				continue;
+
+			if (module->has_processes_warn())
 				continue;
 
 			log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index e5cfcdc08..137182f33 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -50,6 +50,7 @@ smtcinit = False
 smtctop = None
 noinit = False
 binarymode = False
+keep_going = False
 so = SmtOpts()
 
 
@@ -143,7 +144,7 @@ def usage():
 
     --dump-all
         when using -g or -i, create a dump file for each
-        step. The character '%' is replaces in all dump
+        step. The character '%' is replaced in all dump
         filenames with the step number.
 
     --append <num_steps>
@@ -153,6 +154,13 @@ def usage():
 
     --binary
         dump anyconst values as raw bit strings
+
+    --keep-going
+        continue BMC after the first failed assertion and report
+        further failed assertions. To output multiple traces
+        covering all found failed assertions, the character '%' is
+        replaced in all dump filenames with an increasing number.
+
 """ + so.helpmsg())
     sys.exit(1)
 
@@ -161,7 +169,7 @@ try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
             ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
              "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
-             "smtc-init", "smtc-top=", "noinit", "binary"])
+             "smtc-init", "smtc-top=", "noinit", "binary", "keep-going"])
 except:
     usage()
 
@@ -234,6 +242,8 @@ for o, a in opts:
         topmod = a
     elif o == "--binary":
         binarymode = True
+    elif o == "--keep-going":
+        keep_going = True
     elif so.handle(o, a):
         pass
     else:
@@ -341,13 +351,13 @@ for fn in inconstr:
             assert False
 
 
-def get_constr_expr(db, state, final=False, getvalues=False):
+def get_constr_expr(db, state, final=False, getvalues=False, individual=False):
     if final:
         if ("final-%d" % state) not in db:
-            return ([], [], []) if getvalues else "true"
+            return ([], [], []) if getvalues or individual else "true"
     else:
         if state not in db:
-            return ([], [], []) if getvalues else "true"
+            return ([], [], []) if getvalues or individual else "true"
 
     netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]*|\S*)\](?=[ )]|$)')
 
@@ -368,15 +378,18 @@ def get_constr_expr(db, state, final=False, getvalues=False):
     expr_list = list()
     for loc, expr in db[("final-%d" % state) if final else state]:
         actual_expr = netref_regex.sub(replace_netref, expr)
-        if getvalues:
+        if getvalues or individual:
             expr_list.append((loc, expr, actual_expr))
         else:
             expr_list.append(actual_expr)
 
-    if getvalues:
-        loc_list, expr_list, acual_expr_list = zip(*expr_list)
-        value_list = smt.get_list(acual_expr_list)
-        return loc_list, expr_list, value_list
+    if getvalues or individual:
+        loc_list, expr_list, actual_expr_list = zip(*expr_list)
+        if individual:
+            return loc_list, expr_list, actual_expr_list
+        else:
+            value_list = smt.get_list(actual_expr_list)
+            return loc_list, expr_list, value_list
 
     if len(expr_list) == 0:
         return "true"
@@ -492,7 +505,7 @@ if aimfile is not None:
             got_state = True
 
         for entry in f.read().splitlines():
-            if len(entry) == 0 or entry[0] in "bcjfu.":
+            if len(entry) == 0 or entry[0] in "bcjfu.#":
                 continue
 
             if not got_state:
@@ -583,7 +596,10 @@ if aimfile is not None:
 
             if not got_topt:
                 skip_steps = max(skip_steps, step)
-                num_steps = max(num_steps, step+1)
+                # some solvers optimize the properties so that they fail one cycle early,
+                # thus we check the properties in the cycle the aiger witness ends, and
+                # if that doesn't work, we check the cycle after that as well.
+                num_steps = max(num_steps, step+2)
             step += 1
 
 if btorwitfile is not None:
@@ -826,7 +842,7 @@ def char_ok_in_verilog(c,i):
     return False
 
 def escape_identifier(identifier):
-    if type(identifier) is list: 
+    if type(identifier) is list:
         return map(escape_identifier, identifier)
     if "." in identifier:
         return ".".join(escape_identifier(identifier.split(".")))
@@ -1068,7 +1084,7 @@ def write_trace(steps_start, steps_stop, index):
         write_constr_trace(steps_start, steps_stop, index)
 
 
-def print_failed_asserts_worker(mod, state, path, extrainfo):
+def print_failed_asserts_worker(mod, state, path, extrainfo, infomap, infokey=()):
     assert mod in smt.modinfo
     found_failed_assert = False
 
@@ -1076,29 +1092,31 @@ def print_failed_asserts_worker(mod, state, path, extrainfo):
         return
 
     for cellname, celltype in smt.modinfo[mod].cells.items():
-        if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo):
+        cell_infokey = (mod, cellname, infokey)
+        if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo, infomap, cell_infokey):
             found_failed_assert = True
 
     for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
         if smt.get("(|%s| %s)" % (assertfun, state)) in ["false", "#b0"]:
-            print_msg("Assert failed in %s: %s%s" % (path, assertinfo, extrainfo))
+            assert_key = (assertfun, infokey)
+            print_msg("Assert failed in %s: %s%s%s" % (path, assertinfo, extrainfo, infomap.get(assert_key, '')))
             found_failed_assert = True
 
     return found_failed_assert
 
 
-def print_failed_asserts(state, final=False, extrainfo=""):
+def print_failed_asserts(state, final=False, extrainfo="", infomap={}):
     if noinfo: return
     loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True)
     found_failed_assert = False
 
     for loc, expr, value in zip(loc_list, expr_list, value_list):
         if smt.bv2int(value) == 0:
-            print_msg("Assert %s failed: %s%s" % (loc, expr, extrainfo))
+            print_msg("Assert %s failed: %s%s%s" % (loc, expr, extrainfo, infomap.get(loc, '')))
             found_failed_assert = True
 
     if not final:
-        if print_failed_asserts_worker(topmod, "s%d" % state, topmod, extrainfo):
+        if print_failed_asserts_worker(topmod, "s%d" % state, topmod, extrainfo, infomap):
             found_failed_assert = True
 
     return found_failed_assert
@@ -1145,6 +1163,43 @@ def get_cover_list(mod, base):
 
     return cover_expr, cover_desc
 
+
+def get_assert_map(mod, base, path, key_base=()):
+    assert mod in smt.modinfo
+
+    assert_map = dict()
+
+    for expr, desc in smt.modinfo[mod].asserts.items():
+        assert_map[(expr, key_base)] = ("(|%s| %s)" % (expr, base), path, desc)
+
+    for cell, submod in smt.modinfo[mod].cells.items():
+        assert_map.update(get_assert_map(submod, "(|%s_h %s| %s)" % (mod, cell, base), path + "." + cell, (mod, cell, key_base)))
+
+    return assert_map
+
+
+def get_assert_keys():
+    keys = set()
+    keys.update(get_assert_map(topmod, 'state', topmod).keys())
+    for step_constr_asserts in constr_asserts.values():
+        keys.update(loc for loc, expr in step_constr_asserts)
+
+    return keys
+
+
+def get_active_assert_map(step, active):
+    assert_map = dict()
+    for key, assert_data in get_assert_map(topmod, "s%s" % step, topmod).items():
+        if key in active:
+            assert_map[key] = assert_data
+
+    for loc, expr, actual_expr in zip(*get_constr_expr(constr_asserts, step, individual=True)):
+        if loc in active:
+            assert_map[loc] = (actual_expr, None, (expr, loc))
+
+    return assert_map
+
+
 states = list()
 asserts_antecedent_cache = [list()]
 asserts_consequent_cache = [list()]
@@ -1454,6 +1509,10 @@ elif covermode:
                 print_msg("Unreached cover statement at %s." % cover_desc[i])
 
 else:  # not tempind, covermode
+    active_assert_keys = get_assert_keys()
+    failed_assert_infomap = dict()
+    traceidx = 0
+
     step = 0
     retstatus = "PASSED"
     while step < num_steps:
@@ -1507,44 +1566,83 @@ else:  # not tempind, covermode
                     break
 
             if not final_only:
-                if last_check_step == step:
-                    print_msg("Checking assertions in step %d.." % (step))
-                else:
-                    print_msg("Checking assertions in steps %d to %d.." % (step, last_check_step))
-                smt_push()
-
-                smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
-                        [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))
-
-                if smt_check_sat() == "sat":
-                    print("%s BMC failed!" % smt.timestamp())
-                    if append_steps > 0:
-                        for i in range(last_check_step+1, last_check_step+1+append_steps):
-                            print_msg("Appending additional step %d." % i)
-                            smt_state(i)
-                            smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
-                            smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
-                            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 append steps without violating assumptions!" % smt.timestamp())
-                            retstatus = "FAILED"
-                            break
-                    print_anyconsts(step)
+                recheck_current_step = True
+                while recheck_current_step:
+                    recheck_current_step = False
+                    if last_check_step == step:
+                        print_msg("Checking assertions in step %d.." % (step))
+                    else:
+                        print_msg("Checking assertions in steps %d to %d.." % (step, last_check_step))
+                    smt_push()
+
+                    active_assert_maps = dict()
+                    active_assert_exprs = list()
                     for i in range(step, last_check_step+1):
-                        print_failed_asserts(i)
-                    write_trace(0, last_check_step+1+append_steps, '%')
-                    retstatus = "FAILED"
-                    break
+                        assert_expr_map = get_active_assert_map(i, active_assert_keys)
+                        active_assert_maps[i] = assert_expr_map
+                        active_assert_exprs.extend(assert_data[0] for assert_data in assert_expr_map.values())
 
-                smt_pop()
+                    if active_assert_exprs:
+                        if len(active_assert_exprs) == 1:
+                            active_assert_expr = active_assert_exprs[0]
+                        else:
+                            active_assert_expr = "(and %s)" % " ".join(active_assert_exprs)
+
+                        smt_assert("(not %s)" % active_assert_expr)
+                    else:
+                        smt_assert("false")
+
+
+                    if smt_check_sat() == "sat":
+                        if retstatus != "FAILED":
+                            print("%s BMC failed!" % smt.timestamp())
+
+                        if append_steps > 0:
+                            for i in range(last_check_step+1, last_check_step+1+append_steps):
+                                print_msg("Appending additional step %d." % i)
+                                smt_state(i)
+                                smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
+                                smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
+                                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 append steps without violating assumptions!" % smt.timestamp())
+                                retstatus = "FAILED"
+                                break
+                        print_anyconsts(step)
+
+                        for i in range(step, last_check_step+1):
+                            print_failed_asserts(i, infomap=failed_assert_infomap)
+
+                        if keep_going:
+                            for i in range(step, last_check_step+1):
+                                for key, (expr, path, desc) in active_assert_maps[i].items():
+                                    if key in active_assert_keys and not smt.bv2int(smt.get(expr)):
+                                        failed_assert_infomap[key] = " [failed before]"
+
+                                        active_assert_keys.remove(key)
+
+                            if active_assert_keys:
+                                recheck_current_step = True
+
+                        write_trace(0, last_check_step+1+append_steps, "%d" % traceidx if keep_going else '%')
+                        traceidx += 1
+                        retstatus = "FAILED"
+
+                    smt_pop()
+                    if recheck_current_step:
+                        print_msg("Checking remaining assertions..")
+
+                if retstatus == "FAILED" and not (keep_going and active_assert_keys):
+                    break
 
             if (constr_final_start is not None) or (last_check_step+1 != num_steps):
                 for i in range(step, last_check_step+1):
-                    smt_assert("(|%s_a| s%d)" % (topmod, i))
-                    smt_assert(get_constr_expr(constr_asserts, i))
+                    assert_expr_map = get_active_assert_map(i, active_assert_keys)
+                    for assert_data in assert_expr_map.values():
+                        smt_assert(assert_data[0])
 
             if constr_final_start is not None:
                 for i in range(step, last_check_step+1):
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index d73a875ba..91efc13a3 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -20,7 +20,7 @@ import sys, re, os, signal
 import subprocess
 if os.name == "posix":
     import resource
-from copy import deepcopy
+from copy import copy
 from select import select
 from time import time
 from queue import Queue, Empty
@@ -123,6 +123,7 @@ class SmtIo:
         self.forall = False
         self.timeout = 0
         self.produce_models = True
+        self.recheck = False
         self.smt2cache = [list()]
         self.smt2_options = dict()
         self.p = None
@@ -176,7 +177,10 @@ class SmtIo:
             self.unroll = False
 
         if self.solver == "yices":
-            if self.noincr or self.forall:
+            if self.forall:
+                self.noincr = True
+
+            if self.noincr:
                 self.popen_vargs = ['yices-smt2'] + self.solver_opts
             else:
                 self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
@@ -189,11 +193,12 @@ class SmtIo:
             if self.timeout != 0:
                 self.popen_vargs.append('-T:%d' % self.timeout);
 
-        if self.solver == "cvc4":
+        if self.solver in ["cvc4", "cvc5"]:
+            self.recheck = True
             if self.noincr:
-                self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+                self.popen_vargs = [self.solver, '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
             else:
-                self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+                self.popen_vargs = [self.solver, '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
             if self.timeout != 0:
                 self.popen_vargs.append('--tlimit=%d000' % self.timeout);
 
@@ -301,7 +306,7 @@ class SmtIo:
 
             key = tuple(stmt)
             if key not in self.unroll_cache:
-                decl = deepcopy(self.unroll_decls[key[0]])
+                decl = copy(self.unroll_decls[key[0]])
 
                 self.unroll_cache[key] = "|UNROLL#%d|" % self.unroll_idcnt
                 decl[1] = self.unroll_cache[key]
@@ -404,6 +409,15 @@ class SmtIo:
             stmt = re.sub(r" *;.*", "", stmt)
             if stmt == "": return
 
+        recheck = None
+
+        if self.solver != "dummy":
+            if self.noincr:
+                # Don't close the solver yet, if we're just unrolling definitions
+                # required for a (get-...) statement
+                if self.p is not None and not stmt.startswith("(get-") and unroll:
+                    self.p_close()
+
         if unroll and self.unroll:
             stmt = self.unroll_buffer + stmt
             self.unroll_buffer = ""
@@ -415,6 +429,9 @@ class SmtIo:
 
             s = self.parse(stmt)
 
+            if self.recheck and s and s[0].startswith("get-"):
+                recheck = self.unroll_idcnt
+
             if self.debug_print:
                 print("-> %s" % s)
 
@@ -440,12 +457,15 @@ class SmtIo:
 
             stmt = self.unparse(self.unroll_stmt(s))
 
+            if recheck is not None and recheck != self.unroll_idcnt:
+                self.check_sat(["sat"])
+
             if stmt == "(push 1)":
                 self.unroll_stack.append((
-                    deepcopy(self.unroll_sorts),
-                    deepcopy(self.unroll_objs),
-                    deepcopy(self.unroll_decls),
-                    deepcopy(self.unroll_cache),
+                    copy(self.unroll_sorts),
+                    copy(self.unroll_objs),
+                    copy(self.unroll_decls),
+                    copy(self.unroll_cache),
                 ))
 
             if stmt == "(pop 1)":
@@ -460,8 +480,6 @@ class SmtIo:
 
         if self.solver != "dummy":
             if self.noincr:
-                if self.p is not None and not stmt.startswith("(get-"):
-                    self.p_close()
                 if stmt == "(push 1)":
                     self.smt2cache.append(list())
                 elif stmt == "(pop 1)":
@@ -536,10 +554,16 @@ class SmtIo:
                     self.modinfo[self.curmod].clocks[fields[2]] = "event"
 
         if fields[1] == "yosys-smt2-assert":
-            self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]
+            if len(fields) > 4:
+                self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})'
+            else:
+                self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]
 
         if fields[1] == "yosys-smt2-cover":
-            self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
+            if len(fields) > 4:
+                self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})'
+            else:
+                self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
 
         if fields[1] == "yosys-smt2-maximize":
             self.modinfo[self.curmod].maximize.add(fields[2])
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index 7bace6912..7d4f94adc 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -741,6 +741,11 @@ struct SmvBackend : public Backend {
 
 		log_header(design, "Executing SMV backend.\n");
 
+		log_push();
+		Pass::call(design, "bmuxmap");
+		Pass::call(design, "demuxmap");
+		log_pop();
+
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
 		{
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 47ef1c479..aa1d4558c 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -358,7 +358,8 @@ 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 << "\"\"";
+		// See IEEE 1364-2005 Clause 5.1.14.
+		f << "{0{1'b0}}";
 		return;
 	}
 	if (sig.is_chunk()) {
@@ -431,7 +432,7 @@ void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
 			dump_const(f, wire->attributes.at(ID::init));
 		}
 		f << stringf(";\n");
-	} else if (!wire->port_input && !wire->port_output)
+	} else
 		f << stringf("%s" "wire%s %s;\n", indent.c_str(), range.c_str(), id(wire->name).c_str());
 #endif
 }
@@ -2299,6 +2300,12 @@ struct VerilogBackend : public Backend {
 			extmem_prefix = filename.substr(0, filename.rfind('.'));
 		}
 
+		log_push();
+		Pass::call(design, "bmuxmap");
+		Pass::call(design, "demuxmap");
+		Pass::call(design, "clean_zerowidth");
+		log_pop();
+
 		design->sort();
 
 		*f << stringf("/* Generated by %s */\n", yosys_version_str);