Merge branch 'master' into firrtl_err_on_unsupported_cell

# Conflicts:
#	backends/firrtl/firrtl.cc

9 files changed, 287 insertions, 116 deletions

diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 69f63486c..a3a753912 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -53,7 +53,7 @@ PRIVATE_NAMESPACE_BEGIN
 
 inline int32_t to_big_endian(int32_t i32) {
 #if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
-	return __builtin_bswap32(i32);
+	return bswap32(i32);
 #elif __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
 	return i32;
 #else
@@ -610,15 +610,15 @@ struct XAigerWriter
 			std::stringstream h_buffer;
 			auto write_h_buffer = std::bind(write_buffer, std::ref(h_buffer), std::placeholders::_1);
 			write_h_buffer(1);
-			log_debug("ciNum = %zu\n", input_bits.size() + ci_bits.size());
+			log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ci_bits));
 			write_h_buffer(input_bits.size() + ci_bits.size());
-			log_debug("coNum = %zu\n", output_bits.size() + co_bits.size());
+			log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(co_bits));
 			write_h_buffer(output_bits.size() + co_bits.size());
-			log_debug("piNum = %zu\n", input_bits.size());
+			log_debug("piNum = %d\n", GetSize(input_bits));
 			write_h_buffer(input_bits.size());
-			log_debug("poNum = %zu\n", output_bits.size());
+			log_debug("poNum = %d\n", GetSize(output_bits));
 			write_h_buffer(output_bits.size());
-			log_debug("boxNum = %zu\n", box_list.size());
+			log_debug("boxNum = %d\n", GetSize(box_list));
 			write_h_buffer(box_list.size());
 
 			RTLIL::Module *holes_module = nullptr;
@@ -772,7 +772,7 @@ struct XAigerWriter
 
 				if (output_bits.count(b)) {
 					int o = ordered_outputs.at(b);
-					output_lines[o] += stringf("output %lu %d %s\n", o - co_bits.size(), i, log_id(wire));
+					output_lines[o] += stringf("output %d %d %s\n", o - GetSize(co_bits), i, log_id(wire));
 					continue;
 				}
 
diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc
index a1761b662..f32b0f533 100644
--- a/backends/blif/blif.cc
+++ b/backends/blif/blif.cc
@@ -327,6 +327,13 @@ struct BlifDumper
 				goto internal_cell;
 			}
 
+			if (!config->icells_mode && cell->type == "$_NMUX_") {
+				f << stringf(".names %s %s %s %s\n0-0 1\n-01 1\n",
+						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
+						cstr(cell->getPort("\\S")), cstr(cell->getPort("\\Y")));
+				goto internal_cell;
+			}
+
 			if (!config->icells_mode && cell->type == "$_FF_") {
 				f << stringf(".latch %s %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
 						cstr_init(cell->getPort("\\Q")));
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index a507b120b..7bacce2af 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -496,7 +496,7 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in("$mux", "$_MUX_"))
+		if (cell->type.in("$mux", "$_MUX_", "$_NMUX_"))
 		{
 			SigSpec sig_a = sigmap(cell->getPort("\\A"));
 			SigSpec sig_b = sigmap(cell->getPort("\\B"));
@@ -511,6 +511,12 @@ struct BtorWorker
 			int nid = next_nid++;
 			btorf("%d ite %d %d %d %d\n", nid, sid, nid_s, nid_b, nid_a);
 
+			if (cell->type == "$_NMUX_") {
+				int tmp = nid;
+				nid = next_nid++;
+				btorf("%d not %d %d\n", nid, sid, tmp);
+			}
+
 			add_nid_sig(nid, sig_y);
 			goto okay;
 		}
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index b7a798b85..ad4b37353 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -381,10 +381,10 @@ struct FirrtlWorker
 
 	// Given an expression for a shift amount, and a maximum width,
 	//  generate the FIRRTL expression for equivalent dynamic shift taking into account FIRRTL shift semantics.
