Merge remote-tracking branch 'upstream/master'

9 files changed, 984 insertions, 44 deletions

diff --git a/backends/aiger/Makefile.inc b/backends/aiger/Makefile.inc
index 0fc37e95c..4a4cf30bd 100644
--- a/backends/aiger/Makefile.inc
+++ b/backends/aiger/Makefile.inc
@@ -1,3 +1,4 @@
 
 OBJS += backends/aiger/aiger.o
+OBJS += backends/aiger/xaiger.o
 
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index dfe506c66..7c851bb91 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -70,34 +70,35 @@ struct AigerWriter
 
 	int bit2aig(SigBit bit)
 	{
-		if (aig_map.count(bit) == 0)
-		{
-			aig_map[bit] = -1;
-
-			if (initstate_bits.count(bit)) {
-				log_assert(initstate_ff > 0);
-				aig_map[bit] = initstate_ff;
-			} else
-			if (not_map.count(bit)) {
-				int a = bit2aig(not_map.at(bit)) ^ 1;
-				aig_map[bit] = a;
-			} else
-			if (and_map.count(bit)) {
-				auto args = and_map.at(bit);
-				int a0 = bit2aig(args.first);
-				int a1 = bit2aig(args.second);
-				aig_map[bit] = mkgate(a0, a1);
-			} else
-			if (alias_map.count(bit)) {
-				aig_map[bit] = bit2aig(alias_map.at(bit));
-			}
+		auto it = aig_map.find(bit);
+		if (it != aig_map.end()) {
+			log_assert(it->second >= 0);
+			return it->second;
+		}
 
-			if (bit == State::Sx || bit == State::Sz)
-				log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");
+		// NB: Cannot use iterator returned from aig_map.insert()
+		//     since this function is called recursively
+
+		int a = -1;
+		if (not_map.count(bit)) {
+			a = bit2aig(not_map.at(bit)) ^ 1;
+		} else
+		if (and_map.count(bit)) {
+			auto args = and_map.at(bit);
+			int a0 = bit2aig(args.first);
+			int a1 = bit2aig(args.second);
+			a = mkgate(a0, a1);
+		} else
+		if (alias_map.count(bit)) {
+			a = bit2aig(alias_map.at(bit));
 		}
 
-		log_assert(aig_map.at(bit) >= 0);
-		return aig_map.at(bit);
+		if (bit == State::Sx || bit == State::Sz)
+			log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");
+
+		log_assert(a >= 0);
+		aig_map[bit] = a;
+		return a;
 	}
 
 	AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode) : module(module), zinit_mode(zinit_mode), sigmap(module)
