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

14 files changed, 1486 insertions, 204 deletions

diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc
index ee12546ce..f6aac0b41 100644
--- a/backends/blif/blif.cc
+++ b/backends/blif/blif.cc
@@ -28,6 +28,9 @@
 #include "kernel/log.h"
 #include <string>
 
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
 struct BlifDumperConfig
 {
 	bool icells_mode;
@@ -35,11 +38,14 @@ struct BlifDumperConfig
 	bool impltf_mode;
 	bool gates_mode;
 	bool param_mode;
+	bool attr_mode;
+	bool blackbox_mode;
 
 	std::string buf_type, buf_in, buf_out;
-	std::string true_type, true_out, false_type, false_out;
+	std::map<RTLIL::IdString, std::pair<RTLIL::IdString, RTLIL::IdString>> unbuf_types;
+	std::string true_type, true_out, false_type, false_out, undef_type, undef_out;
 
-	BlifDumperConfig() : icells_mode(false), conn_mode(false), impltf_mode(false), gates_mode(false), param_mode(false) { }
+	BlifDumperConfig() : icells_mode(false), conn_mode(false), impltf_mode(false), gates_mode(false), param_mode(false), attr_mode(false), blackbox_mode(false) { }
 };
 
 struct BlifDumper
@@ -69,8 +75,11 @@ struct BlifDumper
 
 	const char *cstr(RTLIL::SigBit sig)
 	{
-		if (sig.wire == NULL)
-			return sig == RTLIL::State::S1 ?  "$true" : "$false";
+		if (sig.wire == NULL) {
+			if (sig == RTLIL::State::S0) return config->false_type == "-" ? config->false_out.c_str() : "$false";
+			if (sig == RTLIL::State::S1) return config->true_type == "-" ? config->true_out.c_str() : "$true";
+			return config->undef_type == "-" ? config->undef_out.c_str() : "$undef";
+		}
 
 		std::string str = RTLIL::unescape_id(sig.wire->name);
 		for (size_t i = 0; i < str.size(); i++)
@@ -95,6 +104,26 @@ struct BlifDumper
 		return "subckt";
 	}
 
+	void dump_params(const char *command, dict<IdString, Const> &params)
+	{
+		for (auto &param : params) {
+			f << stringf("%s %s ", command, RTLIL::id2cstr(param.first));
+			if (param.second.flags & RTLIL::CONST_FLAG_STRING) {
+				std::string str = param.second.decode_string();
+				f << stringf("\"");
+				for (char ch : str)
+					if (ch == '"' || ch == '\\')
+						f << stringf("\\%c", ch);
+					else if (ch < 32 || ch >= 127)
+						f << stringf("\\%03o", ch);
+					else
+						f << stringf("%c", ch);
+				f << stringf("\"\n");
+			} else
+				f << stringf("%s\n", param.second.as_string().c_str());
+		}
+	}
+
 	void dump()
 	{
 		f << stringf("\n");
@@ -126,23 +155,44 @@ struct BlifDumper
 		}
 		f << stringf("\n");
 