-	std::string gen_dshl(const string b_expr, const int b_padded_width)
+	std::string gen_dshl(const string b_expr, const int b_width)
 	{
 		string result = b_expr;
-		if (b_padded_width >= FIRRTL_MAX_DSH_WIDTH_ERROR) {
+		if (b_width >= FIRRTL_MAX_DSH_WIDTH_ERROR) {
 			int max_shift_width_bits = FIRRTL_MAX_DSH_WIDTH_ERROR - 1;
 			string max_shift_string = stringf("UInt<%d>(%d)", max_shift_width_bits, (1<<max_shift_width_bits) - 1);
 			// Deal with the difference in semantics between FIRRTL and verilog
@@ -422,22 +422,33 @@ struct FirrtlWorker
 
 		for (auto cell : module->cells())
 		{
-			bool extract_y_bits = false;		// Assume no extraction of final bits will be required.
+			static Const ndef(0, 0);
+
 		    // Is this cell is a module instance?
 			if (cell->type[0] != '$')
 			{
 				process_instance(cell, wire_exprs);
 				continue;
 			}
+			// Not a module instance. Set up cell properties
+			bool extract_y_bits = false;		// Assume no extraction of final bits will be required.
+			int a_width = cell->parameters.at("\\A_WIDTH", ndef).as_int();	// The width of "A"
+			int b_width = cell->parameters.at("\\B_WIDTH", ndef).as_int();	// The width of "A"
+			const int y_width = cell->parameters.at("\\Y_WIDTH", ndef).as_int();	// The width of the result
+			const bool a_signed = cell->parameters.at("\\A_SIGNED", ndef).as_bool();
+			const bool b_signed = cell->parameters.at("\\B_SIGNED", ndef).as_bool();
+			bool firrtl_is_signed = a_signed;	// The result is signed (subsequent code may change this).
+			int firrtl_width = 0;
+			string primop;
+			bool always_uint = false;
+			string y_id = make_id(cell->name);
+
 			if (cell->type.in("$not", "$logic_not", "$neg", "$reduce_and", "$reduce_or", "$reduce_xor", "$reduce_bool", "$reduce_xnor"))
 			{
-				string y_id = make_id(cell->name);
-				bool is_signed = cell->parameters.at("\\A_SIGNED").as_bool();
-				int y_width =  cell->parameters.at("\\Y_WIDTH").as_int();
 				string a_expr = make_expr(cell->getPort("\\A"));
 				wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", y_id.c_str(), y_width));
 
-				if (cell->parameters.at("\\A_SIGNED").as_bool()) {
+				if (a_signed) {
 					a_expr = "asSInt(" + a_expr + ")";
 				}
 
@@ -446,12 +457,13 @@ struct FirrtlWorker
 					a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
 				}
 
-				string primop;
-				bool always_uint = false;
+				// Assume the FIRRTL width is a single bit.
+				firrtl_width = 1;
 				if (cell->type == "$not") primop = "not";
 				else if (cell->type == "$neg") {
 					primop = "neg";
-					is_signed = true;	// Result of "neg" is signed (an SInt).
+					firrtl_is_signed = true;	// Result of "neg" is signed (an SInt).
+					firrtl_width = a_width;
 				} else if (cell->type == "$logic_not") {
                                         primop = "eq";
                                         a_expr = stringf("%s, UInt(0)", a_expr.c_str());
@@ -466,14 +478,12 @@ struct FirrtlWorker
 				else if (cell->type == "$reduce_bool") {
 					primop = "neq";
 					// Use the sign of the a_expr and its width as the type (UInt/SInt) and width of the comparand.
-					bool a_signed = cell->parameters.at("\\A_SIGNED").as_bool();
-					int a_width =  cell->parameters.at("\\A_WIDTH").as_int();
 					a_expr = stringf("%s, %cInt<%d>(0)", a_expr.c_str(), a_signed ? 'S' : 'U', a_width);
 				}
 
 				string expr = stringf("%s(%s)", primop.c_str(), a_expr.c_str());
 
-				if ((is_signed && !always_uint))
+				if ((firrtl_is_signed && !always_uint))
 					expr = stringf("asUInt(%s)", expr.c_str());
 
 				cell_exprs.push_back(stringf("    %s <= %s\n", y_id.c_str(), expr.c_str()));
@@ -481,81 +491,121 @@ struct FirrtlWorker
 
 				continue;
 			}
-			if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$and", "$or", "$eq", "$eqx",
+			if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$xnor", "$and", "$or", "$eq", "$eqx",
 							  "$gt", "$ge", "$lt", "$le", "$ne", "$nex", "$shr", "$sshr", "$sshl", "$shl",
-							  "$logic_and", "$logic_or"))
+							  "$logic_and", "$logic_or", "$pow"))
 			{
-				string y_id = make_id(cell->name);
-				bool is_signed = cell->parameters.at("\\A_SIGNED").as_bool();
-				int y_width =  cell->parameters.at("\\Y_WIDTH").as_int();
 				string a_expr = make_expr(cell->getPort("\\A"));
 				string b_expr = make_expr(cell->getPort("\\B"));
-				int b_padded_width = cell->parameters.at("\\B_WIDTH").as_int();
 				wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", y_id.c_str(), y_width));
 
-				if (cell->parameters.at("\\A_SIGNED").as_bool()) {
+				if (a_signed) {
 					a_expr = "asSInt(" + a_expr + ")";
-				}
-				// Shift amount is always unsigned, and needn't be padded to result width.
-				if (!cell->type.in("$shr", "$sshr", "$shl", "$sshl")) {
-					if (cell->parameters.at("\\B_SIGNED").as_bool()) {
-						b_expr = "asSInt(" + b_expr + ")";
+					// Expand the "A" operand to the result width
+					if (a_width < y_width) {
+						a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+						a_width = y_width;
 					}
-					if (b_padded_width < y_width) {
-						auto b_sig = cell->getPort("\\B");
-						b_padded_width = y_width;
+				}
+				// Shift amount is always unsigned, and needn't be padded to result width,
+				//  otherwise, we need to cast the b_expr appropriately
+				if (b_signed && !cell->type.in("$shr", "$sshr", "$shl", "$sshl", "$pow")) {
+					b_expr = "asSInt(" + b_expr + ")";
+					// Expand the "B" operand to the result width
+					if (b_width < y_width) {
+						b_expr = stringf("pad(%s, %d)", b_expr.c_str(), y_width);
+						b_width = y_width;
 					}
 				}
 
+				// For the arithmetic ops, expand operand widths to result widths befor performing the operation.
+				// This corresponds (according to iverilog) to what verilog compilers implement.
+				if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$xnor", "$and", "$or"))
+				{
+					if (a_width < y_width) {
+						a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+						a_width = y_width;
+					}
+					if (b_width < y_width) {
+						b_expr = stringf("pad(%s, %d)", b_expr.c_str(), y_width);
+						b_width = y_width;
+					}
+				}
+				// Assume the FIRRTL width is the width of "A"
+				firrtl_width = a_width;
 				auto a_sig = cell->getPort("\\A");
 
-				if (cell->parameters.at("\\A_SIGNED").as_bool()  & (cell->type == "$shr")) {
-					a_expr = "asUInt(" + a_expr + ")";
+				if (cell->type == "$add") {
+					primop = "add";
+					firrtl_is_signed = a_signed | b_signed;
+					firrtl_width = max(a_width, b_width);
+				} else if (cell->type == "$sub") {
+					primop = "sub";
+					firrtl_is_signed = true;
+					int a_widthInc = (!a_signed && b_signed) ? 2 : (a_signed && !b_signed) ? 1 : 0;
+					int b_widthInc = (a_signed && !b_signed) ? 2 : (!a_signed && b_signed) ? 1 : 0;
+					firrtl_width = max(a_width + a_widthInc, b_width + b_widthInc);
+				} else if (cell->type == "$mul") {
+					primop = "mul";
+					firrtl_is_signed = a_signed | b_signed;
+					firrtl_width = a_width + b_width;
+				} else if (cell->type == "$div") {
+					primop = "div";
+					firrtl_is_signed = a_signed | b_signed;
+					firrtl_width = a_width;
+				} else if (cell->type == "$mod") {
+					primop = "rem";
+					firrtl_width = min(a_width, b_width);
+				} else if (cell->type == "$and") {
+					primop = "and";
+					always_uint = true;
+					firrtl_width = max(a_width, b_width);
 				}
-
-				string primop;
-				bool always_uint = false;
-				if (cell->type == "$add") primop = "add";
-				else if (cell->type == "$sub") primop = "sub";
-				else if (cell->type == "$mul") primop = "mul";
-				else if (cell->type == "$div") primop = "div";
-				else if (cell->type == "$mod") primop = "rem";
-				else if (cell->type == "$and") {
-                                        primop = "and";
-                                        always_uint = true;
-                                }
 				else if (cell->type == "$or" ) {
-                                        primop =  "or";
-                                        always_uint = true;
-                                }
+					primop =  "or";
+					always_uint = true;
+					firrtl_width = max(a_width, b_width);
+				}
 				else if (cell->type == "$xor") {
-                                        primop = "xor";
-                                        always_uint = true;
-                                }
+					primop = "xor";
+					always_uint = true;
+					firrtl_width = max(a_width, b_width);
+				}
+				else if (cell->type == "$xnor") {
+					primop = "xnor";
+					always_uint = true;
+					firrtl_width = max(a_width, b_width);
+				}
 				else if ((cell->type == "$eq") | (cell->type == "$eqx")) {
-                                        primop = "eq";
-                                        always_uint = true;
-                                }
+					primop = "eq";
+					always_uint = true;
+					firrtl_width = 1;
+			    }
 				else if ((cell->type == "$ne") | (cell->type == "$nex")) {
-                                        primop = "neq";
-                                        always_uint = true;
-                                }
+					primop = "neq";
+					always_uint = true;
+					firrtl_width = 1;
+				}
 				else if (cell->type == "$gt") {
-                                        primop = "gt";
-                                        always_uint = true;
-                                }
+					primop = "gt";
+					always_uint = true;
+					firrtl_width = 1;
+				}
 				else if (cell->type == "$ge") {
-                                        primop = "geq";
-                                        always_uint = true;
-                                }
+					primop = "geq";
+					always_uint = true;
+					firrtl_width = 1;
+				}
 				else if (cell->type == "$lt") {
-                                        primop = "lt";
-                                        always_uint = true;
-                                }
+					primop = "lt";
+					always_uint = true;
+					firrtl_width = 1;
+				}
 				else if (cell->type == "$le") {
-                                        primop = "leq";
-                                        always_uint = true;
-                                }
+					primop = "leq";
+					always_uint = true;
+					firrtl_width = 1;
+				}
 				else if ((cell->type == "$shl") | (cell->type == "$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.
@@ -564,11 +614,14 @@ 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());
+						int shift_amount = b_sig.as_int();
+						b_expr = std::to_string(shift_amount);
+						firrtl_width = a_width + shift_amount;
 					} else {
 						primop = "dshl";
 						// Convert from FIRRTL left shift semantics.
-						b_expr = gen_dshl(b_expr, b_padded_width);
+						b_expr = gen_dshl(b_expr, b_width);
+						firrtl_width = a_width + (1 << b_width) - 1;
 					}
 				}
 				else if ((cell->type == "$shr") | (cell->type == "$sshr")) {
@@ -578,36 +631,86 @@ 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());
+						int shift_amount = b_sig.as_int();
+						b_expr = std::to_string(shift_amount);
+						firrtl_width = max(1, a_width - shift_amount);
 					} else {
 						primop = "dshr";
+						firrtl_width = a_width;
+					}
+					// We'll need to do some special fixups if the source (and thus result) is signed.
+					if (firrtl_is_signed) {
+						// If this is a "logical" shift right, pretend the source is unsigned.
+						if (cell->type == "$shr") {
+							a_expr = "asUInt(" + a_expr + ")";
+						}
 					}
 				}
 				else if ((cell->type == "$logic_and")) {
-                                        primop = "and";
-                                        a_expr = "neq(" + a_expr + ", UInt(0))";
-                                        b_expr = "neq(" + b_expr + ", UInt(0))";
-                                        always_uint = true;
-                                }
+					primop = "and";
+					a_expr = "neq(" + a_expr + ", UInt(0))";
+					b_expr = "neq(" + b_expr + ", UInt(0))";
+					always_uint = true;
+					firrtl_width = 1;
+				}
 				else if ((cell->type == "$logic_or")) {
-                                        primop = "or";
-                                        a_expr = "neq(" + a_expr + ", UInt(0))";
-                                        b_expr = "neq(" + b_expr + ", UInt(0))";
-                                        always_uint = true;
-                                }
+					primop = "or";
+					a_expr = "neq(" + a_expr + ", UInt(0))";
+					b_expr = "neq(" + b_expr + ", UInt(0))";
+					always_uint = true;
+					firrtl_width = 1;
+				}
+				else if ((cell->type == "$pow")) {
+					if (a_sig.is_fully_const() && a_sig.as_int() == 2) {
+						// We'll convert this to a shift. To simplify things, change the a_expr to "1"
+						//	so we can use b_expr directly as a shift amount.
+						// Only support 2 ** N (i.e., shift left)
+						// 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.
+						a_expr = firrtl_is_signed ? "SInt(1)" : "UInt(1)";
+						extract_y_bits = true;
+						// Is the shift amount constant?
+						auto b_sig = cell->getPort("\\B");
+						if (b_sig.is_fully_const()) {
+							primop = "shl";
+							int shiftAmount = b_sig.as_int();
+							if (shiftAmount < 0) {
+								log_error("Negative power exponent - %d: %s.%s\n", shiftAmount, log_id(module), log_id(cell));
+							}
+							b_expr = std::to_string(shiftAmount);
+							firrtl_width = a_width + shiftAmount;
+						} else {
+							primop = "dshl";
+							// Convert from FIRRTL left shift semantics.
+							b_expr = gen_dshl(b_expr, b_width);
+							firrtl_width = a_width + (1 << b_width) - 1;
+						}
+					} else {
+						log_error("Non power 2: %s.%s\n", log_id(module), log_id(cell));
+					}
+				}
 
 				if (!cell->parameters.at("\\B_SIGNED").as_bool()) {
 					b_expr = "asUInt(" + b_expr + ")";
 				}
 
