Merge remote-tracking branch 'origin/master' into xaig

CHANGELOG

@@ -24,6 +24,7 @@ Yosys 0.8 .. Yosys 0.8-dev
     - Added "synth -abc9" (experimental)
     - Extended "muxcover -mux{4,8,16}=<cost>"
     - "synth_xilinx" to now infer hard shift registers (-nosrl to disable)
+    - Fixed sign extension of unsized constants with 'bx and 'bz MSB
 
 
 Yosys 0.7 .. Yosys 0.8

backends/json/json.cc

@@ -189,6 +189,10 @@ struct JsonWriter
 			f << stringf("        %s: {\n", get_name(w->name).c_str());
 			f << stringf("          \"hide_name\": %s,\n", w->name[0] == '$' ? "1" : "0");
 			f << stringf("          \"bits\": %s,\n", get_bits(w).c_str());
+			if (w->start_offset)
+				f << stringf("          \"offset\": %d,\n", w->start_offset);
+			if (w->upto)
+				f << stringf("          \"upto\": 1,\n");
 			f << stringf("          \"attributes\": {");
 			write_parameters(w->attributes);
 			f << stringf("\n          }\n");

frontends/json/jsonparse.cc

@@ -372,6 +372,18 @@ void json_import(Design *design, string &modname, JsonNode *node)
 			if (wire == nullptr)
 				wire = module->addWire(net_name, GetSize(bits_node->data_array));
 
