Merge branch 'master' of https://github.com/cliffordwolf/yosys into btor

added case for memwr cell that is used in muxes (same cell is used more than one time)
corrected bug for xnor and logic_not
added pmux cell translation

Conflicts:
	backends/btor/btor.cc

6 files changed, 597 insertions, 409 deletions

diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc
index 5c38cc2cf..f07ad943c 100644
--- a/passes/sat/eval.cc
+++ b/passes/sat/eval.cc
@@ -44,7 +44,7 @@ struct BruteForceEquivChecker
 
 	void run_checker(RTLIL::SigSpec &inputs)
 	{
-		if (inputs.width < mod1_inputs.width) {
+		if (inputs.size() < mod1_inputs.size()) {
 			RTLIL::SigSpec inputs0 = inputs, inputs1 = inputs;
 			inputs0.append(RTLIL::Const(0, 1));
 			inputs1.append(RTLIL::Const(1, 1));
@@ -53,8 +53,6 @@ struct BruteForceEquivChecker
 			return;
 		}
 
-		inputs.optimize();
-
 		ConstEval ce1(mod1), ce2(mod2);
 		ce1.set(mod1_inputs, inputs.as_const());
 		ce2.set(mod2_inputs, inputs.as_const());
@@ -70,11 +68,9 @@ struct BruteForceEquivChecker
 					log_signal(undef2), log_signal(mod1_inputs), log_signal(inputs));
 
 		if (ignore_x_mod1) {
-			sig1.expand(), sig2.expand();
-			for (size_t i = 0; i < sig1.chunks.size(); i++)
-				if (sig1.chunks.at(i) == RTLIL::SigChunk(RTLIL::State::Sx))
-					sig2.chunks.at(i) = RTLIL::SigChunk(RTLIL::State::Sx);
-			sig1.optimize(), sig2.optimize();
+			for (int i = 0; i < SIZE(sig1); i++)
+				if (sig1[i] == RTLIL::State::Sx)
+					sig2[i] = RTLIL::State::Sx;
 		}
 
 		if (sig1 != sig2) {
@@ -91,16 +87,16 @@ struct BruteForceEquivChecker
 			mod1(mod1), mod2(mod2), counter(0), errors(0), ignore_x_mod1(ignore_x_mod1)
 	{
 		log("Checking for equivialence (brute-force): %s vs %s\n", mod1->name.c_str(), mod2->name.c_str());
-		for (auto &w : mod1->wires)
+		for (auto &w : mod1->wires_)
 		{
 			RTLIL::Wire *wire1 = w.second;
 			if (wire1->port_id == 0)
 				continue;
 
-			if (mod2->wires.count(wire1->name) == 0)
+			if (mod2->wires_.count(wire1->name) == 0)
 				log_cmd_error("Port %s in module 1 has no counterpart in module 2!\n", wire1->name.c_str());
 
-			RTLIL::Wire *wire2 = mod2->wires.at(wire1->name);
+			RTLIL::Wire *wire2 = mod2->wires_.at(wire1->name);
 			if (wire1->width != wire2->width || wire1->port_input != wire2->port_input || wire1->port_output != wire2->port_output)
 				log_cmd_error("Port %s in module 1 does not match its counterpart in module 2!\n", wire1->name.c_str());
 
@@ -151,17 +147,17 @@ struct VlogHammerReporter
 		SatGen satgen(&ez, &sigmap);
 		satgen.model_undef = model_undef;
 
-		for (auto &c : module->cells)
+		for (auto &c : module->cells_)
 			if (!satgen.importCell(c.second))
 				log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
 
 		ez.assume(satgen.signals_eq(recorded_set_vars, recorded_set_vals));
 
-		std::vector<int> y_vec = satgen.importDefSigSpec(module->wires.at("\\y"));
+		std::vector<int> y_vec = satgen.importDefSigSpec(module->wires_.at("\\y"));
 		std::vector<bool> y_values;
 
 		if (model_undef) {
-			std::vector<int> y_undef_vec = satgen.importUndefSigSpec(module->wires.at("\\y"));
+			std::vector<int> y_undef_vec = satgen.importUndefSigSpec(module->wires_.at("\\y"));
 			y_vec.insert(y_vec.end(), y_undef_vec.begin(), y_undef_vec.end());
 		}
 
@@ -171,12 +167,11 @@ struct VlogHammerReporter
 		if (!ez.solve(y_vec, y_values))
 			log_error("Failed to find solution to SAT problem.\n");
 
-		expected_y.expand();
-		for (int i = 0; i < expected_y.width; i++) {
+		for (int i = 0; i < expected_y.size(); i++) {
 			RTLIL::State solution_bit = y_values.at(i) ? RTLIL::State::S1 : RTLIL::State::S0;
-			RTLIL::State expected_bit = expected_y.chunks.at(i).data.bits.at(0);
+			RTLIL::State expected_bit = expected_y[i].data;
 			if (model_undef) {
-				if (y_values.at(expected_y.width+i))
+				if (y_values.at(expected_y.size()+i))
 					solution_bit = RTLIL::State::Sx;
 			} else {
 				if (expected_bit == RTLIL::State::Sx)
@@ -184,17 +179,16 @@ struct VlogHammerReporter
 			}
 			if (solution_bit != expected_bit) {
 				std::string sat_bits, rtl_bits;
-				for (int k = expected_y.width-1; k >= 0; k--) {
-					if (model_undef && y_values.at(expected_y.width+k))
+				for (int k = expected_y.size()-1; k >= 0; k--) {
+					if (model_undef && y_values.at(expected_y.size()+k))
 						sat_bits += "x";
 					else
 						sat_bits += y_values.at(k) ? "1" : "0";
-					rtl_bits += expected_y.chunks.at(k).data.bits.at(0) == RTLIL::State::Sx ? "x" :
-							expected_y.chunks.at(k).data.bits.at(0) == RTLIL::State::S1 ? "1" : "0";
+					rtl_bits += expected_y[k] == RTLIL::State::Sx ? "x" : expected_y[k] == RTLIL::State::S1 ? "1" : "0";
 				}
 				log_error("Found error in SAT model: y[%d] = %s, should be %s:\n   SAT: %s\n   RTL: %s\n        %*s^\n",
 						int(i), log_signal(solution_bit), log_signal(expected_bit),
-						sat_bits.c_str(), rtl_bits.c_str(), expected_y.width-i-1, "");
+						sat_bits.c_str(), rtl_bits.c_str(), expected_y.size()-i-1, "");
 			}
 		}
 
@@ -203,16 +197,16 @@ struct VlogHammerReporter
 			std::vector<int> cmp_vars;
 			std::vector<bool> cmp_vals;
 
-			std::vector<bool> y_undef(y_values.begin() + expected_y.width, y_values.end());
+			std::vector<bool> y_undef(y_values.begin() + expected_y.size(), y_values.end());
 
-			for (int i = 0; i < expected_y.width; i++)
+			for (int i = 0; i < expected_y.size(); i++)
 				if (y_undef.at(i))
 				{
 					log("    Toggling undef bit %d to test undef gating.\n", i);
 					if (!ez.solve(y_vec, y_values, ez.IFF(y_vec.at(i), y_values.at(i) ? ez.FALSE : ez.TRUE)))
 						log_error("Failed to find solution with toggled bit!\n");
 
-					cmp_vars.push_back(y_vec.at(expected_y.width + i));
+					cmp_vars.push_back(y_vec.at(expected_y.size() + i));
 					cmp_vals.push_back(true);
 				}
 				else
@@ -220,7 +214,7 @@ struct VlogHammerReporter
 					cmp_vars.push_back(y_vec.at(i));
 					cmp_vals.push_back(y_values.at(i));
 
-					cmp_vars.push_back(y_vec.at(expected_y.width + i));
+					cmp_vars.push_back(y_vec.at(expected_y.size() + i));
 					cmp_vals.push_back(false);
 				}
 
@@ -258,10 +252,10 @@ struct VlogHammerReporter
 
 				std::vector<RTLIL::State> bits(patterns[idx].bits.begin(), patterns[idx].bits.begin() + total_input_width);
 				for (int i = 0; i < int(inputs.size()); i++) {
-					RTLIL::Wire *wire = module->wires.at(inputs[i]);
+					RTLIL::Wire *wire = module->wires_.at(inputs[i]);
 					for (int j = input_widths[i]-1; j >= 0; j--) {
-						ce.set(RTLIL::SigSpec(wire, 1, j), bits.back());
-						recorded_set_vars.append(RTLIL::SigSpec(wire, 1, j));
+						ce.set(RTLIL::SigSpec(wire, j), bits.back());
+						recorded_set_vars.append(RTLIL::SigSpec(wire, j));
 						recorded_set_vals.bits.push_back(bits.back());
 						bits.pop_back();
 					}
@@ -274,32 +268,30 @@ struct VlogHammerReporter
 					}
 				}
 
-				if (module->wires.count("\\y") == 0)
+				if (module->wires_.count("\\y") == 0)
 					log_error("No output wire (y) found in module %s!\n", RTLIL::id2cstr(module->name));
 
-				RTLIL::SigSpec sig(module->wires.at("\\y"));
+				RTLIL::SigSpec sig(module->wires_.at("\\y"));
 				RTLIL::SigSpec undef;
 
 				while (!ce.eval(sig, undef)) {
 					// log_error("Evaluation of y in module %s failed: sig=%s, undef=%s\n", RTLIL::id2cstr(module->name), log_signal(sig), log_signal(undef));
 					log("Warning: Setting signal %s in module %s to undef.\n", log_signal(undef), RTLIL::id2cstr(module->name));
-					ce.set(undef, RTLIL::Const(RTLIL::State::Sx, undef.width));
+					ce.set(undef, RTLIL::Const(RTLIL::State::Sx, undef.size()));
 				}
 
 				log("++VAL++ %d %s %s #\n", idx, module_name.c_str(), sig.as_const().as_string().c_str());
 
 				if (module_name == "rtl") {
 					rtl_sig = sig;
-					rtl_sig.expand();
 					sat_check(module, recorded_set_vars, recorded_set_vals, sig, false);
 					sat_check(module, recorded_set_vars, recorded_set_vals, sig, true);
-				} else if (rtl_sig.width > 0) {
-					sig.expand();
-					if (rtl_sig.width != sig.width)
+				} else if (rtl_sig.size() > 0) {
+					if (rtl_sig.size() != sig.size())
 						log_error("Output (y) has a different width in module %s compared to rtl!\n", RTLIL::id2cstr(module->name));
-					for (int i = 0; i < sig.width; i++)
-						if (rtl_sig.chunks.at(i).data.bits.at(0) == RTLIL::State::Sx)
-							sig.chunks.at(i).data.bits.at(0) = RTLIL::State::Sx;
+					for (int i = 0; i < SIZE(sig); i++)
+						if (rtl_sig[i] == RTLIL::State::Sx)
+							sig[i] = RTLIL::State::Sx;
 				}
 
 				log("++RPT++ %d%s %s %s\n", idx, input_pattern_list.c_str(), sig.as_const().as_string().c_str(), module_name.c_str());
@@ -314,10 +306,10 @@ struct VlogHammerReporter
 	{
 		for (auto name : split(module_list, ",")) {
 			RTLIL::IdString esc_name = RTLIL::escape_id(module_prefix + name);
-			if (design->modules.count(esc_name) == 0)
+			if (design->modules_.count(esc_name) == 0)
 				log_error("Can't find module %s in current design!\n", name.c_str());
 			log("Using module %s (%s).\n", esc_name.c_str(), name.c_str());
-			modules.push_back(design->modules.at(esc_name));
+			modules.push_back(design->modules_.at(esc_name));
 			module_names.push_back(name);
 		}
 
@@ -326,9 +318,9 @@ struct VlogHammerReporter
 			int width = -1;
 			RTLIL::IdString esc_name = RTLIL::escape_id(name);
 			for (auto mod : modules) {
-				if (mod->wires.count(esc_name) == 0)
+				if (mod->wires_.count(esc_name) == 0)
 					log_error("Can't find input %s in module %s!\n", name.c_str(), RTLIL::id2cstr(mod->name));
-				RTLIL::Wire *port = mod->wires.at(esc_name);
+				RTLIL::Wire *port = mod->wires_.at(esc_name);
 				if (!port->port_input || port->port_output)
 					log_error("Wire %s in module %s is not an input!\n", name.c_str(), RTLIL::id2cstr(mod->name));
 				if (width >= 0 && width != port->width)
@@ -350,7 +342,7 @@ struct VlogHammerReporter
 			}
 			if (!RTLIL::SigSpec::parse(sig, NULL, pattern) || !sig.is_fully_const())
 				log_error("Failed to parse pattern %s!\n", pattern.c_str());
-			if (sig.width < total_input_width)
+			if (sig.size() < total_input_width)
 				log_error("Pattern %s is to short!\n", pattern.c_str());
 			patterns.push_back(sig.as_const());
 			if (invert_pattern) {
@@ -424,11 +416,11 @@ struct EvalPass : public Pass {
 				/* this should only be used for regression testing of ConstEval -- see vloghammer */
 				std::string mod1_name = RTLIL::escape_id(args[++argidx]);
 				std::string mod2_name = RTLIL::escape_id(args[++argidx]);
-				if (design->modules.count(mod1_name) == 0)
+				if (design->modules_.count(mod1_name) == 0)
 					log_error("Can't find module `%s'!\n", mod1_name.c_str());
-				if (design->modules.count(mod2_name) == 0)
+				if (design->modules_.count(mod2_name) == 0)
 					log_error("Can't find module `%s'!\n", mod2_name.c_str());
-				BruteForceEquivChecker checker(design->modules.at(mod1_name), design->modules.at(mod2_name), args[argidx-2] == "-brute_force_equiv_checker_x");
+				BruteForceEquivChecker checker(design->modules_.at(mod1_name), design->modules_.at(mod2_name), args[argidx-2] == "-brute_force_equiv_checker_x");
 				if (checker.errors > 0)
 					log_cmd_error("Modules are not equivialent!\n");
 				log("Verified %s = %s (using brute-force check on %d cases).\n",
@@ -450,7 +442,7 @@ struct EvalPass : public Pass {
 		extra_args(args, argidx, design);
 
 		RTLIL::Module *module = NULL;
-		for (auto &mod_it : design->modules)
+		for (auto &mod_it : design->modules_)
 			if (design->selected(mod_it.second)) {
 				if (module)
 					log_cmd_error("Only one module must be selected for the EVAL pass! (selected: %s and %s)\n",
@@ -470,16 +462,16 @@ struct EvalPass : public Pass {
 				log_cmd_error("Failed to parse rhs set expression `%s'.\n", it.second.c_str());
 			if (!rhs.is_fully_const())
 				log_cmd_error("Right-hand-side set expression `%s' is not constant.\n", it.second.c_str());
-			if (lhs.width != rhs.width)
+			if (lhs.size() != rhs.size())
 				log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
-						it.first.c_str(), log_signal(lhs), lhs.width, it.second.c_str(), log_signal(rhs), rhs.width);
+						it.first.c_str(), log_signal(lhs), lhs.size(), it.second.c_str(), log_signal(rhs), rhs.size());
 			ce.set(lhs, rhs.as_const());
 		}
 
 		if (shows.size() == 0) {
-			for (auto &it : module->wires)
+			for (auto &it : module->wires_)
 				if (it.second->port_output)
-					shows.push_back(it.second->name);
+					shows.push_back(it.second->name.str());
 		}
 
 		if (tables.empty())
@@ -488,12 +480,11 @@ struct EvalPass : public Pass {
 				RTLIL::SigSpec signal, value, undef;
 				if (!RTLIL::SigSpec::parse_sel(signal, design, module, it))
 					log_cmd_error("Failed to parse show expression `%s'.\n", it.c_str());
-				signal.optimize();
 				value = signal;
 				if (set_undef) {
 					while (!ce.eval(value, undef)) {
 						log("Failed to evaluate signal %s: Missing value for %s. -> setting to undef\n", log_signal(signal), log_signal(undef));
-						ce.set(undef, RTLIL::Const(RTLIL::State::Sx, undef.width));
+						ce.set(undef, RTLIL::Const(RTLIL::State::Sx, undef.size()));
 						undef = RTLIL::SigSpec();
 					}
 					log("Eval result: %s = %s.\n", log_signal(signal), log_signal(value));
@@ -526,15 +517,15 @@ struct EvalPass : public Pass {
 			}
 
 			std::vector<std::string> tab_line;
-			for (auto &c : tabsigs.chunks)
+			for (auto &c : tabsigs.chunks())
 				tab_line.push_back(log_signal(c));
 			tab_sep_colidx = tab_line.size();
-			for (auto &c : signal.chunks)
+			for (auto &c : signal.chunks())
 				tab_line.push_back(log_signal(c));
 			tab.push_back(tab_line);
 			tab_line.clear();
 
-			RTLIL::Const tabvals(0, tabsigs.width);
+			RTLIL::Const tabvals(0, tabsigs.size());
 			do
 			{
 				ce.push();
@@ -548,19 +539,19 @@ struct EvalPass : public Pass {
 								log_signal(tabsigs), log_signal(tabvals), log_signal(this_undef));
 						return;
 					}
-					ce.set(this_undef, RTLIL::Const(RTLIL::State::Sx, this_undef.width));
+					ce.set(this_undef, RTLIL::Const(RTLIL::State::Sx, this_undef.size()));
 					undef.append(this_undef);
 					this_undef = RTLIL::SigSpec();
 				}
 
 				int pos = 0;
-				for (auto &c : tabsigs.chunks) {
+				for (auto &c : tabsigs.chunks()) {
 					tab_line.push_back(log_signal(RTLIL::SigSpec(tabvals).extract(pos, c.width)));
 					pos += c.width;
 				}
 
 				pos = 0;
-				for (auto &c : signal.chunks) {
+				for (auto &c : signal.chunks()) {
 					tab_line.push_back(log_signal(value.extract(pos, c.width)));
 					pos += c.width;
 				}
@@ -602,7 +593,7 @@ struct EvalPass : public Pass {
 			}
 
 			log("\n");
-			if (undef.width > 0) {
+			if (undef.size() > 0) {
 				undef.sort_and_unify();
 				log("Assumend undef (x) value for the following singals: %s\n\n", log_signal(undef));
 			}
diff --git a/passes/sat/example.ys b/passes/sat/example.ys
index 11f5b924b..cc72faac0 100644
--- a/passes/sat/example.ys
+++ b/passes/sat/example.ys
@@ -1,13 +1,14 @@
 
 read_verilog example.v
 proc; opt_clean
+echo on
 
 sat -set y 1'b1 example001
 sat -set y 1'b1 example002
 sat -set y_sshl 8'hf0 -set y_sshr 8'hf0 -set sh 4'd3 example003
-sat -set y 1'b1 example004
+sat -set y 1'b1 -ignore_unknown_cells example004
 sat -show rst,counter -set-at 3 y 1'b1 -seq 4 example004
 
-sat -prove y 1'b0 -show rst,counter,y example004
-sat -prove y 1'b0 -show rst,counter,y -set-at 1 rst 1'b1 -seq 1 example004
+sat -prove y 1'b0 -show rst,counter,y -ignore_unknown_cells example004
+sat -prove y 1'b0 -tempinduct -show rst,counter,y -set-at 1 rst 1'b1 -seq 1 example004
 
diff --git a/passes/sat/expose.cc b/passes/sat/expose.cc
index 2ac7b35f6..e856fdf76 100644
--- a/passes/sat/expose.cc
+++ b/passes/sat/expose.cc
@@ -27,7 +27,7 @@ struct dff_map_info_t {
 	RTLIL::SigSpec sig_d, sig_clk, sig_arst;
 	bool clk_polarity, arst_polarity;
 	RTLIL::Const arst_value;
-	std::vector<std::string> cells;
+	std::vector<RTLIL::IdString> cells;
 };
 
 struct dff_map_bit_info_t {
@@ -37,7 +37,7 @@ struct dff_map_bit_info_t {
 	RTLIL::Cell *cell;
 };
 
-static bool consider_wire(RTLIL::Wire *wire, std::map<std::string, dff_map_info_t> &dff_dq_map)
+static bool consider_wire(RTLIL::Wire *wire, std::map<RTLIL::IdString, dff_map_info_t> &dff_dq_map)
 {
 	if (wire->name[0] == '$' || dff_dq_map.count(wire->name))
 		return false;
@@ -46,11 +46,11 @@ static bool consider_wire(RTLIL::Wire *wire, std::map<std::string, dff_map_info_
 	return true;
 }
 
-static bool consider_cell(RTLIL::Design *design, std::set<std::string> &dff_cells, RTLIL::Cell *cell)
+static bool consider_cell(RTLIL::Design *design, std::set<RTLIL::IdString> &dff_cells, RTLIL::Cell *cell)
 {
 	if (cell->name[0] == '$' || dff_cells.count(cell->name))
 		return false;
-	if (cell->type.at(0) == '\\' && !design->modules.count(cell->type))
+	if (cell->type[0] == '\\' && !design->modules_.count(cell->type))
 		return false;
 	return true;
 }
@@ -73,7 +73,7 @@ static bool compare_cells(RTLIL::Cell *cell1, RTLIL::Cell *cell2)
 	return true;
 }
 
-static void find_dff_wires(std::set<std::string> &dff_wires, RTLIL::Module *module)
+static void find_dff_wires(std::set<RTLIL::IdString> &dff_wires, RTLIL::Module *module)
 {
 	CellTypes ct;
 	ct.setup_internals_mem();
@@ -82,23 +82,23 @@ static void find_dff_wires(std::set<std::string> &dff_wires, RTLIL::Module *modu
 	SigMap sigmap(module);
 	SigPool dffsignals;
 
-	for (auto &it : module->cells) {
-		if (ct.cell_known(it.second->type) && it.second->connections.count("\\Q"))
-			dffsignals.add(sigmap(it.second->connections.at("\\Q")));
+	for (auto &it : module->cells_) {
+		if (ct.cell_known(it.second->type) && it.second->hasPort("\\Q"))
+			dffsignals.add(sigmap(it.second->getPort("\\Q")));
 	}
 
-	for (auto &it : module->wires) {
+	for (auto &it : module->wires_) {
 		if (dffsignals.check_any(it.second))
 			dff_wires.insert(it.first);
 	}
 }
 
-static void create_dff_dq_map(std::map<std::string, dff_map_info_t> &map, RTLIL::Design *design, RTLIL::Module *module)
+static void create_dff_dq_map(std::map<RTLIL::IdString, dff_map_info_t> &map, RTLIL::Design *design, RTLIL::Module *module)
 {
 	std::map<RTLIL::SigBit, dff_map_bit_info_t> bit_info;
 	SigMap sigmap(module);
 
-	for (auto &it : module->cells)
+	for (auto &it : module->cells_)
 	{
 		if (!design->selected(module, it.second))
 			continue;
@@ -113,10 +113,10 @@ static void create_dff_dq_map(std::map<std::string, dff_map_info_t> &map, RTLIL:
 		info.cell = it.second;
 
 		if (info.cell->type == "$dff") {
-			info.bit_clk = sigmap(info.cell->connections.at("\\CLK")).to_single_sigbit();
+			info.bit_clk = sigmap(info.cell->getPort("\\CLK")).to_single_sigbit();
 			info.clk_polarity = info.cell->parameters.at("\\CLK_POLARITY").as_bool();
-			std::vector<RTLIL::SigBit> sig_d = sigmap(info.cell->connections.at("\\D")).to_sigbit_vector();
-			std::vector<RTLIL::SigBit> sig_q = sigmap(info.cell->connections.at("\\Q")).to_sigbit_vector();
+			std::vector<RTLIL::SigBit> sig_d = sigmap(info.cell->getPort("\\D")).to_sigbit_vector();
+			std::vector<RTLIL::SigBit> sig_q = sigmap(info.cell->getPort("\\Q")).to_sigbit_vector();
 			for (size_t i = 0; i < sig_d.size(); i++) {
 				info.bit_d = sig_d.at(i);
 				bit_info[sig_q.at(i)] = info;
@@ -125,12 +125,12 @@ static void create_dff_dq_map(std::map<std::string, dff_map_info_t> &map, RTLIL:
 		}
 
 		if (info.cell->type == "$adff") {
-			info.bit_clk = sigmap(info.cell->connections.at("\\CLK")).to_single_sigbit();
-			info.bit_arst = sigmap(info.cell->connections.at("\\ARST")).to_single_sigbit();
+			info.bit_clk = sigmap(info.cell->getPort("\\CLK")).to_single_sigbit();
+			info.bit_arst = sigmap(info.cell->getPort("\\ARST")).to_single_sigbit();
 			info.clk_polarity = info.cell->parameters.at("\\CLK_POLARITY").as_bool();
 			info.arst_polarity = info.cell->parameters.at("\\ARST_POLARITY").as_bool();
-			std::vector<RTLIL::SigBit> sig_d = sigmap(info.cell->connections.at("\\D")).to_sigbit_vector();
-			std::vector<RTLIL::SigBit> sig_q = sigmap(info.cell->connections.at("\\Q")).to_sigbit_vector();
+			std::vector<RTLIL::SigBit> sig_d = sigmap(info.cell->getPort("\\D")).to_sigbit_vector();
+			std::vector<RTLIL::SigBit> sig_q = sigmap(info.cell->getPort("\\Q")).to_sigbit_vector();
 			std::vector<RTLIL::State> arst_value = info.cell->parameters.at("\\ARST_VALUE").bits;
 			for (size_t i = 0; i < sig_d.size(); i++) {
 				info.bit_d = sig_d.at(i);
@@ -141,27 +141,27 @@ static void create_dff_dq_map(std::map<std::string, dff_map_info_t> &map, RTLIL:
 		}
 
 		if (info.cell->type == "$_DFF_N_" || info.cell->type == "$_DFF_P_") {
-			info.bit_clk = sigmap(info.cell->connections.at("\\C")).to_single_sigbit();
+			info.bit_clk = sigmap(info.cell->getPort("\\C")).to_single_sigbit();
 			info.clk_polarity = info.cell->type == "$_DFF_P_";
-			info.bit_d = sigmap(info.cell->connections.at("\\D")).to_single_sigbit();
-			bit_info[sigmap(info.cell->connections.at("\\Q")).to_single_sigbit()] = info;
+			info.bit_d = sigmap(info.cell->getPort("\\D")).to_single_sigbit();
+			bit_info[sigmap(info.cell->getPort("\\Q")).to_single_sigbit()] = info;
 			continue;
 		}
 
 		if (info.cell->type.size() == 10 && info.cell->type.substr(0, 6) == "$_DFF_") {
-			info.bit_clk = sigmap(info.cell->connections.at("\\C")).to_single_sigbit();
-			info.bit_arst = sigmap(info.cell->connections.at("\\R")).to_single_sigbit();
+			info.bit_clk = sigmap(info.cell->getPort("\\C")).to_single_sigbit();
+			info.bit_arst = sigmap(info.cell->getPort("\\R")).to_single_sigbit();
 			info.clk_polarity = info.cell->type[6] == 'P';
 			info.arst_polarity = info.cell->type[7] == 'P';
 			info.arst_value = info.cell->type[0] == '1' ? RTLIL::State::S1 : RTLIL::State::S0;
-			info.bit_d = sigmap(info.cell->connections.at("\\D")).to_single_sigbit();
-			bit_info[sigmap(info.cell->connections.at("\\Q")).to_single_sigbit()] = info;
+			info.bit_d = sigmap(info.cell->getPort("\\D")).to_single_sigbit();
+			bit_info[sigmap(info.cell->getPort("\\Q")).to_single_sigbit()] = info;
 			continue;
 		}
 	}
 
-	std::map<std::string, dff_map_info_t> empty_dq_map;
-	for (auto &it : module->wires)
+	std::map<RTLIL::IdString, dff_map_info_t> empty_dq_map;
+	for (auto &it : module->wires_)
 	{
 		if (!consider_wire(it.second, empty_dq_map))
 			continue;
@@ -208,11 +208,11 @@ static void create_dff_dq_map(std::map<std::string, dff_map_info_t> &map, RTLIL:
 	}
 }
 
-static void add_new_wire(RTLIL::Module *module, RTLIL::Wire *wire)
+static RTLIL::Wire *add_new_wire(RTLIL::Module *module, RTLIL::IdString name, int width = 1)
 {
-	if (module->count_id(wire->name))
-		log_error("Attempting to create wire %s, but a wire of this name exists already! Hint: Try another value for -sep.\n", RTLIL::id2cstr(wire->name));
-	module->add(wire);
+	if (module->count_id(name))
+		log_error("Attempting to create wire %s, but a wire of this name exists already! Hint: Try another value for -sep.\n", log_id(name));
+	return module->addWire(name, width);
 }
 
 struct ExposePass : public Pass {
@@ -259,6 +259,8 @@ struct ExposePass : public Pass {
 		bool flag_evert_dff = false;
 		std::string sep = ".";
 
+		log_header("Executing EXPOSE pass (exposing internal signals as outputs).\n");
+
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
 		{
@@ -292,15 +294,15 @@ struct ExposePass : public Pass {
 
 		CellTypes ct(design);
 
-		std::map<RTLIL::Module*, std::map<std::string, dff_map_info_t>> dff_dq_maps;
-		std::map<RTLIL::Module*, std::set<std::string>> dff_cells;
+		std::map<RTLIL::Module*, std::map<RTLIL::IdString, dff_map_info_t>> dff_dq_maps;
+		std::map<RTLIL::Module*, std::set<RTLIL::IdString>> dff_cells;
 
 		if (flag_evert_dff)
 		{
 			RTLIL::Module *first_module = NULL;
-			std::set<std::string> shared_dff_wires;
+			std::set<RTLIL::IdString> shared_dff_wires;
 
-			for (auto &mod_it : design->modules)
+			for (auto &mod_it : design->modules_)
 			{
 				if (!design->selected(mod_it.second))
 					continue;
@@ -315,11 +317,11 @@ struct ExposePass : public Pass {
 						shared_dff_wires.insert(it.first);
 					first_module = mod_it.second;
 				} else {
-					std::set<std::string> new_shared_dff_wires;
+					std::set<RTLIL::IdString> new_shared_dff_wires;
 					for (auto &it : shared_dff_wires) {
 						if (!dff_dq_maps[mod_it.second].count(it))
 							continue;
-						if (!compare_wires(first_module->wires.at(it), mod_it.second->wires.at(it)))
+						if (!compare_wires(first_module->wires_.at(it), mod_it.second->wires_.at(it)))
 							continue;
 						new_shared_dff_wires.insert(it);
 					}
@@ -330,7 +332,7 @@ struct ExposePass : public Pass {
 			if (flag_shared)
 				for (auto &map_it : dff_dq_maps)
 				{
-					std::map<std::string, dff_map_info_t> new_map;
+					std::map<RTLIL::IdString, dff_map_info_t> new_map;
 					for (auto &it : map_it.second)
 						if (shared_dff_wires.count(it.first))
 							new_map[it.first] = it.second;
@@ -343,33 +345,33 @@ struct ExposePass : public Pass {
 				dff_cells[it1.first].insert(it3);
 		}
 
-		std::set<std::string> shared_wires, shared_cells;
-		std::set<std::string> used_names;
+		std::set<RTLIL::IdString> shared_wires, shared_cells;
+		std::set<RTLIL::IdString> used_names;
 
 		if (flag_shared)
 		{
 			RTLIL::Module *first_module = NULL;
 
-			for (auto &mod_it : design->modules)
+			for (auto &mod_it : design->modules_)
 			{
 				RTLIL::Module *module = mod_it.second;
 
 				if (!design->selected(module))
 					continue;
 
-				std::set<std::string> dff_wires;
+				std::set<RTLIL::IdString> dff_wires;
 				if (flag_dff)
 					find_dff_wires(dff_wires, module);
 
 				if (first_module == NULL)
 				{
-					for (auto &it : module->wires)
+					for (auto &it : module->wires_)
 						if (design->selected(module, it.second) && consider_wire(it.second, dff_dq_maps[module]))
 							if (!flag_dff || dff_wires.count(it.first))
 								shared_wires.insert(it.first);
 
 					if (flag_evert)
-						for (auto &it : module->cells)
+						for (auto &it : module->cells_)
 							if (design->selected(module, it.second) && consider_cell(design, dff_cells[module], it.second))
 								shared_cells.insert(it.first);
 
@@ -377,22 +379,22 @@ struct ExposePass : public Pass {
 				}
 				else
 				{
-					std::vector<std::string> delete_shared_wires, delete_shared_cells;
+					std::vector<RTLIL::IdString> delete_shared_wires, delete_shared_cells;
 
 					for (auto &it : shared_wires)
 					{
 						RTLIL::Wire *wire;
 
-						if (module->wires.count(it) == 0)
+						if (module->wires_.count(it) == 0)
 							goto delete_shared_wire;
 
-						wire = module->wires.at(it);
+						wire = module->wires_.at(it);
 
 						if (!design->selected(module, wire))
 							goto delete_shared_wire;
 						if (!consider_wire(wire, dff_dq_maps[module]))
 							goto delete_shared_wire;
-						if (!compare_wires(first_module->wires.at(it), wire))
+						if (!compare_wires(first_module->wires_.at(it), wire))
 							goto delete_shared_wire;
 						if (flag_dff && !dff_wires.count(it))
 							goto delete_shared_wire;
@@ -407,16 +409,16 @@ struct ExposePass : public Pass {
 						{
 							RTLIL::Cell *cell;
 
-							if (module->cells.count(it) == 0)
+							if (module->cells_.count(it) == 0)
 								goto delete_shared_cell;
 
-							cell = module->cells.at(it);
+							cell = module->cells_.at(it);
 
 							if (!design->selected(module, cell))
 								goto delete_shared_cell;
 							if (!consider_cell(design, dff_cells[module], cell))
 								goto delete_shared_cell;
-							if (!compare_cells(first_module->cells.at(it), cell))
+							if (!compare_cells(first_module->cells_.at(it), cell))
 								goto delete_shared_cell;
 
 							if (0)
@@ -432,23 +434,22 @@ struct ExposePass : public Pass {
 			}
 		}
 
-		for (auto &mod_it : design->modules)
+		for (auto &mod_it : design->modules_)
 		{
 			RTLIL::Module *module = mod_it.second;
 
 			if (!design->selected(module))
 				continue;
 
-			std::set<std::string> dff_wires;
+			std::set<RTLIL::IdString> dff_wires;
 			if (flag_dff && !flag_shared)
 				find_dff_wires(dff_wires, module);
 
 			SigMap sigmap(module);
 
 			SigMap out_to_in_map;
-			std::vector<RTLIL::Wire*> new_wires;
 
-			for (auto &it : module->wires)
+			for (auto &it : module->wires_)
 			{
 				if (flag_shared) {
 					if (shared_wires.count(it.first) == 0)
@@ -466,29 +467,23 @@ struct ExposePass : public Pass {
 				}
 
 				if (flag_cut) {
-					RTLIL::Wire *in_wire = new RTLIL::Wire;
-					in_wire->name = it.second->name + sep + "i";
-					in_wire->width = it.second->width;
+					RTLIL::Wire *in_wire = add_new_wire(module, it.second->name.str() + sep + "i", it.second->width);
 					in_wire->port_input = true;
 					out_to_in_map.add(sigmap(it.second), in_wire);
-					new_wires.push_back(in_wire);
 				}
 			}
 
 			if (flag_cut)
 			{
-				for (auto it : new_wires)
-					add_new_wire(module, it);
-
-				for (auto &it : module->cells) {
+				for (auto &it : module->cells_) {
 					if (!ct.cell_known(it.second->type))
 						continue;
-					for (auto &conn : it.second->connections)
+					for (auto &conn : it.second->connections_)
 						if (ct.cell_input(it.second->type, conn.first))
 							conn.second = out_to_in_map(sigmap(conn.second));
 				}
 
-				for (auto &conn : module->connections)
+				for (auto &conn : module->connections_)
 					conn.second = out_to_in_map(sigmap(conn.second));
 			}
 
@@ -496,35 +491,29 @@ struct ExposePass : public Pass {
 
 			for (auto &dq : dff_dq_maps[module])
 			{
-				if (!module->wires.count(dq.first))
+				if (!module->wires_.count(dq.first))
 					continue;
 
-				RTLIL::Wire *wire = module->wires.at(dq.first);
+				RTLIL::Wire *wire = module->wires_.at(dq.first);
 				std::set<RTLIL::SigBit> wire_bits_set = sigmap(wire).to_sigbit_set();
 				std::vector<RTLIL::SigBit> wire_bits_vec = sigmap(wire).to_sigbit_vector();
 
 				dff_map_info_t &info = dq.second;
 
-				RTLIL::Wire *wire_dummy_q = new RTLIL::Wire;
-				wire_dummy_q->name = NEW_ID;
-				wire_dummy_q->width = 0;
-				add_new_wire(module, wire_dummy_q);
+				RTLIL::Wire *wire_dummy_q = add_new_wire(module, NEW_ID, 0);
 
 				for (auto &cell_name : info.cells) {
-					RTLIL::Cell *cell = module->cells.at(cell_name);
-					std::vector<RTLIL::SigBit> cell_q_bits = sigmap(cell->connections.at("\\Q")).to_sigbit_vector();
+					RTLIL::Cell *cell = module->cells_.at(cell_name);
+					std::vector<RTLIL::SigBit> cell_q_bits = sigmap(cell->getPort("\\Q")).to_sigbit_vector();
 					for (auto &bit : cell_q_bits)
 						if (wire_bits_set.count(bit))
 							bit = RTLIL::SigBit(wire_dummy_q, wire_dummy_q->width++);
-					cell->connections.at("\\Q") = cell_q_bits;
+					cell->setPort("\\Q", cell_q_bits);
 				}
 
-				RTLIL::Wire *wire_q = new RTLIL::Wire;
-				wire_q->name = wire->name + sep + "q";
-				wire_q->width = wire->width;
+				RTLIL::Wire *wire_q = add_new_wire(module, wire->name.str() + sep + "q", wire->width);
 				wire_q->port_input = true;
 				log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(wire_q->name));
-				add_new_wire(module, wire_q);
 
 				RTLIL::SigSig connect_q;
 				for (size_t i = 0; i < wire_bits_vec.size(); i++) {
@@ -534,71 +523,55 @@ struct ExposePass : public Pass {
 					connect_q.second.append(RTLIL::SigBit(wire_q, i));
 					set_q_bits.insert(wire_bits_vec[i]);
 				}
-				module->connections.push_back(connect_q);
+				module->connect(connect_q);
 
-				RTLIL::Wire *wire_d = new RTLIL::Wire;
-				wire_d->name = wire->name + sep + "d";
-				wire_d->width = wire->width;
+				RTLIL::Wire *wire_d = add_new_wire(module, wire->name.str() + sep + "d", wire->width);
 				wire_d->port_output = true;
 				log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(wire_d->name));
-				add_new_wire(module, wire_d);
-				module->connections.push_back(RTLIL::SigSig(wire_d, info.sig_d));
+				module->connect(RTLIL::SigSig(wire_d, info.sig_d));
 
-				RTLIL::Wire *wire_c = new RTLIL::Wire;
-				wire_c->name = wire->name + sep + "c";
+				RTLIL::Wire *wire_c = add_new_wire(module, wire->name.str() + sep + "c");
 				wire_c->port_output = true;
 				log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(wire_c->name));
-				add_new_wire(module, wire_c);
 				if (info.clk_polarity) {
-					module->connections.push_back(RTLIL::SigSig(wire_c, info.sig_clk));
+					module->connect(RTLIL::SigSig(wire_c, info.sig_clk));
 				} else {
-					RTLIL::Cell *c = new RTLIL::Cell;
-					c->name = NEW_ID;
-					c->type = "$not";
+					RTLIL::Cell *c = module->addCell(NEW_ID, "$not");
 					c->parameters["\\A_SIGNED"] = 0;
 					c->parameters["\\A_WIDTH"] = 1;
 					c->parameters["\\Y_WIDTH"] = 1;
-					c->connections["\\A"] = info.sig_clk;
-					c->connections["\\Y"] = wire_c;
-					module->add(c);
+					c->setPort("\\A", info.sig_clk);
+					c->setPort("\\Y", wire_c);
 				}
 
 				if (info.sig_arst != RTLIL::State::Sm)
 				{
-					RTLIL::Wire *wire_r = new RTLIL::Wire;
-					wire_r->name = wire->name + sep + "r";
+					RTLIL::Wire *wire_r = add_new_wire(module, wire->name.str() + sep + "r");
 					wire_r->port_output = true;
 					log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(wire_r->name));
-					add_new_wire(module, wire_r);
 					if (info.arst_polarity) {
-						module->connections.push_back(RTLIL::SigSig(wire_r, info.sig_arst));
+						module->connect(RTLIL::SigSig(wire_r, info.sig_arst));
 					} else {
-						RTLIL::Cell *c = new RTLIL::Cell;
-						c->name = NEW_ID;
-						c->type = "$not";
+						RTLIL::Cell *c = module->addCell(NEW_ID, "$not");
 						c->parameters["\\A_SIGNED"] = 0;
 						c->parameters["\\A_WIDTH"] = 1;
 						c->parameters["\\Y_WIDTH"] = 1;
-						c->connections["\\A"] = info.sig_arst;
-						c->connections["\\Y"] = wire_r;
-						module->add(c);
+						c->setPort("\\A", info.sig_arst);
+						c->setPort("\\Y", wire_r);
 					}
 
-					RTLIL::Wire *wire_v = new RTLIL::Wire;
-					wire_v->name = wire->name + sep + "v";
-					wire_v->width = wire->width;
+					RTLIL::Wire *wire_v = add_new_wire(module, wire->name.str() + sep + "v", wire->width);
 					wire_v->port_output = true;
 					log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(wire_v->name));
-					add_new_wire(module, wire_v);
-					module->connections.push_back(RTLIL::SigSig(wire_v, info.arst_value));
+					module->connect(RTLIL::SigSig(wire_v, info.arst_value));
 				}
 			}
 
 			if (flag_evert)
 			{
-				std::vector<std::string> delete_cells;
+				std::vector<RTLIL::Cell*> delete_cells;
 
-				for (auto &it : module->cells)
+				for (auto &it : module->cells_)
 				{
 					if (flag_shared) {
 						if (shared_cells.count(it.first) == 0)
@@ -610,66 +583,59 @@ struct ExposePass : public Pass {
 
 					RTLIL::Cell *cell = it.second;
 
-					if (design->modules.count(cell->type))
+					if (design->modules_.count(cell->type))
 					{
-						RTLIL::Module *mod = design->modules.at(cell->type);
+						RTLIL::Module *mod = design->modules_.at(cell->type);
 
-						for (auto &it : mod->wires)
+						for (auto &it : mod->wires_)
 						{
 							RTLIL::Wire *p = it.second;
 							if (!p->port_input && !p->port_output)
 								continue;
 
-							RTLIL::Wire *w = new RTLIL::Wire;
-							w->name = cell->name + sep + RTLIL::unescape_id(p->name);
-							w->width = p->width;
+							RTLIL::Wire *w = add_new_wire(module, cell->name.str() + sep + RTLIL::unescape_id(p->name), p->width);
 							if (p->port_input)
 								w->port_output = true;
 							if (p->port_output)
 								w->port_input = true;
-							add_new_wire(module, w);
 
-							log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(w->name));
+							log("New module port: %s/%s (%s)\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(w->name), RTLIL::id2cstr(cell->type));
 
 							RTLIL::SigSpec sig;
-							if (cell->connections.count(p->name) != 0)
-								sig = cell->connections.at(p->name);
+							if (cell->hasPort(p->name))
+								sig = cell->getPort(p->name);
 							sig.extend(w->width);
 							if (w->port_input)
-								module->connections.push_back(RTLIL::SigSig(sig, w));
+								module->connect(RTLIL::SigSig(sig, w));
 							else
-								module->connections.push_back(RTLIL::SigSig(w, sig));
+								module->connect(RTLIL::SigSig(w, sig));
 						}
 					}
 					else
 					{
-						for (auto &it : cell->connections)
+						for (auto &it : cell->connections())
 						{
-							RTLIL::Wire *w = new RTLIL::Wire;
-							w->name = cell->name + sep + RTLIL::unescape_id(it.first);
-							w->width = it.second.width;
+							RTLIL::Wire *w = add_new_wire(module, cell->name.str() + sep + RTLIL::unescape_id(it.first), it.second.size());
 							if (ct.cell_input(cell->type, it.first))
 								w->port_output = true;
 							if (ct.cell_output(cell->type, it.first))
 								w->port_input = true;
-							add_new_wire(module, w);
 
-							log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(w->name));
+							log("New module port: %s/%s (%s)\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(w->name), RTLIL::id2cstr(cell->type));
 
 							if (w->port_input)
-								module->connections.push_back(RTLIL::SigSig(it.second, w));
+								module->connect(RTLIL::SigSig(it.second, w));
 							else
-								module->connections.push_back(RTLIL::SigSig(w, it.second));
+								module->connect(RTLIL::SigSig(w, it.second));
 						}
 					}
 
-					delete_cells.push_back(cell->name);
+					delete_cells.push_back(cell);
 				}
 
-				for (auto &it : delete_cells) {
-					log("Removing cell: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(it));
-					delete module->cells.at(it);
-					module->cells.erase(it);
+				for (auto cell : delete_cells) {
+					log("Removing cell: %s/%s (%s)\n", log_id(module), log_id(cell), log_id(cell->type));
+					module->remove(cell);
 				}
 			}
 
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index 81250b000..bfed0005d 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -31,8 +31,9 @@
 namespace {
 
 bool inv_mode;
-int verbose_level;
+int verbose_level, reduce_counter, reduce_stop_at;
 typedef std::map<RTLIL::SigBit, std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>>> drivers_t;
+std::string dump_prefix;
 
 struct equiv_bit_t
 {
@@ -112,13 +113,13 @@ struct FindReducedInputs
 		size_t idx_bits = get_bits(idx);
 
 		if (sat_pi_uniq_bitvec.size() != idx_bits) {
-			sat_pi_uniq_bitvec.push_back(ez.literal(stringf("uniq_%d", int(idx_bits)-1)));
+			sat_pi_uniq_bitvec.push_back(ez.frozen_literal(stringf("uniq_%d", int(idx_bits)-1)));
 			for (auto &it : sat_pi)
 				ez.assume(ez.OR(ez.NOT(it.second), ez.NOT(sat_pi_uniq_bitvec.back())));
 		}
 		log_assert(sat_pi_uniq_bitvec.size() == idx_bits);
 
-		sat_pi[bit] = ez.literal(stringf("pi_%s", log_signal(bit)));
+		sat_pi[bit] = ez.frozen_literal(stringf("p, falsei_%s", log_signal(bit)));
 		ez.assume(ez.IFF(ez.XOR(sat_a, sat_b), sat_pi[bit]));
 
 		for (size_t i = 0; i < idx_bits; i++)
@@ -243,7 +244,6 @@ struct PerformReduction
 			return 0;
 		if (sigdepth.count(out) != 0)
 			return sigdepth.at(out);
-		sigdepth[out] = 0;
 
 		if (drivers.count(out) != 0) {
 			std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out);
@@ -252,17 +252,18 @@ struct PerformReduction
 					log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(drv.first->name), RTLIL::id2cstr(drv.first->type));
 				celldone.insert(drv.first);
 			}
-			int max_child_dept = 0;
+			int max_child_depth = 0;
 			for (auto &bit : drv.second)
-				max_child_dept = std::max(register_cone_worker(celldone, sigdepth, bit), max_child_dept);
-			sigdepth[out] = max_child_dept + 1;
+				max_child_depth = std::max(register_cone_worker(celldone, sigdepth, bit), max_child_depth);
+			sigdepth[out] = max_child_depth + 1;
 		} else {
 			pi_bits.push_back(out);
 			sat_pi.push_back(satgen.importSigSpec(out).front());
 			ez.assume(ez.NOT(satgen.importUndefSigSpec(out).front()));
+			sigdepth[out] = 0;
 		}
 
-		return sigdepth[out];
+		return sigdepth.at(out);
 	}
 
 	PerformReduction(SigMap &sigmap, drivers_t &drivers, std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs, std::vector<RTLIL::SigBit> &bits, int cone_size) :
@@ -348,7 +349,7 @@ struct PerformReduction
 			std::vector<RTLIL::SigBit> bucket_sigbits;
 			for (int idx : bucket)
 				bucket_sigbits.push_back(out_bits[idx]);
-			log("%s  Trying to shatter bucket with %d signals: %s\n", indt, int(bucket.size()), log_signal(RTLIL::SigSpec(bucket_sigbits).optimized()));
+			log("%s  Trying to shatter bucket with %d signals: %s\n", indt, int(bucket.size()), log_signal(bucket_sigbits));
 		}
 
 		std::vector<int> sat_set_list, sat_clr_list;
@@ -493,7 +494,7 @@ struct PerformReduction
 				std::vector<RTLIL::SigBit> r_sigbits;
 				for (int idx : r)
 					r_sigbits.push_back(out_bits[idx]);
-				log("  Found group of %d equivialent signals: %s\n", int(r.size()), log_signal(RTLIL::SigSpec(r_sigbits).optimized()));
+				log("  Found group of %d equivialent signals: %s\n", int(r.size()), log_signal(r_sigbits));
 			}
 
 			std::vector<int> undef_slaves;
@@ -559,6 +560,38 @@ struct FreduceWorker
 	{
 	}
 
+	bool find_bit_in_cone(std::set<RTLIL::Cell*> &celldone, RTLIL::SigBit needle, RTLIL::SigBit haystack)
+	{
+		if (needle == haystack)
+			return true;
+		if (haystack.wire == NULL || needle.wire == NULL || drivers.count(haystack) == 0)
+			return false;
+
+		std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(haystack);
+
+		if (celldone.count(drv.first))
+			return false;
+		celldone.insert(drv.first);
+
+		for (auto &bit : drv.second)
+			if (find_bit_in_cone(celldone, needle, bit))
+				return true;
+		return false;
+	}
+
+	bool find_bit_in_cone(RTLIL::SigBit needle, RTLIL::SigBit haystack)
+	{
+		std::set<RTLIL::Cell*> celldone;
+		return find_bit_in_cone(celldone, needle, haystack);
+	}
+
+	void dump()
+	{
+		std::string filename = stringf("%s_%s_%05d.il", dump_prefix.c_str(), RTLIL::id2cstr(module->name), reduce_counter);
+		log("%s    Writing dump file `%s'.\n", reduce_counter ? "  " : "", filename.c_str());
+		Pass::call(design, stringf("dump -outfile %s %s", filename.c_str(), design->selected_active_module.empty() ? module->name.c_str() : ""));
+	}
+
 	int run()
 	{
 		log("Running functional reduction on module %s:\n", RTLIL::id2cstr(module->name));
@@ -569,15 +602,15 @@ struct FreduceWorker
 
 		int bits_full_total = 0;
 		std::vector<std::set<RTLIL::SigBit>> batches;
-		for (auto &it : module->wires)
+		for (auto &it : module->wires_)
 			if (it.second->port_input) {
 				batches.push_back(sigmap(it.second).to_sigbit_set());
 				bits_full_total += it.second->width;
 			}
-		for (auto &it : module->cells) {
+		for (auto &it : module->cells_) {
 			if (ct.cell_known(it.second->type)) {
 				std::set<RTLIL::SigBit> inputs, outputs;
-				for (auto &port : it.second->connections) {
+				for (auto &port : it.second->connections()) {
 					std::vector<RTLIL::SigBit> bits = sigmap(port.second).to_sigbit_vector();
 					if (ct.cell_output(it.second->type, port.first))
 						outputs.insert(bits.begin(), bits.end());
@@ -590,8 +623,8 @@ struct FreduceWorker
 				batches.push_back(outputs);
 				bits_full_total += outputs.size();
 			}
-			if (inv_mode && it.second->type == "$_INV_")
-				inv_pairs.insert(std::pair<RTLIL::SigBit, RTLIL::SigBit>(sigmap(it.second->connections.at("\\A")), sigmap(it.second->connections.at("\\Y"))));
+			if (inv_mode && it.second->type == "$_NOT_")
+				inv_pairs.insert(std::pair<RTLIL::SigBit, RTLIL::SigBit>(sigmap(it.second->getPort("\\A")), sigmap(it.second->getPort("\\Y"))));
 		}
 
 		int bits_count = 0;
@@ -607,7 +640,7 @@ struct FreduceWorker
 
 		found_selected_wire:
 			log("  Finding reduced input cone for signal batch %s%c\n",
-					log_signal(RTLIL::SigSpec(std::vector<RTLIL::SigBit>(batch.begin(), batch.end())).optimized()), verbose_level ? ':' : '.');
+					log_signal(batch), verbose_level ? ':' : '.');
 
 			FindReducedInputs infinder(sigmap, drivers);
 			for (auto &bit : batch) {
@@ -630,12 +663,12 @@ struct FreduceWorker
 				continue;
 
 			if (bucket.first.size() == 0) {
-				log("  Finding const values for bucket %s%c\n", log_signal(RTLIL::SigSpec(bucket.second).optimized()), verbose_level ? ':' : '.');
+				log("  Finding const values for bucket %s%c\n", log_signal(bucket.second), verbose_level ? ':' : '.');
 				PerformReduction worker(sigmap, drivers, inv_pairs, bucket.second, bucket.first.size());
 				for (size_t idx = 0; idx < bucket.second.size(); idx++)
 					worker.analyze_const(equiv, idx);
 			} else {
-				log("  Trying to shatter bucket %s%c\n", log_signal(RTLIL::SigSpec(bucket.second).optimized()), verbose_level ? ':' : '.');
+				log("  Trying to shatter bucket %s%c\n", log_signal(bucket.second), verbose_level ? ':' : '.');
 				PerformReduction worker(sigmap, drivers, inv_pairs, bucket.second, bucket.first.size());
 				worker.analyze(equiv, 100 * bucket_count / (buckets.size() + 1));
 			}
@@ -644,11 +677,14 @@ struct FreduceWorker
 		std::map<RTLIL::SigBit, int> bitusage;
 		module->rewrite_sigspecs(CountBitUsage(sigmap, bitusage));
 
+		if (!dump_prefix.empty())
+			dump();
+
 		log("  Rewiring %d equivialent groups:\n", int(equiv.size()));
 		int rewired_sigbits = 0;
 		for (auto &grp : equiv)
 		{
-			log("    Using as master for group: %s\n", log_signal(grp.front().bit));
+			log("    [%05d] Using as master for group: %s\n", ++reduce_counter, log_signal(grp.front().bit));
 
 			RTLIL::SigSpec inv_sig;
 			for (size_t i = 1; i < grp.size(); i++)
@@ -663,35 +699,45 @@ struct FreduceWorker
 					continue;
 				}
 
+				if (find_bit_in_cone(grp[i].bit, grp.front().bit)) {
+					log("      Skipping dependency of master: %s\n", log_signal(grp[i].bit));
+					continue;
+				}
+
 				log("      Connect slave%s: %s\n", grp[i].inverted ? " using inverter" : "", log_signal(grp[i].bit));
 
 				RTLIL::Cell *drv = drivers.at(grp[i].bit).first;
-				RTLIL::Wire *dummy_wire = module->new_wire(1, NEW_ID);
-				for (auto &port : drv->connections)
+				RTLIL::Wire *dummy_wire = module->addWire(NEW_ID);
+				for (auto &port : drv->connections_)
 					if (ct.cell_output(drv->type, port.first))
 						sigmap(port.second).replace(grp[i].bit, dummy_wire, &port.second);
 
 				if (grp[i].inverted)
 				{
-					if (inv_sig.width == 0)
+					if (inv_sig.size() == 0)
 					{
-						inv_sig = module->new_wire(1, NEW_ID);
-
-						RTLIL::Cell *inv_cell = new RTLIL::Cell;
-						inv_cell->name = NEW_ID;
-						inv_cell->type = "$_INV_";
-						inv_cell->connections["\\A"] = grp[0].bit;
-						inv_cell->connections["\\Y"] = inv_sig;
-						module->add(inv_cell);
+						inv_sig = module->addWire(NEW_ID);
+
+						RTLIL::Cell *inv_cell = module->addCell(NEW_ID, "$_NOT_");
+						inv_cell->setPort("\\A", grp[0].bit);
+						inv_cell->setPort("\\Y", inv_sig);
 					}
 
-					module->connections.push_back(RTLIL::SigSig(grp[i].bit, inv_sig));
+					module->connect(RTLIL::SigSig(grp[i].bit, inv_sig));
 				}
 				else
-					module->connections.push_back(RTLIL::SigSig(grp[i].bit, grp[0].bit));
+					module->connect(RTLIL::SigSig(grp[i].bit, grp[0].bit));
 
 				rewired_sigbits++;
 			}
+
+			if (!dump_prefix.empty())
+				dump();
+
+			if (reduce_counter == reduce_stop_at) {
+				log("    Reached limit passed using -stop option. Skipping all further reductions.\n");
+				break;
+			}
 		}
 
 		log("  Rewired a total of %d signal bits in module %s.\n", rewired_sigbits, RTLIL::id2cstr(module->name));
@@ -711,7 +757,7 @@ struct FreducePass : public Pass {
 		log("\n");
 		log("This pass performs functional reduction in the circuit. I.e. if two nodes are\n");
 		log("equivialent, they are merged to one node and one of the redundant drivers is\n");
-		log("unconnected. A subsequent call to 'clean' will remove the redundant drivers.\n");
+		log("disconnected. A subsequent call to 'clean' will remove the redundant drivers.\n");
 		log("\n");
 		log("    -v, -vv\n");
 		log("        enable verbose or very verbose output\n");
@@ -719,6 +765,14 @@ struct FreducePass : public Pass {
 		log("    -inv\n");
 		log("        enable explicit handling of inverted signals\n");
 		log("\n");
+		log("    -stop <n>\n");
+		log("        stop after <n> reduction operations. this is mostly used for\n");
+		log("        debugging the freduce command itself.\n");
+		log("\n");
+		log("    -dump <prefix>\n");
+		log("        dump the design to <prefix>_<module>_<num>.il after each reduction\n");
+		log("        operation. this is mostly used for debugging the freduce command.\n");
+		log("\n");
 		log("This pass is undef-aware, i.e. it considers don't-care values for detecting\n");
 		log("equivialent nodes.\n");
 		log("\n");
@@ -728,8 +782,11 @@ struct FreducePass : public Pass {
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
+		reduce_counter = 0;
+		reduce_stop_at = 0;
 		verbose_level = 0;
 		inv_mode = false;
+		dump_prefix = std::string();
 
 		log_header("Executing FREDUCE pass (perform functional reduction).\n");
 
@@ -747,12 +804,20 @@ struct FreducePass : public Pass {
 				inv_mode = true;
 				continue;
 			}
+			if (args[argidx] == "-stop" && argidx+1 < args.size()) {
+				reduce_stop_at = atoi(args[++argidx].c_str());
+				continue;
+			}
+			if (args[argidx] == "-dump" && argidx+1 < args.size()) {
+				dump_prefix = args[++argidx];
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
 
 		int bitcount = 0;
-		for (auto &mod_it : design->modules) {
+		for (auto &mod_it : design->modules_) {
 			RTLIL::Module *module = mod_it.second;
 			if (design->selected(module))
 				bitcount += FreduceWorker(design, module).run();
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index db12cb57d..b3adefb92 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -27,6 +27,9 @@ static void create_miter_equiv(struct Pass *that, std::vector<std::string> args,
 	bool flag_make_outputs = false;
 	bool flag_make_outcmp = false;
 	bool flag_make_assert = false;
+	bool flag_flatten = false;
+
+	log_header("Executing MITER pass (creating miter circuit).\n");
 
 	size_t argidx;
 	for (argidx = 2; argidx < args.size(); argidx++)
@@ -47,32 +50,36 @@ static void create_miter_equiv(struct Pass *that, std::vector<std::string> args,
 			flag_make_assert = true;
 			continue;
 		}
+		if (args[argidx] == "-flatten") {
+			flag_flatten = true;
+			continue;
+		}
 		break;
 	}
 	if (argidx+3 != args.size() || args[argidx].substr(0, 1) == "-")
 		that->cmd_error(args, argidx, "command argument error");
 	
-	std::string gold_name = RTLIL::escape_id(args[argidx++]);
-	std::string gate_name = RTLIL::escape_id(args[argidx++]);
-	std::string miter_name = RTLIL::escape_id(args[argidx++]);
+	RTLIL::IdString gold_name = RTLIL::escape_id(args[argidx++]);
+	RTLIL::IdString gate_name = RTLIL::escape_id(args[argidx++]);
+	RTLIL::IdString miter_name = RTLIL::escape_id(args[argidx++]);
 
-	if (design->modules.count(gold_name) == 0)
+	if (design->modules_.count(gold_name) == 0)
 		log_cmd_error("Can't find gold module %s!\n", gold_name.c_str());
-	if (design->modules.count(gate_name) == 0)
+	if (design->modules_.count(gate_name) == 0)
 		log_cmd_error("Can't find gate module %s!\n", gate_name.c_str());
-	if (design->modules.count(miter_name) != 0)
+	if (design->modules_.count(miter_name) != 0)
 		log_cmd_error("There is already a module %s!\n", gate_name.c_str());
 
-	RTLIL::Module *gold_module = design->modules.at(gold_name);
-	RTLIL::Module *gate_module = design->modules.at(gate_name);
+	RTLIL::Module *gold_module = design->modules_.at(gold_name);
+	RTLIL::Module *gate_module = design->modules_.at(gate_name);
 
-	for (auto &it : gold_module->wires) {
+	for (auto &it : gold_module->wires_) {
 		RTLIL::Wire *w1 = it.second, *w2;
 		if (w1->port_id == 0)
 			continue;
-		if (gate_module->wires.count(it.second->name) == 0)
+		if (gate_module->wires_.count(it.second->name) == 0)
 			goto match_gold_port_error;
-		w2 = gate_module->wires.at(it.second->name);
+		w2 = gate_module->wires_.at(it.second->name);
 		if (w1->port_input != w2->port_input)
 			goto match_gold_port_error;
 		if (w1->port_output != w2->port_output)
@@ -84,13 +91,13 @@ static void create_miter_equiv(struct Pass *that, std::vector<std::string> args,
 		log_cmd_error("No matching port in gate module was found for %s!\n", it.second->name.c_str());
 	}
 
-	for (auto &it : gate_module->wires) {
+	for (auto &it : gate_module->wires_) {
 		RTLIL::Wire *w1 = it.second, *w2;
 		if (w1->port_id == 0)
 			continue;
-		if (gold_module->wires.count(it.second->name) == 0)
+		if (gold_module->wires_.count(it.second->name) == 0)
 			goto match_gate_port_error;
-		w2 = gold_module->wires.at(it.second->name);
+		w2 = gold_module->wires_.at(it.second->name);
 		if (w1->port_input != w2->port_input)
 			goto match_gate_port_error;
 		if (w1->port_output != w2->port_output)
@@ -102,187 +109,151 @@ static void create_miter_equiv(struct Pass *that, std::vector<std::string> args,
 		log_cmd_error("No matching port in gold module was found for %s!\n", it.second->name.c_str());
 	}
 
+	log("Creating miter cell \"%s\" with gold cell \"%s\" and gate cell \"%s\".\n", RTLIL::id2cstr(miter_name), RTLIL::id2cstr(gold_name), RTLIL::id2cstr(gate_name));
+
 	RTLIL::Module *miter_module = new RTLIL::Module;
 	miter_module->name = miter_name;
-	design->modules[miter_name] = miter_module;
-
-	RTLIL::Cell *gold_cell = new RTLIL::Cell;
-	gold_cell->name = "\\gold";
-	gold_cell->type = gold_name;
-	miter_module->add(gold_cell);
+	design->add(miter_module);
 
-	RTLIL::Cell *gate_cell = new RTLIL::Cell;
-	gate_cell->name = "\\gate";
-	gate_cell->type = gate_name;
-	miter_module->add(gate_cell);
+	RTLIL::Cell *gold_cell = miter_module->addCell("\\gold", gold_name);
+	RTLIL::Cell *gate_cell = miter_module->addCell("\\gate", gate_name);
 
 	RTLIL::SigSpec all_conditions;
 
-	for (auto &it : gold_module->wires)
+	for (auto &it : gold_module->wires_)
 	{
 		RTLIL::Wire *w1 = it.second;
 
 		if (w1->port_input)
 		{
-			RTLIL::Wire *w2 = new RTLIL::Wire;
-			w2->name = "\\in_" + RTLIL::unescape_id(w1->name);
+			RTLIL::Wire *w2 = miter_module->addWire("\\in_" + RTLIL::unescape_id(w1->name), w1->width);
 			w2->port_input = true;
-			w2->width = w1->width;
-			miter_module->add(w2);
 
-			gold_cell->connections[w1->name] = w2;
-			gate_cell->connections[w1->name] = w2;
+			gold_cell->setPort(w1->name, w2);
+			gate_cell->setPort(w1->name, w2);
 		}
 
 		if (w1->port_output)
 		{
-			RTLIL::Wire *w2_gold = new RTLIL::Wire;
-			w2_gold->name = "\\gold_" + RTLIL::unescape_id(w1->name);
+			RTLIL::Wire *w2_gold = miter_module->addWire("\\gold_" + RTLIL::unescape_id(w1->name), w1->width);
 			w2_gold->port_output = flag_make_outputs;
-			w2_gold->width = w1->width;
-			miter_module->add(w2_gold);
 
-			RTLIL::Wire *w2_gate = new RTLIL::Wire;
-			w2_gate->name = "\\gate_" + RTLIL::unescape_id(w1->name);
+			RTLIL::Wire *w2_gate = miter_module->addWire("\\gate_" + RTLIL::unescape_id(w1->name), w1->width);
 			w2_gate->port_output = flag_make_outputs;
-			w2_gate->width = w1->width;
-			miter_module->add(w2_gate);
 
-			gold_cell->connections[w1->name] = w2_gold;
-			gate_cell->connections[w1->name] = w2_gate;
+			gold_cell->setPort(w1->name, w2_gold);
+			gate_cell->setPort(w1->name, w2_gate);
 
 			RTLIL::SigSpec this_condition;
 
 			if (flag_ignore_gold_x)
 			{
-				RTLIL::SigSpec gold_x = miter_module->new_wire(w2_gold->width, NEW_ID);
+				RTLIL::SigSpec gold_x = miter_module->addWire(NEW_ID, w2_gold->width);
 				for (int i = 0; i < w2_gold->width; i++) {
-					RTLIL::Cell *eqx_cell = new RTLIL::Cell;
-					eqx_cell->name = NEW_ID;
-					eqx_cell->type = "$eqx";
+					RTLIL::Cell *eqx_cell = miter_module->addCell(NEW_ID, "$eqx");
 					eqx_cell->parameters["\\A_WIDTH"] = 1;
 					eqx_cell->parameters["\\B_WIDTH"] = 1;
 					eqx_cell->parameters["\\Y_WIDTH"] = 1;
 					eqx_cell->parameters["\\A_SIGNED"] = 0;
 					eqx_cell->parameters["\\B_SIGNED"] = 0;
-					eqx_cell->connections["\\A"] = RTLIL::SigSpec(w2_gold, 1, i);
-					eqx_cell->connections["\\B"] = RTLIL::State::Sx;
-					eqx_cell->connections["\\Y"] = gold_x.extract(i, 1);
-					miter_module->add(eqx_cell);
+					eqx_cell->setPort("\\A", RTLIL::SigSpec(w2_gold, i));
+					eqx_cell->setPort("\\B", RTLIL::State::Sx);
+					eqx_cell->setPort("\\Y", gold_x.extract(i, 1));
 				}
 
-				RTLIL::SigSpec gold_masked = miter_module->new_wire(w2_gold->width, NEW_ID);
-				RTLIL::SigSpec gate_masked = miter_module->new_wire(w2_gate->width, NEW_ID);
+				RTLIL::SigSpec gold_masked = miter_module->addWire(NEW_ID, w2_gold->width);
+				RTLIL::SigSpec gate_masked = miter_module->addWire(NEW_ID, w2_gate->width);
 
-				RTLIL::Cell *or_gold_cell = new RTLIL::Cell;
-				or_gold_cell->name = NEW_ID;
-				or_gold_cell->type = "$or";
+				RTLIL::Cell *or_gold_cell = miter_module->addCell(NEW_ID, "$or");
 				or_gold_cell->parameters["\\A_WIDTH"] = w2_gold->width;
 				or_gold_cell->parameters["\\B_WIDTH"] = w2_gold->width;
 				or_gold_cell->parameters["\\Y_WIDTH"] = w2_gold->width;
 				or_gold_cell->parameters["\\A_SIGNED"] = 0;
 				or_gold_cell->parameters["\\B_SIGNED"] = 0;
-				or_gold_cell->connections["\\A"] = w2_gold;
-				or_gold_cell->connections["\\B"] = gold_x;
-				or_gold_cell->connections["\\Y"] = gold_masked;
-				miter_module->add(or_gold_cell);
-
-				RTLIL::Cell *or_gate_cell = new RTLIL::Cell;
-				or_gate_cell->name = NEW_ID;
-				or_gate_cell->type = "$or";
+				or_gold_cell->setPort("\\A", w2_gold);
+				or_gold_cell->setPort("\\B", gold_x);
+				or_gold_cell->setPort("\\Y", gold_masked);
+
+				RTLIL::Cell *or_gate_cell = miter_module->addCell(NEW_ID, "$or");
 				or_gate_cell->parameters["\\A_WIDTH"] = w2_gate->width;
 				or_gate_cell->parameters["\\B_WIDTH"] = w2_gate->width;
 				or_gate_cell->parameters["\\Y_WIDTH"] = w2_gate->width;
 				or_gate_cell->parameters["\\A_SIGNED"] = 0;
 				or_gate_cell->parameters["\\B_SIGNED"] = 0;
-				or_gate_cell->connections["\\A"] = w2_gate;
-				or_gate_cell->connections["\\B"] = gold_x;
-				or_gate_cell->connections["\\Y"] = gate_masked;
-				miter_module->add(or_gate_cell);
-
-				RTLIL::Cell *eq_cell = new RTLIL::Cell;
-				eq_cell->name = NEW_ID;
-				eq_cell->type = "$eqx";
+				or_gate_cell->setPort("\\A", w2_gate);
+				or_gate_cell->setPort("\\B", gold_x);
+				or_gate_cell->setPort("\\Y", gate_masked);
+
+				RTLIL::Cell *eq_cell = miter_module->addCell(NEW_ID, "$eqx");
 				eq_cell->parameters["\\A_WIDTH"] = w2_gold->width;
 				eq_cell->parameters["\\B_WIDTH"] = w2_gate->width;
 				eq_cell->parameters["\\Y_WIDTH"] = 1;
 				eq_cell->parameters["\\A_SIGNED"] = 0;
 				eq_cell->parameters["\\B_SIGNED"] = 0;
-				eq_cell->connections["\\A"] = gold_masked;
-				eq_cell->connections["\\B"] = gate_masked;
-				eq_cell->connections["\\Y"] = miter_module->new_wire(1, NEW_ID);
-				this_condition = eq_cell->connections["\\Y"];
-				miter_module->add(eq_cell);
+				eq_cell->setPort("\\A", gold_masked);
+				eq_cell->setPort("\\B", gate_masked);
+				eq_cell->setPort("\\Y", miter_module->addWire(NEW_ID));
+				this_condition = eq_cell->getPort("\\Y");
 			}
 			else
 			{
-				RTLIL::Cell *eq_cell = new RTLIL::Cell;
-				eq_cell->name = NEW_ID;
-				eq_cell->type = "$eqx";
+				RTLIL::Cell *eq_cell = miter_module->addCell(NEW_ID, "$eqx");
 				eq_cell->parameters["\\A_WIDTH"] = w2_gold->width;
 				eq_cell->parameters["\\B_WIDTH"] = w2_gate->width;
 				eq_cell->parameters["\\Y_WIDTH"] = 1;
 				eq_cell->parameters["\\A_SIGNED"] = 0;
 				eq_cell->parameters["\\B_SIGNED"] = 0;
-				eq_cell->connections["\\A"] = w2_gold;
-				eq_cell->connections["\\B"] = w2_gate;
-				eq_cell->connections["\\Y"] = miter_module->new_wire(1, NEW_ID);
-				this_condition = eq_cell->connections["\\Y"];
-				miter_module->add(eq_cell);
+				eq_cell->setPort("\\A", w2_gold);
+				eq_cell->setPort("\\B", w2_gate);
+				eq_cell->setPort("\\Y", miter_module->addWire(NEW_ID));
+				this_condition = eq_cell->getPort("\\Y");
 			}
 
 			if (flag_make_outcmp)
 			{
-				RTLIL::Wire *w_cmp = new RTLIL::Wire;
-				w_cmp->name = "\\cmp_" + RTLIL::unescape_id(w1->name);
+				RTLIL::Wire *w_cmp = miter_module->addWire("\\cmp_" + RTLIL::unescape_id(w1->name));
 				w_cmp->port_output = true;
-				miter_module->add(w_cmp);
-				miter_module->connections.push_back(RTLIL::SigSig(w_cmp, this_condition));
+				miter_module->connect(RTLIL::SigSig(w_cmp, this_condition));
 			}
 
 			all_conditions.append(this_condition);
 		}
 	}
 
-	if (all_conditions.width != 1) {
-		RTLIL::Cell *reduce_cell = new RTLIL::Cell;
-		reduce_cell->name = NEW_ID;
-		reduce_cell->type = "$reduce_and";
-		reduce_cell->parameters["\\A_WIDTH"] = all_conditions.width;
+	if (all_conditions.size() != 1) {
+		RTLIL::Cell *reduce_cell = miter_module->addCell(NEW_ID, "$reduce_and");
+		reduce_cell->parameters["\\A_WIDTH"] = all_conditions.size();
 		reduce_cell->parameters["\\Y_WIDTH"] = 1;
 		reduce_cell->parameters["\\A_SIGNED"] = 0;
-		reduce_cell->connections["\\A"] = all_conditions;
-		reduce_cell->connections["\\Y"] = miter_module->new_wire(1, NEW_ID);
-		all_conditions = reduce_cell->connections["\\Y"];
-		miter_module->add(reduce_cell);
+		reduce_cell->setPort("\\A", all_conditions);
+		reduce_cell->setPort("\\Y", miter_module->addWire(NEW_ID));
+		all_conditions = reduce_cell->getPort("\\Y");
 	}
 
 	if (flag_make_assert) {
-		RTLIL::Cell *assert_cell = new RTLIL::Cell;
-		assert_cell->name = NEW_ID;
-		assert_cell->type = "$assert";
-		assert_cell->connections["\\A"] = all_conditions;
-		assert_cell->connections["\\EN"] = RTLIL::SigSpec(1, 1);
-		miter_module->add(assert_cell);
+		RTLIL::Cell *assert_cell = miter_module->addCell(NEW_ID, "$assert");
+		assert_cell->setPort("\\A", all_conditions);
+		assert_cell->setPort("\\EN", RTLIL::SigSpec(1, 1));
 	}
 
-	RTLIL::Wire *w_trigger = new RTLIL::Wire;
-	w_trigger->name = "\\trigger";
+	RTLIL::Wire *w_trigger = miter_module->addWire("\\trigger");
 	w_trigger->port_output = true;
-	miter_module->add(w_trigger);
 
-	RTLIL::Cell *not_cell = new RTLIL::Cell;
-	not_cell->name = NEW_ID;
-	not_cell->type = "$not";
-	not_cell->parameters["\\A_WIDTH"] = all_conditions.width;
-	not_cell->parameters["\\A_WIDTH"] = all_conditions.width;
+	RTLIL::Cell *not_cell = miter_module->addCell(NEW_ID, "$not");
+	not_cell->parameters["\\A_WIDTH"] = all_conditions.size();
+	not_cell->parameters["\\A_WIDTH"] = all_conditions.size();
 	not_cell->parameters["\\Y_WIDTH"] = w_trigger->width;
 	not_cell->parameters["\\A_SIGNED"] = 0;
-	not_cell->connections["\\A"] = all_conditions;
-	not_cell->connections["\\Y"] = w_trigger;
-	miter_module->add(not_cell);
+	not_cell->setPort("\\A", all_conditions);
+	not_cell->setPort("\\Y", w_trigger);
 
 	miter_module->fixup_ports();
+
+	if (flag_flatten) {
+		log_push();
+		Pass::call_on_module(design, miter_module, "flatten; opt_const -keepdc -undriven;;");
+		log_pop();
+	}
 }
 
 struct MiterPass : public Pass {
@@ -313,6 +284,9 @@ struct MiterPass : public Pass {
 		log("    -make_assert\n");
 		log("        also create an 'assert' cell that checks if trigger is always low.\n");
 		log("\n");
+		log("    -flatten\n");
+		log("        call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit.\n");
+		log("\n");
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index c08271590..fd0abf4a5 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -30,6 +30,8 @@
 #include <stdlib.h>
 #include <stdio.h>
 #include <algorithm>
+#include <errno.h>
+#include <string.h>
 
 namespace {
 
@@ -92,19 +94,35 @@ struct SatHelper
 
 		RTLIL::SigSpec big_lhs, big_rhs;
 
-		for (auto &it : module->wires)
+		for (auto &it : module->wires_)
 		{
 			if (it.second->attributes.count("\\init") == 0)
 				continue;
 
 			RTLIL::SigSpec lhs = sigmap(it.second);
 			RTLIL::SigSpec rhs = it.second->attributes.at("\\init");
-			log_assert(lhs.width == rhs.width);
+			log_assert(lhs.size() == rhs.size());
+
+			RTLIL::SigSpec removed_bits;
+			for (int i = 0; i < lhs.size(); i++) {
+				RTLIL::SigSpec bit = lhs.extract(i, 1);
+				if (!satgen.initial_state.check_all(bit)) {
+					removed_bits.append(bit);
+					lhs.remove(i, 1);
+					rhs.remove(i, 1);
+					i--;
+				}
+			}
 
-			log("Import set-constraint from init attribute: %s = %s\n", log_signal(lhs), log_signal(rhs));
-			big_lhs.remove2(lhs, &big_rhs);
-			big_lhs.append(lhs);
-			big_rhs.append(rhs);
+			if (removed_bits.size())
+				log("Warning: ignoring initial value on non-register: %s\n", log_signal(removed_bits));
+
+			if (lhs.size()) {
+				log("Import set-constraint from init attribute: %s = %s\n", log_signal(lhs), log_signal(rhs));
+				big_lhs.remove2(lhs, &big_rhs);
+				big_lhs.append(lhs);
+				big_rhs.append(rhs);
+			}
 		}
 
 		for (auto &s : sets_init)
@@ -118,9 +136,9 @@ struct SatHelper
 			show_signal_pool.add(sigmap(lhs));
 			show_signal_pool.add(sigmap(rhs));
 
-			if (lhs.width != rhs.width)
+			if (lhs.size() != rhs.size())
 				log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
-					s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+					s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
 
 			log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
 			big_lhs.remove2(lhs, &big_rhs);
@@ -130,7 +148,6 @@ struct SatHelper
 
 		if (!satgen.initial_state.check_all(big_lhs)) {
 			RTLIL::SigSpec rem = satgen.initial_state.remove(big_lhs);
-			rem.optimize();
 			log_cmd_error("Found -set-init bits that are not part of the initial_state: %s\n", log_signal(rem));
 		}
 
@@ -144,17 +161,17 @@ struct SatHelper
 			RTLIL::SigSpec rem = satgen.initial_state.export_all();
 			rem.remove(big_lhs);
 			big_lhs.append(rem);
-			big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.width));
+			big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.size()));
 		}
 
 		if (set_init_zero) {
 			RTLIL::SigSpec rem = satgen.initial_state.export_all();
 			rem.remove(big_lhs);
 			big_lhs.append(rem);
-			big_rhs.append(RTLIL::SigSpec(RTLIL::State::S0, rem.width));
+			big_rhs.append(RTLIL::SigSpec(RTLIL::State::S0, rem.size()));
 		}
 
-		if (big_lhs.width == 0) {
+		if (big_lhs.size() == 0) {
 			log("No constraints for initial state found.\n\n");
 			return;
 		}
@@ -187,9 +204,9 @@ struct SatHelper
 			show_signal_pool.add(sigmap(lhs));
 			show_signal_pool.add(sigmap(rhs));
 
-			if (lhs.width != rhs.width)
+			if (lhs.size() != rhs.size())
 				log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
-					s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+					s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
 
 			log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
 			big_lhs.remove2(lhs, &big_rhs);
@@ -208,11 +225,11 @@ struct SatHelper
 			show_signal_pool.add(sigmap(lhs));
 			show_signal_pool.add(sigmap(rhs));
 
-			if (lhs.width != rhs.width)
+			if (lhs.size() != rhs.size())
 				log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
-					s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+					s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
 
-			log("Import set-constraint for timestep: %s = %s\n", log_signal(lhs), log_signal(rhs));
+			log("Import set-constraint for this timestep: %s = %s\n", log_signal(lhs), log_signal(rhs));
 			big_lhs.remove2(lhs, &big_rhs);
 			big_lhs.append(lhs);
 			big_rhs.append(rhs);
@@ -226,7 +243,7 @@ struct SatHelper
 				log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.c_str());
 			show_signal_pool.add(sigmap(lhs));
 
-			log("Import unset-constraint for timestep: %s\n", log_signal(lhs));
+			log("Import unset-constraint for this timestep: %s\n", log_signal(lhs));
 			big_lhs.remove2(lhs, &big_rhs);
 		}
 
@@ -289,7 +306,7 @@ struct SatHelper
 
 		for (int t = 0; t < 3; t++)
 		for (auto &sig : sets_def_undef[t]) {
-			log("Import %s constraint for timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
+			log("Import %s constraint for this timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
 			std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep);
 			if (t == 0)
 				ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig)));
@@ -300,11 +317,11 @@ struct SatHelper
 		}
 
 		int import_cell_counter = 0;
-		for (auto &c : module->cells)
+		for (auto &c : module->cells_)
 			if (design->selected(module, c.second)) {
 				// log("Import cell: %s\n", RTLIL::id2cstr(c.first));
 				if (satgen.importCell(c.second, timestep)) {
-					for (auto &p : c.second->connections)
+					for (auto &p : c.second->connections())
 						if (ct.cell_output(c.second->type, p.first))
 							show_drivers.insert(sigmap(p.second), c.second);
 					import_cell_counter++;
@@ -318,7 +335,7 @@ struct SatHelper
 
 	int setup_proof(int timestep = -1)
 	{
-		assert(prove.size() || prove_x.size() || prove_asserts);
+		log_assert(prove.size() || prove_x.size() || prove_asserts);
 
 		RTLIL::SigSpec big_lhs, big_rhs;
 		std::vector<int> prove_bits;
@@ -336,9 +353,9 @@ struct SatHelper
 				show_signal_pool.add(sigmap(lhs));
 				show_signal_pool.add(sigmap(rhs));
 
-				if (lhs.width != rhs.width)
+				if (lhs.size() != rhs.size())
 					log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
-						s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+						s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
 
 				log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
 				big_lhs.remove2(lhs, &big_rhs);
@@ -364,9 +381,9 @@ struct SatHelper
 				show_signal_pool.add(sigmap(lhs));
 				show_signal_pool.add(sigmap(rhs));
 
-				if (lhs.width != rhs.width)
+				if (lhs.size() != rhs.size())
 					log_cmd_error("Proof-x expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
-						s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+						s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
 
 				log("Import proof-x-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
 				big_lhs.remove2(lhs, &big_rhs);
@@ -389,10 +406,8 @@ struct SatHelper
 		if (prove_asserts) {
 			RTLIL::SigSpec asserts_a, asserts_en;
 			satgen.getAsserts(asserts_a, asserts_en, timestep);
-			asserts_a.expand();
-			asserts_en.expand();
-			for (size_t i = 0; i < asserts_a.chunks.size(); i++)
-				log("Import proof for assert: %s when %s.\n", log_signal(asserts_a.chunks[i]), log_signal(asserts_en.chunks[i]));
+			for (int i = 0; i < SIZE(asserts_a); i++)
+				log("Import proof for assert: %s when %s.\n", log_signal(asserts_a[i]), log_signal(asserts_en[i]));
 			prove_bits.push_back(satgen.importAsserts(timestep));
 		}
 
@@ -490,7 +505,7 @@ struct SatHelper
 					final_signals.add(sig);
 				} else {
 					for (auto &d : drivers)
-					for (auto &p : d->connections) {
+					for (auto &p : d->connections()) {
 						if (d->type == "$dff" && p.first == "\\CLK")
 							continue;
 						if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C")
@@ -521,12 +536,12 @@ struct SatHelper
 
 		std::vector<int> modelUndefExpressions;
 
-		for (auto &c : modelSig.chunks)
+		for (auto &c : modelSig.chunks())
 			if (c.wire != NULL)
 			{
 				ModelBlockInfo info;
 				RTLIL::SigSpec chunksig = c;
-				info.width = chunksig.width;
+				info.width = chunksig.size();
 				info.description = log_signal(chunksig);
 
 				for (int timestep = -1; timestep <= max_timestep; timestep++)
@@ -551,7 +566,7 @@ struct SatHelper
 		// Add initial state signals as collected by satgen
 		//
 		modelSig = satgen.initial_state.export_all();
-		for (auto &c : modelSig.chunks)
+		for (auto &c : modelSig.chunks())
 			if (c.wire != NULL)
 			{
 				ModelBlockInfo info;
@@ -559,7 +574,7 @@ struct SatHelper
 
 				info.timestep = 0;
 				info.offset = modelExpressions.size();
-				info.width = chunksig.width;
+				info.width = chunksig.size();
 				info.description = log_signal(chunksig);
 				modelInfo.insert(info);
 
@@ -631,6 +646,109 @@ struct SatHelper
 			log("  no model variables selected for display.\n");
 	}
 
+	void dump_model_to_vcd(std::string 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));
+
+		log("Dumping SAT model to VCD file %s\n", vcd_file_name.c_str());
+
+		time_t timestamp;
+		struct tm* now;
+		char stime[128] = {};
+		time(&timestamp);
+		now = localtime(&timestamp);
+		strftime(stime, sizeof(stime), "%c", now);
+
+		std::string module_fname = "unknown";
+		auto apos = module->attributes.find("\\src");
+		if(apos != module->attributes.end())
+			module_fname = module->attributes["\\src"].decode_string();
+
+		fprintf(f, "$date\n");
+		fprintf(f, "    %s\n", stime);
+		fprintf(f, "$end\n");
+		fprintf(f, "$version\n");
+		fprintf(f, "    Generated by %s\n", yosys_version_str); 
+		fprintf(f, "$end\n");
+		fprintf(f, "$comment\n");
+		fprintf(f, "    Generated from SAT problem in module %s (declared at %s)\n",
+			module->name.c_str(), module_fname.c_str());
+		fprintf(f, "$end\n");
+
+		// VCD has some limits on internal (non-display) identifier names, so make legal ones
+		std::map<std::string, std::string> vcdnames;
+
+		fprintf(f, "$timescale 1ns\n"); // arbitrary time scale since actual clock period is unknown/unimportant
+		fprintf(f, "$scope module %s $end\n", module->name.c_str());
+		for (auto &info : modelInfo)
+		{
+			if (vcdnames.find(info.description) != vcdnames.end())
+				continue;
+
+			char namebuf[16];
+			snprintf(namebuf, sizeof(namebuf), "v%d", static_cast<int>(vcdnames.size()));
+			vcdnames[info.description] = namebuf;
+
+			// Even display identifiers can't use some special characters
+			std::string legal_desc = info.description.c_str();
+			for (auto &c : legal_desc) {
+				if(c == '$')
+					c = '_';
+				if(c == ':')
+					c = '_';
+			}
+
+			fprintf(f, "$var wire %d %s %s $end\n", info.width, namebuf, legal_desc.c_str());
+
+			// Need to look at first *two* cycles!
+			// We need to put a name on all variables but those without an initialization clause
+			// have no value at timestep 0
+			if(info.timestep > 1)
+				break;
+		}
+		fprintf(f, "$upscope $end\n");
+		fprintf(f, "$enddefinitions $end\n");
+		fprintf(f, "$dumpvars\n");
+
+		static const char bitvals[] = "01xzxx";
+
+		int last_timestep = -2;
+		for (auto &info : modelInfo)
+		{
+			RTLIL::Const value;
+
+			for (int i = 0; i < info.width; i++) {
+				value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
+				if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
+					value.bits.back() = RTLIL::State::Sx;
+			}
+
+			if (info.timestep != last_timestep) {
+				if(last_timestep == 0)
+					fprintf(f, "$end\n");
+				else
+					fprintf(f, "#%d\n", info.timestep);
+				last_timestep = info.timestep;
+			}
+
+			if(info.width == 1) {
+				fprintf(f, "%c%s\n", bitvals[value.bits[0]], vcdnames[info.description].c_str());
+			} else {
+				fprintf(f, "b");
+				for(int k=info.width-1; k >= 0; k --)	//need to flip bit ordering for VCD
+					fprintf(f, "%c", bitvals[value.bits[k]]);
+				fprintf(f, " %s\n", vcdnames[info.description].c_str());
+			}
+		}
+
+		if (last_timestep == -2)
+			log("  no model variables selected for display.\n");
+
+		fclose(f);
+	}
+
 	void invalidate_model(bool max_undef)
 	{
 		std::vector<int> clause;
@@ -756,7 +874,7 @@ struct SatPass : public Pass {
 		log("    -set-def-at <N> <signal>\n");
 		log("    -set-any-undef-at <N> <signal>\n");
 		log("    -set-all-undef-at <N> <signal>\n");
-		log("        add undef contraints in the given timestep.\n");
+		log("        add undef constraints in the given timestep.\n");
 		log("\n");
 		log("    -set-init <signal> <value>\n");
 		log("        set the initial value for the register driving the signal to the value\n");
@@ -770,6 +888,13 @@ struct SatPass : public Pass {
 		log("    -set-init-zero\n");
 		log("        set all initial states (not set using -set-init) to zero\n");
 		log("\n");
+		log("    -dump_vcd <vcd-file-name>\n");
+		log("        dump SAT model (counter example in proof) to VCD file\n");
+		log("\n");
+		log("    -dump_cnf <cnf-file-name>\n");
+		log("        dump CNF of SAT problem (in DIMACS format). in temporal induction\n");
+		log("        proofs this is the CNF of the first induction step.\n");
+		log("\n");
 		log("The following additional options can be used to set up a proof. If also -seq\n");
 		log("is passed, a temporal induction proof is performed.\n");
 		log("\n");
@@ -792,9 +917,15 @@ struct SatPass : public Pass {
 		log("    -prove-asserts\n");
 		log("        Prove that all asserts in the design hold.\n");
 		log("\n");
+		log("    -prove-skip <N>\n");
+		log("        Do not enforce the prove-condition for the first <N> time steps.\n");
+		log("\n");
 		log("    -maxsteps <N>\n");
 		log("        Set a maximum length for the induction.\n");
 		log("\n");
+		log("    -initsteps <N>\n");
+		log("        Set initial length for the induction.\n");
+		log("\n");
 		log("    -timeout <N>\n");
 		log("        Maximum number of seconds a single SAT instance may take.\n");
 		log("\n");
@@ -817,11 +948,12 @@ struct SatPass : public Pass {
 		std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
 		std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
 		std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
-		int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
+		int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0, prove_skip = 0;
 		bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
 		bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
 		bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
 		bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
+		std::string vcd_file_name, cnf_file_name;
 
 		log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
 
@@ -861,6 +993,10 @@ struct SatPass : public Pass {
 				maxsteps = atoi(args[++argidx].c_str());
 				continue;
 			}
+			if (args[argidx] == "-initsteps" && argidx+1 < args.size()) {
+				initsteps = atoi(args[++argidx].c_str());
+				continue;
+			}
 			if (args[argidx] == "-ignore_div_by_zero") {
 				ignore_div_by_zero = true;
 				continue;
@@ -926,6 +1062,10 @@ struct SatPass : public Pass {
 				prove_asserts = true;
 				continue;
 			}
+			if (args[argidx] == "-prove-skip" && argidx+1 < args.size()) {
+				prove_skip = atoi(args[++argidx].c_str());
+				continue;
+			}
 			if (args[argidx] == "-seq" && argidx+1 < args.size()) {
 				seq_len = atoi(args[++argidx].c_str());
 				continue;
@@ -995,12 +1135,20 @@ struct SatPass : public Pass {
 				ignore_unknown_cells = true;
 				continue;
 			}
+			if (args[argidx] == "-dump_vcd" && argidx+1 < args.size()) {
+				vcd_file_name = args[++argidx];
+				continue;
+			}
+			if (args[argidx] == "-dump_cnf" && argidx+1 < args.size()) {
+				cnf_file_name = args[++argidx];
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
 
 		RTLIL::Module *module = NULL;
-		for (auto &mod_it : design->modules)
+		for (auto &mod_it : design->modules_)
 			if (design->selected(mod_it.second)) {
 				if (module)
 					log_cmd_error("Only one module must be selected for the SAT pass! (selected: %s and %s)\n",
@@ -1013,25 +1161,31 @@ struct SatPass : public Pass {
 		if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
 			log_cmd_error("Got -tempinduct but nothing to prove!\n");
 
+		if (prove_skip && tempinduct)
+			log_cmd_error("Options -prove-skip and -tempinduct don't work with each other.\n");
+
+		if (prove_skip >= seq_len && prove_skip > 0)
+			log_cmd_error("The value of -prove-skip must be smaller than the one of -seq.\n");
+
 		if (set_init_undef + set_init_zero + set_init_def > 1)
 			log_cmd_error("The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!\n");
 
 		if (set_def_inputs) {
-			for (auto &it : module->wires)
+			for (auto &it : module->wires_)
 				if (it.second->port_input)
-					sets_def.push_back(it.second->name);
+					sets_def.push_back(it.second->name.str());
 		}
 
 		if (show_inputs) {
-			for (auto &it : module->wires)
+			for (auto &it : module->wires_)
 				if (it.second->port_input)
-					shows.push_back(it.second->name);
+					shows.push_back(it.second->name.str());
 		}
 
 		if (show_outputs) {
-			for (auto &it : module->wires)
+			for (auto &it : module->wires_)
 				if (it.second->port_output)
-					shows.push_back(it.second->name);
+					shows.push_back(it.second->name.str());
 		}
 
 		if (tempinduct)
@@ -1107,6 +1261,8 @@ struct SatPass : public Pass {
 					log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
 					print_proof_failed();
 					basecase.print_model();
+					if(!vcd_file_name.empty())
+						basecase.dump_model_to_vcd(vcd_file_name);
 					goto tip_failed;
 				}
 
@@ -1125,24 +1281,47 @@ struct SatPass : public Pass {
 				if (inductlen > 1)
 					inductstep.force_unique_state(1, inductlen + 1);
 
-				log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
-						inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
-
-				if (!inductstep.solve(inductstep.ez.NOT(property))) {
-					if (inductstep.gotTimeout)
-						goto timeout;
-					log("Induction step proven: SUCCESS!\n");
-					print_qed();
-					goto tip_success;
+				if (inductlen < initsteps)
+				{
+					log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n",
+							inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
+					inductstep.ez.assume(property);
 				}
+				else
+				{
+					if (!cnf_file_name.empty())
+					{
+						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));
 
-				log("Induction step failed. Incrementing induction length.\n");
-				inductstep.ez.assume(property);
+						log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
+						cnf_file_name.clear();
+
+						inductstep.ez.printDIMACS(f, false);
+						fclose(f);
+					}
 
-				inductstep.print_model();
+					log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
+							inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
+
+					if (!inductstep.solve(inductstep.ez.NOT(property))) {
+						if (inductstep.gotTimeout)
+							goto timeout;
+						log("Induction step proven: SUCCESS!\n");
+						print_qed();
+						goto tip_success;
+					}
+
+					log("Induction step failed. Incrementing induction length.\n");
+					inductstep.ez.assume(property);
+					inductstep.print_model();
+				}
 			}
 
 			log("\nReached maximum number of time steps -> proof failed.\n");
+			if(!vcd_file_name.empty())
+				inductstep.dump_model_to_vcd(vcd_file_name);
 			print_proof_failed();
 
 		tip_failed:
@@ -1195,7 +1374,8 @@ struct SatPass : public Pass {
 				for (int timestep = 1; timestep <= seq_len; timestep++) {
 					sathelper.setup(timestep);
 					if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
-						prove_bits.push_back(sathelper.setup_proof(timestep));
+						if (timestep > prove_skip)
+							prove_bits.push_back(sathelper.setup_proof(timestep));
 				}
 				if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
 					sathelper.ez.assume(sathelper.ez.NOT(sathelper.ez.expression(ezSAT::OpAnd, prove_bits)));
@@ -1203,10 +1383,18 @@ struct SatPass : public Pass {
 			}
 			sathelper.generate_model();
 
-#if 0
-			// print CNF for debugging
-			sathelper.ez.printDIMACS(stdout, true);
-#endif
+			if (!cnf_file_name.empty())
+			{
+				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));
+
+				log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
+				cnf_file_name.clear();
+
+				sathelper.ez.printDIMACS(f, false);
+				fclose(f);
+			}
 
 			int rerun_counter = 0;
 
@@ -1230,6 +1418,9 @@ struct SatPass : public Pass {
 
 				sathelper.print_model();
 
+				if(!vcd_file_name.empty())
+					sathelper.dump_model_to_vcd(vcd_file_name);
+
 				if (loopcount != 0) {
 					loopcount--, rerun_counter++;
 					sathelper.invalidate_model(max_undef);