-				string expr = stringf("%s(%s, %s)", primop.c_str(), a_expr.c_str(), b_expr.c_str());
+				string expr;
+				// Deal with $xnor == ~^ (not xor)
+				if (primop == "xnor") {
+					expr = stringf("not(xor(%s, %s))", a_expr.c_str(), b_expr.c_str());
+				} else {
+					expr = stringf("%s(%s, %s)", primop.c_str(), a_expr.c_str(), b_expr.c_str());
+				}
 
-				// Deal with FIRRTL's "shift widens" semantics
+				// Deal with FIRRTL's "shift widens" semantics, or the need to widen the FIRRTL result.
+				// If the operation is signed, the FIRRTL width will be 1 one bit larger.
 				if (extract_y_bits) {
 					expr = stringf("bits(%s, %d, 0)", expr.c_str(), y_width - 1);
+				} else if (firrtl_is_signed && (firrtl_width + 1) < y_width) {
+					expr = stringf("pad(%s, %d)", expr.c_str(), y_width);
 				}
 
-				if ((is_signed && !always_uint) || cell->type.in("$sub"))
+				if ((firrtl_is_signed && !always_uint))
 					expr = stringf("asUInt(%s)", expr.c_str());
 
 				cell_exprs.push_back(stringf("    %s <= %s\n", y_id.c_str(), expr.c_str()));