@@ -685,7 +686,7 @@ struct AigerBackend : public Backend {
 		log("invariant constraints.\n");
 		log("\n");
 		log("    -ascii\n");
-		log("        write ASCII version of AGIER format\n");
+		log("        write ASCII version of AIGER format\n");
 		log("\n");
 		log("    -zinit\n");
 		log("        convert FFs to zero-initialized FFs, adding additional inputs for\n");
@@ -776,6 +777,7 @@ struct AigerBackend : public Backend {
 		writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode);
 
 		if (!map_filename.empty()) {
+			rewrite_filename(filename);
 			std::ofstream mapf;
 			mapf.open(map_filename.c_str(), std::ofstream::trunc);
 			if (mapf.fail())
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
new file mode 100644
index 000000000..69f63486c
--- /dev/null
+++ b/backends/aiger/xaiger.cc
@@ -0,0 +1,878 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *                2019  Eddie Hung <eddie@fpgeh.com>
+ *
+ *  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.
+ *
+ */
+
+// https://stackoverflow.com/a/46137633
+#ifdef _MSC_VER
+#include <stdlib.h>
+#define bswap32 _byteswap_ulong
+#elif defined(__APPLE__)
+#include <libkern/OSByteOrder.h>
+#define bswap32 OSSwapInt32
+#elif defined(__GNUC__)
+#define bswap32 __builtin_bswap32
+#else
+#include <cstdint>
+inline static uint32_t bswap32(uint32_t x)
+{
+	// https://stackoverflow.com/a/27796212
+	register uint32_t value = number_to_be_reversed;
+	uint8_t lolo = (value >> 0) & 0xFF;
+	uint8_t lohi = (value >> 8) & 0xFF;
+	uint8_t hilo = (value >> 16) & 0xFF;
+	uint8_t hihi = (value >> 24) & 0xFF;
+	return (hihi << 24)
+		| (hilo << 16)
+		| (lohi << 8)
+		| (lolo << 0);
+}
+#endif
+
+#include "kernel/yosys.h"
+#include "kernel/sigtools.h"
+#include "kernel/utils.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+inline int32_t to_big_endian(int32_t i32) {
+#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+	return __builtin_bswap32(i32);
+#elif __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
+	return i32;
+#else
+#error "Unknown endianness"
+#endif
+}
+
+void aiger_encode(std::ostream &f, int x)
+{
+	log_assert(x >= 0);
+
+	while (x & ~0x7f) {
+		f.put((x & 0x7f) | 0x80);
+		x = x >> 7;
+	}
+
+	f.put(x);
+}
+
+struct XAigerWriter
+{
+	Module *module;
+	SigMap sigmap;
+
+	pool<SigBit> input_bits, output_bits;
+	dict<SigBit, SigBit> not_map, alias_map;
+	dict<SigBit, pair<SigBit, SigBit>> and_map;
+	vector<std::tuple<SigBit,RTLIL::Cell*,RTLIL::IdString,int>> ci_bits;
+	vector<std::tuple<SigBit,RTLIL::Cell*,RTLIL::IdString,int,int>> co_bits;
+
+	vector<pair<int, int>> aig_gates;
+	vector<int> aig_outputs;
+	int aig_m = 0, aig_i = 0, aig_l = 0, aig_o = 0, aig_a = 0;
+
+	dict<SigBit, int> aig_map;
+	dict<SigBit, int> ordered_outputs;
+
+	vector<Cell*> box_list;
+	bool omode = false;
+
+	int mkgate(int a0, int a1)
+	{
+		aig_m++, aig_a++;
+		aig_gates.push_back(a0 > a1 ? make_pair(a0, a1) : make_pair(a1, a0));
+		return 2*aig_m;
+	}
+
+	int bit2aig(SigBit bit)
+	{
+		auto it = aig_map.find(bit);
+		if (it != aig_map.end()) {
+			log_assert(it->second >= 0);
+			return it->second;
+		}
+
+		// NB: Cannot use iterator returned from aig_map.insert()
+		//     since this function is called recursively
+
+		int a = -1;
+		if (not_map.count(bit)) {
+			a = bit2aig(not_map.at(bit)) ^ 1;
+		} else
+		if (and_map.count(bit)) {
+			auto args = and_map.at(bit);
+			int a0 = bit2aig(args.first);
+			int a1 = bit2aig(args.second);
+			a = mkgate(a0, a1);
+		} else
+		if (alias_map.count(bit)) {
+			a = bit2aig(alias_map.at(bit));
+		}
+
+		if (bit == State::Sx || bit == State::Sz) {
+			log_debug("Design contains 'x' or 'z' bits. Treating as 1'b0.\n");
+			a = aig_map.at(State::S0);
+		}
+
+		log_assert(a >= 0);
+		aig_map[bit] = a;
+		return a;
+	}
+
+	XAigerWriter(Module *module, bool holes_mode=false) : module(module), sigmap(module)
+	{
+		pool<SigBit> undriven_bits;
+		pool<SigBit> unused_bits;
+		pool<SigBit> keep_bits;
+
+		// promote public wires
+		for (auto wire : module->wires())
+			if (wire->name[0] == '\\')
+				sigmap.add(wire);
+
+		// promote input wires
+		for (auto wire : module->wires())
+			if (wire->port_input)
+				sigmap.add(wire);
+
+		// promote output wires
+		for (auto wire : module->wires())
+			if (wire->port_output)
+				sigmap.add(wire);
+
+		for (auto wire : module->wires())
+		{
+			bool keep = wire->attributes.count("\\keep");
+
+			for (int i = 0; i < GetSize(wire); i++)
+			{
+				SigBit wirebit(wire, i);
+				SigBit bit = sigmap(wirebit);
+
+				if (bit.wire) {
+					undriven_bits.insert(bit);
+					unused_bits.insert(bit);
+				}
+
+				if (keep)
+					keep_bits.insert(bit);
+
+				if (wire->port_input || keep) {
+					if (bit != wirebit)
+						alias_map[bit] = wirebit;
+					input_bits.insert(wirebit);
+				}
+
+				if (wire->port_output || keep) {
+					if (bit != RTLIL::Sx) {
+						if (bit != wirebit)
+							alias_map[wirebit] = bit;
+						output_bits.insert(wirebit);
+					}
+					else
+						log_debug("Skipping PO '%s' driven by 1'bx\n", log_signal(wirebit));
+				}
+			}
+		}
+
+		for (auto bit : input_bits)
+			undriven_bits.erase(sigmap(bit));
+		for (auto bit : output_bits)
+			if (!bit.wire->port_input)
+				unused_bits.erase(bit);
+
+		// TODO: Speed up toposort -- ultimately we care about
+		//       box ordering, but not individual AIG cells
+		dict<SigBit, pool<IdString>> bit_drivers, bit_users;
+		TopoSort<IdString, RTLIL::sort_by_id_str> toposort;
+		bool abc_box_seen = false;
+
+		for (auto cell : module->selected_cells()) {
+			if (cell->type == "$_NOT_")
+			{
+				SigBit A = sigmap(cell->getPort("\\A").as_bit());
+				SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
+				unused_bits.erase(A);
+				undriven_bits.erase(Y);
+				not_map[Y] = A;
+				if (!holes_mode) {
+					toposort.node(cell->name);
+					bit_users[A].insert(cell->name);
+					bit_drivers[Y].insert(cell->name);
+				}
+				continue;
+			}
+
+			if (cell->type == "$_AND_")
+			{
+				SigBit A = sigmap(cell->getPort("\\A").as_bit());
+				SigBit B = sigmap(cell->getPort("\\B").as_bit());
+				SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
+				unused_bits.erase(A);
+				unused_bits.erase(B);
+				undriven_bits.erase(Y);
+				and_map[Y] = make_pair(A, B);
+				if (!holes_mode) {
+					toposort.node(cell->name);
+					bit_users[A].insert(cell->name);
+					bit_users[B].insert(cell->name);
+					bit_drivers[Y].insert(cell->name);
+				}
+				continue;
+			}
+
+			log_assert(!holes_mode);
+
+			RTLIL::Module* inst_module = module->design->module(cell->type);
+			if (inst_module && inst_module->attributes.count("\\abc_box_id")) {
+				abc_box_seen = true;
+
+				if (!holes_mode) {
+					toposort.node(cell->name);
+					for (const auto &conn : cell->connections()) {
+						if (cell->input(conn.first)) {
+							// Ignore inout for the sake of topographical ordering
+							if (cell->output(conn.first)) continue;
+							for (auto bit : sigmap(conn.second))
+								bit_users[bit].insert(cell->name);
+						}
+
+						if (cell->output(conn.first))
+							for (auto bit : sigmap(conn.second))
+								bit_drivers[bit].insert(cell->name);
+					}
+				}
+			}
+			else {
+				bool cell_known = cell->known();
+				for (const auto &c : cell->connections()) {
+					if (c.second.is_fully_const()) continue;
+					auto is_input = !cell_known || cell->input(c.first);
+					auto is_output = !cell_known || cell->output(c.first);
+					if (!is_input && !is_output)
+						log_error("Connection '%s' on cell '%s' (type '%s') not recognised!\n", log_id(c.first), log_id(cell), log_id(cell->type));
+
+					if (is_input) {
+						for (auto b : c.second.bits()) {
+							Wire *w = b.wire;
+							if (!w) continue;
+							if (!w->port_output || !cell_known) {
+								SigBit I = sigmap(b);
+								if (I != b)
+									alias_map[b] = I;
+								output_bits.insert(b);
+								unused_bits.erase(b);
+
+								if (!cell_known)
+									keep_bits.insert(b);
+							}
+						}
+					}
+					if (is_output) {
+						for (auto b : c.second.bits()) {
+							Wire *w = b.wire;
+							if (!w) continue;
+							input_bits.insert(b);
+							SigBit O = sigmap(b);
+							if (O != b)
+								alias_map[O] = b;
+							undriven_bits.erase(O);
+						}
+					}
+				}
+			}
+
+			//log_warning("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
+		}
+
+		if (abc_box_seen) {
+			for (auto &it : bit_users)
+				if (bit_drivers.count(it.first))
+					for (auto driver_cell : bit_drivers.at(it.first))
+					for (auto user_cell : it.second)
+						toposort.edge(driver_cell, user_cell);
+
+#if 0
+			toposort.analyze_loops = true;
+#endif
+			bool no_loops = toposort.sort();
+#if 0
+			unsigned i = 0;
+			for (auto &it : toposort.loops) {
+				log("  loop %d\n", i++);
+				for (auto cell_name : it) {
+					auto cell = module->cell(cell_name);
+					log_assert(cell);
+					log("\t%s (%s @ %s)\n", log_id(cell), log_id(cell->type), cell->get_src_attribute().c_str());
+				}
+			}
+#endif
+			log_assert(no_loops);
+
+			pool<IdString> seen_boxes;
+			for (auto cell_name : toposort.sorted) {
+				RTLIL::Cell *cell = module->cell(cell_name);
+				log_assert(cell);
+
+				RTLIL::Module* box_module = module->design->module(cell->type);
+				if (!box_module || !box_module->attributes.count("\\abc_box_id"))
+					continue;
+
+				if (seen_boxes.insert(cell->type).second) {
+					auto it = box_module->attributes.find("\\abc_carry");
+					if (it != box_module->attributes.end()) {
+						RTLIL::Wire *carry_in = nullptr, *carry_out = nullptr;
+						auto carry_in_out = it->second.decode_string();
+						auto pos = carry_in_out.find(',');
+						if (pos == std::string::npos)
+							log_error("'abc_carry' attribute on module '%s' does not contain ','.\n", log_id(cell->type));
+						auto carry_in_name = RTLIL::escape_id(carry_in_out.substr(0, pos));
+						carry_in = box_module->wire(carry_in_name);
+						if (!carry_in || !carry_in->port_input)
+							log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an input port.\n", log_id(cell->type), carry_in_name.c_str());
+
+						auto carry_out_name = RTLIL::escape_id(carry_in_out.substr(pos+1));
+						carry_out = box_module->wire(carry_out_name);
+						if (!carry_out || !carry_out->port_output)
+							log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an output port.\n", log_id(cell->type), carry_out_name.c_str());
+
+						auto &ports = box_module->ports;
+						for (auto jt = ports.begin(); jt != ports.end(); ) {
+							RTLIL::Wire* w = box_module->wire(*jt);
+							log_assert(w);
+							if (w == carry_in || w == carry_out) {
+								jt = ports.erase(jt);
+								continue;
+							}
+							if (w->port_id > carry_in->port_id)
+								--w->port_id;
+							if (w->port_id > carry_out->port_id)
+								--w->port_id;
+							log_assert(w->port_input || w->port_output);
+							log_assert(ports[w->port_id-1] == w->name);
+							++jt;
+						}
+						ports.push_back(carry_in->name);
+						carry_in->port_id = ports.size();
+						ports.push_back(carry_out->name);
+						carry_out->port_id = ports.size();
+					}
+				}
+
+				// Fully pad all unused input connections of this box cell with S0
+				// Fully pad all undriven output connections of this box cell with anonymous wires
+				// NB: Assume box_module->ports are sorted alphabetically
+				//     (as RTLIL::Module::fixup_ports() would do)
+				for (const auto &port_name : box_module->ports) {
+					RTLIL::Wire* w = box_module->wire(port_name);
+					log_assert(w);
+					auto it = cell->connections_.find(port_name);
+					if (w->port_input) {
+						RTLIL::SigSpec rhs;
+						if (it != cell->connections_.end()) {
+							if (GetSize(it->second) < GetSize(w))
+								it->second.append(RTLIL::SigSpec(RTLIL::S0, GetSize(w)-GetSize(it->second)));
+							rhs = it->second;
+						}
+						else {
+							rhs = RTLIL::SigSpec(RTLIL::S0, GetSize(w));
+							cell->setPort(port_name, rhs);
+						}
+
+						int offset = 0;
+						for (auto b : rhs.bits()) {
+							SigBit I = sigmap(b);
+							if (b == RTLIL::Sx)
+								b = RTLIL::S0;
+							else if (I != b) {
+								if (I == RTLIL::Sx)
+									alias_map[b] = RTLIL::S0;
+								else
+									alias_map[b] = I;
+							}
+							co_bits.emplace_back(b, cell, port_name, offset++, 0);
+							unused_bits.erase(b);
+						}
+					}
+					if (w->port_output) {
+						RTLIL::SigSpec rhs;
+						auto it = cell->connections_.find(w->name);
+						if (it != cell->connections_.end()) {
+							if (GetSize(it->second) < GetSize(w))
+								it->second.append(module->addWire(NEW_ID, GetSize(w)-GetSize(it->second)));
+							rhs = it->second;
+						}
+						else {
+							rhs = module->addWire(NEW_ID, GetSize(w));
+							cell->setPort(port_name, rhs);
+						}
+
+						int offset = 0;
+						for (const auto &b : rhs.bits()) {
+							ci_bits.emplace_back(b, cell, port_name, offset++);
+							SigBit O = sigmap(b);
+							if (O != b)
+								alias_map[O] = b;
+							undriven_bits.erase(O);
+
+							auto jt = input_bits.find(b);
+							if (jt != input_bits.end()) {
+								log_assert(keep_bits.count(O));
+								input_bits.erase(b);
+							}
+						}
+					}
+				}
+				box_list.emplace_back(cell);
+			}
+
+			// TODO: Free memory from toposort, bit_drivers, bit_users
+		}
+
+		for (auto bit : input_bits) {
+			if (!output_bits.count(bit))
+				continue;
+			RTLIL::Wire *wire = bit.wire;
+			// If encountering an inout port, or a keep-ed wire, then create a new wire
+			// with $inout.out suffix, make it a PO driven by the existing inout, and
+			// inherit existing inout's drivers
+			if ((wire->port_input && wire->port_output && !undriven_bits.count(bit))
+					|| keep_bits.count(bit)) {
+				RTLIL::IdString wire_name = wire->name.str() + "$inout.out";
+				RTLIL::Wire *new_wire = module->wire(wire_name);
+				if (!new_wire)
+					new_wire = module->addWire(wire_name, GetSize(wire));
+				SigBit new_bit(new_wire, bit.offset);
+				module->connect(new_bit, bit);
+				if (not_map.count(bit)) {
+					auto a = not_map.at(bit);
+					not_map[new_bit] = a;
+				}
+				else if (and_map.count(bit)) {
+					auto a = and_map.at(bit);
+					and_map[new_bit] = a;
+				}
+				else if (alias_map.count(bit)) {
+					auto a = alias_map.at(bit);
+					alias_map[new_bit] = a;
+				}
+				else
+					alias_map[new_bit] = bit;
+				output_bits.erase(bit);
+				output_bits.insert(new_bit);
+			}
+		}
+
+		for (auto bit : unused_bits)
+			undriven_bits.erase(bit);
+
+		if (!undriven_bits.empty() && !holes_mode) {
+			undriven_bits.sort();
+			for (auto bit : undriven_bits) {
+				log_warning("Treating undriven bit %s.%s like $anyseq.\n", log_id(module), log_signal(bit));
+				input_bits.insert(bit);
+			}
+			log_warning("Treating a total of %d undriven bits in %s like $anyseq.\n", GetSize(undriven_bits), log_id(module));
+		}
+
+		if (holes_mode) {
+			struct sort_by_port_id {
+				bool operator()(const RTLIL::SigBit& a, const RTLIL::SigBit& b) const {
+					return a.wire->port_id < b.wire->port_id;
+				}
+			};
+			input_bits.sort(sort_by_port_id());
+			output_bits.sort(sort_by_port_id());
+		}
+		else {
+			input_bits.sort();
+			output_bits.sort();
+		}
+
+		not_map.sort();
+		and_map.sort();
+
+		aig_map[State::S0] = 0;
+		aig_map[State::S1] = 1;
+
+		for (auto bit : input_bits) {
+			aig_m++, aig_i++;
+			log_assert(!aig_map.count(bit));
+			aig_map[bit] = 2*aig_m;
+		}
+
+		for (auto &c : ci_bits) {
+			RTLIL::SigBit bit = std::get<0>(c);
+			aig_m++, aig_i++;
+			aig_map[bit] = 2*aig_m;
+		}
+
+		for (auto &c : co_bits) {
+			RTLIL::SigBit bit = std::get<0>(c);
+			std::get<4>(c) = ordered_outputs[bit] = aig_o++;
+			aig_outputs.push_back(bit2aig(bit));
+		}
+
+		for (auto bit : output_bits) {
+			ordered_outputs[bit] = aig_o++;
+			aig_outputs.push_back(bit2aig(bit));
+		}
+
+		if (output_bits.empty()) {
+			aig_o++;
+			aig_outputs.push_back(0);
+			omode = true;
+		}
+	}
+
+	void write_aiger(std::ostream &f, bool ascii_mode)
+	{
+		int aig_obc = aig_o;
+		int aig_obcj = aig_obc;
+		int aig_obcjf = aig_obcj;
+
+		log_assert(aig_m == aig_i + aig_l + aig_a);
+		log_assert(aig_obcjf == GetSize(aig_outputs));
+
+		f << stringf("%s %d %d %d %d %d", ascii_mode ? "aag" : "aig", aig_m, aig_i, aig_l, aig_o, aig_a);
+		f << stringf("\n");
+
+		if (ascii_mode)
+		{
+			for (int i = 0; i < aig_i; i++)
+				f << stringf("%d\n", 2*i+2);
+
+			for (int i = 0; i < aig_obc; i++)
+				f << stringf("%d\n", aig_outputs.at(i));
+
+			for (int i = aig_obc; i < aig_obcj; i++)
+				f << stringf("1\n");
+
+			for (int i = aig_obc; i < aig_obcj; i++)
+				f << stringf("%d\n", aig_outputs.at(i));
+
+			for (int i = aig_obcj; i < aig_obcjf; i++)
+				f << stringf("%d\n", aig_outputs.at(i));
+
+			for (int i = 0; i < aig_a; i++)
+				f << stringf("%d %d %d\n", 2*(aig_i+aig_l+i)+2, aig_gates.at(i).first, aig_gates.at(i).second);
+		}
+		else
+		{
+			for (int i = 0; i < aig_obc; i++)
+				f << stringf("%d\n", aig_outputs.at(i));
+
+			for (int i = aig_obc; i < aig_obcj; i++)
+				f << stringf("1\n");
+
+			for (int i = aig_obc; i < aig_obcj; i++)
+				f << stringf("%d\n", aig_outputs.at(i));
+
+			for (int i = aig_obcj; i < aig_obcjf; i++)
+				f << stringf("%d\n", aig_outputs.at(i));
+
+			for (int i = 0; i < aig_a; i++) {
+				int lhs = 2*(aig_i+aig_l+i)+2;
+				int rhs0 = aig_gates.at(i).first;
+				int rhs1 = aig_gates.at(i).second;
+				int delta0 = lhs - rhs0;
+				int delta1 = rhs0 - rhs1;
+				aiger_encode(f, delta0);
+				aiger_encode(f, delta1);
+			}
+		}
+
+		f << "c";
+
+		if (!box_list.empty()) {
+			auto write_buffer = [](std::stringstream &buffer, int i32) {
+				int32_t i32_be = to_big_endian(i32);
+				buffer.write(reinterpret_cast<const char*>(&i32_be), sizeof(i32_be));
+			};
+
+			std::stringstream h_buffer;
+			auto write_h_buffer = std::bind(write_buffer, std::ref(h_buffer), std::placeholders::_1);
+			write_h_buffer(1);
+			log_debug("ciNum = %zu\n", input_bits.size() + ci_bits.size());
+			write_h_buffer(input_bits.size() + ci_bits.size());
+			log_debug("coNum = %zu\n", output_bits.size() + co_bits.size());
+			write_h_buffer(output_bits.size() + co_bits.size());
+			log_debug("piNum = %zu\n", input_bits.size());
+			write_h_buffer(input_bits.size());
+			log_debug("poNum = %zu\n", output_bits.size());
+			write_h_buffer(output_bits.size());
+			log_debug("boxNum = %zu\n", box_list.size());
+			write_h_buffer(box_list.size());
+
+			RTLIL::Module *holes_module = nullptr;
+			holes_module = module->design->addModule("$__holes__");
+			log_assert(holes_module);
+
+			int port_id = 1;
+			int box_count = 0;
+			for (auto cell : box_list) {
+				RTLIL::Module* box_module = module->design->module(cell->type);
+				int box_inputs = 0, box_outputs = 0;
+				Cell *holes_cell = nullptr;
+				if (box_module->get_bool_attribute("\\whitebox")) {
+					holes_cell = holes_module->addCell(cell->name, cell->type);
+					holes_cell->parameters = cell->parameters;
+				}
+
+				// NB: Assume box_module->ports are sorted alphabetically
+				//     (as RTLIL::Module::fixup_ports() would do)
+				for (const auto &port_name : box_module->ports) {
+					RTLIL::Wire *w = box_module->wire(port_name);
+					log_assert(w);
+					RTLIL::Wire *holes_wire;
+					RTLIL::SigSpec port_wire;
+					if (w->port_input) {
+						for (int i = 0; i < GetSize(w); i++) {
+							box_inputs++;
+							holes_wire = holes_module->wire(stringf("\\i%d", box_inputs));
+							if (!holes_wire) {
+								holes_wire = holes_module->addWire(stringf("\\i%d", box_inputs));
+								holes_wire->port_input = true;
+								holes_wire->port_id = port_id++;
+								holes_module->ports.push_back(holes_wire->name);
+							}
+							if (holes_cell)
+								port_wire.append(holes_wire);
+						}
+						if (!port_wire.empty())
+							holes_cell->setPort(w->name, port_wire);
+					}
+					if (w->port_output) {
+						box_outputs += GetSize(w);
+						for (int i = 0; i < GetSize(w); i++) {
+							if (GetSize(w) == 1)
+								holes_wire = holes_module->addWire(stringf("%s.%s", cell->name.c_str(), w->name.c_str()));
+							else
+								holes_wire = holes_module->addWire(stringf("%s.%s[%d]", cell->name.c_str(), w->name.c_str(), i));
+							holes_wire->port_output = true;
+							holes_wire->port_id = port_id++;
+							holes_module->ports.push_back(holes_wire->name);
+							if (holes_cell)
+								port_wire.append(holes_wire);
+							else
+								holes_module->connect(holes_wire, RTLIL::S0);
+						}
+						if (!port_wire.empty())
+							holes_cell->setPort(w->name, port_wire);
+					}
+				}
+
+				write_h_buffer(box_inputs);
+				write_h_buffer(box_outputs);
+				write_h_buffer(box_module->attributes.at("\\abc_box_id").as_int());
+				write_h_buffer(box_count++);
+			}
+
+			f << "h";
+			std::string buffer_str = h_buffer.str();
+			int32_t buffer_size_be = to_big_endian(buffer_str.size());
+			f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+			f.write(buffer_str.data(), buffer_str.size());
+
+			std::stringstream r_buffer;
+			auto write_r_buffer = std::bind(write_buffer, std::ref(r_buffer), std::placeholders::_1);
+			write_r_buffer(0);
+
+			f << "r";
+			buffer_str = r_buffer.str();
+			buffer_size_be = to_big_endian(buffer_str.size());
+			f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+			f.write(buffer_str.data(), buffer_str.size());
+
+			if (holes_module) {
+				log_push();
+
+				// NB: fixup_ports() will sort ports by name
+				//holes_module->fixup_ports();
+				holes_module->check();
+
+				holes_module->design->selection_stack.emplace_back(false);
+				RTLIL::Selection& sel = holes_module->design->selection_stack.back();
+				sel.select(holes_module);
+
+				// TODO: Should not need to opt_merge if we only instantiate
+				//       each box type once...
+				Pass::call(holes_module->design, "opt_merge -share_all");
+
+				Pass::call(holes_module->design, "flatten -wb");
+
+				// TODO: Should techmap/aigmap/check all lib_whitebox-es just once,
+				// instead of per write_xaiger call
+				Pass::call(holes_module->design, "techmap");
+				Pass::call(holes_module->design, "aigmap");
+				for (auto cell : holes_module->cells())
+					if (!cell->type.in("$_NOT_", "$_AND_"))
+						log_error("Whitebox contents cannot be represented as AIG. Please verify whiteboxes are synthesisable.\n");
+
+				Pass::call(holes_module->design, "clean -purge");
+
+				std::stringstream a_buffer;
+				XAigerWriter writer(holes_module, true /* holes_mode */);
+				writer.write_aiger(a_buffer, false /*ascii_mode*/);
+
+				holes_module->design->selection_stack.pop_back();
+
+				f << "a";
+				std::string buffer_str = a_buffer.str();
+				int32_t buffer_size_be = to_big_endian(buffer_str.size());
+				f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+				f.write(buffer_str.data(), buffer_str.size());
+				holes_module->design->remove(holes_module);
+
+				log_pop();
+			}
+		}
+
+		f << stringf("Generated by %s\n", yosys_version_str);
+	}
+
+	void write_map(std::ostream &f, bool verbose_map)
+	{
+		dict<int, string> input_lines;
+		dict<int, string> output_lines;
+		dict<int, string> wire_lines;
+
+		for (auto wire : module->wires())
+		{
+			//if (!verbose_map && wire->name[0] == '$')
+			//	continue;
+
+			SigSpec sig = sigmap(wire);
+
+			for (int i = 0; i < GetSize(wire); i++)
+			{
+				RTLIL::SigBit b(wire, i);
+				if (input_bits.count(b)) {
+					int a = aig_map.at(b);
+					log_assert((a & 1) == 0);
+					input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, i, log_id(wire));
+				}
+
+				if (output_bits.count(b)) {
+					int o = ordered_outputs.at(b);
+					output_lines[o] += stringf("output %lu %d %s\n", o - co_bits.size(), i, log_id(wire));
+					continue;
+				}
+
+				if (verbose_map) {
+					if (aig_map.count(sig[i]) == 0)
+						continue;
+
+					int a = aig_map.at(sig[i]);
+					wire_lines[a] += stringf("wire %d %d %s\n", a, i, log_id(wire));
+				}
+			}
+		}
+
+		input_lines.sort();
+		for (auto &it : input_lines)
+			f << it.second;
+		log_assert(input_lines.size() == input_bits.size());
+
+		int box_count = 0;
+		for (auto cell : box_list)
+			f << stringf("box %d %d %s\n", box_count++, 0, log_id(cell->name));
+
+		output_lines.sort();
+		for (auto &it : output_lines)
+			f << it.second;
+		log_assert(output_lines.size() == output_bits.size());
+		if (omode && output_bits.empty())
+			f << "output " << output_lines.size() << " 0 $__dummy__\n";
+
+		wire_lines.sort();
+		for (auto &it : wire_lines)
+			f << it.second;
+	}
+};
+
+struct XAigerBackend : public Backend {
+	XAigerBackend() : Backend("xaiger", "write design to XAIGER file") { }
+	void help() YS_OVERRIDE
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    write_xaiger [options] [filename]\n");
+		log("\n");
+		log("Write the current design to an XAIGER file. The design must be flattened and\n");
+		log("all unsupported cells will be converted into psuedo-inputs and pseudo-outputs.\n");
+		log("\n");
+		log("    -ascii\n");
+		log("        write ASCII version of AIGER format\n");
+		log("\n");
+		log("    -map <filename>\n");
+		log("        write an extra file with port and latch symbols\n");
+		log("\n");
+		log("    -vmap <filename>\n");
+		log("        like -map, but more verbose\n");
+		log("\n");
+	}
+	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+	{
+		bool ascii_mode = false;
+		bool verbose_map = false;
+		std::string map_filename;
+
+		log_header(design, "Executing XAIGER backend.\n");
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			if (args[argidx] == "-ascii") {
+				ascii_mode = true;
+				continue;
+			}
+			if (map_filename.empty() && args[argidx] == "-map" && argidx+1 < args.size()) {
+				map_filename = args[++argidx];
+				continue;
+			}
+			if (map_filename.empty() && args[argidx] == "-vmap" && argidx+1 < args.size()) {
+				map_filename = args[++argidx];
+				verbose_map = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(f, filename, args, argidx);
+
+		Module *top_module = design->top_module();
+
+		if (top_module == nullptr)
+			log_error("Can't find top module in current design!\n");
+
+		XAigerWriter writer(top_module);
+		writer.write_aiger(*f, ascii_mode);
+
+		if (!map_filename.empty()) {
+			std::ofstream mapf;
+			mapf.open(map_filename.c_str(), std::ofstream::trunc);
+			if (mapf.fail())
+				log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
+			writer.write_map(mapf, verbose_map);
+		}
+	}
+} XAigerBackend;
+
+PRIVATE_NAMESPACE_END
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 511a11942..a507b120b 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -17,6 +17,11 @@
  *
  */
 
