diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/aiger/xaiger.cc | 14 | ||||
| -rw-r--r-- | backends/blif/blif.cc | 7 | ||||
| -rw-r--r-- | backends/btor/btor.cc | 8 | ||||
| -rw-r--r-- | backends/firrtl/firrtl.cc | 296 | ||||
| -rw-r--r-- | backends/json/json.cc | 50 | ||||
| -rw-r--r-- | backends/simplec/simplec.cc | 6 | ||||
| -rw-r--r-- | backends/smt2/smt2.cc | 1 | ||||
| -rw-r--r-- | backends/smv/smv.cc | 7 | ||||
| -rw-r--r-- | backends/verilog/verilog_backend.cc | 14 | 
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> ¶meters, bool for_module=false)  	{  		bool first = true;  		for (auto ¶m : 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"));  | 