@@ -618,7 +721,6 @@ struct FirrtlWorker
 
 			if (cell->type.in("$mux"))
 			{
-				string y_id = make_id(cell->name);
 				int width = cell->parameters.at("\\WIDTH").as_int();
 				string a_expr = make_expr(cell->getPort("\\A"));
 				string b_expr = make_expr(cell->getPort("\\B"));
@@ -762,15 +864,14 @@ struct FirrtlWorker
 				if (clkpol == false)
 					log_error("Negative edge clock on FF %s.%s.\n", log_id(module), log_id(cell));
 
-				string q_id = make_id(cell->name);
 				int width = cell->parameters.at("\\WIDTH").as_int();
 				string expr = make_expr(cell->getPort("\\D"));
 				string clk_expr = "asClock(" + make_expr(cell->getPort("\\CLK")) + ")";
 
-				wire_decls.push_back(stringf("    reg %s: UInt<%d>, %s\n", q_id.c_str(), width, clk_expr.c_str()));
+				wire_decls.push_back(stringf("    reg %s: UInt<%d>, %s\n", y_id.c_str(), width, clk_expr.c_str()));
 
-				cell_exprs.push_back(stringf("    %s <= %s\n", q_id.c_str(), expr.c_str()));
-				register_reverse_wire_map(q_id, cell->getPort("\\Q"));
+				cell_exprs.push_back(stringf("    %s <= %s\n", y_id.c_str(), expr.c_str()));
+				register_reverse_wire_map(y_id, cell->getPort("\\Q"));
 
 				continue;
 			}