+// [[CITE]] Btor2 , BtorMC and Boolector 3.0
+// Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
+// Computer Aided Verification - 30th International Conference, CAV 2018
+// https://cs.stanford.edu/people/niemetz/publication/2018/niemetzpreinerwolfbiere-cav18/
+
 #include "kernel/rtlil.h"
 #include "kernel/register.h"
 #include "kernel/sigtools.h"
@@ -875,9 +880,28 @@ struct BtorWorker
 					else
 					{
 						if (bit_cell.count(bit) == 0)
-							log_error("No driver for signal bit %s.\n", log_signal(bit));
-						export_cell(bit_cell.at(bit));
-						log_assert(bit_nid.count(bit));
+						{
+							SigSpec s = bit;
+
+							while (i+GetSize(s) < GetSize(sig) && sig[i+GetSize(s)].wire != nullptr &&
+									bit_cell.count(sig[i+GetSize(s)]) == 0)
+								s.append(sig[i+GetSize(s)]);
+
+							log_warning("No driver for signal %s.\n", log_signal(s));
+
+							int sid = get_bv_sid(GetSize(s));
+							int nid = next_nid++;
+							btorf("%d input %d %s\n", nid, sid);
+							nid_width[nid] = GetSize(s);
+
+							i += GetSize(s)-1;
+							continue;
+						}
+						else
+						{
+							export_cell(bit_cell.at(bit));
+							log_assert(bit_nid.count(bit));
+						}
 					}
 				}
 
diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index 04d1ee311..313af7d5c 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -204,6 +204,11 @@ void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const
 
 	for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it)
 	{
+		for (auto ait = (*it)->attributes.begin(); ait != (*it)->attributes.end(); ++ait) {
+			f << stringf("%s  attribute %s ", indent.c_str(), ait->first.c_str());
+			dump_const(f, ait->second);
+			f << stringf("\n");
+		}
 		f << stringf("%s  case ", indent.c_str());
 		for (size_t i = 0; i < (*it)->compare.size(); i++) {
 			if (i > 0)
@@ -483,6 +488,7 @@ struct DumpPass : public Pass {
 		std::stringstream buf;
 
 		if (!filename.empty()) {
+			rewrite_filename(filename);
 			std::ofstream *ff = new std::ofstream;
 			ff->open(filename.c_str(), append ? std::ofstream::app : std::ofstream::trunc);
 			if (ff->fail()) {
diff --git a/backends/json/json.cc b/backends/json/json.cc
index f5c687981..dda4dfedd 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -126,6 +126,10 @@ struct JsonWriter
 			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");
+			if (w->start_offset)
+				f << stringf("          \"offset\": %d,\n", w->start_offset);
+			if (w->upto)
+				f << stringf("          \"upto\": 1,\n");
 			f << stringf("          \"bits\": %s\n", get_bits(w).c_str());
 			f << stringf("        }");
 			first = false;
@@ -189,6 +193,10 @@ struct JsonWriter
 			f << stringf("        %s: {\n", get_name(w->name).c_str());
 			f << stringf("          \"hide_name\": %s,\n", w->name[0] == '$' ? "1" : "0");
 			f << stringf("          \"bits\": %s,\n", get_bits(w).c_str());
+			if (w->start_offset)
+				f << stringf("          \"offset\": %d,\n", w->start_offset);
+			if (w->upto)
+				f << stringf("          \"upto\": 1,\n");
 			f << stringf("          \"attributes\": {");
 			write_parameters(w->attributes);
 			f << stringf("\n          }\n");
@@ -525,6 +533,7 @@ struct JsonPass : public Pass {
 		std::stringstream buf;
 
 		if (!filename.empty()) {
+			rewrite_filename(filename);
 			std::ofstream *ff = new std::ofstream;
 			ff->open(filename.c_str(), std::ofstream::trunc);
 			if (ff->fail()) {
diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc
index 549fc73ae..fff110bb0 100644
--- a/backends/protobuf/protobuf.cc
+++ b/backends/protobuf/protobuf.cc
@@ -336,6 +336,7 @@ struct ProtobufPass : public Pass {
 		std::stringstream buf;
 
 		if (!filename.empty()) {
+			rewrite_filename(filename);
 			std::ofstream *ff = new std::ofstream;
 			ff->open(filename.c_str(), std::ofstream::trunc);
 			if (ff->fail()) {
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index ab20a4af2..bac68ac70 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -43,7 +43,11 @@ if os.name == "posix":
         if current_rlimit_stack[1] != resource.RLIM_INFINITY:
             smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1])
         if current_rlimit_stack[0] < smtio_stacksize:
-            resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
+            try:
+                resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
+            except ValueError:
+                # couldn't get more stack, just run with what we have
+                pass
 
 
 # currently running solvers (so we can kill them)
@@ -1023,6 +1027,8 @@ class MkVcd:
         assert t >= self.t
         if t != self.t:
             if self.t == -1:
+                print("$version Generated by Yosys-SMTBMC $end", file=self.f)
+                print("$timescale 1ns $end", file=self.f)
                 print("$var integer 32 t smt_step $end", file=self.f)
                 print("$var event 1 ! smt_clock $end", file=self.f)
 
@@ -1041,7 +1047,10 @@ class MkVcd:
                         scope = scope[:-1]
 
                     while uipath[:-1] != scope:
-                        print("$scope module %s $end" % uipath[len(scope)], file=self.f)
+                        scopename = uipath[len(scope)]
+                        if scopename.startswith("$"):
+                            scopename = "\\" + scopename
+                        print("$scope module %s $end" % scopename, file=self.f)
                         scope.append(uipath[len(scope)])
 
                     if path in self.clocks and self.clocks[path][1] == "event":
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 827af5d85..e0b3a6f80 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -189,7 +189,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
 	if (width < 0)
 		width = data.bits.size() - offset;
 	if (width == 0) {
-		f << "\"\"";
+		// See IEEE 1364-2005 Clause 5.1.14.
+		f << "{0{1'b0}}";
 		return;
 	}
 	if (nostr)
@@ -222,7 +223,7 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
 				case RTLIL::S1: bin_digits.push_back('1'); break;
 				case RTLIL::Sx: bin_digits.push_back('x'); break;
 				case RTLIL::Sz: bin_digits.push_back('z'); break;
-				case RTLIL::Sa: bin_digits.push_back('z'); break;
+				case RTLIL::Sa: bin_digits.push_back('?'); break;
 				case RTLIL::Sm: log_error("Found marker state in final netlist.");
 				}
 			}
@@ -251,6 +252,12 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
 					hex_digits.push_back('z');
 					continue;
 				}
+				if (bit_3 == '?' || bit_2 == '?' || bit_1 == '?' || bit_0 == '?') {
+					if (bit_3 != '?' || bit_2 != '?' || bit_1 != '?' || bit_0 != '?')
+						goto dump_bin;
+					hex_digits.push_back('?');
+					continue;
+				}
 				int val = 8*(bit_3 - '0') + 4*(bit_2 - '0') + 2*(bit_1 - '0') + (bit_0 - '0');
 				hex_digits.push_back(val < 10 ? '0' + val : 'a' + val - 10);
 			}
@@ -270,7 +277,7 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
 				case RTLIL::S1: f << stringf("1"); break;
 				case RTLIL::Sx: f << stringf("x"); break;
 				case RTLIL::Sz: f << stringf("z"); break;
-				case RTLIL::Sa: f << stringf("z"); break;
+				case RTLIL::Sa: f << stringf("?"); break;
 				case RTLIL::Sm: log_error("Found marker state in final netlist.");
 				}
 			}
@@ -364,20 +371,22 @@ void dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig)
 	}
 }
 