+			if (net_node->data_dict.count("upto") != 0) {
+				JsonNode *val = net_node->data_dict.at("upto");
+				if (val->type == 'N')
+					wire->upto = val->data_number != 0;
+			}
+
+			if (net_node->data_dict.count("offset") != 0) {
+				JsonNode *val = net_node->data_dict.at("offset");
+				if (val->type == 'N')
+					wire->start_offset = val->data_number;
+			}
+
 			for (int i = 0; i < GetSize(bits_node->data_array); i++)
 			{
 				JsonNode *bitval_node = bits_node->data_array.at(i);

frontends/verilog/const2ast.cc

@@ -204,7 +204,7 @@ AstNode *VERILOG_FRONTEND::const2ast(std::string code, char case_type, bool warn
 	{
 		std::vector<RTLIL::State> data;
 		bool is_signed = false;
-		bool is_unsized = false;
+		bool is_unsized = len_in_bits < 0;
 		if (*(endptr+1) == 's') {
 			is_signed = true;
 			endptr++;
@@ -213,25 +213,25 @@ AstNode *VERILOG_FRONTEND::const2ast(std::string code, char case_type, bool warn
 		{
 		case 'b':
 		case 'B':
-			my_strtobin(data, endptr+2, len_in_bits, 2, case_type, false);
+			my_strtobin(data, endptr+2, len_in_bits, 2, case_type, is_unsized);
 			break;
 		case 'o':
 		case 'O':
-			my_strtobin(data, endptr+2, len_in_bits, 8, case_type, false);
+			my_strtobin(data, endptr+2, len_in_bits, 8, case_type, is_unsized);
 			break;
 		case 'd':
 		case 'D':
-			my_strtobin(data, endptr+2, len_in_bits, 10, case_type, false);
+			my_strtobin(data, endptr+2, len_in_bits, 10, case_type, is_unsized);
 			break;
 		case 'h':
 		case 'H':
-			my_strtobin(data, endptr+2, len_in_bits, 16, case_type, false);
+			my_strtobin(data, endptr+2, len_in_bits, 16, case_type, is_unsized);
 			break;
 		default:
 			char next_char = char(tolower(*(endptr+1)));
 			if (next_char == '0' || next_char == '1' || next_char == 'x' || next_char == 'z') {
-				my_strtobin(data, endptr+1, 1, 2, case_type, true);
 				is_unsized = true;
+				my_strtobin(data, endptr+1, 1, 2, case_type, is_unsized);
 			} else {
 				return NULL;
 			}

frontends/verilog/verilog_parser.y

@@ -517,6 +517,7 @@ wire_type_token:
 	TOK_GENVAR {
 		astbuf3->type = AST_GENVAR;
 		astbuf3->is_reg = true;
+		astbuf3->is_signed = true;
 		astbuf3->range_left = 31;
 		astbuf3->range_right = 0;
 	} |

kernel/register.cc

@@ -545,6 +545,7 @@ void Backend::extra_args(std::ostream *&f, std::string &filename, std::vector<st
 		}
 
 		filename = arg;
+		rewrite_filename(filename);
 		std::ofstream *ff = new std::ofstream;
 		ff->open(filename.c_str(), std::ofstream::trunc);
 		yosys_output_files.insert(filename);

passes/sat/sat.cc

@@ -659,6 +659,7 @@ struct SatHelper
 
 	void dump_model_to_vcd(std::string vcd_file_name)
 	{
+		rewrite_filename(vcd_file_name);
 		FILE *f = fopen(vcd_file_name.c_str(), "w");
 		if (!f)
 			log_cmd_error("Can't open output file `%s' for writing: %s\n", vcd_file_name.c_str(), strerror(errno));
@@ -761,6 +762,7 @@ struct SatHelper
 
 	void dump_model_to_json(std::string json_file_name)
 	{
+		rewrite_filename(json_file_name);
 		FILE *f = fopen(json_file_name.c_str(), "w");
 		if (!f)
 			log_cmd_error("Can't open output file `%s' for writing: %s\n", json_file_name.c_str(), strerror(errno));
@@ -1505,6 +1507,7 @@ struct SatPass : public Pass {
 					{
 						if (!cnf_file_name.empty())
 						{
+							rewrite_filename(cnf_file_name);
 							FILE *f = fopen(cnf_file_name.c_str(), "w");
 							if (!f)
 								log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
@@ -1608,6 +1611,7 @@ struct SatPass : public Pass {
 
 			if (!cnf_file_name.empty())
 			{
+				rewrite_filename(cnf_file_name);
 				FILE *f = fopen(cnf_file_name.c_str(), "w");
 				if (!f)
 					log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));

passes/techmap/muxcover.cc

@@ -23,6 +23,7 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+#define COST_DMUX   90
 #define COST_MUX2  100
 #define COST_MUX4  220
 #define COST_MUX8  460
@@ -57,7 +58,9 @@ struct MuxcoverWorker
 	bool use_mux8;
 	bool use_mux16;
 	bool nodecode;
+	bool nopartial;
 
+	int cost_dmux;
 	int cost_mux2;
 	int cost_mux4;
 	int cost_mux8;
@@ -69,6 +72,8 @@ struct MuxcoverWorker
 		use_mux8 = false;
 		use_mux16 = false;
 		nodecode = false;
+		nopartial = false;
+		cost_dmux = COST_DMUX;
 		cost_mux2 = COST_MUX2;
 		cost_mux4 = COST_MUX4;
 		cost_mux8 = COST_MUX8;
@@ -133,13 +138,20 @@ struct MuxcoverWorker
 		log("    Finished treeification: Found %d trees.\n", GetSize(tree_list));
 	}
 
-	bool follow_muxtree(SigBit &ret_bit, tree_t &tree, SigBit bit, const char *path)
+	bool follow_muxtree(SigBit &ret_bit, tree_t &tree, SigBit bit, const char *path, bool first_layer = true)
 	{
 		if (*path) {
-			if (tree.muxes.count(bit) == 0)
+			if (tree.muxes.count(bit) == 0) {
-				return false;
+				if (first_layer || nopartial)
+					return false;
+				if (path[0] == 'S')
+					ret_bit = State::Sx;
+				else
+					ret_bit = bit;
+				return true;
+			}
 			char port_name[3] = {'\\', *path, 0};
-			return follow_muxtree(ret_bit, tree, sigmap(tree.muxes.at(bit)->getPort(port_name)), path+1);
+			return follow_muxtree(ret_bit, tree, sigmap(tree.muxes.at(bit)->getPort(port_name)), path+1, false);
 		} else {
 			ret_bit = bit;
 			return true;
@@ -148,7 +160,7 @@ struct MuxcoverWorker
 
 	int prepare_decode_mux(SigBit &A, SigBit B, SigBit sel, SigBit bit)
 	{
-		if (A == B)
+		if (A == B || sel == State::Sx)
 			return 0;
 
 		tuple<SigBit, SigBit, SigBit> key(A, B, sel);
@@ -166,7 +178,10 @@ struct MuxcoverWorker
 		if (std::get<2>(entry))
 			return 0;
 
-		return cost_mux2 / GetSize(std::get<1>(entry));
+		if (A == State::Sx || B == State::Sx)
+			return 0;
+
+		return cost_dmux / GetSize(std::get<1>(entry));
 	}
 
 	void implement_decode_mux(SigBit ctrl_bit)
@@ -183,9 +198,32 @@ struct MuxcoverWorker
 		implement_decode_mux(std::get<0>(key));
 		implement_decode_mux(std::get<1>(key));
 
-		module->addMuxGate(NEW_ID, std::get<0>(key), std::get<1>(key), std::get<2>(key), ctrl_bit);
+		if (std::get<0>(key) == State::Sx) {
+			module->addBufGate(NEW_ID, std::get<1>(key), ctrl_bit);
+		} else if (std::get<1>(key) == State::Sx) {
+			module->addBufGate(NEW_ID, std::get<0>(key), ctrl_bit);
+		} else {
+			module->addMuxGate(NEW_ID, std::get<0>(key), std::get<1>(key), std::get<2>(key), ctrl_bit);
+			decode_mux_counter++;
+		}
 		std::get<2>(entry) = true;
-		decode_mux_counter++;
+	}
+
+	void find_best_covers(tree_t &tree, const vector<SigBit> &bits)
+	{
+		for (auto bit : bits)
+			find_best_cover(tree, bit);
+	}
+
+	int sum_best_covers(tree_t &tree, const vector<SigBit> &bits)
+	{
+		int sum = 0;
+		for (auto bit : pool<SigBit>(bits.begin(), bits.end())) {
+			int cost = tree.newmuxes.at(bit).cost;
+			log_debug("        Best cost for %s: %d\n", log_signal(bit), cost);
+			sum += cost;
+		}
+		return sum;
 	}
 
 	int find_best_cover(tree_t &tree, SigBit bit)
@@ -218,9 +256,13 @@ struct MuxcoverWorker
 			mux.inputs.push_back(B);
 			mux.selects.push_back(S1);
 
+			find_best_covers(tree, mux.inputs);
+			log_debug("        Decode cost for mux2 at %s: %d\n", log_signal(bit), mux.cost);
+
 			mux.cost += cost_mux2;
-			mux.cost += find_best_cover(tree, A);
+			mux.cost += sum_best_covers(tree, mux.inputs);
-			mux.cost += find_best_cover(tree, B);
+
+			log_debug("      Cost of mux2 at %s: %d\n", log_signal(bit), mux.cost);
 
 			best_mux = mux;
 		}
@@ -256,13 +298,15 @@ struct MuxcoverWorker
 				mux.selects.push_back(S1);
 				mux.selects.push_back(T1);
 
-				mux.cost += cost_mux4;
+				find_best_covers(tree, mux.inputs);
-				mux.cost += find_best_cover(tree, A);
+				log_debug("        Decode cost for mux4 at %s: %d\n", log_signal(bit), mux.cost);
-				mux.cost += find_best_cover(tree, B);
-				mux.cost += find_best_cover(tree, C);
-				mux.cost += find_best_cover(tree, D);
 
-				if (best_mux.cost > mux.cost)
+				mux.cost += cost_mux4;
+				mux.cost += sum_best_covers(tree, mux.inputs);
+
+				log_debug("      Cost of mux4 at %s: %d\n", log_signal(bit), mux.cost);
+
+				if (best_mux.cost >= mux.cost)
 					best_mux = mux;
 			}
 		}
@@ -319,17 +363,15 @@ struct MuxcoverWorker
 				mux.selects.push_back(T1);
 				mux.selects.push_back(U1);
 
-				mux.cost += cost_mux8;
+				find_best_covers(tree, mux.inputs);
-				mux.cost += find_best_cover(tree, A);
+				log_debug("        Decode cost for mux8 at %s: %d\n", log_signal(bit), mux.cost);
-				mux.cost += find_best_cover(tree, B);
-				mux.cost += find_best_cover(tree, C);
-				mux.cost += find_best_cover(tree, D);
-				mux.cost += find_best_cover(tree, E);
-				mux.cost += find_best_cover(tree, F);
-				mux.cost += find_best_cover(tree, G);
-				mux.cost += find_best_cover(tree, H);
 
-				if (best_mux.cost > mux.cost)
+				mux.cost += cost_mux8;
+				mux.cost += sum_best_covers(tree, mux.inputs);
+
+				log_debug("      Cost of mux8 at %s: %d\n", log_signal(bit), mux.cost);
+
+				if (best_mux.cost >= mux.cost)
 					best_mux = mux;
 			}
 		}
@@ -423,25 +465,15 @@ struct MuxcoverWorker
 				mux.selects.push_back(U1);
 				mux.selects.push_back(V1);
 
-				mux.cost += cost_mux16;
+				find_best_covers(tree, mux.inputs);
-				mux.cost += find_best_cover(tree, A);
+				log_debug("        Decode cost for mux16 at %s: %d\n", log_signal(bit), mux.cost);
-				mux.cost += find_best_cover(tree, B);
-				mux.cost += find_best_cover(tree, C);
-				mux.cost += find_best_cover(tree, D);
-				mux.cost += find_best_cover(tree, E);
-				mux.cost += find_best_cover(tree, F);
-				mux.cost += find_best_cover(tree, G);
-				mux.cost += find_best_cover(tree, H);
-				mux.cost += find_best_cover(tree, I);
-				mux.cost += find_best_cover(tree, J);
-				mux.cost += find_best_cover(tree, K);
-				mux.cost += find_best_cover(tree, L);
-				mux.cost += find_best_cover(tree, M);
-				mux.cost += find_best_cover(tree, N);
-				mux.cost += find_best_cover(tree, O);
-				mux.cost += find_best_cover(tree, P);
 
-				if (best_mux.cost > mux.cost)
+				mux.cost += cost_mux16;
+				mux.cost += sum_best_covers(tree, mux.inputs);
+
+				log_debug("      Cost of mux16 at %s: %d\n", log_signal(bit), mux.cost);
+
+				if (best_mux.cost >= mux.cost)
 					best_mux = mux;
 			}
 		}
@@ -537,6 +569,7 @@ struct MuxcoverWorker
 	void treecover(tree_t &tree)
 	{
 		int count_muxes_by_type[4] = {0, 0, 0, 0};
+		log_debug("    Searching for best cover for tree at %s.\n", log_signal(tree.root));
 		find_best_cover(tree, tree.root);
 		implement_best_cover(tree, tree.root, count_muxes_by_type);
 		log("    Replaced tree at %s: %d MUX2, %d MUX4, %d MUX8, %d MUX16\n", log_signal(tree.root),
@@ -553,12 +586,13 @@ struct MuxcoverWorker
 
 		log("  Covering trees:\n");
 
-		// pre-fill cache of decoder muxes
+		if (!nodecode) {
-		if (!nodecode)
+			log_debug("    Populating cache of decoder muxes.\n");
 			for (auto &tree : tree_list) {
 				find_best_cover(tree, tree.root);
 				tree.newmuxes.clear();
 			}
+		}
 
 		for (auto &tree : tree_list)
 			treecover(tree);
@@ -584,11 +618,19 @@ struct MuxcoverPass : public Pass {
 		log("        Default costs: $_MUX_ = %d, $_MUX4_ = %d,\n", COST_MUX2, COST_MUX4);
 		log("                       $_MUX8_ = %d, $_MUX16_ = %d\n", COST_MUX8, COST_MUX16);
 		log("\n");
+		log("    -dmux=cost\n");
+		log("        Use the specified cost for $_MUX_ cells used in decoders.\n");
+		log("        Default cost: %d\n", COST_DMUX);
+		log("\n");
 		log("    -nodecode\n");
 		log("        Do not insert decoder logic. This reduces the number of possible\n");
 		log("        substitutions, but guarantees that the resulting circuit is not\n");
 		log("        less efficient than the original circuit.\n");
 		log("\n");
+		log("    -nopartial\n");
+		log("        Do not consider mappings that use $_MUX<N>_ to select from less\n");
+		log("        than <N> different signals.\n");
+		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
@@ -598,6 +640,8 @@ struct MuxcoverPass : public Pass {
 		bool use_mux8 = false;
 		bool use_mux16 = false;
 		bool nodecode = false;
+		bool nopartial = false;
+		int cost_dmux = COST_DMUX;
 		int cost_mux4 = COST_MUX4;
 		int cost_mux8 = COST_MUX8;
 		int cost_mux16 = COST_MUX16;
@@ -630,10 +674,18 @@ struct MuxcoverPass : public Pass {
 				}
 				continue;
 			}
+			if (arg.size() >= 6 && arg.substr(0,6) == "-dmux=") {
+				cost_dmux = atoi(arg.substr(6).c_str());
+				continue;
+			}
 			if (arg == "-nodecode") {
 				nodecode = true;
 				continue;
 			}
+			if (arg == "-nopartial") {
+				nopartial = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -650,10 +702,12 @@ struct MuxcoverPass : public Pass {
 			worker.use_mux4 = use_mux4;
 			worker.use_mux8 = use_mux8;
 			worker.use_mux16 = use_mux16;
+			worker.cost_dmux = cost_dmux;
 			worker.cost_mux4 = cost_mux4;
 			worker.cost_mux8 = cost_mux8;
 			worker.cost_mux16 = cost_mux16;
 			worker.nodecode = nodecode;
+			worker.nopartial = nopartial;
 			worker.run();
 		}
 	}

passes/techmap/shregmap.cc

@@ -293,10 +293,22 @@ struct ShregmapWorker
 
 				if (opts.init || sigbit_init.count(q_bit) == 0)
 				{
-					if (sigbit_chain_next.count(d_bit)) {
+					auto r = sigbit_chain_next.insert(std::make_pair(d_bit, cell));
+					if (!r.second) {
+						// Insertion not successful means that d_bit is already
+						// connected to another register, thus mark it as a
+						// non chain user ...
 						sigbit_with_non_chain_users.insert(d_bit);
-					} else
+						// ... and clone d_bit into another wire, and use that
-						sigbit_chain_next[d_bit] = cell;
+						// wire as a different key in the d_bit-to-cell dictionary
+						// so that it can be identified as another chain
+						// (omitting this common flop)
+						// Link: https://github.com/YosysHQ/yosys/pull/1085
+						Wire *wire = module->addWire(NEW_ID);
+						module->connect(wire, d_bit);
+						sigmap.add(wire, d_bit);
+						sigbit_chain_next.insert(std::make_pair(wire, cell));
+					}
 
 					sigbit_chain_prev[q_bit] = cell;
 					continue;

techlibs/ecp5/arith_map.v

@@ -50,20 +50,21 @@ module _80_ecp5_alu (A, B, CI, BI, X, Y, CO);
 
 	wire [Y_WIDTH2-1:0] AA = A_buf;
 	wire [Y_WIDTH2-1:0] BB = BI ? ~B_buf : B_buf;
+	wire [Y_WIDTH2-1:0] BX = B_buf;
 	wire [Y_WIDTH2-1:0] C = {CO, CI};
 	wire [Y_WIDTH2-1:0] FCO, Y1;
 
 	genvar i;
 	generate for (i = 0; i < Y_WIDTH2; i = i + 2) begin:slice
 		CCU2C #(
-			.INIT0(16'b0110011010101010),
+			.INIT0(16'b1001011010101010),
-			.INIT1(16'b0110011010101010),
+			.INIT1(16'b1001011010101010),
 			.INJECT1_0("NO"),
 			.INJECT1_1("NO")
 	   ) ccu2c_i (
 			.CIN(C[i]),
-			.A0(AA[i]), .B0(BB[i]), .C0(1'b0), .D0(1'b1),
+			.A0(AA[i]), .B0(BX[i]), .C0(BI), .D0(1'b1),
-			.A1(AA[i+1]), .B1(BB[i+1]), .C1(1'b0), .D1(1'b1),
+			.A1(AA[i+1]), .B1(BX[i+1]), .C1(BI), .D1(1'b1),
 			.S0(Y[i]), .S1(Y1[i]),
 			.COUT(FCO[i])
 		);

tests/simple/generate.v

@@ -148,3 +148,14 @@ generate
 endgenerate
 assign out = steps[WIDTH].outer[0].val;
 endmodule
+
+// ------------------------------------------
+
+module gen_test6(output [3:0] o);
+generate
+    genvar i;
+    for (i = 3; i >= 0; i = i-1) begin
+        assign o[i] = 1'b0;
+    end
+endgenerate
+endmodule

tests/various/muxcover.ys

@@ -13,7 +13,7 @@ read_verilog -formal <<EOT
 EOT
 
 
-## Examle usage for "pmuxtree" and "muxcover"
+## Example usage for "pmuxtree" and "muxcover"
 
 proc
 pmuxtree
@@ -49,3 +49,142 @@ hierarchy -top equiv
 equiv_simple -undef
 equiv_status -assert
 
+## Partial matching MUX4
+
+design -reset
+read_verilog -formal <<EOT
+module mux_if_bal_3_1 #(parameter N=3, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {{W{{1'bx}}}};
+    if (s[0] == 1'b0)
+     if (s[1] == 1'b0)
+      o <= i[0*W+:W];
+     else
+      o <= i[1*W+:W];
+    else
+     if (s[1] == 1'b0)
+      o <= i[2*W+:W];
+end
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux4=150
+select -assert-count 0 t:$_MUX_
+select -assert-count 1 t:$_MUX4_
+select -assert-count 0 t:$_MUX8_
+select -assert-count 0 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX4_
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+## Partial matching MUX8
+
+design -reset
+read_verilog -formal <<EOT
+module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {{W{{1'bx}}}};
+    if (s[0] == 1'b0)
+     if (s[1] == 1'b0)
+      if (s[2] == 1'b0)
+       o <= i[0*W+:W];
+      else
+       o <= i[1*W+:W];
+     else
+      if (s[2] == 1'b0)
+       o <= i[2*W+:W];
+      else
+       o <= i[3*W+:W];
+    else
+     if (s[1] == 1'b0)
+      if (s[2] == 1'b0)
+       o <= i[4*W+:W];
+end
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux4=150 -mux8=200
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 1 t:$_MUX8_
+select -assert-count 0 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX8_
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+## Partial matching MUX16
+
+design -reset
+read_verilog -formal <<EOT
+module mux_if_bal_9_1 #(parameter N=9, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {{W{{1'bx}}}};
+    if (s[0] == 1'b0)
+     if (s[1] == 1'b0)
+      if (s[2] == 1'b0)
+       if (s[3] == 1'b0)
+        o <= i[0*W+:W];
+       else
+        o <= i[1*W+:W];
+      else
+       if (s[3] == 1'b0)
+        o <= i[2*W+:W];
+       else
+        o <= i[3*W+:W];
+     else
+      if (s[2] == 1'b0)
+       if (s[3] == 1'b0)
+        o <= i[4*W+:W];
+       else
+        o <= i[5*W+:W];
+      else
+       if (s[3] == 1'b0)
+        o <= i[6*W+:W];
+       else
+        o <= i[7*W+:W];
+    else
+     if (s[1] == 1'b0)
+      if (s[2] == 1'b0)
+       if (s[3] == 1'b0)
+        o <= i[8*W+:W];
+end
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux4=150 -mux8=200 -mux16=250
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 0 t:$_MUX8_
+select -assert-count 1 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX16_
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+

tests/various/shregmap.v

@@ -0,0 +1,48 @@
+module shregmap_static_test(input i, clk, output [1:0] q);
+reg head = 1'b0;
+reg [3:0] shift1 = 4'b0000;
+reg [3:0] shift2 = 4'b0000;
+
+always @(posedge clk) begin
+    head <= i;
+    shift1 <= {shift1[2:0], head};
+    shift2 <= {shift2[2:0], head};
+end
+
+assign q = {shift2[3], shift1[3]};
+endmodule
+
+module $__SHREG_DFF_P_(input C, D, output Q);
+parameter DEPTH = 1;
+parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
+reg [DEPTH-1:0] r = INIT;
+always @(posedge C) 
+    r <= { r[DEPTH-2:0], D };
+assign Q = r[DEPTH-1];
+endmodule
+
+module shregmap_variable_test(input i, clk, input [1:0] l1, l2, output [1:0] q);
+reg head = 1'b0;
+reg [3:0] shift1 = 4'b0000;
+reg [3:0] shift2 = 4'b0000;
+
+always @(posedge clk) begin
+    head <= i;
+    shift1 <= {shift1[2:0], head};
+    shift2 <= {shift2[2:0], head};
+end
+
+assign q = {shift2[l2], shift1[l1]};
+endmodule
+
+module $__XILINX_SHREG_(input C, D, input [1:0] L, output Q);
+parameter CLKPOL = 1;
+parameter ENPOL = 1;
+parameter DEPTH = 1;
+parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
+reg [DEPTH-1:0] r = INIT;
+wire clk = C ^ CLKPOL;
+always @(posedge C)
+    r <= { r[DEPTH-2:0], D };
+assign Q = r[L];
+endmodule

tests/various/shregmap.ys

@@ -0,0 +1,66 @@
+read_verilog shregmap.v
+design -save read
+
+design -copy-to model $__SHREG_DFF_P_
+hierarchy -top shregmap_static_test
+prep
+design -save gold
+
+techmap
+shregmap -init
+
+opt
+
+stat
+# show -width
+select -assert-count 1 t:$_DFF_P_
+select -assert-count 2 t:$__SHREG_DFF_P_
+
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+design -copy-from model -as $__SHREG_DFF_P_ \$__SHREG_DFF_P_
+prep
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -seq 5 miter
+
+design -load gold
+stat
+
+design -load gate
+stat
+
+##########
+
+design -load read
+design -copy-to model $__XILINX_SHREG_
+hierarchy -top shregmap_variable_test
+prep
+design -save gold
+
+simplemap t:$dff t:$dffe
+shregmap -tech xilinx
+
+stat
+# show -width
+write_verilog -noexpr -norename
+select -assert-count 1 t:$_DFF_P_
+select -assert-count 2 t:$__XILINX_SHREG_
+
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_
+prep
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -seq 5 miter
+
+design -load gold
+stat
+
+design -load gate
+stat

tests/various/signext.ys

@@ -0,0 +1,33 @@
+
+read_verilog -formal <<EOT
+module gate(input clk, output [32:0] o, p, q, r, s, t, u);
+assign o = 'bx;
+assign p = 1'bx;
+assign q = 'bz;
+assign r = 1'bz;
+assign s = 1'b0;
+assign t = 'b1;
+assign u = -'sb1;
+endmodule
+EOT
+
+proc
+
+## Equivalence checking
+
+read_verilog -formal <<EOT
+module gold(input clk, output [32:0] o, p, q, r, s, t, u);
+assign o = {33{1'bx}};
+assign p = {{32{1'b0}}, 1'bx};
+assign q = {33{1'bz}};
+assign r = {{32{1'b0}}, 1'bz};
+assign s = {33{1'b0}};
+assign t = {{32{1'b0}}, 1'b1};
+assign u = {33{1'b1}};
+endmodule
+EOT
+
+proc
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -enable_undef miter