+		if (module->get_bool_attribute("\\blackbox")) {
+			f << stringf(".blackbox\n");
+			f << stringf(".end\n");
+			return;
+		}
+
 		if (!config->impltf_mode) {
-			if (!config->false_type.empty())
-				f << stringf(".%s %s %s=$false\n", subckt_or_gate(config->false_type),
-						config->false_type.c_str(), config->false_out.c_str());
-			else
+			if (!config->false_type.empty()) {
+				if (config->false_type != "-")
+					f << stringf(".%s %s %s=$false\n", subckt_or_gate(config->false_type),
+							config->false_type.c_str(), config->false_out.c_str());
+			} else
 				f << stringf(".names $false\n");
-			if (!config->true_type.empty())
-				f << stringf(".%s %s %s=$true\n", subckt_or_gate(config->true_type),
-						config->true_type.c_str(), config->true_out.c_str());
-			else
+			if (!config->true_type.empty()) {
+				if (config->true_type != "-")
+					f << stringf(".%s %s %s=$true\n", subckt_or_gate(config->true_type),
+							config->true_type.c_str(), config->true_out.c_str());
+			} else
 				f << stringf(".names $true\n1\n");
+			if (!config->undef_type.empty()) {
+				if (config->undef_type != "-")
+					f << stringf(".%s %s %s=$undef\n", subckt_or_gate(config->undef_type),
+							config->undef_type.c_str(), config->undef_out.c_str());
+			} else
+				f << stringf(".names $undef\n");
 		}
 
 		for (auto &cell_it : module->cells_)
 		{
 			RTLIL::Cell *cell = cell_it.second;
 
+			if (config->unbuf_types.count(cell->type)) {
+				auto portnames = config->unbuf_types.at(cell->type);
+				f << stringf(".names %s %s\n1 1\n",
+						cstr(cell->getPort(portnames.first)), cstr(cell->getPort(portnames.second)));
+				continue;
+			}
+
 			if (!config->icells_mode && cell->type == "$_NOT_") {
 				f << stringf(".names %s %s\n0 1\n",
 						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\Y")));
@@ -191,21 +241,21 @@ struct BlifDumper
 				auto &inputs = cell->getPort("\\A");
 				auto width = cell->parameters.at("\\WIDTH").as_int();
 				log_assert(inputs.size() == width);
-				for (int i = 0; i < inputs.size(); i++) {
+				for (int i = width-1; i >= 0; i--) {
 					f << stringf(" %s", cstr(inputs.extract(i, 1)));
 				}
 				auto &output = cell->getPort("\\Y");
 				log_assert(output.size() == 1);
 				f << stringf(" %s", cstr(output));
 				f << stringf("\n");
-				auto mask = cell->parameters.at("\\LUT").as_string();
-				for (int i = 0; i < (1 << width); i++) {
-					if (mask[i] == '0') continue;
-					for (int j = width-1; j >= 0; j--) {
-						f << ((i>>j)&1 ? '1' : '0');
+				RTLIL::SigSpec mask = cell->parameters.at("\\LUT");
+				for (int i = 0; i < (1 << width); i++)
+					if (mask[i] == RTLIL::S1) {
+						for (int j = width-1; j >= 0; j--) {
+							f << ((i>>j)&1 ? '1' : '0');
+						}
+						f << " 1\n";
 					}
-					f << stringf(" %c\n", mask[i]);
-				}
 				continue;
 			}
 
@@ -220,23 +270,10 @@ struct BlifDumper
 			}
 			f << stringf("\n");
 
+			if (config->attr_mode)
+				dump_params(".attr", cell->attributes);
 			if (config->param_mode)
-				for (auto &param : cell->parameters) {
-					f << stringf(".param %s ", RTLIL::id2cstr(param.first));
-					if (param.second.flags & RTLIL::CONST_FLAG_STRING) {
-						std::string str = param.second.decode_string();
-						f << stringf("\"");
-						for (char ch : str)
-							if (ch == '"' || ch == '\\')
-								f << stringf("\\%c", ch);
-							else if (ch < 32 || ch >= 127)
-								f << stringf("\\%03o", ch);
-							else
-								f << stringf("%c", ch);
-						f << stringf("\"\n");
-					} else
-						f << stringf("%s\n", param.second.as_string().c_str());
-				}
+				dump_params(".param", cell->parameters);
 		}
 
 		for (auto &conn : module->connections())
@@ -276,9 +313,17 @@ struct BlifBackend : public Backend {
 		log("    -buf <cell-type> <in-port> <out-port>\n");
 		log("        use cells of type <cell-type> with the specified port names for buffers\n");
 		log("\n");
+		log("    -unbuf <cell-type> <in-port> <out-port>\n");
+		log("        replace buffer cells with the specified name and port names with\n");
+		log("        a .names statement that models a buffer\n");
+		log("\n");
 		log("    -true <cell-type> <out-port>\n");
 		log("    -false <cell-type> <out-port>\n");
-		log("        use the specified cell types to drive nets that are constant 1 or 0\n");
+		log("    -undef <cell-type> <out-port>\n");
+		log("        use the specified cell types to drive nets that are constant 1, 0, or\n");
+		log("        undefined. when '-' is used as <cell-type>, then <out-port> specifies\n");
+		log("        the wire name to be used for the constant signal and no cell driving\n");
+		log("        that wire is generated.\n");
 		log("\n");
 		log("The following options can be useful when the generated file is not going to be\n");
 		log("read by a BLIF parser but a custom tool. It is recommended to not name the output\n");
@@ -296,11 +341,17 @@ struct BlifBackend : public Backend {
 		log("        do not generate buffers for connected wires. instead use the\n");
 		log("        non-standard .conn statement.\n");
 		log("\n");
+		log("    -attr\n");
+		log("        use the non-standard .attr statement to write cell attributes\n");
+		log("\n");
 		log("    -param\n");
-		log("        use the non-standard .param statement to write module parameters\n");
+		log("        use the non-standard .param statement to write cell parameters\n");
+		log("\n");
+		log("    -blackbox\n");
+		log("        write blackbox cells with .blackbox statement.\n");
 		log("\n");
 		log("    -impltf\n");
-		log("        do not write definitions for the $true and $false wires.\n");
+		log("        do not write definitions for the $true, $false and $undef wires.\n");
 		log("\n");
 	}
 	virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
@@ -326,6 +377,13 @@ struct BlifBackend : public Backend {
 				config.buf_out = args[++argidx];
 				continue;
 			}
+			if (args[argidx] == "-unbuf" && argidx+3 < args.size()) {
+				RTLIL::IdString unbuf_type = RTLIL::escape_id(args[++argidx]);
+				RTLIL::IdString unbuf_in = RTLIL::escape_id(args[++argidx]);
+				RTLIL::IdString unbuf_out = RTLIL::escape_id(args[++argidx]);
+				config.unbuf_types[unbuf_type] = std::pair<RTLIL::IdString, RTLIL::IdString>(unbuf_in, unbuf_out);
+				continue;
+			}
 			if (args[argidx] == "-true" && argidx+2 < args.size()) {
 				config.true_type = args[++argidx];
 				config.true_out = args[++argidx];
@@ -336,6 +394,11 @@ struct BlifBackend : public Backend {
 				config.false_out = args[++argidx];
 				continue;
 			}
+			if (args[argidx] == "-undef" && argidx+2 < args.size()) {
+				config.undef_type = args[++argidx];
+				config.undef_out = args[++argidx];
+				continue;
+			}
 			if (args[argidx] == "-icells") {
 				config.icells_mode = true;
 				continue;
@@ -352,6 +415,14 @@ struct BlifBackend : public Backend {
 				config.param_mode = true;
 				continue;
 			}
+			if (args[argidx] == "-attr") {
+				config.attr_mode = true;
+				continue;
+			}
+			if (args[argidx] == "-blackbox") {
+				config.blackbox_mode = true;
+				continue;
+			}
 			if (args[argidx] == "-impltf") {
 				config.impltf_mode = true;
 				continue;
@@ -372,7 +443,7 @@ struct BlifBackend : public Backend {
 		for (auto module_it : design->modules_)
 		{
 			RTLIL::Module *module = module_it.second;
-			if (module->get_bool_attribute("\\blackbox"))
+			if (module->get_bool_attribute("\\blackbox") && !config.blackbox_mode)
 				continue;
 
 			if (module->processes.size() != 0)
@@ -397,3 +468,4 @@ struct BlifBackend : public Backend {
 	}
 } BlifBackend;
 
+PRIVATE_NAMESPACE_END
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 8ce5bb5ed..c8fbf8d67 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -30,6 +30,9 @@
 #include <string>
 #include <math.h>
 
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
 struct BtorDumperConfig
 {
 	bool subckt_mode;
@@ -476,7 +479,7 @@ struct BtorDumper
 				log_assert(!(cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" ||
 					cell->type == "$ge" || cell->type == "$gt") || output_width == 1);
 				bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
-				bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
+				bool l2_signed YS_ATTRIBUTE(unused) = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
 				int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
 				int l2_width = 	cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
 				
@@ -817,7 +820,7 @@ struct BtorDumper
 				int input_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
 				log_assert(input->size() == input_width);
 				int input_line = dump_sigspec(input, input_width);
-				const RTLIL::SigSpec* output = &cell->getPort(RTLIL::IdString("\\Y"));
+				const RTLIL::SigSpec* output YS_ATTRIBUTE(unused) = &cell->getPort(RTLIL::IdString("\\Y"));
 				int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
 				log_assert(output->size() == output_width);
 				int offset = cell->parameters.at(RTLIL::IdString("\\OFFSET")).as_int();	
@@ -1057,3 +1060,4 @@ struct BtorBackend : public Backend {
 	}
 } BtorBackend;
 
+PRIVATE_NAMESPACE_END
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index ccedd91d2..b089be143 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -27,6 +27,9 @@
 #include "kernel/log.h"
 #include <string>
 
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
 #define EDIF_DEF(_id) edif_names(RTLIL::unescape_id(_id), true).c_str()
 #define EDIF_REF(_id) edif_names(RTLIL::unescape_id(_id), false).c_str()
 
@@ -108,7 +111,7 @@ struct EdifBackend : public Backend {
 		log_header("Executing EDIF backend.\n");
 
 		std::string top_module_name;
-		std::map<RTLIL::IdString, std::set<RTLIL::IdString>> lib_cell_ports;
+		std::map<RTLIL::IdString, std::map<RTLIL::IdString, int>> lib_cell_ports;
 		CellTypes ct(design);
 		EdifNames edif_names;
 
@@ -147,12 +150,8 @@ struct EdifBackend : public Backend {
 				RTLIL::Cell *cell = cell_it.second;
 				if (!design->modules_.count(cell->type) || design->modules_.at(cell->type)->get_bool_attribute("\\blackbox")) {
 					lib_cell_ports[cell->type];
-					for (auto p : cell->connections()) {
-						if (p.second.size() > 1)
-							log_error("Found multi-bit port %s on library cell %s.%s (%s): not supported in EDIF backend!\n",
-									RTLIL::id2cstr(p.first), RTLIL::id2cstr(module->name), RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
-						lib_cell_ports[cell->type].insert(p.first);
-					}
+					for (auto p : cell->connections())
+						lib_cell_ports[cell->type][p.first] = GetSize(p.second);
 				}
 			}
 		}
@@ -195,12 +194,15 @@ struct EdifBackend : public Backend {
 			for (auto &port_it : cell_it.second) {
 				const char *dir = "INOUT";
 				if (ct.cell_known(cell_it.first)) {
-					if (!ct.cell_output(cell_it.first, port_it))
+					if (!ct.cell_output(cell_it.first, port_it.first))
 						dir = "INPUT";
-					else if (!ct.cell_input(cell_it.first, port_it))
+					else if (!ct.cell_input(cell_it.first, port_it.first))
 						dir = "OUTPUT";
 				}
-				*f << stringf("          (port %s (direction %s))\n", EDIF_DEF(port_it), dir);
+				if (port_it.second == 1)
+					*f << stringf("          (port %s (direction %s))\n", EDIF_DEF(port_it.first), dir);
+				else
+					*f << stringf("          (port (array %s %d) (direction %s))\n", EDIF_DEF(port_it.first), port_it.second, dir);
 			}
 			*f << stringf("        )\n");
 			*f << stringf("      )\n");
@@ -300,12 +302,12 @@ struct EdifBackend : public Backend {
 							char digit_str[2] = { "0123456789abcdef"[digit_value], 0 };
 							hex_string = std::string(digit_str) + hex_string;
 						}
-						*f << stringf("\n            (property %s (string \"%s\"))", EDIF_DEF(p.first), hex_string.c_str());
+						*f << stringf("\n            (property %s (string \"%d'h%s\"))", EDIF_DEF(p.first), GetSize(p.second.bits), hex_string.c_str());
 					}
 				*f << stringf(")\n");
 				for (auto &p : cell->connections()) {
 					RTLIL::SigSpec sig = sigmap(p.second);
-					for (int i = 0; i < SIZE(sig); i++)
+					for (int i = 0; i < GetSize(sig); i++)
 						if (sig.size() == 1)
 							net_join_db[sig[i]].insert(stringf("(portRef %s (instanceRef %s))", EDIF_REF(p.first), EDIF_REF(cell->name)));
 						else
@@ -345,3 +347,4 @@ struct EdifBackend : public Backend {
 	}
 } EdifBackend;
 
+PRIVATE_NAMESPACE_END
diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index 48d818d76..814d3e8fe 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -26,7 +26,9 @@
 #include "kernel/yosys.h"
 #include <errno.h>
 
+USING_YOSYS_NAMESPACE
 using namespace ILANG_BACKEND;
+YOSYS_NAMESPACE_BEGIN
 
 void ILANG_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int width, int offset, bool autoint)
 {
@@ -101,7 +103,7 @@ void ILANG_BACKEND::dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, boo
 		dump_sigchunk(f, sig.as_chunk(), autoint);
 	} else {
 		f << stringf("{ ");
-		for (auto it = sig.chunks().rbegin(); it != sig.chunks().rend(); it++) {
+		for (auto it = sig.chunks().rbegin(); it != sig.chunks().rend(); ++it) {
 			dump_sigchunk(f, *it, false);
 			f << stringf(" ");
 		}
@@ -111,11 +113,9 @@ void ILANG_BACKEND::dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, boo
 
 void ILANG_BACKEND::dump_wire(std::ostream &f, std::string indent, const RTLIL::Wire *wire)
 {
-	std::map<RTLIL::IdString, RTLIL::Const, RTLIL::sort_by_id_str> sorted_attributes(wire->attributes.begin(), wire->attributes.end());
-
-	for (auto it = sorted_attributes.begin(); it != sorted_attributes.end(); it++) {
-		f << stringf("%s" "attribute %s ", indent.c_str(), it->first.c_str());
-		dump_const(f, it->second);
+	for (auto &it : wire->attributes) {
+		f << stringf("%s" "attribute %s ", indent.c_str(), it.first.c_str());
+		dump_const(f, it.second);
 		f << stringf("\n");
 	}
 	f << stringf("%s" "wire ", indent.c_str());
@@ -136,11 +136,9 @@ void ILANG_BACKEND::dump_wire(std::ostream &f, std::string indent, const RTLIL::
 
 void ILANG_BACKEND::dump_memory(std::ostream &f, std::string indent, const RTLIL::Memory *memory)
 {
-	std::map<RTLIL::IdString, RTLIL::Const, RTLIL::sort_by_id_str> sorted_attributes(memory->attributes.begin(), memory->attributes.end());
-
-	for (auto it = sorted_attributes.begin(); it != sorted_attributes.end(); it++) {
-		f << stringf("%s" "attribute %s ", indent.c_str(), it->first.c_str());
-		dump_const(f, it->second);
+	for (auto &it : memory->attributes) {
+		f << stringf("%s" "attribute %s ", indent.c_str(), it.first.c_str());
+		dump_const(f, it.second);
 		f << stringf("\n");
 	}
 	f << stringf("%s" "memory ", indent.c_str());
@@ -148,29 +146,27 @@ void ILANG_BACKEND::dump_memory(std::ostream &f, std::string indent, const RTLIL
 		f << stringf("width %d ", memory->width);
 	if (memory->size != 0)
 		f << stringf("size %d ", memory->size);
+	if (memory->start_offset != 0)
+		f << stringf("offset %d ", memory->start_offset);
 	f << stringf("%s\n", memory->name.c_str());
 }
 
 void ILANG_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL::Cell *cell)
 {
-	std::map<RTLIL::IdString, RTLIL::Const, RTLIL::sort_by_id_str> sorted_attributes(cell->attributes.begin(), cell->attributes.end());
-	std::map<RTLIL::IdString, RTLIL::Const, RTLIL::sort_by_id_str> sorted_parameters(cell->parameters.begin(), cell->parameters.end());
-	std::map<RTLIL::IdString, RTLIL::SigSpec, RTLIL::sort_by_id_str> sorted_connections(cell->connections().begin(), cell->connections().end());
-
-	for (auto it = sorted_attributes.begin(); it != sorted_attributes.end(); it++) {
-		f << stringf("%s" "attribute %s ", indent.c_str(), it->first.c_str());
-		dump_const(f, it->second);
+	for (auto &it : cell->attributes) {
+		f << stringf("%s" "attribute %s ", indent.c_str(), it.first.c_str());
+		dump_const(f, it.second);
 		f << stringf("\n");
 	}
 	f << stringf("%s" "cell %s %s\n", indent.c_str(), cell->type.c_str(), cell->name.c_str());
-	for (auto it = sorted_parameters.begin(); it != sorted_parameters.end(); it++) {
-		f << stringf("%s  parameter%s %s ", indent.c_str(), (it->second.flags & RTLIL::CONST_FLAG_SIGNED) != 0 ? " signed" : "", it->first.c_str());
-		dump_const(f, it->second);
+	for (auto &it : cell->parameters) {
+		f << stringf("%s  parameter%s %s ", indent.c_str(), (it.second.flags & RTLIL::CONST_FLAG_SIGNED) != 0 ? " signed" : "", it.first.c_str());
+		dump_const(f, it.second);
 		f << stringf("\n");
 	}
-	for (auto it = sorted_connections.begin(); it != sorted_connections.end(); it++) {
-		f << stringf("%s  connect %s ", indent.c_str(), it->first.c_str());
-		dump_sigspec(f, it->second);
+	for (auto &it : cell->connections()) {
+		f << stringf("%s  connect %s ", indent.c_str(), it.first.c_str());
+		dump_sigspec(f, it.second);
 		f << stringf("\n");
 	}
 	f << stringf("%s" "end\n", indent.c_str());
@@ -178,7 +174,7 @@ void ILANG_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL::
 
 void ILANG_BACKEND::dump_proc_case_body(std::ostream &f, std::string indent, const RTLIL::CaseRule *cs)
 {
-	for (auto it = cs->actions.begin(); it != cs->actions.end(); it++)
+	for (auto it = cs->actions.begin(); it != cs->actions.end(); ++it)
 	{
 		f << stringf("%s" "assign ", indent.c_str());
 		dump_sigspec(f, it->first);
@@ -187,13 +183,13 @@ void ILANG_BACKEND::dump_proc_case_body(std::ostream &f, std::string indent, con
 		f << stringf("\n");
 	}
 
-	for (auto it = cs->switches.begin(); it != cs->switches.end(); it++)
+	for (auto it = cs->switches.begin(); it != cs->switches.end(); ++it)
 		dump_proc_switch(f, indent, *it);
 }
 
 void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const RTLIL::SwitchRule *sw)
 {
-	for (auto it = sw->attributes.begin(); it != sw->attributes.end(); it++) {
+	for (auto it = sw->attributes.begin(); it != sw->attributes.end(); ++it) {
 		f << stringf("%s" "attribute %s ", indent.c_str(), it->first.c_str());
 		dump_const(f, it->second);
 		f << stringf("\n");
@@ -203,7 +199,7 @@ void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const
 	dump_sigspec(f, sw->signal);
 	f << stringf("\n");
 
-	for (auto it = sw->cases.begin(); it != sw->cases.end(); it++)
+	for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it)
 	{
 		f << stringf("%s  case ", indent.c_str());
 		for (size_t i = 0; i < (*it)->compare.size(); i++) {
@@ -235,7 +231,7 @@ void ILANG_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RT
 	case RTLIL::STi: f << stringf("init\n"); break;
 	}
 
-	for (auto it = sy->actions.begin(); it != sy->actions.end(); it++) {
+	for (auto it = sy->actions.begin(); it != sy->actions.end(); ++it) {
 		f << stringf("%s  update ", indent.c_str());
 		dump_sigspec(f, it->first);
 		f << stringf(" ");
@@ -246,14 +242,14 @@ void ILANG_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RT
 
 void ILANG_BACKEND::dump_proc(std::ostream &f, std::string indent, const RTLIL::Process *proc)
 {
-	for (auto it = proc->attributes.begin(); it != proc->attributes.end(); it++) {
+	for (auto it = proc->attributes.begin(); it != proc->attributes.end(); ++it) {
 		f << stringf("%s" "attribute %s ", indent.c_str(), it->first.c_str());
 		dump_const(f, it->second);
 		f << stringf("\n");
 	}
 	f << stringf("%s" "process %s\n", indent.c_str(), proc->name.c_str());
 	dump_proc_case_body(f, indent + "  ", &proc->root_case);
-	for (auto it = proc->syncs.begin(); it != proc->syncs.end(); it++)
+	for (auto it = proc->syncs.begin(); it != proc->syncs.end(); ++it)
 		dump_proc_sync(f, indent + "  ", *it);
 	f << stringf("%s" "end\n", indent.c_str());
 }
@@ -274,7 +270,7 @@ void ILANG_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Modu
 
 	if (print_header)
 	{
-		for (auto it = module->attributes.begin(); it != module->attributes.end(); it++) {
+		for (auto it = module->attributes.begin(); it != module->attributes.end(); ++it) {
 			f << stringf("%s" "attribute %s ", indent.c_str(), it->first.c_str());
 			dump_const(f, it->second);
 			f << stringf("\n");
@@ -285,56 +281,36 @@ void ILANG_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Modu
 
 	if (print_body)
 	{
-		std::vector<RTLIL::Wire*> sorted_wires;
 		for (auto it : module->wires())
-			sorted_wires.push_back(it);
-		std::sort(sorted_wires.begin(), sorted_wires.end(), RTLIL::sort_by_name_str<RTLIL::Wire>());
-
-		std::vector<RTLIL::Memory*> sorted_memories;
-		for (auto it : module->memories)
-			sorted_memories.push_back(it.second);
-		std::sort(sorted_memories.begin(), sorted_memories.end(), RTLIL::sort_by_name_str<RTLIL::Memory>());
-
-		std::vector<RTLIL::Cell*> sorted_cells;
-		for (auto it : module->cells())
-			sorted_cells.push_back(it);
-		std::sort(sorted_cells.begin(), sorted_cells.end(), RTLIL::sort_by_name_str<RTLIL::Cell>());
-
-		std::vector<RTLIL::Process*> sorted_processes;
-		for (auto it : module->processes)
-			sorted_processes.push_back(it.second);
-		std::sort(sorted_processes.begin(), sorted_processes.end(), RTLIL::sort_by_name_str<RTLIL::Process>());
-
-		for (auto it : sorted_wires)
 			if (!only_selected || design->selected(module, it)) {
 				if (only_selected)
 					f << stringf("\n");
 				dump_wire(f, indent + "  ", it);
 			}
 
-		for (auto it : sorted_memories)
-			if (!only_selected || design->selected(module, it)) {
+		for (auto it : module->memories)
+			if (!only_selected || design->selected(module, it.second)) {
 				if (only_selected)
 					f << stringf("\n");
-				dump_memory(f, indent + "  ", it);
+				dump_memory(f, indent + "  ", it.second);
 			}
 
-		for (auto it : sorted_cells)
+		for (auto it : module->cells())
 			if (!only_selected || design->selected(module, it)) {
 				if (only_selected)
 					f << stringf("\n");
 				dump_cell(f, indent + "  ", it);
 			}
 
-		for (auto it : sorted_processes)
-			if (!only_selected || design->selected(module, it)) {
+		for (auto it : module->processes)
+			if (!only_selected || design->selected(module, it.second)) {
 				if (only_selected)
 					f << stringf("\n");
-				dump_proc(f, indent + "  ", it);
+				dump_proc(f, indent + "  ", it.second);
 			}
 
 		bool first_conn_line = true;
-		for (auto it = module->connections().begin(); it != module->connections().end(); it++) {
+		for (auto it = module->connections().begin(); it != module->connections().end(); ++it) {
 			bool show_conn = !only_selected;
 			if (only_selected) {
 				RTLIL::SigSpec sigs = it->first;
@@ -360,11 +336,13 @@ void ILANG_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Modu
 
 void ILANG_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n)
 {
+#ifndef NDEBUG
 	int init_autoidx = autoidx;
+#endif
 
 	if (!flag_m) {
 		int count_selected_mods = 0;
-		for (auto it = design->modules_.begin(); it != design->modules_.end(); it++) {
+		for (auto it = design->modules_.begin(); it != design->modules_.end(); ++it) {
 			if (design->selected_whole_module(it->first))
 				flag_m = true;
 			if (design->selected(it->second))
@@ -380,7 +358,7 @@ void ILANG_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool onl
 		f << stringf("autoidx %d\n", autoidx);
 	}
 
-	for (auto it = design->modules_.begin(); it != design->modules_.end(); it++) {
+	for (auto it = design->modules_.begin(); it != design->modules_.end(); ++it) {
 		if (!only_selected || design->selected(it->second)) {
 			if (only_selected)
 				f << stringf("\n");
@@ -391,6 +369,9 @@ void ILANG_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool onl
 	log_assert(init_autoidx == autoidx);
 }
 
+YOSYS_NAMESPACE_END
+PRIVATE_NAMESPACE_BEGIN
+
 struct IlangBackend : public Backend {
 	IlangBackend() : Backend("ilang", "write design to ilang file") { }
 	virtual void help()
@@ -423,6 +404,8 @@ struct IlangBackend : public Backend {
 		}
 		extra_args(f, filename, args, argidx);
 
+		design->sort();
+
 		log("Output filename: %s\n", filename.c_str());
 		*f << stringf("# Generated by %s\n", yosys_version_str);
 		ILANG_BACKEND::dump_design(*f, design, selected, true, false);
@@ -447,10 +430,10 @@ struct DumpPass : public Pass {
 		log("    -n\n");
 		log("        only dump the module headers if the entire module is selected\n");
 		log("\n");
-		log("    -outfile <filename>\n");
+		log("    -o <filename>\n");
 		log("        write to the specified file.\n");
 		log("\n");
-		log("    -append <filename>\n");
+		log("    -a <filename>\n");
 		log("        like -outfile but append instead of overwrite\n");
 		log("\n");
 	}
@@ -463,12 +446,12 @@ struct DumpPass : public Pass {
 		for (argidx = 1; argidx < args.size(); argidx++)
 		{
 			std::string arg = args[argidx];
-			if (arg == "-outfile" && argidx+1 < args.size()) {
+			if ((arg == "-o" || arg == "-outfile") && argidx+1 < args.size()) {
 				filename = args[++argidx];
 				append = false;
 				continue;
 			}
-			if (arg == "-append" && argidx+1 < args.size()) {
+			if ((arg == "-a" || arg == "-append") && argidx+1 < args.size()) {
 				filename = args[++argidx];
 				append = true;
 				continue;
@@ -510,3 +493,4 @@ struct DumpPass : public Pass {
 	}
 } DumpPass;
  
+PRIVATE_NAMESPACE_END
diff --git a/backends/intersynth/intersynth.cc b/backends/intersynth/intersynth.cc
index 8502d90fc..6d4731e73 100644
--- a/backends/intersynth/intersynth.cc
+++ b/backends/intersynth/intersynth.cc
@@ -24,6 +24,8 @@
 #include "kernel/log.h"
 #include <string>
 
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
 
 static std::string netname(std::set<std::string> &conntypes_code, std::set<std::string> &celltypes_code, std::set<std::string> &constcells_code, RTLIL::SigSpec sig)
 {
@@ -215,3 +217,4 @@ struct IntersynthBackend : public Backend {
 	}
 } IntersynthBackend;
 
+PRIVATE_NAMESPACE_END
diff --git a/backends/json/Makefile.inc b/backends/json/Makefile.inc
new file mode 100644
index 000000000..a463daf91
--- /dev/null
+++ b/backends/json/Makefile.inc
@@ -0,0 +1,3 @@
+
+OBJS += backends/json/json.o
+
diff --git a/backends/json/json.cc b/backends/json/json.cc
new file mode 100644
index 000000000..7d73fb11d
--- /dev/null
+++ b/backends/json/json.cc
@@ -0,0 +1,407 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *  
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *  
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/rtlil.h"
+#include "kernel/register.h"
+#include "kernel/sigtools.h"
+#include "kernel/celltypes.h"
+#include "kernel/log.h"
+#include <string>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct JsonWriter
+{
+	std::ostream &f;
+	bool use_selection;
+
+	Design *design;
+	Module *module;
+
+	SigMap sigmap;
+	int sigidcounter;
+	dict<SigBit, string> sigids;
+
+	JsonWriter(std::ostream &f, bool use_selection) : f(f), use_selection(use_selection) { }
+
+	string get_string(string str)
+	{
+		string newstr = "\"";
+		for (char c : str) {
+			if (c == '\\')
+				newstr += c;
+			newstr += c;
+		}
+		return newstr + "\"";
+	}
+
+	string get_name(IdString name)
+	{
+		return get_string(RTLIL::unescape_id(name));
+	}
+
+	string get_bits(SigSpec sig)
+	{
+		bool first = true;
+		string str = "[";
+		for (auto bit : sigmap(sig)) {
+			str += first ? " " : ", ";
+			first = false;
+			if (sigids.count(bit) == 0) {
+				string &s = sigids[bit];
+				if (bit.wire == nullptr) {
+					if (bit == State::S0) s = "\"0\"";
+					else if (bit == State::S1) s = "\"1\"";
+					else if (bit == State::Sz) s = "\"z\"";
+					else s = "\"x\"";
+				} else
+					s = stringf("%d", sigidcounter++);
+			}
+			str += sigids[bit];
+		}
+		return str + " ]";
+	}
+
+	void write_parameters(const dict<IdString, Const> &parameters)
+	{
+		bool first = true;
+		for (auto &param : parameters) {
+			f << stringf("%s\n", first ? "" : ",");
+			f << stringf("            %s: ", get_name(param.first).c_str());
+			if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0)
+				f << get_string(param.second.decode_string());
+			else if (GetSize(param.second.bits) > 32)
+				f << get_string(param.second.as_string());
+			else
+				f << stringf("%d", param.second.as_int());
+			first = false;
+		}
+	}
+
+	void write_module(Module *module_)
+	{
+		module = module_;
+		log_assert(module->design == design);
+		sigmap.set(module);
+		sigids.clear();
+
+		// reserve 0 and 1 to avoid confusion with "0" and "1"
+		sigidcounter = 2;
+
+		f << stringf("    %s: {\n", get_name(module->name).c_str());
+
+		f << stringf("      \"ports\": {");
+		bool first = true;
+		for (auto n : module->ports) {
+			Wire *w = module->wire(n);
+			if (use_selection && !module->selected(w))
+				continue;
+			f << stringf("%s\n", first ? "" : ",");
+			f << stringf("        %s: {\n", get_name(n).c_str());
+			f << stringf("          \"direction\": \"%s\",\n", w->port_input ? w->port_output ? "inout" : "input" : "output");
+			f << stringf("          \"bits\": %s\n", get_bits(w).c_str());
+			f << stringf("        }");
+			first = false;
+		}
+		f << stringf("\n      },\n");
+
+		f << stringf("      \"cells\": {");
+		first = true;
+		for (auto c : module->cells()) {
+			if (use_selection && !module->selected(c))
+				continue;
+			f << stringf("%s\n", first ? "" : ",");
+			f << stringf("        %s: {\n", get_name(c->name).c_str());
+			f << stringf("          \"hide_name\": %s,\n", c->name[0] == '$' ? "1" : "0");
+			f << stringf("          \"type\": %s,\n", get_name(c->type).c_str());
+			f << stringf("          \"parameters\": {");
+			write_parameters(c->parameters);
+			f << stringf("\n          },\n");
+			f << stringf("          \"attributes\": {");
+			write_parameters(c->attributes);
+			f << stringf("\n          },\n");
+			f << stringf("          \"connections\": {");
+			bool first2 = true;
+			for (auto &conn : c->connections()) {
+				f << stringf("%s\n", first2 ? "" : ",");
+				f << stringf("            %s: %s", get_name(conn.first).c_str(), get_bits(conn.second).c_str());
+				first2 = false;
+			}
+			f << stringf("\n          }\n");
+			f << stringf("        }");
+			first = false;
+		}
+		f << stringf("\n      },\n");
+
+		f << stringf("      \"netnames\": {");
+		first = true;
+		for (auto w : module->wires()) {
+			if (use_selection && !module->selected(w))
+				continue;
+			f << stringf("%s\n", first ? "" : ",");
+			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());
+			f << stringf("          \"attributes\": {");
+			write_parameters(w->attributes);
+			f << stringf("\n          }\n");
+			f << stringf("        }");
+			first = false;
+		}
+		f << stringf("\n      }\n");
+
+		f << stringf("    }");
+	}
+
+	void write_design(Design *design_)
+	{
+		design = design_;
+		f << stringf("{\n");
+		f << stringf("  \"creator\": %s,\n", get_string(yosys_version_str).c_str());
+		f << stringf("  \"modules\": {\n");
+		vector<Module*> modules = use_selection ? design->selected_modules() : design->modules();
+		bool first_module = true;
+		for (auto mod : modules) {
+			if (!first_module)
+				f << stringf(",\n");
+			write_module(mod);
+			first_module = false;
+		}
+		f << stringf("\n  }\n");
+		f << stringf("}\n");
+	}
+};
+
+struct JsonBackend : public Backend {
+	JsonBackend() : Backend("json", "write design to a JSON file") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    write_json [options] [filename]\n");
+		log("\n");
+		log("Write a JSON netlist of the current design.\n");
+		log("\n");
+		log("The general syntax of the JSON output created by this command is as follows:\n");
+		log("\n");
+		log("    {\n");
+		log("      \"modules\": {\n");
+		log("        <module_name>: {\n");
+		log("          \"ports\": {\n");
+		log("            <port_name>: <port_details>,\n");
+		log("            ...\n");
+		log("          },\n");
+		log("          \"cells\": {\n");
+		log("            <cell_name>: <cell_details>,\n");
+		log("            ...\n");
+		log("          },\n");
+		log("          \"netnames\": {\n");
+		log("            <net_name>: <net_details>,\n");
+		log("            ...\n");
+		log("          }\n");
+		log("        }\n");
+		log("      }\n");
+		log("    }\n");
+		log("\n");
+		log("Where <port_details> is:\n");
+		log("\n");
+		log("    {\n");
+		log("      \"direction\": <\"input\" | \"output\" | \"inout\">,\n");
+		log("      \"bits\": <bit_vector>\n");
+		log("    }\n");
+		log("\n");
+		log("And <cell_details> is:\n");
+		log("\n");
+		log("    {\n");
+		log("      \"hide_name\": <1 | 0>,\n");
+		log("      \"type\": <cell_type>,\n");
+		log("      \"parameters\": {\n");
+		log("        <parameter_name>: <parameter_value>,\n");
+		log("        ...\n");
+		log("      },\n");
+		log("      \"attributes\": {\n");
+		log("        <attribute_name>: <attribute_value>,\n");
+		log("        ...\n");
+		log("      },\n");
+		log("      \"connections\": {\n");
+		log("        <port_name>: <bit_vector>,\n");
+		log("        ...\n");
+		log("      },\n");
+		log("    }\n");
+		log("\n");
+		log("And <net_details> is:\n");
+		log("\n");
+		log("    {\n");
+		log("      \"hide_name\": <1 | 0>,\n");
+		log("      \"bits\": <bit_vector>\n");
+		log("    }\n");
+		log("\n");
+		log("The \"hide_name\" fields are set to 1 when the name of this cell or net is\n");
+		log("automatically created and is likely not of interest for a regular user.\n");
+		log("\n");
+		log("Module and cell ports and nets can be single bit wide or vectors of multiple\n");
+		log("bits. Each individual signal bit is assigned a unique integer. The <bit_vector>\n");
+		log("values referenced above are vectors of this integers. Signal bits that are\n");
+		log("connected to a constant driver are denoted as string \"0\" or \"1\" instead of\n");
+		log("a number.\n");
+		log("\n");
+		log("For example the following verilog code:\n");
+		log("\n");
+		log("    module test(input x, y);\n");
+		log("      (* keep *) foo #(.P(42), .Q(1337))\n");
+		log("          foo_inst (.A({x, y}), .B({y, x}), .C({4'd10, {4{x}}}));\n");
+		log("    endmodule\n");
+		log("\n");
+		log("Translates to the following JSON output:\n");
+		log("\n");
+		log("    {\n");
+		log("      \"modules\": {\n");
+		log("        \"test\": {\n");
+		log("          \"ports\": {\n");
+		log("            \"x\": {\n");
+		log("              \"direction\": \"input\",\n");
+		log("              \"bits\": [ 2 ]\n");
+		log("            },\n");
+		log("            \"y\": {\n");
+		log("              \"direction\": \"input\",\n");
+		log("              \"bits\": [ 3 ]\n");
+		log("            }\n");
+		log("          },\n");
+		log("          \"cells\": {\n");
+		log("            \"foo_inst\": {\n");
+		log("              \"hide_name\": 0,\n");
+		log("              \"type\": \"foo\",\n");
+		log("              \"parameters\": {\n");
+		log("                \"Q\": 1337,\n");
+		log("                \"P\": 42\n");
+		log("              },\n");
+		log("              \"attributes\": {\n");
+		log("                \"keep\": 1,\n");
+		log("                \"src\": \"test.v:2\"\n");
+		log("              },\n");
+		log("              \"connections\": {\n");
+		log("                \"C\": [ 2, 2, 2, 2, \"0\", \"1\", \"0\", \"1\" ],\n");
+		log("                \"B\": [ 2, 3 ],\n");
+		log("                \"A\": [ 3, 2 ]\n");
+		log("              }\n");
+		log("            }\n");
+		log("          },\n");
+		log("          \"netnames\": {\n");
+		log("            \"y\": {\n");
+		log("              \"hide_name\": 0,\n");
+		log("              \"bits\": [ 3 ],\n");
+		log("              \"attributes\": {\n");
+		log("                \"src\": \"test.v:1\"\n");
+		log("              }\n");
+		log("            },\n");
+		log("            \"x\": {\n");
+		log("              \"hide_name\": 0,\n");
+		log("              \"bits\": [ 2 ],\n");
+		log("              \"attributes\": {\n");
+		log("                \"src\": \"test.v:1\"\n");
+		log("              }\n");
+		log("            }\n");
+		log("          }\n");
+		log("        }\n");
+		log("      }\n");
+		log("    }\n");
+		log("\n");
+		log("Future version of Yosys might add support for additional fields in the JSON\n");
+		log("format. A program processing this format must ignore all unkown fields.\n");
+		log("\n");
+	}
+	virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+	{
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			// if (args[argidx] == "-verbose") {
+			// 	verbose = true;
+			// 	continue;
+			// }
+			break;
+		}
+		extra_args(f, filename, args, argidx);
+
+		log_header("Executing JSON backend.\n");
+
+		JsonWriter json_writer(*f, false);
+		json_writer.write_design(design);
+	}
+} JsonBackend;
+
+struct JsonPass : public Pass {
+	JsonPass() : Pass("json", "write design in JSON format") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    json [options] [selection]\n");
+		log("\n");
+		log("Write a JSON netlist of all selected objects.\n");
+		log("\n");
+		log("    -o <filename>\n");
+		log("        write to the specified file.\n");
+		log("\n");
+		log("See 'help write_json' for a description of the JSON format used.\n");
+		log("\n");
+	}
+	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+	{
+		std::string filename;
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			if (args[argidx] == "-o" && argidx+1 < args.size()) {
+				filename = args[++argidx];
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
+
+		std::ostream *f;
+		std::stringstream buf;
+
+		if (!filename.empty()) {
+			std::ofstream *ff = new std::ofstream;
+			ff->open(filename.c_str(), std::ofstream::trunc);
+			if (ff->fail()) {
+				delete ff;
+				log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
+			}
+			f = ff;
+		} else {
+			f = &buf;
+		}
+
+		JsonWriter json_writer(*f, true);
+		json_writer.write_design(design);
+
+		if (!filename.empty()) {
+			delete f;
+		} else {
+			log("%s", buf.str().c_str());
+		}
+	}
+} JsonPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/backends/smt2/.gitignore b/backends/smt2/.gitignore
new file mode 100644
index 000000000..313ea0a1a
--- /dev/null
+++ b/backends/smt2/.gitignore
@@ -0,0 +1 @@
+test_cells
diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
new file mode 100644
index 000000000..4e0a393a8
--- /dev/null
+++ b/backends/smt2/Makefile.inc
@@ -0,0 +1,3 @@
+
+OBJS += backends/smt2/smt2.o
+
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
new file mode 100644
index 000000000..3d872c63a
--- /dev/null
+++ b/backends/smt2/smt2.cc
@@ -0,0 +1,711 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *  
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *  
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/rtlil.h"
+#include "kernel/register.h"
+#include "kernel/sigtools.h"
+#include "kernel/celltypes.h"
+#include "kernel/log.h"
+#include <string>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct Smt2Worker
+{
+	CellTypes ct;
+	SigMap sigmap;
+	RTLIL::Module *module;
+	bool bvmode, verbose;
+	int idcounter;
+
+	std::vector<std::string> decls, trans;
+	std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
+	std::set<RTLIL::Cell*> exported_cells;
+	pool<Cell*> recursive_cells, registers;
+
+	std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
+	std::map<int, int> bvsizes;
+
+	Smt2Worker(RTLIL::Module *module, bool bvmode, bool verbose) :
+			ct(module->design), sigmap(module), module(module), bvmode(bvmode), verbose(verbose), idcounter(0)
+	{
+		decls.push_back(stringf("(declare-sort |%s_s| 0)\n", log_id(module)));
+
+		for (auto cell : module->cells())
+		for (auto &conn : cell->connections()) {
+			bool is_input = ct.cell_input(cell->type, conn.first);
+			bool is_output = ct.cell_output(cell->type, conn.first);
+			if (is_output && !is_input)
+				for (auto bit : sigmap(conn.second)) {
+					if (bit_driver.count(bit))
+						log_error("Found multiple drivers for %s.\n", log_signal(bit));
+					bit_driver[bit] = cell;
+				}
+			else if (is_output || !is_input)
+				log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n",
+						log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type));
+		}
+	}
+
+	void register_bool(RTLIL::SigBit bit, int id)
+	{
+		if (verbose) log("%*s-> register_bool: %s %d\n", 2+2*GetSize(recursive_cells), "",
+				log_signal(bit), id);
+
+		sigmap.apply(bit);
+		log_assert(fcache.count(bit) == 0);
+		fcache[bit] = std::pair<int, int>(id, -1);
+	}
+
+	void register_bv(RTLIL::SigSpec sig, int id)
+	{
+		if (verbose) log("%*s-> register_bv: %s %d\n", 2+2*GetSize(recursive_cells), "",
+				log_signal(sig), id);
+
+		log_assert(bvmode);
+		sigmap.apply(sig);
+
+		log_assert(bvsizes.count(id) == 0);
+		bvsizes[id] = GetSize(sig);
+
+		for (int i = 0; i < GetSize(sig); i++) {
+			log_assert(fcache.count(sig[i]) == 0);
+			fcache[sig[i]] = std::pair<int, int>(id, i);
+		}
+	}
+
+	void register_boolvec(RTLIL::SigSpec sig, int id)
+	{
+		if (verbose) log("%*s-> register_boolvec: %s %d\n", 2+2*GetSize(recursive_cells), "",
+				log_signal(sig), id);
+
+		log_assert(bvmode);
+		sigmap.apply(sig);
+		register_bool(sig[0], id);
+
+		for (int i = 1; i < GetSize(sig); i++)
+			sigmap.add(sig[i], RTLIL::State::S0);
+	}
+
+	std::string get_bool(RTLIL::SigBit bit, const char *state_name = "state")
+	{
+		sigmap.apply(bit);
+
+		if (bit.wire == nullptr)
+			return bit == RTLIL::State::S1 ? "true" : "false";
+
+		if (bit_driver.count(bit))
+			export_cell(bit_driver.at(bit));
+		sigmap.apply(bit);
+
+		if (fcache.count(bit) == 0) {
+			if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "",
+					log_signal(bit));
+			decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
+					log_id(module), idcounter, log_id(module), log_signal(bit)));
+			register_bool(bit, idcounter++);
+		}
+
+		auto f = fcache.at(bit);
+		if (f.second >= 0)
+			return stringf("(= ((_ extract %d %d) (|%s#%d| %s)) #b1)", f.second, f.second, log_id(module), f.first, state_name);
+		return stringf("(|%s#%d| %s)", log_id(module), f.first, state_name);
+	}
+
+	std::string get_bool(RTLIL::SigSpec sig, const char *state_name = "state")
+	{
+		return get_bool(sig.to_single_sigbit(), state_name);
+	}
+
+	std::string get_bv(RTLIL::SigSpec sig, const char *state_name = "state")
+	{
+		log_assert(bvmode);
+		sigmap.apply(sig);
+
+		std::vector<std::string> subexpr;
+
+		SigSpec orig_sig;
+		while (orig_sig != sig) {
+			for (auto bit : sig)
+				if (bit_driver.count(bit))
+					export_cell(bit_driver.at(bit));
+			orig_sig = sig;
+			sigmap.apply(sig);
+		}
+
+		for (int i = 0, j = 1; i < GetSize(sig); i += j, j = 1)
+		{
+			if (sig[i].wire == nullptr) {
+				while (i+j < GetSize(sig) && sig[i+j].wire == nullptr) j++;
+				subexpr.push_back("#b");
+				for (int k = i+j-1; k >= i; k--)
+					subexpr.back() += sig[k] == RTLIL::State::S1 ? "1" : "0";
+				continue;
+			}
+
+			if (fcache.count(sig[i]) && fcache.at(sig[i]).second == -1) {
+				subexpr.push_back(stringf("(ite %s #b1 #b0)", get_bool(sig[i], state_name).c_str()));
+				continue;
+			}
+
+			if (fcache.count(sig[i])) {
+				auto t1 = fcache.at(sig[i]);
+				while (i+j < GetSize(sig)) {
+					if (fcache.count(sig[i+j]) == 0)
+						break;
+					auto t2 = fcache.at(sig[i+j]);
+					if (t1.first != t2.first)
+						break;
+					if (t1.second+j != t2.second)
+						break;
+					j++;
+				}
+				if (t1.second == 0 && j == bvsizes.at(t1.first))
+					subexpr.push_back(stringf("(|%s#%d| %s)", log_id(module), t1.first, state_name));
+				else
+					subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| %s))",
+							t1.second + j - 1, t1.second, log_id(module), t1.first, state_name));
+				continue;
+			}
+
+			std::set<RTLIL::SigBit> seen_bits = { sig[i] };
+			while (i+j < GetSize(sig) && sig[i+j].wire && !fcache.count(sig[i+j]) && !seen_bits.count(sig[i+j]))
+				seen_bits.insert(sig[i+j]), j++;
+
+			if (verbose) log("%*s-> external bv: %s\n", 2+2*GetSize(recursive_cells), "",
+					log_signal(sig.extract(i, j)));
+			for (auto bit : sig.extract(i, j))
+				log_assert(bit_driver.count(bit) == 0);
+			decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
+					log_id(module), idcounter, log_id(module), j, log_signal(sig.extract(i, j))));
+			subexpr.push_back(stringf("(|%s#%d| %s)", log_id(module), idcounter, state_name));
+			register_bv(sig.extract(i, j), idcounter++);
+		}
+
+		if (GetSize(subexpr) > 1) {
+			std::string expr = "(concat";
+			for (int i = GetSize(subexpr)-1; i >= 0; i--)
+				expr += " " + subexpr[i];
+			return expr + ")";
+		} else {
+			log_assert(GetSize(subexpr) == 1);
+			return subexpr[0];
+		}
+	}
+
+	void export_gate(RTLIL::Cell *cell, std::string expr)
+	{
+		RTLIL::SigBit bit = sigmap(cell->getPort("\\Y").to_single_sigbit());
+		std::string processed_expr;
+
+		for (char ch : expr) {
+			if (ch == 'A') processed_expr += get_bool(cell->getPort("\\A"));
+			else if (ch == 'B') processed_expr += get_bool(cell->getPort("\\B"));
+			else if (ch == 'C') processed_expr += get_bool(cell->getPort("\\C"));
+			else if (ch == 'D') processed_expr += get_bool(cell->getPort("\\D"));
+			else if (ch == 'S') processed_expr += get_bool(cell->getPort("\\S"));
+			else processed_expr += ch;
+		}
+
+		if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+				log_id(cell));
+		decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
+				log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(bit)));
+		register_bool(bit, idcounter++);
+		recursive_cells.erase(cell);
+	}
+
+	void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0)
+	{
+		RTLIL::SigSpec sig_a, sig_b;
+		RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y"));
+		bool is_signed = cell->getParam("\\A_SIGNED").as_bool();
+		int width = GetSize(sig_y);
+
+		if (type == 's' || type == 'd' || type == 'b') {
+			width = std::max(width, GetSize(cell->getPort("\\A")));
+			width = std::max(width, GetSize(cell->getPort("\\B")));
+		}
+
+		if (cell->hasPort("\\A")) {
+			sig_a = cell->getPort("\\A");
+			sig_a.extend_u0(width, is_signed);
+		}
+
+		if (cell->hasPort("\\B")) {
+			sig_b = cell->getPort("\\B");
+			sig_b.extend_u0(width, is_signed && !(type == 's'));
+		}
+
+		std::string processed_expr;
+
+		for (char ch : expr) {
+			if (ch == 'A') processed_expr += get_bv(sig_a);
+			else if (ch == 'B') processed_expr += get_bv(sig_b);
+			else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
+			else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
+			else processed_expr += ch;
+		}
+
+		if (width != GetSize(sig_y) && type != 'b')
+			processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str());
+
+		if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+				log_id(cell));
+
+		if (type == 'b') {
+			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
+					log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(sig_y)));
+			register_boolvec(sig_y, idcounter++);
+		} else {
+			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+					log_id(module), idcounter, log_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y)));
+			register_bv(sig_y, idcounter++);
+		}
+
+		recursive_cells.erase(cell);
+	}
+
+	void export_reduce(RTLIL::Cell *cell, std::string expr, bool identity_val)
+	{
+		RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y"));
+		std::string processed_expr;
+
+		for (char ch : expr)
+			if (ch == 'A' || ch == 'B') {
+				RTLIL::SigSpec sig = sigmap(cell->getPort(stringf("\\%c", ch)));
+				for (auto bit : sig)
+					processed_expr += " " + get_bool(bit);
+				if (GetSize(sig) == 1)
+					processed_expr += identity_val ? " true" : " false";
+			} else
+				processed_expr += ch;
+
+		if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+				log_id(cell));
+		decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
+				log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(sig_y)));
+		register_boolvec(sig_y, idcounter++);
+		recursive_cells.erase(cell);
+	}
+
+	void export_cell(RTLIL::Cell *cell)
+	{
+		if (verbose) log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "",
+				log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new");
+
+		if (recursive_cells.count(cell))
+			log_error("Found logic loop in module %s! See cell %s.\n", log_id(module), log_id(cell));
+
+		if (exported_cells.count(cell))
+			return;
+		exported_cells.insert(cell);
+		recursive_cells.insert(cell);
+
+		if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
+		{
+			registers.insert(cell);
+			decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
+					log_id(module), idcounter, log_id(module), log_signal(cell->getPort("\\Q"))));
+			register_bool(cell->getPort("\\Q"), idcounter++);
+			recursive_cells.erase(cell);
+			return;
+		}
+
+		if (cell->type == "$_BUF_") return export_gate(cell, "A");
+		if (cell->type == "$_NOT_") return export_gate(cell, "(not A)");
+		if (cell->type == "$_AND_") return export_gate(cell, "(and A B)");
+		if (cell->type == "$_NAND_") return export_gate(cell, "(not (and A B))");
+		if (cell->type == "$_OR_") return export_gate(cell, "(or A B)");
+		if (cell->type == "$_NOR_") return export_gate(cell, "(not (or A B))");
+		if (cell->type == "$_XOR_") return export_gate(cell, "(xor A B)");
+		if (cell->type == "$_XNOR_") return export_gate(cell, "(not (xor A B))");
+		if (cell->type == "$_MUX_") return export_gate(cell, "(ite S B A)");
+		if (cell->type == "$_AOI3_") return export_gate(cell, "(not (or (and A B) C))");
+		if (cell->type == "$_OAI3_") return export_gate(cell, "(not (and (or A B) C))");
+		if (cell->type == "$_AOI4_") return export_gate(cell, "(not (or (and A B) (and C D)))");
+		if (cell->type == "$_OAI4_") return export_gate(cell, "(not (and (or A B) (or C D)))");
+
+		// FIXME: $lut
+
+		if (!bvmode)
+			log_error("Unsupported cell type %s for cell %s.%s. (Maybe this cell type would be supported in -bv mode?)\n",
+					log_id(cell->type), log_id(module), log_id(cell));
+
+		if (cell->type == "$dff")
+		{
+			registers.insert(cell);
+			decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
+					log_id(module), idcounter, log_id(module), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q"))));
+			register_bv(cell->getPort("\\Q"), idcounter++);
+			recursive_cells.erase(cell);
+			return;
+		}
+
+		if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
+		if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
+		if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
+		if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)");
+
+		if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's');
+		if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's');
+		if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's');
+		if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's');
+
+		// FIXME: $shift $shiftx
+
+		if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b');
+		if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b');
+		if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b');
+		if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b');
+
+		if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b');
+		if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b');
+		if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b');
+		if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b');
+
+		if (cell->type == "$not") return export_bvop(cell, "(bvnot A)");
+		if (cell->type == "$pos") return export_bvop(cell, "A");
+		if (cell->type == "$neg") return export_bvop(cell, "(bvneg A)");
+
+		if (cell->type == "$add") return export_bvop(cell, "(bvadd A B)");
+		if (cell->type == "$sub") return export_bvop(cell, "(bvsub A B)");
+		if (cell->type == "$mul") return export_bvop(cell, "(bvmul A B)");
+		if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
+		if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');
+
+		if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
+		if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
+		if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);
+		if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false);
+		if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false);
+
+		if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false);
+		if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
+		if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);
+
+		if (cell->type == "$mux" || cell->type == "$pmux")
+		{
+			int width = GetSize(cell->getPort("\\Y"));
+			std::string processed_expr = get_bv(cell->getPort("\\A"));
+
+			RTLIL::SigSpec sig_b = cell->getPort("\\B");
+			RTLIL::SigSpec sig_s = cell->getPort("\\S");
+			get_bv(sig_b);
+			get_bv(sig_s);
+
+			for (int i = 0; i < GetSize(sig_s); i++)
+				processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
+						get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());
+
+			if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+					log_id(cell));
+			RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
+			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+					log_id(module), idcounter, log_id(module), width, processed_expr.c_str(), log_signal(sig)));
+			register_bv(sig, idcounter++);
+			recursive_cells.erase(cell);
+			return;
+		}
+
+		// FIXME: $slice $concat
+
+		log_error("Unsupported cell type %s for cell %s.%s.\n",
+				log_id(cell->type), log_id(module), log_id(cell));
+	}
+
+	void run()
+	{
+		if (verbose) log("=> export logic driving outputs\n");
+
+		for (auto wire : module->wires())
+			if (wire->port_id || wire->get_bool_attribute("\\keep")) {
+				RTLIL::SigSpec sig = sigmap(wire);
+				if (bvmode && GetSize(sig) > 1) {
+					decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
+							log_id(module), log_id(wire), log_id(module), GetSize(sig), get_bv(sig).c_str()));
+				} else {
+					for (int i = 0; i < GetSize(sig); i++)
+						if (GetSize(sig) > 1)
+							decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
+									log_id(module), log_id(wire), i, log_id(module), get_bool(sig[i]).c_str()));
+						else
+							decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
+									log_id(module), log_id(wire), log_id(module), get_bool(sig[i]).c_str()));
+				}
+			}
+
+		if (verbose) log("=> export logic associated with the initial state\n");
+
+		vector<string> init_list;
+		for (auto wire : module->wires())
+			if (wire->attributes.count("\\init")) {
+				RTLIL::SigSpec sig = sigmap(wire);
+				Const val = wire->attributes.at("\\init");
+				val.bits.resize(GetSize(sig));
+				if (bvmode && GetSize(sig) > 1) {
+					init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), log_id(wire)));
+				} else {
+					for (int i = 0; i < GetSize(sig); i++)
+						init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val.bits[i] == State::S1 ? "true" : "false", log_id(wire)));
+				}
+			}
+
+		if (verbose) log("=> export logic driving asserts\n");
+
+		vector<int> assert_list, assume_list;
+		for (auto cell : module->cells())
+			if (cell->type.in("$assert", "$assume")) {
+				string name_a = get_bool(cell->getPort("\\A"));
+				string name_en = get_bool(cell->getPort("\\EN"));
+				decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
+					log_id(module), idcounter, log_id(module), name_a.c_str(), name_en.c_str(), log_id(cell)));
+				if (cell->type == "$assert")
+					assert_list.push_back(idcounter++);
+				else
+					assume_list.push_back(idcounter++);
+			}
+
+		for (int iter = 1; !registers.empty(); iter++)
+		{
+			pool<Cell*> this_regs;
+			this_regs.swap(registers);
+
+			if (verbose) log("=> export logic driving registers [iteration %d]\n", iter);
+
+			for (auto cell : this_regs) {
+				if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_") {
+					std::string expr_d = get_bool(cell->getPort("\\D"));
+					std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
+					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell), log_signal(cell->getPort("\\Q"))));
+				}
+				if (cell->type == "$dff") {
+					std::string expr_d = get_bv(cell->getPort("\\D"));
+					std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
+					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell), log_signal(cell->getPort("\\Q"))));
+				}
+			}
+		}
+
+		string assert_expr = assert_list.empty() ? "true" : "(and";
+		if (!assert_list.empty()) {
+			for (int i : assert_list)
+				assert_expr += stringf(" (|%s#%d| state)", log_id(module), i);
+			assert_expr += ")";
+		}
+		decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n",
+				log_id(module), log_id(module), assert_expr.c_str()));
+
+		string assume_expr = assume_list.empty() ? "true" : "(and";
+		if (!assume_list.empty()) {
+			for (int i : assume_list)
+				assume_expr += stringf(" (|%s#%d| state)", log_id(module), i);
+			assume_expr += ")";
+		}
+		decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n",
+				log_id(module), log_id(module), assume_expr.c_str()));
+
+		string init_expr = init_list.empty() ? "true" : "(and";
+		if (!init_list.empty()) {
+			for (auto &str : init_list)
+				init_expr += stringf("\n\t%s", str.c_str());
+			init_expr += "\n)";
+		}
+		decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\n",
+				log_id(module), log_id(module), init_expr.c_str()));
+	}
+
+	void write(std::ostream &f)
+	{
+		for (auto it : decls)
+			f << it;
+
+		f << stringf("(define-fun |%s_t| ((state |%s_s|) (next_state |%s_s|)) Bool ", log_id(module), log_id(module), log_id(module));
+		if (GetSize(trans) > 1) {
+			f << "(and\n";
+			for (auto it : trans)
+				f << it;
+			f << "))";
+		} else
+		if (GetSize(trans) == 1)
+			f << "\n" + trans.front() + ")";
+		else
+			f << "true)";
+		f << stringf(" ; end of module %s\n", log_id(module));
+	}
+};
+
+struct Smt2Backend : public Backend {
+	Smt2Backend() : Backend("smt2", "write design to SMT-LIBv2 file") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    write_smt2 [options] [filename]\n");
+		log("\n");
+		log("Write a SMT-LIBv2 [1] description of the current design. For a module with name\n");
+		log("'<mod>' this will declare the sort '<mod>_s' (state of the module) and the\n");
+		log("functions operating on that state.\n");
+		log("\n");
+		log("The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions\n");
+		log("are provided that can be used to access the values of the signals in the module.\n");
+		log("Only ports, and signals with the 'keep' attribute set are made available via\n");
+		log("such functions. Without the -bv option, multi-bit wires are exported as\n");
+		log("separate functions of type Bool for the individual bits. With the -bv option\n");
+		log("multi-bit wires are exported as single functions of type BitVec.\n");
+		log("\n");
+		log("The '<mod>_t' function evaluates to 'true' when the given pair of states\n");
+		log("describes a valid state transition.\n");
+		log("\n");
+		log("The '<mod>_a' function evaluates to 'true' when the given state satisfies\n");
+		log("the asserts in the module.\n");
+		log("\n");
+		log("The '<mod>_u' function evaluates to 'true' when the given state satisfies\n");
+		log("the assumptions in the module.\n");
+		log("\n");
+		log("The '<mod>_i' function evaluates to 'true' when the given state conforms\n");
+		log("to the initial state.\n");
+		log("\n");
+		log("    -verbose\n");
+		log("        this will print the recursive walk used to export the modules.\n");
+		log("\n");
+		log("    -bv\n");
+		log("        enable support for BitVec (FixedSizeBitVectors theory). with this\n");
+		log("        option set multi-bit wires are represented using the BitVec sort and\n");
+		log("        support for coarse grain cells (incl. arithmetic) is enabled.\n");
+		log("\n");
+		log("    -tpl <template_file>\n");
+		log("        use the given template file. the line containing only the token '%%%%'\n");
+		log("        is replaced with the regular output of this command.\n");
+		log("\n");
+		log("[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David\n");
+		log("R. Cok's tutorial: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf\n");
+		log("\n");
+		log("---------------------------------------------------------------------------\n");
+		log("\n");
+		log("Example:\n");
+		log("\n");
+		log("Consider the following module (test.v). We want to prove that the output can\n");
+		log("never transition from a non-zero value to a zero value.\n");
+		log("\n");
+		log("        module test(input clk, output reg [3:0] y);\n");
+		log("          always @(posedge clk)\n");
+		log("            y <= (y << 1) | ^y;\n");
+		log("        endmodule\n");
+		log("\n");
+		log("For this proof we create the following template (test.tpl).\n");
+		log("\n");
+		log("        ; we need QF_UFBV for this poof\n");
+		log("        (set-logic QF_UFBV)\n");
+		log("\n");
+		log("        ; insert the auto-generated code here\n");
+		log("        %%%%\n");
+		log("\n");
+		log("        ; declare two state variables s1 and s2\n");
+		log("        (declare-fun s1 () test_s)\n");
+		log("        (declare-fun s2 () test_s)\n");
+		log("\n");
+		log("        ; state s2 is the successor of state s1\n");
+		log("        (assert (test_t s1 s2))\n");
+		log("\n");
+		log("        ; we are looking for a model with y non-zero in s1\n");
+		log("        (assert (distinct (|test_n y| s1) #b0000))\n");
+		log("\n");
+		log("        ; we are looking for a model with y zero in s2\n");
+		log("        (assert (= (|test_n y| s2) #b0000))\n");
+		log("\n");
+		log("        ; is there such a model?\n");
+		log("        (check-sat)\n");
+		log("\n");
+		log("The following yosys script will create a 'test.smt2' file for our proof:\n");
+		log("\n");
+		log("        read_verilog test.v\n");
+		log("        hierarchy -check; proc; opt; check -assert\n");
+		log("        write_smt2 -bv -tpl test.tpl test.smt2\n");
+		log("\n");
+		log("Running 'cvc4 test.smt2' will print 'unsat' because y can never transition\n");
+		log("from non-zero to zero in the test design.\n");
+		log("\n");
+	}
+	virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+	{
+		std::ifstream template_f;
+		bool bvmode = false, verbose = false;
+
+		log_header("Executing SMT2 backend.\n");
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			if (args[argidx] == "-tpl" && argidx+1 < args.size()) {
+				template_f.open(args[++argidx]);
+				if (template_f.fail())
+					log_error("Can't open template file `%s'.\n", args[argidx].c_str());
+				continue;
+			}
+			if (args[argidx] == "-bv") {
+				bvmode = true;
+				continue;
+			}
+			if (args[argidx] == "-verbose") {
+				verbose = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(f, filename, args, argidx);
+
+		if (template_f.is_open()) {
+			std::string line;
+			while (std::getline(template_f, line)) {
+				int indent = 0;
+				while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
+					indent++;
+				if (line.substr(indent, 2) == "%%")
+					break;
+				*f << line << std::endl;
+			}
+		}
+
+		*f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_version_str);
+
+		for (auto module : design->modules())
+		{
+			if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn())
+				continue;
+
+			log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
+
+			Smt2Worker worker(module, bvmode, verbose);
+			worker.run();
+			worker.write(*f);
+		}
+
+		*f << stringf("; end of yosys output\n");
+
+		if (template_f.is_open()) {
+			std::string line;
+			while (std::getline(template_f, line))
+				*f << line << std::endl;
+		}
+	}
+} Smt2Backend;
+
+PRIVATE_NAMESPACE_END
diff --git a/backends/smt2/test_cells.sh b/backends/smt2/test_cells.sh
new file mode 100644
index 000000000..34adb7af3
--- /dev/null
+++ b/backends/smt2/test_cells.sh
@@ -0,0 +1,55 @@
+#!/bin/bash
+
+set -ex
+
+rm -rf test_cells
+mkdir test_cells
+cd test_cells
+
+../../../yosys -p 'test_cell -muxdiv -w test all /$alu /$macc /$fa /$lcu /$lut /$shift /$shiftx'
+
+cat > miter.tpl <<- EOT
+; #model# (set-option :produce-models true)
+(set-logic QF_UFBV)
+%%
+(declare-fun s () miter_s)
+(assert (|miter_n trigger| s))
+(check-sat)
+; #model# (get-value ((|miter_n in_A| s) (|miter_n in_B| s) (|miter_n gold_Y| s) (|miter_n gate_Y| s) (|miter_n trigger| s)))
+EOT
+
+for x in $(set +x; ls test_*.il | sort -R); do
+	x=${x%.il}
+	cat > $x.ys <<- EOT
+		read_ilang $x.il
+		copy gold gate
+
+		cd gate
+		techmap; opt; abc;;
+		cd ..
+
+		miter -equiv -flatten -make_outputs gold gate miter
+		hierarchy -check -top miter
+
+		dump
+		write_smt2 -bv -tpl miter.tpl $x.smt2
+	EOT
+	../../../yosys -q $x.ys
+	if ! cvc4 $x.smt2 > $x.result; then
+		cat $x.result
+		exit 1
+	fi
+	if ! grep unsat $x.result; then
+		echo "Proof failed! Extracting model..."
+		sed -i 's/^; #model# //' $x.smt2
+		cvc4 $x.smt2
+		exit 1
+	fi
+done
+
+set +x
+echo ""
+echo "  All tests passed."
+echo ""
+exit 0
+
diff --git a/backends/spice/spice.cc b/backends/spice/spice.cc
index b057063cd..2c614178b 100644
--- a/backends/spice/spice.cc
+++ b/backends/spice/spice.cc
@@ -24,6 +24,9 @@
 #include "kernel/log.h"
 #include <string>
 
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
 static void print_spice_net(std::ostream &f, RTLIL::SigBit s, std::string &neg, std::string &pos, std::string &ncpf, int &nc_counter)
 {
 	if (s.wire) {
@@ -55,7 +58,7 @@ static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::De
 
 		if (design->modules_.count(cell->type) == 0)
 		{
-			log("Warning: no (blackbox) module for cell type `%s' (%s.%s) found! Guessing order of ports.\n",
+			log_warning("no (blackbox) module for cell type `%s' (%s.%s) found! Guessing order of ports.\n",
 					RTLIL::id2cstr(cell->type), RTLIL::id2cstr(module->name), RTLIL::id2cstr(cell->name));
 			for (auto &conn : cell->connections()) {
 				RTLIL::SigSpec sig = sigmap(conn.second);
@@ -81,7 +84,7 @@ static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::De
 				RTLIL::SigSpec sig(RTLIL::State::Sz, wire->width);
 				if (cell->hasPort(wire->name)) {
 					sig = sigmap(cell->getPort(wire->name));
-					sig.extend(wire->width, false);
+					sig.extend_u0(wire->width, false);
 				}
 				port_sigs.push_back(sig);
 			}
@@ -231,3 +234,4 @@ struct SpiceBackend : public Backend {
 	}
 } SpiceBackend;
 
+PRIVATE_NAMESPACE_END
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index bbdbbbfaf..ba57e8814 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -26,7 +26,6 @@
  *
  */
 
-#include "verilog_backend.h"
 #include "kernel/register.h"
 #include "kernel/celltypes.h"
 #include "kernel/log.h"
@@ -35,7 +34,8 @@
 #include <set>
 #include <map>
 
-namespace {
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
 
 bool norename, noattr, attr2comment, noexpr;
 int auto_name_counter, auto_name_offset, auto_name_digits;
@@ -51,16 +51,17 @@ void reset_auto_counter_id(RTLIL::IdString id, bool may_rename)
 	if (*str == '$' && may_rename && !norename)
 		auto_name_map[id] = auto_name_counter++;
 
-	if (str[0] != '_' && str[1] != 0)
+	if (str[0] != '\\' || str[1] != '_' || str[2] == 0)
 		return;
-	for (int i = 0; str[i] != 0; i++) {
-		if (str[i] == '_')
+
+	for (int i = 2; str[i] != 0; i++) {
+		if (str[i] == '_' && str[i+1] == 0)
 			continue;
 		if (str[i] < '0' || str[i] > '9')
 			return;
 	}
 
-	int num = atoi(str+1);
+	int num = atoi(str+2);
 	if (num >= auto_name_offset)
 		auto_name_offset = num + 1;
 }
@@ -73,22 +74,22 @@ void reset_auto_counter(RTLIL::Module *module)
 
 	reset_auto_counter_id(module->name, false);
 
-	for (auto it = module->wires_.begin(); it != module->wires_.end(); it++)
+	for (auto it = module->wires_.begin(); it != module->wires_.end(); ++it)
 		reset_auto_counter_id(it->second->name, true);
 
-	for (auto it = module->cells_.begin(); it != module->cells_.end(); it++) {
+	for (auto it = module->cells_.begin(); it != module->cells_.end(); ++it) {
 		reset_auto_counter_id(it->second->name, true);
 		reset_auto_counter_id(it->second->type, false);
 	}
 
-	for (auto it = module->processes.begin(); it != module->processes.end(); it++)
+	for (auto it = module->processes.begin(); it != module->processes.end(); ++it)
 		reset_auto_counter_id(it->second->name, false);
 
 	auto_name_digits = 1;
 	for (size_t i = 10; i < auto_name_offset + auto_name_map.size(); i = i*10)
 		auto_name_digits++;
 
-	for (auto it = auto_name_map.begin(); it != auto_name_map.end(); it++)
+	for (auto it = auto_name_map.begin(); it != auto_name_map.end(); ++it)
 		log("  renaming `%s' to `_%0*d_'.\n", it->first.c_str(), auto_name_digits, auto_name_offset + it->second);
 }
 
@@ -150,7 +151,7 @@ bool is_reg_wire(RTLIL::SigSpec sig, std::string &reg_name)
 	return true;
 }
 
-void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool no_decimal = false, bool set_signed = false)
+void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool no_decimal = false, bool set_signed = false, bool escape_comment = false)
 {
 	if (width < 0)
 		width = data.bits.size() - offset;
@@ -166,7 +167,7 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
 				if (data.bits[i] == RTLIL::S1)
 					val |= 1 << (i - offset);
 			}
-			f << stringf("32'%sd%d", set_signed ? "s" : "", val);
+			f << stringf("32'%sd %d", set_signed ? "s" : "", val);
 		} else {
 	dump_bits:
 			f << stringf("%d'%sb", width, set_signed ? "s" : "");
@@ -198,6 +199,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
 				f << stringf("\\\"");
 			else if (str[i] == '\\')
 				f << stringf("\\\\");
+			else if (str[i] == '/' && escape_comment && i > 0 && str[i-1] == '*')
+				f << stringf("\\/");
 			else
 				f << str[i];
 		}