@@ -785,8 +886,6 @@ struct FirrtlWorker
 				// assign y = a[b +: y_width];
 				// We'll extract the correct bits as part of the primop.
 
-				string y_id = make_id(cell->name);
-				int y_width =  cell->parameters.at("\\Y_WIDTH").as_int();
 				string a_expr = make_expr(cell->getPort("\\A"));
 				// Get the initial bit selector
 				string b_expr = make_expr(cell->getPort("\\B"));
@@ -808,18 +907,15 @@ struct FirrtlWorker
 				// assign y = a >> b;
 				//  where b may be negative
 
-				string y_id = make_id(cell->name);
-				int y_width =  cell->parameters.at("\\Y_WIDTH").as_int();
 				string a_expr = make_expr(cell->getPort("\\A"));
 				string b_expr = make_expr(cell->getPort("\\B"));
 				auto b_string = b_expr.c_str();
-				int b_padded_width = cell->parameters.at("\\B_WIDTH").as_int();
 				string expr;
 				wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", y_id.c_str(), y_width));
 
 				if (cell->getParam("\\B_SIGNED").as_bool()) {
 					// We generate a left or right shift based on the sign of b.
-					std::string dshl = stringf("bits(dshl(%s, %s), 0, %d)", a_expr.c_str(), gen_dshl(b_expr, b_padded_width).c_str(), y_width);
+					std::string dshl = stringf("bits(dshl(%s, %s), 0, %d)", a_expr.c_str(), gen_dshl(b_expr, b_width).c_str(), y_width);
 					std::string dshr = stringf("dshr(%s, %s)", a_expr.c_str(), b_string);
 					expr = stringf("mux(%s < 0, %s, %s)",
 									 b_string,
@@ -833,6 +929,20 @@ struct FirrtlWorker
 				register_reverse_wire_map(y_id, cell->getPort("\\Y"));
 				continue;
 			}
+			if (cell->type == "$pos") {
+				// assign y = a;
+//				printCell(cell);
+				string a_expr = make_expr(cell->getPort("\\A"));
+				// Verilog appears to treat the result as signed, so if the result is wider than "A",
+				//  we need to pad.
+				if (a_width < y_width) {
+					a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+				}
+				wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", y_id.c_str(), y_width));
+				cell_exprs.push_back(stringf("    %s <= %s\n", y_id.c_str(), a_expr.c_str()));
+				register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+				continue;
+			}
 			log_error("Cell type not supported: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
 		}
 
diff --git a/backends/json/json.cc b/backends/json/json.cc
index dda4dfedd..107009ee4 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -83,20 +83,43 @@ struct JsonWriter
 		return str + " ]";
 	}
 
