diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/aiger/xaiger.cc | 420 | 
1 files changed, 308 insertions, 112 deletions
| diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 46890b071..f17a4c775 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -78,11 +78,13 @@ struct XAigerWriter  	Module *module;  	SigMap sigmap; +	dict<SigBit, bool> init_map;  	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; +	dict<SigBit, int> ff_bits;  	dict<SigBit, float> arrival_times;  	vector<pair<int, int>> aig_gates; @@ -153,13 +155,16 @@ struct XAigerWriter  			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())  		{ +			if (wire->attributes.count("\\init")) { +				SigSpec initsig = sigmap(wire); +				Const initval = wire->attributes.at("\\init"); +				for (int i = 0; i < GetSize(wire) && i < GetSize(initval); i++) +					if (initval[i] == State::S0 || initval[i] == State::S1) +						init_map[initsig[i]] = initval[i] == State::S1; +			} +  			bool keep = wire->attributes.count("\\keep");  			for (int i = 0; i < GetSize(wire); i++) @@ -173,12 +178,13 @@ struct XAigerWriter  				}  				if (keep) -					keep_bits.insert(bit); +					keep_bits.insert(wirebit);  				if (wire->port_input || keep) {  					if (bit != wirebit)  						alias_map[bit] = wirebit;  					input_bits.insert(wirebit); +					undriven_bits.erase(bit);  				}  				if (wire->port_output || keep) { @@ -186,6 +192,8 @@ struct XAigerWriter  						if (bit != wirebit)  							alias_map[wirebit] = bit;  						output_bits.insert(wirebit); +						if (!wire->port_input) +							unused_bits.erase(bit);  					}  					else  						log_debug("Skipping PO '%s' driven by 1'bx\n", log_signal(wirebit)); @@ -193,17 +201,12 @@ struct XAigerWriter  			}  		} -		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 abc9_box_seen = false; +		std::vector<Cell*> flop_boxes;  		for (auto cell : module->selected_cells()) {  			if (cell->type == "$_NOT_") @@ -241,76 +244,90 @@ struct XAigerWriter  			log_assert(!holes_mode); +			if (cell->type == "$__ABC9_FF_") +			{ +				SigBit D = sigmap(cell->getPort("\\D").as_bit()); +				SigBit Q = sigmap(cell->getPort("\\Q").as_bit()); +				unused_bits.erase(D); +				undriven_bits.erase(Q); +				alias_map[Q] = D; +				auto r = ff_bits.insert(std::make_pair(D, 0)); +				log_assert(r.second); +				continue; +			} +  			RTLIL::Module* inst_module = module->design->module(cell->type);  			if (inst_module && inst_module->attributes.count("\\abc9_box_id")) {  				abc9_box_seen = true; -				if (!holes_mode) { -					toposort.node(cell->name); -					for (const auto &conn : cell->connections()) { -						auto port_wire = inst_module->wire(conn.first); -						if (port_wire->port_input) { -							// Ignore inout for the sake of topographical ordering -							if (port_wire->port_output) continue; -							for (auto bit : sigmap(conn.second)) -								bit_users[bit].insert(cell->name); -						} +				toposort.node(cell->name); -						if (port_wire->port_output) -							for (auto bit : sigmap(conn.second)) -								bit_drivers[bit].insert(cell->name); +				for (const auto &conn : cell->connections()) { +					auto port_wire = inst_module->wire(conn.first); +					if (port_wire->port_input) { +						// Ignore inout for the sake of topographical ordering +						if (port_wire->port_output) continue; +						for (auto bit : sigmap(conn.second)) +							bit_users[bit].insert(cell->name);  					} + +					if (port_wire->port_output) +						for (auto bit : sigmap(conn.second)) +							bit_drivers[bit].insert(cell->name);  				} + +				if (inst_module->attributes.count("\\abc9_flop")) +					flop_boxes.push_back(cell); +				continue;  			} -			else { -				bool cell_known = inst_module || cell->known(); -				for (const auto &c : cell->connections()) { -					if (c.second.is_fully_const()) continue; -					auto port_wire = inst_module ? inst_module->wire(c.first) : nullptr; -					auto is_input = (port_wire && port_wire->port_input) || !cell_known || cell->input(c.first); -					auto is_output = (port_wire && port_wire->port_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) { -							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); -							} +			bool cell_known = inst_module || cell->known(); +			for (const auto &c : cell->connections()) { +				if (c.second.is_fully_const()) continue; +				auto port_wire = inst_module ? inst_module->wire(c.first) : nullptr; +				auto is_input = (port_wire && port_wire->port_input) || !cell_known || cell->input(c.first); +				auto is_output = (port_wire && port_wire->port_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) { +						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) { -						int arrival = 0; -						if (port_wire) { -							auto it = port_wire->attributes.find("\\abc9_arrival"); -							if (it != port_wire->attributes.end()) { -								if (it->second.flags != 0) -									log_error("Attribute 'abc9_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type)); -								arrival = it->second.as_int(); -							} +				} +				if (is_output) { +					int arrival = 0; +					if (port_wire) { +						auto it = port_wire->attributes.find("\\abc9_arrival"); +						if (it != port_wire->attributes.end()) { +							if (it->second.flags != 0) +								log_error("Attribute 'abc9_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type)); +							arrival = it->second.as_int();  						} +					} -						for (auto b : c.second) { -							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); - -							if (arrival) -								arrival_times[b] = arrival; -						} +					for (auto b : c.second) { +						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); + +						if (arrival) +							arrival_times[b] = arrival;  					}  				}  			} @@ -319,6 +336,45 @@ struct XAigerWriter  		}  		if (abc9_box_seen) { +			dict<IdString, std::pair<IdString,int>> flop_q; +			for (auto cell : flop_boxes) { +				auto r = flop_q.insert(std::make_pair(cell->type, std::make_pair(IdString(), 0))); +				SigBit d; +				if (r.second) { +					for (const auto &conn : cell->connections()) { +						const SigSpec &rhs = conn.second; +						if (!rhs.is_bit()) +							continue; +						if (!ff_bits.count(rhs)) +							continue; +						r.first->second.first = conn.first; +						Module *inst_module = module->design->module(cell->type); +						Wire *wire = inst_module->wire(conn.first); +						log_assert(wire); +						auto jt = wire->attributes.find("\\abc9_arrival"); +						if (jt != wire->attributes.end()) { +							if (jt->second.flags != 0) +								log_error("Attribute 'abc9_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(wire), log_id(cell->type)); +							r.first->second.second = jt->second.as_int(); +						} +						d = rhs; +						log_assert(d == sigmap(d)); +						break; +					} +				} +				else +					d = cell->getPort(r.first->second.first); + +				auto it = cell->attributes.find(ID(abc9_mergeability)); +				log_assert(it != cell->attributes.end()); +				ff_bits.at(d) = it->second.as_int(); +				cell->attributes.erase(it); + +				auto arrival = r.first->second.second; +				if (arrival) +					arrival_times[d] = arrival; +			} +  			for (auto &it : bit_users)  				if (bit_drivers.count(it.first))  					for (auto driver_cell : bit_drivers.at(it.first)) @@ -414,6 +470,29 @@ struct XAigerWriter  						}  					}  				} + +				// Connect <cell>.$abc9_currQ (inserted by abc9_map.v) as an input to the flop box +				if (box_module->get_bool_attribute("\\abc9_flop")) { +					SigSpec rhs = module->wire(stringf("%s.$abc9_currQ", cell->name.c_str())); +					if (rhs.empty()) +						log_error("'%s.$abc9_currQ' is not a wire present in module '%s'.\n", log_id(cell), log_id(module)); + +					int offset = 0; +					for (auto b : rhs) { +						SigBit I = sigmap(b); +						if (b == RTLIL::Sx) +							b = State::S0; +						else if (I != b) { +							if (I == RTLIL::Sx) +								alias_map[b] = State::S0; +							else +								alias_map[b] = I; +						} +						co_bits.emplace_back(b, cell, "\\$abc9_currQ", offset++, 0); +						unused_bits.erase(b); +					} +				} +  				box_list.emplace_back(cell);  			} @@ -492,10 +571,20 @@ struct XAigerWriter  			aig_map[bit] = 2*aig_m;  		} +		for (const auto &i : ff_bits) { +			const SigBit &bit = i.first; +			aig_m++, aig_i++; +			log_assert(!aig_map.count(bit)); +			aig_map[bit] = 2*aig_m; +		} + +		dict<SigBit, int> ff_aig_map;  		for (auto &c : ci_bits) {  			RTLIL::SigBit bit = std::get<0>(c);  			aig_m++, aig_i++; -			aig_map[bit] = 2*aig_m; +			auto r = aig_map.insert(std::make_pair(bit, 2*aig_m)); +			if (!r.second) +				ff_aig_map[bit] = 2*aig_m;  		}  		for (auto &c : co_bits) { @@ -514,6 +603,17 @@ struct XAigerWriter  			aig_outputs.push_back(bit2aig(bit));  		} +		for (auto &i : ff_bits) { +			const SigBit &bit = i.first; +			aig_o++; +			aig_outputs.push_back(ff_aig_map.at(bit)); +		} + +		if (output_bits.empty()) { +			aig_o++; +			aig_outputs.push_back(0); +			omode = true; +		}  	}  	void write_aiger(std::ostream &f, bool ascii_mode) @@ -583,14 +683,14 @@ struct XAigerWriter  		std::stringstream h_buffer;  		auto write_h_buffer = std::bind(write_buffer, std::ref(h_buffer), std::placeholders::_1);  		write_h_buffer(1); -		log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ci_bits)); -		write_h_buffer(input_bits.size() + ci_bits.size()); -		log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(co_bits)); -		write_h_buffer(output_bits.size() + GetSize(co_bits)); -		log_debug("piNum = %d\n", GetSize(input_bits)); -		write_h_buffer(input_bits.size()); -		log_debug("poNum = %d\n", GetSize(output_bits)); -		write_h_buffer(output_bits.size()); +		log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ff_bits) + GetSize(ci_bits)); +		write_h_buffer(input_bits.size() + ff_bits.size() + ci_bits.size()); +		log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(ff_bits) + GetSize(co_bits)); +		write_h_buffer(output_bits.size() + GetSize(ff_bits) + GetSize(co_bits)); +		log_debug("piNum = %d\n", GetSize(input_bits) + GetSize(ff_bits)); +		write_h_buffer(input_bits.size() + ff_bits.size()); +		log_debug("poNum = %d\n", GetSize(output_bits) + GetSize(ff_bits)); +		write_h_buffer(output_bits.size() + ff_bits.size());  		log_debug("boxNum = %d\n", GetSize(box_list));  		write_h_buffer(box_list.size()); @@ -606,19 +706,29 @@ struct XAigerWriter  		//for (auto bit : output_bits)  		//	write_o_buffer(0); -		if (!box_list.empty()) { +		if (!box_list.empty() || !ff_bits.empty()) {  			RTLIL::Module *holes_module = module->design->addModule("$__holes__");  			log_assert(holes_module); +			dict<IdString, Cell*> cell_cache; +  			int port_id = 1;  			int box_count = 0;  			for (auto cell : box_list) {  				RTLIL::Module* box_module = module->design->module(cell->type); +				log_assert(box_module); +				IdString derived_name = box_module->derive(module->design, cell->parameters); +				box_module = module->design->module(derived_name); +				if (box_module->has_processes()) +					Pass::call_on_module(module->design, box_module, "proc"); +  				int box_inputs = 0, box_outputs = 0; -				Cell *holes_cell = nullptr; -				if (box_module->get_bool_attribute("\\whitebox")) { +				auto r = cell_cache.insert(std::make_pair(derived_name, nullptr)); +				Cell *holes_cell = r.first->second; +				if (r.second && !holes_cell && box_module->get_bool_attribute("\\whitebox")) {  					holes_cell = holes_module->addCell(cell->name, cell->type);  					holes_cell->parameters = cell->parameters; +					r.first->second = holes_cell;  				}  				// NB: Assume box_module->ports are sorted alphabetically @@ -627,8 +737,8 @@ struct XAigerWriter  					RTLIL::Wire *w = box_module->wire(port_name);  					log_assert(w);  					RTLIL::Wire *holes_wire; -					RTLIL::SigSpec port_wire; -					if (w->port_input) { +					RTLIL::SigSpec port_sig; +					if (w->port_input)  						for (int i = 0; i < GetSize(w); i++) {  							box_inputs++;  							holes_wire = holes_module->wire(stringf("\\i%d", box_inputs)); @@ -639,29 +749,47 @@ struct XAigerWriter  								holes_module->ports.push_back(holes_wire->name);  							}  							if (holes_cell) -								port_wire.append(holes_wire); +								port_sig.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())); +								holes_wire = holes_module->addWire(stringf("$abc%s.%s", cell->name.c_str(), log_id(w->name)));  							else -								holes_wire = holes_module->addWire(stringf("%s.%s[%d]", cell->name.c_str(), w->name.c_str(), i)); +								holes_wire = holes_module->addWire(stringf("$abc%s.%s[%d]", cell->name.c_str(), log_id(w->name), 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); +								port_sig.append(holes_wire);  							else  								holes_module->connect(holes_wire, State::S0);  						} -						if (!port_wire.empty()) -							holes_cell->setPort(w->name, port_wire);  					} +					if (!port_sig.empty()) { +						if (r.second) +							holes_cell->setPort(w->name, port_sig); +						else +							holes_module->connect(holes_cell->getPort(w->name), port_sig); +					} +				} + +				// For flops only, create an extra 1-bit input that drives a new wire +				//   called "<cell>.$abc9_currQ" that is used below +				if (box_module->get_bool_attribute("\\abc9_flop")) { +					log_assert(holes_cell); + +					box_inputs++; +					Wire *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); +					} +					Wire *w = holes_module->addWire(stringf("%s.$abc9_currQ", cell->name.c_str())); +					holes_module->connect(w, holes_wire);  				}  				write_h_buffer(box_inputs); @@ -672,13 +800,44 @@ struct XAigerWriter  			std::stringstream r_buffer;  			auto write_r_buffer = std::bind(write_buffer, std::ref(r_buffer), std::placeholders::_1); -			write_r_buffer(0); +			log_debug("flopNum = %d\n", GetSize(ff_bits)); +			write_r_buffer(ff_bits.size()); +			for (const auto &i : ff_bits) { +				log_assert(i.second > 0); +				write_r_buffer(i.second); +				const SigBit &bit = i.first; +				write_i_buffer(arrival_times.at(bit, 0)); +				//write_o_buffer(0); +			} +  			f << "r";  			std::string buffer_str = r_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 s_buffer; +			auto write_s_buffer = std::bind(write_buffer, std::ref(s_buffer), std::placeholders::_1); +			write_s_buffer(ff_bits.size()); +			for (const auto &i : ff_bits) { +				const SigBit &bit = i.first; +				auto it = bit.wire->attributes.find("\\init"); +				if (it != bit.wire->attributes.end()) { +					auto init = it->second[bit.offset]; +					if (init == RTLIL::S1) { +						write_s_buffer(1); +						continue; +					} +				} +				// Default flop init is zero +				write_s_buffer(0); +			} +			f << "s"; +			buffer_str = s_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(); @@ -686,37 +845,63 @@ struct XAigerWriter  				//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_")) +				Pass::call_on_module(holes_module->design, holes_module, "flatten -wb; techmap; aigmap"); + +				dict<SigSig, SigSig> replace; +				for (auto it = holes_module->cells_.begin(); it != holes_module->cells_.end(); ) { +					auto cell = it->second; +					if (cell->type.in("$_DFF_N_", "$_DFF_NN0_", "$_DFF_NN1_", "$_DFF_NP0_", "$_DFF_NP1_", +											"$_DFF_P_", "$_DFF_PN0_", "$_DFF_PN1", "$_DFF_PP0_", "$_DFF_PP1_")) { +						SigBit D = cell->getPort("\\D"); +						SigBit Q = cell->getPort("\\Q"); +						// Remove the DFF cell from what needs to be a combinatorial box +						it = holes_module->cells_.erase(it); +						Wire *port; +						if (GetSize(Q.wire) == 1) +							port = holes_module->wire(stringf("$abc%s", Q.wire->name.c_str())); +						else +							port = holes_module->wire(stringf("$abc%s[%d]", Q.wire->name.c_str(), Q.offset)); +						log_assert(port); +						// Prepare to replace "assign <port> = DFF.Q;" with "assign <port> = DFF.D;" +						//   in order to extract the combinatorial control logic that feeds the box +						//   (i.e. clock enable, synchronous reset, etc.) +						replace.insert(std::make_pair(SigSig(port,Q), SigSig(port,D))); +						// Since `flatten` above would have created wires named "<cell>.Q", +						//   extract the pre-techmap cell name +						auto pos = Q.wire->name.str().rfind("."); +						log_assert(pos != std::string::npos); +						IdString driver = Q.wire->name.substr(0, pos); +						// And drive the signal that was previously driven by "DFF.Q" (typically +						//   used to implement clock-enable functionality) with the "<cell>.$abc9_currQ" +						//   wire (which itself is driven an input port) we inserted above +						Wire *currQ = holes_module->wire(stringf("%s.$abc9_currQ", driver.c_str())); +						log_assert(currQ); +						holes_module->connect(Q, currQ); +						continue; +					} +					else if (!cell->type.in("$_NOT_", "$_AND_"))  						log_error("Whitebox contents cannot be represented as AIG. Please verify whiteboxes are synthesisable.\n"); +					++it; +				} -				holes_module->design->selection_stack.pop_back(); +				for (auto &conn : holes_module->connections_) { +					auto it = replace.find(conn); +					if (it != replace.end()) +						conn = it->second; +				}  				// Move into a new (temporary) design so that "clean" will only  				// operate (and run checks on) this one module  				RTLIL::Design *holes_design = new RTLIL::Design; -				holes_module->design->modules_.erase(holes_module->name); +				module->design->modules_.erase(holes_module->name);  				holes_design->add(holes_module);  				Pass::call(holes_design, "clean -purge");  				std::stringstream a_buffer;  				XAigerWriter writer(holes_module, true /* holes_mode */);  				writer.write_aiger(a_buffer, false /*ascii_mode*/); -  				delete holes_design;  				f << "a"; @@ -752,6 +937,7 @@ struct XAigerWriter  	void write_map(std::ostream &f, bool verbose_map)  	{  		dict<int, string> input_lines; +		dict<int, string> init_lines;  		dict<int, string> output_lines;  		dict<int, string> wire_lines; @@ -773,7 +959,11 @@ struct XAigerWriter  				if (output_bits.count(b)) {  					int o = ordered_outputs.at(b); -					output_lines[o] += stringf("output %d %d %s\n", o - GetSize(co_bits), i, log_id(wire)); +					int init = 0; +					auto it = init_map.find(b); +					if (it != init_map.end() && it->second) +						init = 1; +					output_lines[o] += stringf("output %d %d %s %d\n", o - GetSize(co_bits), i, log_id(wire), init);  					continue;  				} @@ -792,6 +982,10 @@ struct XAigerWriter  			f << it.second;  		log_assert(input_lines.size() == input_bits.size()); +		init_lines.sort(); +		for (auto &it : init_lines) +			f << it.second; +  		int box_count = 0;  		for (auto cell : box_list)  			f << stringf("box %d %d %s\n", box_count++, 0, log_id(cell->name)); @@ -802,6 +996,8 @@ struct XAigerWriter  		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) @@ -824,7 +1020,7 @@ struct XAigerBackend : public Backend {  		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("        write an extra file with port and box symbols\n");  		log("\n");  		log("    -vmap <filename>\n");  		log("        like -map, but more verbose\n"); | 