@@ -236,7 +239,7 @@ void dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig)
 		dump_sigchunk(f, sig.as_chunk());
 	} else {
 		f << stringf("{ ");
-		for (auto it = sig.chunks().rbegin(); it != sig.chunks().rend(); it++) {
+		for (auto it = sig.chunks().rbegin(); it != sig.chunks().rend(); ++it) {
 			if (it != sig.chunks().rbegin())
 				f << stringf(", ");
 			dump_sigchunk(f, *it, true);
@@ -245,14 +248,19 @@ void dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig)
 	}
 }
 
-void dump_attributes(std::ostream &f, std::string indent, std::map<RTLIL::IdString, RTLIL::Const> &attributes, char term = '\n')
+void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString, RTLIL::Const> &attributes, char term = '\n', bool modattr = false)
 {
 	if (noattr)
 		return;
-	for (auto it = attributes.begin(); it != attributes.end(); it++) {
+	for (auto it = attributes.begin(); it != attributes.end(); ++it) {
 		f << stringf("%s" "%s %s", indent.c_str(), attr2comment ? "/*" : "(*", id(it->first).c_str());
 		f << stringf(" = ");
-		dump_const(f, it->second);
+		if (modattr && (it->second == Const(0, 1) || it->second == Const(0)))
+			f << stringf(" 0 ");
+		else if (modattr && (it->second == Const(1, 1) || it->second == Const(1)))
+			f << stringf(" 1 ");
+		else
+			dump_const(f, it->second, -1, 0, false, false, attr2comment);
 		f << stringf(" %s%c", attr2comment ? "*/" : "*)", term);
 	}
 }
@@ -315,7 +323,7 @@ std::string cellname(RTLIL::Cell *cell)
 	if (!norename && cell->name[0] == '$' && reg_ct.count(cell->type) && cell->hasPort("\\Q"))
 	{
 		RTLIL::SigSpec sig = cell->getPort("\\Q");
-		if (SIZE(sig) != 1 || sig.is_fully_const())
+		if (GetSize(sig) != 1 || sig.is_fully_const())
 			goto no_special_reg_name;
 
 		RTLIL::Wire *wire = sig[0].wire;
@@ -663,10 +671,60 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
-	if (cell->type == "$dff" || cell->type == "$adff")
+	if (cell->type == "$dffsr")
+	{
+		SigSpec sig_clk = cell->getPort("\\CLK");
+		SigSpec sig_set = cell->getPort("\\SET");
+		SigSpec sig_clr = cell->getPort("\\CLR");
+		SigSpec sig_d = cell->getPort("\\D");
+		SigSpec sig_q = cell->getPort("\\Q");
+
+		int width = cell->parameters["\\WIDTH"].as_int();
+		bool pol_clk = cell->parameters["\\CLK_POLARITY"].as_bool();
+		bool pol_set = cell->parameters["\\SET_POLARITY"].as_bool();
+		bool pol_clr = cell->parameters["\\CLR_POLARITY"].as_bool();
+
+		std::string reg_name = cellname(cell);
+		bool out_is_reg_wire = is_reg_wire(sig_q, reg_name);
+
+		if (!out_is_reg_wire)
+			f << stringf("%s" "reg [%d:0] %s;\n", indent.c_str(), width-1, reg_name.c_str());
+
+		for (int i = 0; i < width; i++) {
+			f << stringf("%s" "always @(%sedge ", indent.c_str(), pol_clk ? "pos" : "neg");
+			dump_sigspec(f, sig_clk);
+			f << stringf(", %sedge ", pol_set ? "pos" : "neg");
+			dump_sigspec(f, sig_set);
+			f << stringf(", %sedge ", pol_clr ? "pos" : "neg");
+			dump_sigspec(f, sig_clr);
+			f << stringf(")\n");
+
+			f << stringf("%s" "  if (%s", indent.c_str(), pol_clr ? "" : "!");
+			dump_sigspec(f, sig_clr);
+			f << stringf(") %s[%d] <= 1'b0;\n", reg_name.c_str(), i);
+
+			f << stringf("%s" "  else if (%s", indent.c_str(), pol_set ? "" : "!");
+			dump_sigspec(f, sig_set);
+			f << stringf(") %s[%d] <= 1'b1;\n", reg_name.c_str(), i);
+
+			f << stringf("%s" "  else  %s[%d] <= ", indent.c_str(), reg_name.c_str(), i);
+			dump_sigspec(f, sig_d[i]);
+			f << stringf(";\n");
+		}
+
+		if (!out_is_reg_wire) {
+			f << stringf("%s" "assign ", indent.c_str());
+			dump_sigspec(f, sig_q);
+			f << stringf(" = %s;\n", reg_name.c_str());
+		}
+
+		return true;
+	}
+
+	if (cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffe")
 	{
-		RTLIL::SigSpec sig_clk, sig_arst, val_arst;
-		bool pol_clk, pol_arst = false;
+		RTLIL::SigSpec sig_clk, sig_arst, sig_en, val_arst;
+		bool pol_clk, pol_arst = false, pol_en = false;
 
 		sig_clk = cell->getPort("\\CLK");
 		pol_clk = cell->parameters["\\CLK_POLARITY"].as_bool();
@@ -677,6 +735,11 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 			val_arst = RTLIL::SigSpec(cell->parameters["\\ARST_VALUE"]);
 		}
 
+		if (cell->type == "$dffe") {
+			sig_en = cell->getPort("\\EN");
+			pol_en = cell->parameters["\\EN_POLARITY"].as_bool();
+		}
+
 		std::string reg_name = cellname(cell);
 		bool out_is_reg_wire = is_reg_wire(cell->getPort("\\Q"), reg_name);
 
@@ -701,6 +764,12 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 			f << stringf("%s" "  else\n", indent.c_str());
 		}
 
+		if (cell->type == "$dffe") {
+			f << stringf("%s" "  if (%s", indent.c_str(), pol_en ? "" : "!");
+			dump_sigspec(f, sig_en);
+			f << stringf(")\n");
+		}
+
 		f << stringf("%s" "    %s <= ", indent.c_str(), reg_name.c_str());
 		dump_cell_expr_port(f, cell, "D", false);
 		f << stringf(";\n");
@@ -715,7 +784,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 	}
 
 	// FIXME: $_SR_[PN][PN]_, $_DLATCH_[PN]_, $_DLATCHSR_[PN][PN][PN]_
-	// FIXME: $sr, $dffsr, $dlatch, $memrd, $memwr, $mem, $fsm
+	// FIXME: $sr, $dlatch, $memrd, $memwr, $mem, $fsm
 
 	return false;
 }