+	void write_parameter_value(const Const &value)
+	{
+		if ((value.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0) {
+			string str = value.decode_string();
+			int state = 0;
+			for (char c : str) {
+				if (state == 0) {
+					if (c == '0' || c == '1' || c == 'x' || c == 'z')
+						state = 0;
+					else if (c == ' ')
+						state = 1;
+					else
+						state = 2;
+				} else if (state == 1 && c != ' ')
+					state = 2;
+			}
+			if (state < 2)
+				str += " ";
+			f << get_string(str);
+		} else
+		if (GetSize(value) == 32 && value.is_fully_def()) {
+			if ((value.flags & RTLIL::ConstFlags::CONST_FLAG_SIGNED) != 0)
+				f << stringf("%d", value.as_int());
+			else
+				f << stringf("%u", value.as_int());
+		} else {
+			f << get_string(value.as_string());
+		}
+	}
+
 	void write_parameters(const dict<IdString, Const> &parameters, bool for_module=false)
 	{
 		bool first = true;
 		for (auto &param : parameters) {
 			f << stringf("%s\n", first ? "" : ",");
 			f << stringf("        %s%s: ", for_module ? "" : "    ", get_name(param.first).c_str());
-			if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0)
-				f << get_string(param.second.decode_string());
-			else if (GetSize(param.second.bits) > 32)
-				f << get_string(param.second.as_string());
-			else if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_SIGNED) != 0)
-				f << stringf("%d", param.second.as_int());
-			else
-				f << stringf("%u", param.second.as_int());
+			write_parameter_value(param.second);
 			first = false;
 		}
 	}