-void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString, RTLIL::Const> &attributes, char term = '\n', bool modattr = false)
+void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString, RTLIL::Const> &attributes, char term = '\n', bool modattr = false, bool as_comment = false)
 {
 	if (noattr)
 		return;
+	if (attr2comment)
+		as_comment = true;
 	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("%s" "%s %s", indent.c_str(), as_comment ? "/*" : "(*", id(it->first).c_str());
 		f << stringf(" = ");
 		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, attr2comment);
-		f << stringf(" %s%c", attr2comment ? "*/" : "*)", term);
+			dump_const(f, it->second, -1, 0, false, as_comment);
+		f << stringf(" %s%c", as_comment ? "*/" : "*)", term);
 	}
 }
 
@@ -780,7 +789,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
-	if (cell->type == "$pmux" || cell->type == "$pmux_safe")
+	if (cell->type == "$pmux")
 	{
 		int width = cell->parameters["\\WIDTH"].as_int();
 		int s_width = cell->getPort("\\S").size();
@@ -792,18 +801,17 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		f << stringf("%s" "  input [%d:0] s;\n", indent.c_str(), s_width-1);
 
 		dump_attributes(f, indent + "  ", cell->attributes);
-		if (cell->type != "$pmux_safe" && !noattr)
+		if (!noattr)
 			f << stringf("%s" "  (* parallel_case *)\n", indent.c_str());
 		f << stringf("%s" "  casez (s)", indent.c_str());
-		if (cell->type != "$pmux_safe")
-			f << stringf(noattr ? " // synopsys parallel_case\n" : "\n");
+		f << stringf(noattr ? " // synopsys parallel_case\n" : "\n");
 
 		for (int i = 0; i < s_width; i++)
 		{
 			f << stringf("%s" "    %d'b", indent.c_str(), s_width);
 
 			for (int j = s_width-1; j >= 0; j--)
-				f << stringf("%c", j == i ? '1' : cell->type == "$pmux_safe" ? '0' : '?');
+				f << stringf("%c", j == i ? '1' : '?');
 
 			f << stringf(":\n");
 			f << stringf("%s" "      %s = b[%d:%d];\n", indent.c_str(), func_name.c_str(), (i+1)*width-1, i*width);
@@ -1492,12 +1500,14 @@ void dump_proc_switch(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw
 		return;
 	}
 
+	dump_attributes(f, indent, sw->attributes);
 	f << stringf("%s" "casez (", indent.c_str());
 	dump_sigspec(f, sw->signal);
 	f << stringf(")\n");
 
 	bool got_default = false;
 	for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it) {
+		dump_attributes(f, indent + "  ", (*it)->attributes, '\n', /*modattr=*/false, /*as_comment=*/true);
 		if ((*it)->compare.size() == 0) {
 			if (got_default)
 				continue;
@@ -1662,7 +1672,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 		}
 	}
 
-	dump_attributes(f, indent, module->attributes, '\n', true);
+	dump_attributes(f, indent, module->attributes, '\n', /*attr2comment=*/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++) {