@@ -732,12 +801,12 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 
 	if (cell->parameters.size() > 0) {
 		f << stringf(" #(");
-		for (auto it = cell->parameters.begin(); it != cell->parameters.end(); it++) {
+		for (auto it = cell->parameters.begin(); it != cell->parameters.end(); ++it) {
 			if (it != cell->parameters.begin())
 				f << stringf(",");
 			f << stringf("\n%s  .%s(", indent.c_str(), id(it->first).c_str());
 			bool is_signed = (it->second.flags & RTLIL::CONST_FLAG_SIGNED) != 0;
-			dump_const(f, it->second, -1, 0, !is_signed, is_signed);
+			dump_const(f, it->second, -1, 0, false, is_signed);
 			f << stringf(")");
 		}
 		f << stringf("\n%s" ")", indent.c_str());
@@ -754,7 +823,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 	for (int i = 1; true; i++) {
 		char str[16];
 		snprintf(str, 16, "$%d", i);
-		for (auto it = cell->connections().begin(); it != cell->connections().end(); it++) {
+		for (auto it = cell->connections().begin(); it != cell->connections().end(); ++it) {
 			if (it->first != str)
 				continue;
 			if (!first_arg)
@@ -768,7 +837,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		break;
 	found_numbered_port:;
 	}
-	for (auto it = cell->connections().begin(); it != cell->connections().end(); it++) {
+	for (auto it = cell->connections().begin(); it != cell->connections().end(); ++it) {
 		if (numbered_ports.count(it->first))
 			continue;
 		if (!first_arg)
@@ -800,7 +869,7 @@ void dump_case_body(std::ostream &f, std::string indent, RTLIL::CaseRule *cs, bo
 	if (!omit_trailing_begin && number_of_stmts >= 2)
 		f << stringf("%s" "begin\n", indent.c_str());
 
-	for (auto it = cs->actions.begin(); it != cs->actions.end(); it++) {
+	for (auto it = cs->actions.begin(); it != cs->actions.end(); ++it) {
 		if (it->first.size() == 0)
 			continue;
 		f << stringf("%s  ", indent.c_str());
@@ -810,7 +879,7 @@ void dump_case_body(std::ostream &f, std::string indent, RTLIL::CaseRule *cs, bo
 		f << stringf(";\n");
 	}
 
-	for (auto it = cs->switches.begin(); it != cs->switches.end(); it++)
+	for (auto it = cs->switches.begin(); it != cs->switches.end(); ++it)
 		dump_proc_switch(f, indent + "  ", *it);
 
 	if (!omit_trailing_begin && number_of_stmts == 0)
@@ -824,7 +893,7 @@ void dump_proc_switch(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw
 {
 	if (sw->signal.size() == 0) {
 		f << stringf("%s" "begin\n", indent.c_str());
-		for (auto it = sw->cases.begin(); it != sw->cases.end(); it++) {
+		for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it) {
 			if ((*it)->compare.size() == 0)
 				dump_case_body(f, indent + "  ", *it);
 		}
@@ -836,7 +905,7 @@ void dump_proc_switch(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw
 	dump_sigspec(f, sw->signal);
 	f << stringf(")\n");
 
-	for (auto it = sw->cases.begin(); it != sw->cases.end(); it++) {
+	for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it) {
 		f << stringf("%s  ", indent.c_str());
 		if ((*it)->compare.size() == 0)
 			f << stringf("default");
@@ -856,11 +925,11 @@ void dump_proc_switch(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw
 
 void case_body_find_regs(RTLIL::CaseRule *cs)
 {
-	for (auto it = cs->switches.begin(); it != cs->switches.end(); it++)
+	for (auto it = cs->switches.begin(); it != cs->switches.end(); ++it)
 	for (auto it2 = (*it)->cases.begin(); it2 != (*it)->cases.end(); it2++)
 		case_body_find_regs(*it2);
 
-	for (auto it = cs->actions.begin(); it != cs->actions.end(); it++) {
+	for (auto it = cs->actions.begin(); it != cs->actions.end(); ++it) {
 		for (auto &c : it->first.chunks())
 			if (c.wire != NULL)
 				reg_wires.insert(c.wire->name);
@@ -871,7 +940,7 @@ void dump_process(std::ostream &f, std::string indent, RTLIL::Process *proc, boo
 {
 	if (find_regs) {
 		case_body_find_regs(&proc->root_case);
-		for (auto it = proc->syncs.begin(); it != proc->syncs.end(); it++)
+		for (auto it = proc->syncs.begin(); it != proc->syncs.end(); ++it)
 		for (auto it2 = (*it)->actions.begin(); it2 != (*it)->actions.end(); it2++) {
 			for (auto &c : it2->first.chunks())
 				if (c.wire != NULL)
@@ -925,7 +994,7 @@ void dump_process(std::ostream &f, std::string indent, RTLIL::Process *proc, boo
 			}
 		}
 
-		for (auto it = sync->actions.begin(); it != sync->actions.end(); it++) {
+		for (auto it = sync->actions.begin(); it != sync->actions.end(); ++it) {
 			if (it->first.size() == 0)
 				continue;
 			f << stringf("%s  ", indent.c_str());
@@ -946,7 +1015,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 	active_module = module;
 
 	f << stringf("\n");
-	for (auto it = module->processes.begin(); it != module->processes.end(); it++)
+	for (auto it = module->processes.begin(); it != module->processes.end(); ++it)
 		dump_process(f, indent + "  ", it->second, true);
 
 	if (!noexpr)
@@ -979,12 +1048,12 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 		}
 	}
 
-	dump_attributes(f, indent, module->attributes);
+	dump_attributes(f, indent, module->attributes, '\n', true);
 	f << stringf("%s" "module %s(", indent.c_str(), id(module->name, false).c_str());
 	bool keep_running = true;
 	for (int port_id = 1; keep_running; port_id++) {
 		keep_running = false;
-		for (auto it = module->wires_.begin(); it != module->wires_.end(); it++) {
+		for (auto it = module->wires_.begin(); it != module->wires_.end(); ++it) {
 			RTLIL::Wire *wire = it->second;
 			if (wire->port_id == port_id) {
 				if (port_id != 1)
@@ -997,27 +1066,25 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 	}
 	f << stringf(");\n");
 
-	for (auto it = module->wires_.begin(); it != module->wires_.end(); it++)
+	for (auto it = module->wires_.begin(); it != module->wires_.end(); ++it)
 		dump_wire(f, indent + "  ", it->second);
 
-	for (auto it = module->memories.begin(); it != module->memories.end(); it++)
+	for (auto it = module->memories.begin(); it != module->memories.end(); ++it)
 		dump_memory(f, indent + "  ", it->second);
 
-	for (auto it = module->cells_.begin(); it != module->cells_.end(); it++)
+	for (auto it = module->cells_.begin(); it != module->cells_.end(); ++it)
 		dump_cell(f, indent + "  ", it->second);
 
-	for (auto it = module->processes.begin(); it != module->processes.end(); it++)
+	for (auto it = module->processes.begin(); it != module->processes.end(); ++it)
 		dump_process(f, indent + "  ", it->second);
 
-	for (auto it = module->connections().begin(); it != module->connections().end(); it++)
+	for (auto it = module->connections().begin(); it != module->connections().end(); ++it)
 		dump_conn(f, indent + "  ", it->first, it->second);
 
 	f << stringf("%s" "endmodule\n", indent.c_str());
 	active_module = NULL;
 }
 
-} /* namespace */
-
 struct VerilogBackend : public Backend {
 	VerilogBackend() : Backend("verilog", "write design to verilog file") { }
 	virtual void help()
@@ -1122,8 +1189,10 @@ struct VerilogBackend : public Backend {
 		}
 		extra_args(f, filename, args, argidx);
 
+		design->sort();
+
 		*f << stringf("/* Generated by %s */\n", yosys_version_str);
-		for (auto it = design->modules_.begin(); it != design->modules_.end(); it++) {
+		for (auto it = design->modules_.begin(); it != design->modules_.end(); ++it) {
 			if (it->second->get_bool_attribute("\\blackbox") != blackboxes)
 				continue;
 			if (selected && !design->selected_whole_module(it->first)) {
@@ -1139,3 +1208,4 @@ struct VerilogBackend : public Backend {
 	}
 } VerilogBackend;
 
+PRIVATE_NAMESPACE_END
diff --git a/backends/verilog/verilog_backend.h b/backends/verilog/verilog_backend.h
deleted file mode 100644
index 7e6ef5ab9..000000000
--- a/backends/verilog/verilog_backend.h
+++ /dev/null
@@ -1,38 +0,0 @@
-/*
- *  yosys -- Yosys Open SYnthesis Suite
- *
- *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
- *  
- *  Permission to use, copy, modify, and/or distribute this software for any
- *  purpose with or without fee is hereby granted, provided that the above
- *  copyright notice and this permission notice appear in all copies.
- *  
- *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *
- *  ---
- *
- *  A simple and straightforward verilog backend.
- *
- *  Note that RTLIL processes can't always be mapped easily to a Verilog
- *  process. Therefore this frontend should only be used to export a
- *  Verilog netlist (i.e. after the "proc" pass has converted all processes
- *  to logic networks and registers).
- *
- */
-
-#ifndef VERILOG_BACKEND_H
-#define VERILOG_BACKEND_H
-
-#include "kernel/yosys.h"
-
-namespace VERILOG_BACKEND {
-	void verilog_backend(std::ostream &f, std::vector<std::string> args, RTLIL::Design *design);
-}
-
-#endif