@@ -342,12 +365,13 @@ struct JsonBackend : public Backend {
 		log("Module and cell ports and nets can be single bit wide or vectors of multiple\n");
 		log("bits. Each individual signal bit is assigned a unique integer. The <bit_vector>\n");
 		log("values referenced above are vectors of this integers. Signal bits that are\n");
-		log("connected to a constant driver are denoted as string \"0\" or \"1\" instead of\n");
-		log("a number.\n");
+		log("connected to a constant driver are denoted as string \"0\", \"1\", \"x\", or\n");
+		log("\"z\" instead of a number.\n");
 		log("\n");
-		log("Numeric parameter and attribute values up to 32 bits are written as decimal\n");
-		log("values. Numbers larger than that are written as string holding the binary\n");
-		log("representation of the value.\n");
+		log("Numeric 32-bit parameter and attribute values are written as decimal values.\n");
+		log("Bit verctors of different sizes, or ones containing 'x' or 'z' bits, are written\n");
+		log("as string holding the binary representation of the value. Strings are written\n");
+		log("as strings, with an appended blank in cases of strings of the form /[01xz]* */.\n");
 		log("\n");
 		log("For example the following Verilog code:\n");
 		log("\n");
diff --git a/backends/simplec/simplec.cc b/backends/simplec/simplec.cc
index 6f2ccbe20..54dbb84af 100644
--- a/backends/simplec/simplec.cc
+++ b/backends/simplec/simplec.cc
@@ -472,7 +472,7 @@ struct SimplecWorker
 			return;
 		}
 
-		if (cell->type == "$_MUX_")
+		if (cell->type.in("$_MUX_", "$_NMUX_"))
 		{
 			SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
 			SigBit b = sigmaps.at(work->module)(cell->getPort("\\B"));
@@ -484,7 +484,9 @@ struct SimplecWorker
 			string s_expr = s.wire ? util_get_bit(work->prefix + cid(s.wire->name), s.wire->width, s.offset) : s.data ? "1" : "0";
 
 			// casts to bool are a workaround for CBMC bug (https://github.com/diffblue/cbmc/issues/933)
-			string expr = stringf("%s ? (bool)%s : (bool)%s", s_expr.c_str(), b_expr.c_str(), a_expr.c_str());
+			string expr = stringf("%s ? %s(bool)%s : %s(bool)%s", s_expr.c_str(),
+					cell->type == "$_NMUX_" ? "!" : "", b_expr.c_str(),
+					cell->type == "$_NMUX_" ? "!" : "", a_expr.c_str());
 
 			log_assert(y.wire);
 			funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index e318a4051..ddd680782 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -510,6 +510,7 @@ struct Smt2Worker
 		if (cell->type == "$_ANDNOT_") return export_gate(cell, "(and A (not B))");
 		if (cell->type == "$_ORNOT_") return export_gate(cell, "(or A (not B))");
 		if (cell->type == "$_MUX_") return export_gate(cell, "(ite S B A)");
+		if (cell->type == "$_NMUX_") return export_gate(cell, "(not (ite S B A))");
 		if (cell->type == "$_AOI3_") return export_gate(cell, "(not (or (and A B) C))");
 		if (cell->type == "$_OAI3_") return export_gate(cell, "(not (and (or A B) C))");
 		if (cell->type == "$_AOI4_") return export_gate(cell, "(not (or (and A B) (and C D)))");
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index d75456c1b..e9586fae0 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -537,6 +537,13 @@ struct SmvWorker
 				continue;
 			}
 
+			if (cell->type == "$_NMUX_")
+			{
+				definitions.push_back(stringf("%s := !(bool(%s) ? %s : %s);", lvalue(cell->getPort("\\Y")),
+						rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A"))));
+				continue;
+			}
+
 			if (cell->type == "$_AOI3_")
 			{
 				definitions.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")),
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index e0b3a6f80..776f4eacb 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -558,6 +558,20 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
+	if (cell->type == "$_NMUX_") {
+		f << stringf("%s" "assign ", indent.c_str());
+		dump_sigspec(f, cell->getPort("\\Y"));
+		f << stringf(" = !(");
+		dump_cell_expr_port(f, cell, "S", false);
+		f << stringf(" ? ");
+		dump_attributes(f, "", cell->attributes, ' ');
+		dump_cell_expr_port(f, cell, "B", false);
+		f << stringf(" : ");
+		dump_cell_expr_port(f, cell, "A", false);
+		f << stringf(");\n");
+		return true;
+	}
+
 	if (cell->type.in("$_AOI3_", "$_OAI3_")) {
 		f << stringf("%s" "assign ", indent.c_str());
 		dump_sigspec(f, cell->getPort("\\Y"));