Merge branch 'master' of github.com:YosysHQ/yosys into firrtl_backend_fileinfo

14 files changed, 1243 insertions, 1131 deletions

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index a51e3648c..cac32a8da 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -126,9 +126,9 @@ struct AigerWriter
 
 		for (auto wire : module->wires())
 		{
-			if (wire->attributes.count("\\init")) {
+			if (wire->attributes.count(ID::init)) {
 				SigSpec initsig = sigmap(wire);
-				Const initval = wire->attributes.at("\\init");
+				Const initval = wire->attributes.at(ID::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;
@@ -169,31 +169,31 @@ struct AigerWriter
 
 		for (auto cell : module->cells())
 		{
-			if (cell->type == "$_NOT_")
+			if (cell->type == ID($_NOT_))
 			{
-				SigBit A = sigmap(cell->getPort("\\A").as_bit());
-				SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
+				SigBit A = sigmap(cell->getPort(ID::A).as_bit());
+				SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
 				unused_bits.erase(A);
 				undriven_bits.erase(Y);
 				not_map[Y] = A;
 				continue;
 			}
 
-			if (cell->type.in("$_FF_", "$_DFF_N_", "$_DFF_P_"))
+			if (cell->type.in(ID($_FF_), ID($_DFF_N_), ID($_DFF_P_)))
 			{
-				SigBit D = sigmap(cell->getPort("\\D").as_bit());
-				SigBit Q = sigmap(cell->getPort("\\Q").as_bit());
+				SigBit D = sigmap(cell->getPort(ID::D).as_bit());
+				SigBit Q = sigmap(cell->getPort(ID::Q).as_bit());
 				unused_bits.erase(D);
 				undriven_bits.erase(Q);
 				ff_map[Q] = D;
 				continue;
 			}
 
-			if (cell->type == "$_AND_")
+			if (cell->type == ID($_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());
+				SigBit A = sigmap(cell->getPort(ID::A).as_bit());
+				SigBit B = sigmap(cell->getPort(ID::B).as_bit());
+				SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
 				unused_bits.erase(A);
 				unused_bits.erase(B);
 				undriven_bits.erase(Y);
@@ -201,66 +201,66 @@ struct AigerWriter
 				continue;
 			}
 
-			if (cell->type == "$initstate")
+			if (cell->type == ID($initstate))
 			{
-				SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
+				SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
 				undriven_bits.erase(Y);
 				initstate_bits.insert(Y);
 				continue;
 			}
 
-			if (cell->type == "$assert")
+			if (cell->type == ID($assert))
 			{
-				SigBit A = sigmap(cell->getPort("\\A").as_bit());
-				SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
+				SigBit A = sigmap(cell->getPort(ID::A).as_bit());
+				SigBit EN = sigmap(cell->getPort(ID::EN).as_bit());
 				unused_bits.erase(A);
 				unused_bits.erase(EN);
 				asserts.push_back(make_pair(A, EN));
 				continue;
 			}
 
-			if (cell->type == "$assume")
+			if (cell->type == ID($assume))
 			{
-				SigBit A = sigmap(cell->getPort("\\A").as_bit());
-				SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
+				SigBit A = sigmap(cell->getPort(ID::A).as_bit());
+				SigBit EN = sigmap(cell->getPort(ID::EN).as_bit());
 				unused_bits.erase(A);
 				unused_bits.erase(EN);
 				assumes.push_back(make_pair(A, EN));
 				continue;
 			}
 
-			if (cell->type == "$live")
+			if (cell->type == ID($live))
 			{
-				SigBit A = sigmap(cell->getPort("\\A").as_bit());
-				SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
+				SigBit A = sigmap(cell->getPort(ID::A).as_bit());
+				SigBit EN = sigmap(cell->getPort(ID::EN).as_bit());
 				unused_bits.erase(A);
 				unused_bits.erase(EN);
 				liveness.push_back(make_pair(A, EN));
 				continue;
 			}
 
-			if (cell->type == "$fair")
+			if (cell->type == ID($fair))
 			{
-				SigBit A = sigmap(cell->getPort("\\A").as_bit());
-				SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
+				SigBit A = sigmap(cell->getPort(ID::A).as_bit());
+				SigBit EN = sigmap(cell->getPort(ID::EN).as_bit());
 				unused_bits.erase(A);
 				unused_bits.erase(EN);
 				fairness.push_back(make_pair(A, EN));
 				continue;
 			}
 
-			if (cell->type == "$anyconst")
+			if (cell->type == ID($anyconst))
 			{
-				for (auto bit : sigmap(cell->getPort("\\Y"))) {
+				for (auto bit : sigmap(cell->getPort(ID::Y))) {
 					undriven_bits.erase(bit);
 					ff_map[bit] = bit;
 				}
 				continue;
 			}
 
-			if (cell->type == "$anyseq")
+			if (cell->type == ID($anyseq))
 			{
-				for (auto bit : sigmap(cell->getPort("\\Y"))) {
+				for (auto bit : sigmap(cell->getPort(ID::Y))) {
 					undriven_bits.erase(bit);
 					input_bits.insert(bit);
 				}
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index cde6d066a..3b51d8685 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -174,7 +174,7 @@ struct XAigerWriter
 				undriven_bits.insert(bit);
 				unused_bits.insert(bit);
 
-				bool scc = wire->attributes.count(ID(abc9_scc));
+				bool scc = wire->attributes.count(ID::abc9_scc);
 				if (wire->port_input || scc)
 					input_bits.insert(bit);
 
@@ -190,21 +190,21 @@ struct XAigerWriter
 
 		for (auto cell : module->cells()) {
 			if (!cell->has_keep_attr()) {
-				if (cell->type == "$_NOT_")
+				if (cell->type == ID($_NOT_))
 				{
-					SigBit A = sigmap(cell->getPort("\\A").as_bit());
-					SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
+					SigBit A = sigmap(cell->getPort(ID::A).as_bit());
+					SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
 					unused_bits.erase(A);
 					undriven_bits.erase(Y);
 					not_map[Y] = A;
 					continue;
 				}
 
-				if (cell->type == "$_AND_")
+				if (cell->type == ID($_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());
+					SigBit A = sigmap(cell->getPort(ID::A).as_bit());
+					SigBit B = sigmap(cell->getPort(ID::B).as_bit());
+					SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
 					unused_bits.erase(A);
 					unused_bits.erase(B);
 					undriven_bits.erase(Y);
@@ -212,13 +212,13 @@ struct XAigerWriter
 					continue;
 				}
 
-				if (cell->type == "$__ABC9_FF_" &&
+				if (cell->type == ID($__ABC9_FF_) &&
 						// The presence of an abc9_mergeability attribute indicates
 						//   that we do want to pass this flop to ABC
-						cell->attributes.count("\\abc9_mergeability"))
+						cell->attributes.count(ID::abc9_mergeability))
 				{
-					SigBit D = sigmap(cell->getPort("\\D").as_bit());
-					SigBit Q = sigmap(cell->getPort("\\Q").as_bit());
+					SigBit D = sigmap(cell->getPort(ID::D).as_bit());
+					SigBit Q = sigmap(cell->getPort(ID::Q).as_bit());
 					unused_bits.erase(D);
 					undriven_bits.erase(Q);
 					alias_map[Q] = D;
@@ -227,7 +227,7 @@ struct XAigerWriter
 					continue;
 				}
 
-				if (cell->type.in("$specify2", "$specify3", "$specrule"))
+				if (cell->type.in(ID($specify2), ID($specify3), ID($specrule)))
 					continue;
 			}
 
@@ -239,7 +239,7 @@ struct XAigerWriter
 
 				bool abc9_flop = false;
 				if (!cell->has_keep_attr()) {
-					auto it = cell->attributes.find("\\abc9_box_seq");
+					auto it = cell->attributes.find(ID::abc9_box_seq);
 					if (it != cell->attributes.end()) {
 						int abc9_box_seq = it->second.as_int();
 						if (GetSize(box_list) <= abc9_box_seq)
@@ -247,7 +247,7 @@ struct XAigerWriter
 						box_list[abc9_box_seq] = cell;
 						// Only flop boxes may have arrival times
 						//   (all others are combinatorial)
-						abc9_flop = inst_module->get_bool_attribute("\\abc9_flop");
+						abc9_flop = inst_module->get_bool_attribute(ID::abc9_flop);
 						if (!abc9_flop)
 							continue;
 					}
@@ -315,7 +315,7 @@ struct XAigerWriter
 
 			RTLIL::Module* box_module = module->design->module(cell->type);
 			log_assert(box_module);
-			log_assert(box_module->attributes.count("\\abc9_box_id") || box_module->get_bool_attribute("\\abc9_flop"));
+			log_assert(box_module->attributes.count(ID::abc9_box_id) || box_module->get_bool_attribute(ID::abc9_flop));
 
 			auto r = box_ports.insert(cell->type);
 			if (r.second) {
@@ -325,7 +325,7 @@ struct XAigerWriter
 				for (const auto &port_name : box_module->ports) {
 					auto w = box_module->wire(port_name);
 					log_assert(w);
-					if (w->get_bool_attribute("\\abc9_carry")) {
+					if (w->get_bool_attribute(ID::abc9_carry)) {
 						if (w->port_input) {
 							if (carry_in != IdString())
 								log_error("Module '%s' contains more than one 'abc9_carry' input port.\n", log_id(box_module));
@@ -381,7 +381,7 @@ struct XAigerWriter
 			}
 
 			// Connect <cell>.abc9_ff.Q (inserted by abc9_map.v) as the last input to the flop box
-			if (box_module->get_bool_attribute("\\abc9_flop")) {
+			if (box_module->get_bool_attribute(ID::abc9_flop)) {
 				SigSpec rhs = module->wire(stringf("%s.abc9_ff.Q", cell->name.c_str()));
 				if (rhs.empty())
 					log_error("'%s.abc9_ff.Q' is not a wire present in module '%s'.\n", log_id(cell), log_id(module));
@@ -437,7 +437,7 @@ struct XAigerWriter
 
 		for (const auto &i : ff_bits) {
 			const Cell *cell = i.second;
-			const SigBit &q = sigmap(cell->getPort("\\Q"));
+			const SigBit &q = sigmap(cell->getPort(ID::Q));
 			aig_m++, aig_i++;
 			log_assert(!aig_map.count(q));
 			aig_map[q] = 2*aig_m;
@@ -608,12 +608,12 @@ struct XAigerWriter
 
 					// For flops only, create an extra 1-bit input that drives a new wire
 					//   called "<cell>.abc9_ff.Q" that is used below
-					if (box_module->get_bool_attribute("\\abc9_flop"))
+					if (box_module->get_bool_attribute(ID::abc9_flop))
 						box_inputs++;
 
 					std::get<0>(v) = box_inputs;
 					std::get<1>(v) = box_outputs;
-					std::get<2>(v) = box_module->attributes.at("\\abc9_box_id").as_int();
+					std::get<2>(v) = box_module->attributes.at(ID::abc9_box_id).as_int();
 				}
 
 				write_h_buffer(std::get<0>(v));
@@ -635,11 +635,11 @@ struct XAigerWriter
 				const SigBit &d = i.first;
 				const Cell *cell = i.second;
 
-				int mergeability = cell->attributes.at(ID(abc9_mergeability)).as_int();
+				int mergeability = cell->attributes.at(ID::abc9_mergeability).as_int();
 				log_assert(mergeability > 0);
 				write_r_buffer(mergeability);
 
-				Const init = cell->attributes.at(ID(abc9_init), State::Sx);
+				Const init = cell->attributes.at(ID::abc9_init, State::Sx);
 				log_assert(GetSize(init) == 1);
 				if (init == State::S1)
 					write_s_buffer(1);
diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc
index b6e38c16c..b028df848 100644
--- a/backends/blif/blif.cc
+++ b/backends/blif/blif.cc
@@ -69,9 +69,9 @@ struct BlifDumper
 			f(f), module(module), design(design), config(config), ct(design), sigmap(module)
 	{
 		for (Wire *wire : module->wires())
-			if (wire->attributes.count("\\init")) {
+			if (wire->attributes.count(ID::init)) {
 				SigSpec initsig = sigmap(wire);
-				Const initval = wire->attributes.at("\\init");
+				Const initval = wire->attributes.at(ID::init);
 				for (int i = 0; i < GetSize(initsig) && i < GetSize(initval); i++)
 					switch (initval[i]) {
 						case State::S0:
@@ -138,9 +138,9 @@ struct BlifDumper
 	{
 		if (!config->gates_mode)
 			return "subckt";
-		if (!design->modules_.count(RTLIL::escape_id(cell_type)))
+		if (design->module(RTLIL::escape_id(cell_type)) == nullptr)
 			return "gate";
-		if (design->modules_.at(RTLIL::escape_id(cell_type))->get_blackbox_attribute())
+		if (design->module(RTLIL::escape_id(cell_type))->get_blackbox_attribute())
 			return "gate";
 		return "subckt";
 	}
@@ -148,7 +148,7 @@ struct BlifDumper
 	void dump_params(const char *command, dict<IdString, Const> &params)
 	{
 		for (auto &param : params) {
-			f << stringf("%s %s ", command, RTLIL::id2cstr(param.first));
+			f << stringf("%s %s ", command, log_id(param.first));
 			if (param.second.flags & RTLIL::CONST_FLAG_STRING) {
 				std::string str = param.second.decode_string();
 				f << stringf("\"");
@@ -172,8 +172,7 @@ struct BlifDumper
 
 		std::map<int, RTLIL::Wire*> inputs, outputs;
 
-		for (auto &wire_it : module->wires_) {
-			RTLIL::Wire *wire = wire_it.second;
+		for (auto wire : module->wires()) {
 			if (wire->port_input)
 				inputs[wire->port_id] = wire;
 			if (wire->port_output)
@@ -229,10 +228,8 @@ struct BlifDumper
 				f << stringf(".names $undef\n");
 		}
 
-		for (auto &cell_it : module->cells_)
+		for (auto cell : 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",
@@ -240,142 +237,142 @@ struct BlifDumper
 				continue;
 			}
 
-			if (!config->icells_mode && cell->type == "$_NOT_") {
+			if (!config->icells_mode && cell->type == ID($_NOT_)) {
 				f << stringf(".names %s %s\n0 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_AND_") {
+			if (!config->icells_mode && cell->type == ID($_AND_)) {
 				f << stringf(".names %s %s %s\n11 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_OR_") {
+			if (!config->icells_mode && cell->type == ID($_OR_)) {
 				f << stringf(".names %s %s %s\n1- 1\n-1 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_XOR_") {
+			if (!config->icells_mode && cell->type == ID($_XOR_)) {
 				f << stringf(".names %s %s %s\n10 1\n01 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_NAND_") {
+			if (!config->icells_mode && cell->type == ID($_NAND_)) {
 				f << stringf(".names %s %s %s\n0- 1\n-0 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_NOR_") {
+			if (!config->icells_mode && cell->type == ID($_NOR_)) {
 				f << stringf(".names %s %s %s\n00 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_XNOR_") {
+			if (!config->icells_mode && cell->type == ID($_XNOR_)) {
 				f << stringf(".names %s %s %s\n11 1\n00 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_ANDNOT_") {
+			if (!config->icells_mode && cell->type == ID($_ANDNOT_)) {
 				f << stringf(".names %s %s %s\n10 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_ORNOT_") {
+			if (!config->icells_mode && cell->type == ID($_ORNOT_)) {
 				f << stringf(".names %s %s %s\n1- 1\n-0 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_AOI3_") {
+			if (!config->icells_mode && cell->type == ID($_AOI3_)) {
 				f << stringf(".names %s %s %s %s\n-00 1\n0-0 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\C")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_OAI3_") {
+			if (!config->icells_mode && cell->type == ID($_OAI3_)) {
 				f << stringf(".names %s %s %s %s\n00- 1\n--0 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\C")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_AOI4_") {
+			if (!config->icells_mode && cell->type == ID($_AOI4_)) {
 				f << stringf(".names %s %s %s %s %s\n-0-0 1\n-00- 1\n0--0 1\n0-0- 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
-						cstr(cell->getPort("\\C")), cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)),
+						cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_OAI4_") {
+			if (!config->icells_mode && cell->type == ID($_OAI4_)) {
 				f << stringf(".names %s %s %s %s %s\n00-- 1\n--00 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
-						cstr(cell->getPort("\\C")), cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)),
+						cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_MUX_") {
+			if (!config->icells_mode && cell->type == ID($_MUX_)) {
 				f << stringf(".names %s %s %s %s\n1-0 1\n-11 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
-						cstr(cell->getPort("\\S")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)),
+						cstr(cell->getPort(ID::S)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_NMUX_") {
+			if (!config->icells_mode && cell->type == ID($_NMUX_)) {
 				f << stringf(".names %s %s %s %s\n0-0 1\n-01 1\n",
-						cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
-						cstr(cell->getPort("\\S")), cstr(cell->getPort("\\Y")));
+						cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)),
+						cstr(cell->getPort(ID::S)), cstr(cell->getPort(ID::Y)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_FF_") {
-				f << stringf(".latch %s %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
-						cstr_init(cell->getPort("\\Q")));
+			if (!config->icells_mode && cell->type == ID($_FF_)) {
+				f << stringf(".latch %s %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)),
+						cstr_init(cell->getPort(ID::Q)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_DFF_N_") {
-				f << stringf(".latch %s %s fe %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
-						cstr(cell->getPort("\\C")), cstr_init(cell->getPort("\\Q")));
+			if (!config->icells_mode && cell->type == ID($_DFF_N_)) {
+				f << stringf(".latch %s %s fe %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)),
+						cstr(cell->getPort(ID::C)), cstr_init(cell->getPort(ID::Q)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_DFF_P_") {
-				f << stringf(".latch %s %s re %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
-						cstr(cell->getPort("\\C")), cstr_init(cell->getPort("\\Q")));
+			if (!config->icells_mode && cell->type == ID($_DFF_P_)) {
+				f << stringf(".latch %s %s re %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)),
+						cstr(cell->getPort(ID::C)), cstr_init(cell->getPort(ID::Q)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_DLATCH_N_") {
-				f << stringf(".latch %s %s al %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
-						cstr(cell->getPort("\\E")), cstr_init(cell->getPort("\\Q")));
+			if (!config->icells_mode && cell->type == ID($_DLATCH_N_)) {
+				f << stringf(".latch %s %s al %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)),
+						cstr(cell->getPort(ID::E)), cstr_init(cell->getPort(ID::Q)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$_DLATCH_P_") {
-				f << stringf(".latch %s %s ah %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
-						cstr(cell->getPort("\\E")), cstr_init(cell->getPort("\\Q")));
+			if (!config->icells_mode && cell->type == ID($_DLATCH_P_)) {
+				f << stringf(".latch %s %s ah %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)),
+						cstr(cell->getPort(ID::E)), cstr_init(cell->getPort(ID::Q)));
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$lut") {
+			if (!config->icells_mode && cell->type == ID($lut)) {
 				f << stringf(".names");
-				auto &inputs = cell->getPort("\\A");
-				auto width = cell->parameters.at("\\WIDTH").as_int();
+				auto &inputs = cell->getPort(ID::A);
+				auto width = cell->parameters.at(ID::WIDTH).as_int();
 				log_assert(inputs.size() == width);
 				for (int i = width-1; i >= 0; i--)
 					f << stringf(" %s", cstr(inputs.extract(i, 1)));
-				auto &output = cell->getPort("\\Y");
+				auto &output = cell->getPort(ID::Y);
 				log_assert(output.size() == 1);
 				f << stringf(" %s", cstr(output));
 				f << stringf("\n");
-				RTLIL::SigSpec mask = cell->parameters.at("\\LUT");
+				RTLIL::SigSpec mask = cell->parameters.at(ID::LUT);
 				for (int i = 0; i < (1 << width); i++)
 					if (mask[i] == State::S1) {
 						for (int j = width-1; j >= 0; j--) {
@@ -386,18 +383,18 @@ struct BlifDumper
 				goto internal_cell;
 			}
 
-			if (!config->icells_mode && cell->type == "$sop") {
+			if (!config->icells_mode && cell->type == ID($sop)) {
 				f << stringf(".names");
-				auto &inputs = cell->getPort("\\A");
-				auto width = cell->parameters.at("\\WIDTH").as_int();
-				auto depth = cell->parameters.at("\\DEPTH").as_int();
-				vector<State> table = cell->parameters.at("\\TABLE").bits;
+				auto &inputs = cell->getPort(ID::A);
+				auto width = cell->parameters.at(ID::WIDTH).as_int();
+				auto depth = cell->parameters.at(ID::DEPTH).as_int();
+				vector<State> table = cell->parameters.at(ID::TABLE).bits;
 				while (GetSize(table) < 2*width*depth)
 					table.push_back(State::S0);
 				log_assert(inputs.size() == width);
 				for (int i = 0; i < width; i++)
 					f << stringf(" %s", cstr(inputs.extract(i, 1)));
-				auto &output = cell->getPort("\\Y");
+				auto &output = cell->getPort(ID::Y);
 				log_assert(output.size() == 1);
 				f << stringf(" %s", cstr(output));
 				f << stringf("\n");
@@ -649,25 +646,24 @@ struct BlifBackend : public Backend {
 		extra_args(f, filename, args, argidx);
 
 		if (top_module_name.empty())
-			for (auto & mod_it:design->modules_)
-				if (mod_it.second->get_bool_attribute("\\top"))
-					top_module_name = mod_it.first.str();
+			for (auto module : design->modules())
+				if (module->get_bool_attribute(ID::top))
+					top_module_name = module->name.str();
 
 		*f << stringf("# Generated by %s\n", yosys_version_str);
 
 		std::vector<RTLIL::Module*> mod_list;
 
 		design->sort();
-		for (auto module_it : design->modules_)
+		for (auto module : design->modules())
 		{
-			RTLIL::Module *module = module_it.second;
 			if (module->get_blackbox_attribute() && !config.blackbox_mode)
 				continue;
 
 			if (module->processes.size() != 0)
-				log_error("Found unmapped processes in module %s: unmapped processes are not supported in BLIF backend!\n", RTLIL::id2cstr(module->name));
+				log_error("Found unmapped processes in module %s: unmapped processes are not supported in BLIF backend!\n", log_id(module->name));
 			if (module->memories.size() != 0)
-				log_error("Found unmapped memories in module %s: unmapped memories are not supported in BLIF backend!\n", RTLIL::id2cstr(module->name));
+				log_error("Found unmapped memories in module %s: unmapped memories are not supported in BLIF backend!\n", log_id(module->name));
 
 			if (module->name == RTLIL::escape_id(top_module_name)) {
 				BlifDumper::dump(*f, module, design, config);
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index c1da4b127..14c8484e8 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -39,6 +39,7 @@ struct BtorWorker
 	RTLIL::Module *module;
 	bool verbose;
 	bool single_bad;
+	bool cover_mode;
 
 	int next_nid = 1;
 	int initstate_nid = -1;
@@ -71,7 +72,11 @@ struct BtorWorker
 	vector<int> bad_properties;
 	dict<SigBit, bool> initbits;
 	pool<Wire*> statewires;
-	string indent;
+	pool<string> srcsymbols;
+
+	string indent, info_filename;
+	vector<string> info_lines;
+	dict<int, int> info_clocks;
 
 	void btorf(const char *fmt, ...)
 	{
@@ -81,6 +86,40 @@ struct BtorWorker
 		va_end(ap);
 	}
 
+	void infof(const char *fmt, ...)
+	{
+		va_list ap;
+		va_start(ap, fmt);
+		info_lines.push_back(vstringf(fmt, ap));
+		va_end(ap);
+	}
+
+	template<typename T>
+	string getinfo(T *obj, bool srcsym = false)
+	{
+		string infostr = log_id(obj);
+		if (obj->attributes.count(ID::src)) {
+			string src = obj->attributes.at(ID::src).decode_string().c_str();
+			if (srcsym && infostr[0] == '$') {
+				std::replace(src.begin(), src.end(), ' ', '_');
+				if (srcsymbols.count(src) || module->count_id("\\" + src)) {
+					for (int i = 1;; i++) {
+						string s = stringf("%s-%d", src.c_str(), i);
+						if (!srcsymbols.count(s) && !module->count_id("\\" + s)) {
+							src = s;
+							break;
+						}
+					}
+				}
+				srcsymbols.insert(src);
+				infostr = src;
+			} else {
+				infostr += " ; " + src;
+			}
+		}
+		return infostr;
+	}
+
 	void btorf_push(const string &id)
 	{
 		if (verbose) {
@@ -144,40 +183,40 @@ struct BtorWorker
 		cell_recursion_guard.insert(cell);
 		btorf_push(log_id(cell));
 
-		if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx",
-				"$concat", "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
+		if (cell->type.in(ID($add), ID($sub), ID($mul), ID($and), ID($or), ID($xor), ID($xnor), ID($shl), ID($sshl), ID($shr), ID($sshr), ID($shift), ID($shiftx),
+				ID($concat), ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_)))
 		{
 			string btor_op;
-			if (cell->type == "$add") btor_op = "add";
-			if (cell->type == "$sub") btor_op = "sub";
-			if (cell->type == "$mul") btor_op = "mul";
-			if (cell->type.in("$shl", "$sshl")) btor_op = "sll";
-			if (cell->type == "$shr") btor_op = "srl";
-			if (cell->type == "$sshr") btor_op = "sra";
-			if (cell->type.in("$shift", "$shiftx")) btor_op = "shift";
-			if (cell->type.in("$and", "$_AND_")) btor_op = "and";
-			if (cell->type.in("$or", "$_OR_")) btor_op = "or";
-			if (cell->type.in("$xor", "$_XOR_")) btor_op = "xor";
-			if (cell->type == "$concat") btor_op = "concat";
-			if (cell->type == "$_NAND_") btor_op = "nand";
-			if (cell->type == "$_NOR_") btor_op = "nor";
-			if (cell->type.in("$xnor", "$_XNOR_")) btor_op = "xnor";
+			if (cell->type == ID($add)) btor_op = "add";
+			if (cell->type == ID($sub)) btor_op = "sub";
+			if (cell->type == ID($mul)) btor_op = "mul";
+			if (cell->type.in(ID($shl), ID($sshl))) btor_op = "sll";
+			if (cell->type == ID($shr)) btor_op = "srl";
+			if (cell->type == ID($sshr)) btor_op = "sra";
+			if (cell->type.in(ID($shift), ID($shiftx))) btor_op = "shift";
+			if (cell->type.in(ID($and), ID($_AND_))) btor_op = "and";
+			if (cell->type.in(ID($or), ID($_OR_))) btor_op = "or";
+			if (cell->type.in(ID($xor), ID($_XOR_))) btor_op = "xor";
+			if (cell->type == ID($concat)) btor_op = "concat";
+			if (cell->type == ID($_NAND_)) btor_op = "nand";
+			if (cell->type == ID($_NOR_)) btor_op = "nor";
+			if (cell->type.in(ID($xnor), ID($_XNOR_))) btor_op = "xnor";
 			log_assert(!btor_op.empty());
 
-			int width = GetSize(cell->getPort("\\Y"));
-			width = std::max(width, GetSize(cell->getPort("\\A")));
-			width = std::max(width, GetSize(cell->getPort("\\B")));
+			int width = GetSize(cell->getPort(ID::Y));
+			width = std::max(width, GetSize(cell->getPort(ID::A)));
+			width = std::max(width, GetSize(cell->getPort(ID::B)));
 
-			bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
-			bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
+			bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
+			bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false;
 
 			if (btor_op == "shift" && !b_signed)
 				btor_op = "srl";
 
-			if (cell->type.in("$shl", "$sshl", "$shr", "$sshr"))
+			if (cell->type.in(ID($shl), ID($sshl), ID($shr), ID($sshr)))
 				b_signed = false;
 
-			if (cell->type == "$sshr" && !a_signed)
+			if (cell->type == ID($sshr) && !a_signed)
 				btor_op = "srl";
 
 			int sid = get_bv_sid(width);
@@ -185,8 +224,8 @@ struct BtorWorker
 
 			if (btor_op == "shift")
 			{
-				int nid_a = get_sig_nid(cell->getPort("\\A"), width, false);
-				int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
+				int nid_a = get_sig_nid(cell->getPort(ID::A), width, false);
+				int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
 
 				int nid_r = next_nid++;
 				btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b);
@@ -203,18 +242,18 @@ struct BtorWorker
 				btorf("%d slt %d %d %d\n", nid_b_ltz, sid_bit, nid_b, nid_zero);
 
 				nid = next_nid++;
-				btorf("%d ite %d %d %d %d\n", nid, sid, nid_b_ltz, nid_l, nid_r);
+				btorf("%d ite %d %d %d %d %s\n", nid, sid, nid_b_ltz, nid_l, nid_r, getinfo(cell).c_str());
 			}
 			else
 			{
-				int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
-				int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
+				int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
+				int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
 
 				nid = next_nid++;
-				btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
+				btorf("%d %s %d %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
 			}
 
-			SigSpec sig = sigmap(cell->getPort("\\Y"));
+			SigSpec sig = sigmap(cell->getPort(ID::Y));
 
 			if (GetSize(sig) < width) {
 				int sid = get_bv_sid(GetSize(sig));
@@ -227,28 +266,28 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in("$div", "$mod"))
+		if (cell->type.in(ID($div), ID($mod)))
 		{
 			string btor_op;
-			if (cell->type == "$div") btor_op = "div";
-			if (cell->type == "$mod") btor_op = "rem";
+			if (cell->type == ID($div)) btor_op = "div";
+			if (cell->type == ID($mod)) btor_op = "rem";
 			log_assert(!btor_op.empty());
 
-			int width = GetSize(cell->getPort("\\Y"));
-			width = std::max(width, GetSize(cell->getPort("\\A")));
-			width = std::max(width, GetSize(cell->getPort("\\B")));
+			int width = GetSize(cell->getPort(ID::Y));
+			width = std::max(width, GetSize(cell->getPort(ID::A)));
+			width = std::max(width, GetSize(cell->getPort(ID::B)));
 
-			bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
-			bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
+			bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
+			bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false;
 
-			int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
-			int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
+			int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
+			int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
 
 			int sid = get_bv_sid(width);
 			int nid = next_nid++;
-			btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b);
+			btorf("%d %c%s %d %d %d %s\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
 
-			SigSpec sig = sigmap(cell->getPort("\\Y"));
+			SigSpec sig = sigmap(cell->getPort(ID::Y));
 
 			if (GetSize(sig) < width) {
 				int sid = get_bv_sid(GetSize(sig));
@@ -261,120 +300,120 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in("$_ANDNOT_", "$_ORNOT_"))
+		if (cell->type.in(ID($_ANDNOT_), ID($_ORNOT_)))
 		{
 			int sid = get_bv_sid(1);
-			int nid_a = get_sig_nid(cell->getPort("\\A"));
-			int nid_b = get_sig_nid(cell->getPort("\\B"));
+			int nid_a = get_sig_nid(cell->getPort(ID::A));
+			int nid_b = get_sig_nid(cell->getPort(ID::B));
 
 			int nid1 = next_nid++;
 			int nid2 = next_nid++;
 
-			if (cell->type == "$_ANDNOT_") {
+			if (cell->type == ID($_ANDNOT_)) {
 				btorf("%d not %d %d\n", nid1, sid, nid_b);
-				btorf("%d and %d %d %d\n", nid2, sid, nid_a, nid1);
+				btorf("%d and %d %d %d %s\n", nid2, sid, nid_a, nid1, getinfo(cell).c_str());
 			}
 
-			if (cell->type == "$_ORNOT_") {
+			if (cell->type == ID($_ORNOT_)) {
 				btorf("%d not %d %d\n", nid1, sid, nid_b);
-				btorf("%d or %d %d %d\n", nid2, sid, nid_a, nid1);
+				btorf("%d or %d %d %d %s\n", nid2, sid, nid_a, nid1, getinfo(cell).c_str());
 			}
 
-			SigSpec sig = sigmap(cell->getPort("\\Y"));
+			SigSpec sig = sigmap(cell->getPort(ID::Y));
 			add_nid_sig(nid2, sig);
 			goto okay;
 		}
 
-		if (cell->type.in("$_OAI3_", "$_AOI3_"))
+		if (cell->type.in(ID($_OAI3_), ID($_AOI3_)))
 		{
 			int sid = get_bv_sid(1);
-			int nid_a = get_sig_nid(cell->getPort("\\A"));
-			int nid_b = get_sig_nid(cell->getPort("\\B"));
-			int nid_c = get_sig_nid(cell->getPort("\\C"));
+			int nid_a = get_sig_nid(cell->getPort(ID::A));
+			int nid_b = get_sig_nid(cell->getPort(ID::B));
+			int nid_c = get_sig_nid(cell->getPort(ID::C));
 
 			int nid1 = next_nid++;
 			int nid2 = next_nid++;
 			int nid3 = next_nid++;
 
-			if (cell->type == "$_OAI3_") {
+			if (cell->type == ID($_OAI3_)) {
 				btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b);
 				btorf("%d and %d %d %d\n", nid2, sid, nid1, nid_c);
-				btorf("%d not %d %d\n", nid3, sid, nid2);
+				btorf("%d not %d %d %s\n", nid3, sid, nid2, getinfo(cell).c_str());
 			}
 
-			if (cell->type == "$_AOI3_") {
+			if (cell->type == ID($_AOI3_)) {
 				btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b);
 				btorf("%d or %d %d %d\n", nid2, sid, nid1, nid_c);
-				btorf("%d not %d %d\n", nid3, sid, nid2);
+				btorf("%d not %d %d %s\n", nid3, sid, nid2, getinfo(cell).c_str());
 			}
 
-			SigSpec sig = sigmap(cell->getPort("\\Y"));
+			SigSpec sig = sigmap(cell->getPort(ID::Y));
 			add_nid_sig(nid3, sig);
 			goto okay;
 		}
 
-		if (cell->type.in("$_OAI4_", "$_AOI4_"))
+		if (cell->type.in(ID($_OAI4_), ID($_AOI4_)))
 		{
 			int sid = get_bv_sid(1);
-			int nid_a = get_sig_nid(cell->getPort("\\A"));
-			int nid_b = get_sig_nid(cell->getPort("\\B"));
-			int nid_c = get_sig_nid(cell->getPort("\\C"));
-			int nid_d = get_sig_nid(cell->getPort("\\D"));
+			int nid_a = get_sig_nid(cell->getPort(ID::A));
+			int nid_b = get_sig_nid(cell->getPort(ID::B));
+			int nid_c = get_sig_nid(cell->getPort(ID::C));
+			int nid_d = get_sig_nid(cell->getPort(ID::D));
 
 			int nid1 = next_nid++;
 			int nid2 = next_nid++;
 			int nid3 = next_nid++;
 			int nid4 = next_nid++;
 
-			if (cell->type == "$_OAI4_") {
+			if (cell->type == ID($_OAI4_)) {
 				btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b);
 				btorf("%d or %d %d %d\n", nid2, sid, nid_c, nid_d);
 				btorf("%d and %d %d %d\n", nid3, sid, nid1, nid2);
-				btorf("%d not %d %d\n", nid4, sid, nid3);
+				btorf("%d not %d %d %s\n", nid4, sid, nid3, getinfo(cell).c_str());
 			}
 
-			if (cell->type == "$_AOI4_") {
+			if (cell->type == ID($_AOI4_)) {
 				btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b);
 				btorf("%d and %d %d %d\n", nid2, sid, nid_c, nid_d);
 				btorf("%d or %d %d %d\n", nid3, sid, nid1, nid2);
-				btorf("%d not %d %d\n", nid4, sid, nid3);
+				btorf("%d not %d %d %s\n", nid4, sid, nid3, getinfo(cell).c_str());
 			}
 
-			SigSpec sig = sigmap(cell->getPort("\\Y"));
+			SigSpec sig = sigmap(cell->getPort(ID::Y));
 			add_nid_sig(nid4, sig);
 			goto okay;
 		}
 
-		if (cell->type.in("$lt", "$le", "$eq", "$eqx", "$ne", "$nex", "$ge", "$gt"))
+		if (cell->type.in(ID($lt), ID($le), ID($eq), ID($eqx), ID($ne), ID($nex), ID($ge), ID($gt)))
 		{
 			string btor_op;
-			if (cell->type == "$lt") btor_op = "lt";
-			if (cell->type == "$le") btor_op = "lte";
-			if (cell->type.in("$eq", "$eqx")) btor_op = "eq";
-			if (cell->type.in("$ne", "$nex")) btor_op = "neq";
-			if (cell->type == "$ge") btor_op = "gte";
-			if (cell->type == "$gt") btor_op = "gt";
+			if (cell->type == ID($lt)) btor_op = "lt";
+			if (cell->type == ID($le)) btor_op = "lte";
+			if (cell->type.in(ID($eq), ID($eqx))) btor_op = "eq";
+			if (cell->type.in(ID($ne), ID($nex))) btor_op = "neq";
+			if (cell->type == ID($ge)) btor_op = "gte";
+			if (cell->type == ID($gt)) btor_op = "gt";
 			log_assert(!btor_op.empty());
 
 			int width = 1;
-			width = std::max(width, GetSize(cell->getPort("\\A")));
-			width = std::max(width, GetSize(cell->getPort("\\B")));
+			width = std::max(width, GetSize(cell->getPort(ID::A)));
+			width = std::max(width, GetSize(cell->getPort(ID::B)));
 
-			bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
-			bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
+			bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
+			bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false;
 
 			int sid = get_bv_sid(1);
-			int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
-			int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
+			int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
+			int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
 
 			int nid = next_nid++;
-			if (cell->type.in("$lt", "$le", "$ge", "$gt")) {
-				btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b);
+			if (cell->type.in(ID($lt), ID($le), ID($ge), ID($gt))) {
+				btorf("%d %c%s %d %d %d %s\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
 			} else {
-				btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
+				btorf("%d %s %d %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
 			}
 
-			SigSpec sig = sigmap(cell->getPort("\\Y"));
+			SigSpec sig = sigmap(cell->getPort(ID::Y));
 
 			if (GetSize(sig) > 1) {
 				int sid = get_bv_sid(GetSize(sig));
@@ -387,25 +426,24 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in("$not", "$neg", "$_NOT_"))
+		if (cell->type.in(ID($not), ID($neg), ID($_NOT_)))
 		{
 			string btor_op;
-			if (cell->type.in("$not", "$_NOT_")) btor_op = "not";
-			if (cell->type == "$neg") btor_op = "neg";
+			if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not";
+			if (cell->type == ID($neg)) btor_op = "neg";
 			log_assert(!btor_op.empty());
 
-			int width = GetSize(cell->getPort("\\Y"));
-			width = std::max(width, GetSize(cell->getPort("\\A")));
+			int width = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y)));
 
-			bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
+			bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
 
 			int sid = get_bv_sid(width);
-			int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
+			int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
 
 			int nid = next_nid++;
-			btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
+			btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
 
-			SigSpec sig = sigmap(cell->getPort("\\Y"));
+			SigSpec sig = sigmap(cell->getPort(ID::Y));
 
 			if (GetSize(sig) < width) {
 				int sid = get_bv_sid(GetSize(sig));
@@ -418,25 +456,25 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in("$logic_and", "$logic_or", "$logic_not"))
+		if (cell->type.in(ID($logic_and), ID($logic_or), ID($logic_not)))
 		{
 			string btor_op;
-			if (cell->type == "$logic_and") btor_op = "and";
-			if (cell->type == "$logic_or")  btor_op = "or";
-			if (cell->type == "$logic_not") btor_op = "not";
+			if (cell->type == ID($logic_and)) btor_op = "and";
+			if (cell->type == ID($logic_or))  btor_op = "or";
+			if (cell->type == ID($logic_not)) btor_op = "not";
 			log_assert(!btor_op.empty());
 
 			int sid = get_bv_sid(1);
-			int nid_a = get_sig_nid(cell->getPort("\\A"));
-			int nid_b = btor_op != "not" ? get_sig_nid(cell->getPort("\\B")) : 0;
+			int nid_a = get_sig_nid(cell->getPort(ID::A));
+			int nid_b = btor_op != "not" ? get_sig_nid(cell->getPort(ID::B)) : 0;
 
-			if (GetSize(cell->getPort("\\A")) > 1) {
+			if (GetSize(cell->getPort(ID::A)) > 1) {
 				int nid_red_a = next_nid++;
 				btorf("%d redor %d %d\n", nid_red_a, sid, nid_a);
 				nid_a = nid_red_a;
 			}
 
-			if (btor_op != "not" && GetSize(cell->getPort("\\B")) > 1) {
+			if (btor_op != "not" && GetSize(cell->getPort(ID::B)) > 1) {
 				int nid_red_b = next_nid++;
 				btorf("%d redor %d %d\n", nid_red_b, sid, nid_b);
 				nid_b = nid_red_b;
@@ -444,11 +482,11 @@ struct BtorWorker
 
 			int nid = next_nid++;
 			if (btor_op != "not")
-				btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
+				btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
 			else
-				btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
+				btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
 
-			SigSpec sig = sigmap(cell->getPort("\\Y"));
+			SigSpec sig = sigmap(cell->getPort(ID::Y));
 
 			if (GetSize(sig) > 1) {
 				int sid = get_bv_sid(GetSize(sig));
@@ -462,27 +500,29 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool", "$reduce_xor", "$reduce_xnor"))
+		if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool), ID($reduce_xor), ID($reduce_xnor)))
 		{
 			string btor_op;
-			if (cell->type == "$reduce_and") btor_op = "redand";
-			if (cell->type.in("$reduce_or", "$reduce_bool")) btor_op = "redor";
-			if (cell->type.in("$reduce_xor", "$reduce_xnor")) btor_op = "redxor";
+			if (cell->type == ID($reduce_and)) btor_op = "redand";
+			if (cell->type.in(ID($reduce_or), ID($reduce_bool))) btor_op = "redor";
+			if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) btor_op = "redxor";
 			log_assert(!btor_op.empty());
 
 			int sid = get_bv_sid(1);
-			int nid_a = get_sig_nid(cell->getPort("\\A"));
+			int nid_a = get_sig_nid(cell->getPort(ID::A));
 
 			int nid = next_nid++;
-			btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
 
-			if (cell->type == "$reduce_xnor") {
+			if (cell->type == ID($reduce_xnor)) {
 				int nid2 = next_nid++;
+				btorf("%d %s %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
 				btorf("%d not %d %d %d\n", nid2, sid, nid);
 				nid = nid2;
+			} else {
+				btorf("%d %s %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
 			}
 
-			SigSpec sig = sigmap(cell->getPort("\\Y"));
+			SigSpec sig = sigmap(cell->getPort(ID::Y));
 
 			if (GetSize(sig) > 1) {
 				int sid = get_bv_sid(GetSize(sig));
@@ -496,12 +536,12 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in("$mux", "$_MUX_", "$_NMUX_"))
+		if (cell->type.in(ID($mux), ID($_MUX_), ID($_NMUX_)))
 		{
-			SigSpec sig_a = sigmap(cell->getPort("\\A"));
-			SigSpec sig_b = sigmap(cell->getPort("\\B"));
-			SigSpec sig_s = sigmap(cell->getPort("\\S"));
-			SigSpec sig_y = sigmap(cell->getPort("\\Y"));
+			SigSpec sig_a = sigmap(cell->getPort(ID::A));
+			SigSpec sig_b = sigmap(cell->getPort(ID::B));
+			SigSpec sig_s = sigmap(cell->getPort(ID::S));
+			SigSpec sig_y = sigmap(cell->getPort(ID::Y));
 
 			int nid_a = get_sig_nid(sig_a);
 			int nid_b = get_sig_nid(sig_b);
@@ -509,24 +549,26 @@ struct BtorWorker
 
 			int sid = get_bv_sid(GetSize(sig_y));
 			int nid = next_nid++;
-			btorf("%d ite %d %d %d %d\n", nid, sid, nid_s, nid_b, nid_a);
 
-			if (cell->type == "$_NMUX_") {
+			if (cell->type == ID($_NMUX_)) {
 				int tmp = nid;
 				nid = next_nid++;
-				btorf("%d not %d %d\n", nid, sid, tmp);
+				btorf("%d ite %d %d %d %d\n", tmp, sid, nid_s, nid_b, nid_a);
+				btorf("%d not %d %d %s\n", nid, sid, tmp, getinfo(cell).c_str());
+			} else {
+				btorf("%d ite %d %d %d %d %s\n", nid, sid, nid_s, nid_b, nid_a, getinfo(cell).c_str());
 			}
 
 			add_nid_sig(nid, sig_y);
 			goto okay;
 		}
 
-		if (cell->type == "$pmux")
+		if (cell->type == ID($pmux))
 		{
-			SigSpec sig_a = sigmap(cell->getPort("\\A"));
-			SigSpec sig_b = sigmap(cell->getPort("\\B"));
-			SigSpec sig_s = sigmap(cell->getPort("\\S"));
-			SigSpec sig_y = sigmap(cell->getPort("\\Y"));
+			SigSpec sig_a = sigmap(cell->getPort(ID::A));
+			SigSpec sig_b = sigmap(cell->getPort(ID::B));
+			SigSpec sig_s = sigmap(cell->getPort(ID::S));
+			SigSpec sig_y = sigmap(cell->getPort(ID::Y));
 
 			int width = GetSize(sig_a);
 			int sid = get_bv_sid(width);
@@ -536,7 +578,10 @@ struct BtorWorker
 				int nid_b = get_sig_nid(sig_b.extract(i*width, width));
 				int nid_s = get_sig_nid(sig_s.extract(i));
 				int nid2 = next_nid++;
-				btorf("%d ite %d %d %d %d\n", nid2, sid, nid_s, nid_b, nid);
+				if (i == GetSize(sig_s)-1)
+					btorf("%d ite %d %d %d %d %s\n", nid2, sid, nid_s, nid_b, nid, getinfo(cell).c_str());
+				else
+					btorf("%d ite %d %d %d %d\n", nid2, sid, nid_s, nid_b, nid);
 				nid = nid2;
 			}
 
@@ -544,10 +589,25 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N", "$_FF_"))
+		if (cell->type.in(ID($dff), ID($ff), ID($_DFF_P_), ID($_DFF_N), ID($_FF_)))
 		{
-			SigSpec sig_d = sigmap(cell->getPort("\\D"));
-			SigSpec sig_q = sigmap(cell->getPort("\\Q"));
+			SigSpec sig_d = sigmap(cell->getPort(ID::D));
+			SigSpec sig_q = sigmap(cell->getPort(ID::Q));
+
+			if (!info_filename.empty() && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)))
+			{
+				SigSpec sig_c = sigmap(cell->getPort(cell->type == ID($dff) ? ID::CLK : ID::C));
+				int nid = get_sig_nid(sig_c);
+				bool negedge = false;
+
+				if (cell->type == ID($_DFF_N_))
+					negedge = true;
+
+				if (cell->type == ID($dff) && !cell->getParam(ID::CLK_POLARITY).as_bool())
+					negedge = true;
+
+				info_clocks[nid] |= negedge ? 2 : 1;
+			}
 
 			IdString symbol;
 
@@ -591,16 +651,16 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in("$anyconst", "$anyseq"))
+		if (cell->type.in(ID($anyconst), ID($anyseq)))
 		{
-			SigSpec sig_y = sigmap(cell->getPort("\\Y"));
+			SigSpec sig_y = sigmap(cell->getPort(ID::Y));
 
 			int sid = get_bv_sid(GetSize(sig_y));
 			int nid = next_nid++;
 
 			btorf("%d state %d\n", nid, sid);
 
-			if (cell->type == "$anyconst") {
+			if (cell->type == ID($anyconst)) {
 				int nid2 = next_nid++;
 				btorf("%d next %d %d %d\n", nid2, sid, nid, nid);
 			}
@@ -609,9 +669,9 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type == "$initstate")
+		if (cell->type == ID($initstate))
 		{
-			SigSpec sig_y = sigmap(cell->getPort("\\Y"));
+			SigSpec sig_y = sigmap(cell->getPort(ID::Y));
 
 			if (initstate_nid < 0)
 			{
@@ -628,16 +688,16 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type == "$mem")
+		if (cell->type == ID($mem))
 		{
-			int abits = cell->getParam("\\ABITS").as_int();
-			int width = cell->getParam("\\WIDTH").as_int();
-			int nwords = cell->getParam("\\SIZE").as_int();
-			int rdports = cell->getParam("\\RD_PORTS").as_int();
-			int wrports = cell->getParam("\\WR_PORTS").as_int();
+			int abits = cell->getParam(ID::ABITS).as_int();
+			int width = cell->getParam(ID::WIDTH).as_int();
+			int nwords = cell->getParam(ID::SIZE).as_int();
+			int rdports = cell->getParam(ID::RD_PORTS).as_int();
+			int wrports = cell->getParam(ID::WR_PORTS).as_int();
 
-			Const wr_clk_en = cell->getParam("\\WR_CLK_ENABLE");
-			Const rd_clk_en = cell->getParam("\\RD_CLK_ENABLE");
+			Const wr_clk_en = cell->getParam(ID::WR_CLK_ENABLE);
+			Const rd_clk_en = cell->getParam(ID::RD_CLK_ENABLE);
 
 			bool asyncwr = wr_clk_en.is_fully_zero();
 
@@ -649,18 +709,18 @@ struct BtorWorker
 				log_error("Memory %s.%s has sync read ports.\n",
 						log_id(module), log_id(cell));
 
-			SigSpec sig_rd_addr = sigmap(cell->getPort("\\RD_ADDR"));
-			SigSpec sig_rd_data = sigmap(cell->getPort("\\RD_DATA"));
+			SigSpec sig_rd_addr = sigmap(cell->getPort(ID::RD_ADDR));
+			SigSpec sig_rd_data = sigmap(cell->getPort(ID::RD_DATA));
 
-			SigSpec sig_wr_addr = sigmap(cell->getPort("\\WR_ADDR"));
-			SigSpec sig_wr_data = sigmap(cell->getPort("\\WR_DATA"));
-			SigSpec sig_wr_en = sigmap(cell->getPort("\\WR_EN"));
+			SigSpec sig_wr_addr = sigmap(cell->getPort(ID::WR_ADDR));
+			SigSpec sig_wr_data = sigmap(cell->getPort(ID::WR_DATA));
+			SigSpec sig_wr_en = sigmap(cell->getPort(ID::WR_EN));
 
 			int data_sid = get_bv_sid(width);
 			int bool_sid = get_bv_sid(1);
 			int sid = get_mem_sid(abits, width);
 
-			Const initdata = cell->getParam("\\INIT");
+			Const initdata = cell->getParam(ID::INIT);
 			initdata.exts(nwords*width);
 			int nid_init_val = -1;
 
@@ -983,15 +1043,18 @@ struct BtorWorker
 		return nid;
 	}
 
-	BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad) :
-			f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad)
+	BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, string info_filename) :
+			f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad), cover_mode(cover_mode), info_filename(info_filename)
 	{
+		if (!info_filename.empty())
+			infof("name %s\n", log_id(module));
+
 		btorf_push("inputs");
 
 		for (auto wire : module->wires())
 		{
-			if (wire->attributes.count("\\init")) {
-				Const attrval = wire->attributes.at("\\init");
+			if (wire->attributes.count(ID::init)) {
+				Const attrval = wire->attributes.at(ID::init);
 				for (int i = 0; i < GetSize(wire) && i < GetSize(attrval); i++)
 					if (attrval[i] == State::S0 || attrval[i] == State::S1)
 						initbits[sigmap(SigBit(wire, i))] = (attrval[i] == State::S1);
@@ -1004,7 +1067,7 @@ struct BtorWorker
 			int sid = get_bv_sid(GetSize(sig));
 			int nid = next_nid++;
 
-			btorf("%d input %d %s\n", nid, sid, log_id(wire));
+			btorf("%d input %d %s\n", nid, sid, getinfo(wire).c_str());
 			add_nid_sig(nid, sig);
 		}
 
@@ -1028,20 +1091,20 @@ struct BtorWorker
 			btorf_push(stringf("output %s", log_id(wire)));
 
 			int nid = get_sig_nid(wire);
-			btorf("%d output %d %s\n", next_nid++, nid, log_id(wire));
+			btorf("%d output %d %s\n", next_nid++, nid, getinfo(wire).c_str());
 
 			btorf_pop(stringf("output %s", log_id(wire)));
 		}
 
 		for (auto cell : module->cells())
 		{
-			if (cell->type == "$assume")
+			if (cell->type == ID($assume))
 			{
 				btorf_push(log_id(cell));
 
 				int sid = get_bv_sid(1);
-				int nid_a = get_sig_nid(cell->getPort("\\A"));
-				int nid_en = get_sig_nid(cell->getPort("\\EN"));
+				int nid_a = get_sig_nid(cell->getPort(ID::A));
+				int nid_en = get_sig_nid(cell->getPort(ID::EN));
 				int nid_not_en = next_nid++;
 				int nid_a_or_not_en = next_nid++;
 				int nid = next_nid++;
@@ -1053,29 +1116,49 @@ struct BtorWorker
 				btorf_pop(log_id(cell));
 			}
 
-			if (cell->type == "$assert")
+			if (cell->type == ID($assert))
 			{
 				btorf_push(log_id(cell));
 
 				int sid = get_bv_sid(1);
-				int nid_a = get_sig_nid(cell->getPort("\\A"));
-				int nid_en = get_sig_nid(cell->getPort("\\EN"));
+				int nid_a = get_sig_nid(cell->getPort(ID::A));
+				int nid_en = get_sig_nid(cell->getPort(ID::EN));
 				int nid_not_a = next_nid++;
 				int nid_en_and_not_a = next_nid++;
 
 				btorf("%d not %d %d\n", nid_not_a, sid, nid_a);
 				btorf("%d and %d %d %d\n", nid_en_and_not_a, sid, nid_en, nid_not_a);
 
-				if (single_bad) {
+				if (single_bad && !cover_mode) {
 					bad_properties.push_back(nid_en_and_not_a);
 				} else {
-					int nid = next_nid++;
-					string infostr = log_id(cell);
-					if (infostr[0] == '$' && cell->attributes.count("\\src")) {
-						infostr = cell->attributes.at("\\src").decode_string().c_str();
-						std::replace(infostr.begin(), infostr.end(), ' ', '_');
+					if (cover_mode) {
+						infof("bad %d %s\n", nid_en_and_not_a, getinfo(cell, true).c_str());
+					} else {
+						int nid = next_nid++;
+						btorf("%d bad %d %s\n", nid, nid_en_and_not_a, getinfo(cell, true).c_str());
 					}
-					btorf("%d bad %d %s\n", nid, nid_en_and_not_a, infostr.c_str());
+				}
+
+				btorf_pop(log_id(cell));
+			}
+
+			if (cell->type == ID($cover) && cover_mode)
+			{
+				btorf_push(log_id(cell));
+
+				int sid = get_bv_sid(1);
+				int nid_a = get_sig_nid(cell->getPort(ID::A));
+				int nid_en = get_sig_nid(cell->getPort(ID::EN));
+				int nid_en_and_a = next_nid++;
+
+				btorf("%d and %d %d %d\n", nid_en_and_a, sid, nid_en, nid_a);
+
+				if (single_bad) {
+					bad_properties.push_back(nid_en_and_a);
+				} else {
+					int nid = next_nid++;
+					btorf("%d bad %d %s\n", nid, nid_en_and_a, getinfo(cell, true).c_str());
 				}
 
 				btorf_pop(log_id(cell));
@@ -1096,7 +1179,7 @@ struct BtorWorker
 				continue;
 
 			int this_nid = next_nid++;
-			btorf("%d uext %d %d %d %s\n", this_nid, sid, nid, 0, log_id(wire));
+			btorf("%d uext %d %d %d %s\n", this_nid, sid, nid, 0, getinfo(wire).c_str());
 
 			btorf_pop(stringf("wire %s", log_id(wire)));
 			continue;
@@ -1114,15 +1197,15 @@ struct BtorWorker
 
 				btorf_push(stringf("next %s", log_id(cell)));
 
-				if (cell->type == "$mem")
+				if (cell->type == ID($mem))
 				{
-					int abits = cell->getParam("\\ABITS").as_int();
-					int width = cell->getParam("\\WIDTH").as_int();
-					int wrports = cell->getParam("\\WR_PORTS").as_int();
+					int abits = cell->getParam(ID::ABITS).as_int();
+					int width = cell->getParam(ID::WIDTH).as_int();
+					int wrports = cell->getParam(ID::WR_PORTS).as_int();
 
-					SigSpec sig_wr_addr = sigmap(cell->getPort("\\WR_ADDR"));
-					SigSpec sig_wr_data = sigmap(cell->getPort("\\WR_DATA"));
-					SigSpec sig_wr_en = sigmap(cell->getPort("\\WR_EN"));
+					SigSpec sig_wr_addr = sigmap(cell->getPort(ID::WR_ADDR));
+					SigSpec sig_wr_data = sigmap(cell->getPort(ID::WR_DATA));
+					SigSpec sig_wr_en = sigmap(cell->getPort(ID::WR_EN));
 
 					int data_sid = get_bv_sid(width);
 					int bool_sid = get_bv_sid(1);
@@ -1167,14 +1250,14 @@ struct BtorWorker
 					}
 
 					int nid2 = next_nid++;
-					btorf("%d next %d %d %d\n", nid2, sid, nid, nid_head);
+					btorf("%d next %d %d %d %s\n", nid2, sid, nid, nid_head, getinfo(cell).c_str());
 				}
 				else
 				{
-					SigSpec sig = sigmap(cell->getPort("\\D"));
+					SigSpec sig = sigmap(cell->getPort(ID::D));
 					int nid_q = get_sig_nid(sig);
 					int sid = get_bv_sid(GetSize(sig));
-					btorf("%d next %d %d %d\n", next_nid++, sid, nid, nid_q);
+					btorf("%d next %d %d %d %s\n", next_nid++, sid, nid, nid_q, getinfo(cell).c_str());
 				}
 
 				btorf_pop(stringf("next %s", log_id(cell)));
@@ -1210,6 +1293,35 @@ struct BtorWorker
 				btorf("%d bad %d\n", nid, todo[cursor]);
 			}
 		}
+
+		if (!info_filename.empty())
+		{
+			for (auto &it : info_clocks)
+			{
+				switch (it.second)
+				{
+				case 1:
+					infof("posedge %d\n", it.first);
+					break;
+				case 2:
+					infof("negedge %d\n", it.first);
+					break;
+				case 3:
+					infof("event %d\n", it.first);
+					break;
+				default:
+					log_abort();
+				}
+			}
+
+			std::ofstream f;
+			f.open(info_filename.c_str(), std::ofstream::trunc);
+			if (f.fail())
+				log_error("Can't open file `%s' for writing: %s\n", info_filename.c_str(), strerror(errno));
+			for (auto &it : info_lines)
+				f << it;
+			f.close();
+		}
 	}
 };
 
@@ -1229,10 +1341,17 @@ struct BtorBackend : public Backend {
 		log("  -s\n");
 		log("    Output only a single bad property for all asserts\n");
 		log("\n");
+		log("  -c\n");
+		log("    Output cover properties using 'bad' statements instead of asserts\n");
+		log("\n");
+		log("  -i <filename>\n");
+		log("    Create additional info file with auxiliary information\n");
+		log("\n");
 	}
 	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
-		bool verbose = false, single_bad = false;
+		bool verbose = false, single_bad = false, cover_mode = false;
+		string info_filename;
 
 		log_header(design, "Executing BTOR backend.\n");
 
@@ -1247,6 +1366,14 @@ struct BtorBackend : public Backend {
 				single_bad = true;
 				continue;
 			}
+			if (args[argidx] == "-c") {
+				cover_mode = true;
+				continue;
+			}
+			if (args[argidx] == "-i" && argidx+1 < args.size()) {
+				info_filename = args[++argidx];
+				continue;
+			}
 			break;
 		}
 		extra_args(f, filename, args, argidx);
@@ -1259,7 +1386,7 @@ struct BtorBackend : public Backend {
 		*f << stringf("; BTOR description generated by %s for module %s.\n",
 				yosys_version_str, log_id(topmod));
 
-		BtorWorker(*f, topmod, verbose, single_bad);
+		BtorWorker(*f, topmod, verbose, single_bad, cover_mode, info_filename);
 
 		*f << stringf("; end of yosys output\n");
 	}
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index 199560ad0..cc20f17fc 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -171,13 +171,12 @@ struct EdifBackend : public Backend {
 		extra_args(f, filename, args, argidx);
 
 		if (top_module_name.empty())
-			for (auto & mod_it:design->modules_)
-				if (mod_it.second->get_bool_attribute("\\top"))
-					top_module_name = mod_it.first.str();
+			for (auto module : design->modules())
+				if (module->get_bool_attribute(ID::top))
+					top_module_name = module->name.str();
 
-		for (auto module_it : design->modules_)
+		for (auto module : design->modules())
 		{
-			RTLIL::Module *module = module_it.second;
 			if (module->get_blackbox_attribute())
 				continue;
 
@@ -185,14 +184,13 @@ struct EdifBackend : public Backend {
 				top_module_name = module->name.str();
 
 			if (module->processes.size() != 0)
-				log_error("Found unmapped processes in module %s: unmapped processes are not supported in EDIF backend!\n", RTLIL::id2cstr(module->name));
+				log_error("Found unmapped processes in module %s: unmapped processes are not supported in EDIF backend!\n", log_id(module->name));
 			if (module->memories.size() != 0)
-				log_error("Found unmapped memories in module %s: unmapped memories are not supported in EDIF backend!\n", RTLIL::id2cstr(module->name));
+				log_error("Found unmapped memories in module %s: unmapped memories are not supported in EDIF backend!\n", log_id(module->name));
 
-			for (auto cell_it : module->cells_)
+			for (auto cell : module->cells())
 			{
-				RTLIL::Cell *cell = cell_it.second;
-				if (!design->modules_.count(cell->type) || design->modules_.at(cell->type)->get_blackbox_attribute()) {
+				if (design->module(cell->type) == nullptr || design->module(cell->type)->get_blackbox_attribute()) {
 					lib_cell_ports[cell->type];
 					for (auto p : cell->connections())
 						lib_cell_ports[cell->type][p.first] = GetSize(p.second);
@@ -277,11 +275,11 @@ struct EdifBackend : public Backend {
 
 		// extract module dependencies
 		std::map<RTLIL::Module*, std::set<RTLIL::Module*>> module_deps;
-		for (auto &mod_it : design->modules_) {
-			module_deps[mod_it.second] = std::set<RTLIL::Module*>();
-			for (auto &cell_it : mod_it.second->cells_)
-				if (design->modules_.count(cell_it.second->type) > 0)
-					module_deps[mod_it.second].insert(design->modules_.at(cell_it.second->type));
+		for (auto module : design->modules()) {
+			module_deps[module] = std::set<RTLIL::Module*>();
+			for (auto cell : module->cells())
+				if (design->module(cell->type) != nullptr)
+					module_deps[module].insert(design->module(cell->type));
 		}
 
 		// simple good-enough topological sort
@@ -292,12 +290,12 @@ struct EdifBackend : public Backend {
 				for (auto &dep : it.second)
 					if (module_deps.count(dep) > 0)
 						goto not_ready_yet;
-				// log("Next in topological sort: %s\n", RTLIL::id2cstr(it.first->name));
+				// log("Next in topological sort: %s\n", log_id(it.first->name));
 				sorted_modules.push_back(it.first);
 			not_ready_yet:;
 			}
 			if (sorted_modules_idx == sorted_modules.size())
-				log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", RTLIL::id2cstr(module_deps.begin()->first->name));
+				log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", log_id(module_deps.begin()->first->name));
 			while (sorted_modules_idx < sorted_modules.size())
 				module_deps.erase(sorted_modules.at(sorted_modules_idx++));
 		}
@@ -339,8 +337,7 @@ struct EdifBackend : public Backend {
 			*f << stringf("      (view VIEW_NETLIST\n");
 			*f << stringf("        (viewType NETLIST)\n");
 			*f << stringf("        (interface\n");
-			for (auto &wire_it : module->wires_) {
-				RTLIL::Wire *wire = wire_it.second;
+			for (auto wire : module->wires()) {
 				if (wire->port_id == 0)
 					continue;
 				const char *dir = "INOUT";
@@ -378,8 +375,7 @@ struct EdifBackend : public Backend {
 				*f << stringf("          (instance GND (viewRef VIEW_NETLIST (cellRef GND (libraryRef LIB))))\n");
 				*f << stringf("          (instance VCC (viewRef VIEW_NETLIST (cellRef VCC (libraryRef LIB))))\n");
 			}
-			for (auto &cell_it : module->cells_) {
-				RTLIL::Cell *cell = cell_it.second;
+			for (auto cell : module->cells()) {
 				*f << stringf("          (instance %s\n", EDIF_DEF(cell->name));
 				*f << stringf("            (viewRef VIEW_NETLIST (cellRef %s%s))", EDIF_REF(cell->type),
 						lib_cell_ports.count(cell->type) > 0 ? " (libraryRef LIB)" : "");
@@ -459,8 +455,7 @@ struct EdifBackend : public Backend {
 						add_prop(p.first, p.second);
 				*f << stringf("\n          )\n");
 			}
-			for (auto &wire_it : module->wires_) {
-				RTLIL::Wire *wire = wire_it.second;
+			for (auto wire : module->wires()) {
 				if (!wire->get_bool_attribute(ID::keep))
 					continue;
 				for(int i = 0; i < wire->width; i++) {
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index 3ef886664..94d3e14c1 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -208,7 +208,7 @@ struct FirrtlWorker
 		const char *atLine() {
 			if (srcLine == "") {
 				if (pCell) {
-					auto p = pCell->attributes.find("\\src");
+					auto p = pCell->attributes.find(ID::src);
 					srcLine = " at " + p->second.decode_string();
 				}
 			}
@@ -414,9 +414,9 @@ struct FirrtlWorker
 			std::string wireFileinfo = getFileinfo(wire);
 
 			// If a wire has initial data, issue a warning since FIRRTL doesn't currently support it.
-			if (wire->attributes.count("\\init")) {
+			if (wire->attributes.count(ID::init)) {
 				log_warning("Initial value (%s) for (%s.%s) not supported\n",
-							wire->attributes.at("\\init").as_string().c_str(),
+							wire->attributes.at(ID::init).as_string().c_str(),
 							log_id(module), log_id(wire));
 			}
 			if (wire->port_id)
@@ -444,11 +444,11 @@ struct FirrtlWorker
 			}
 			// Not a module instance. Set up cell properties
 			bool extract_y_bits = false;		// Assume no extraction of final bits will be required.
-			int a_width = cell->parameters.at("\\A_WIDTH", ndef).as_int();	// The width of "A"
-			int b_width = cell->parameters.at("\\B_WIDTH", ndef).as_int();	// The width of "A"
-			const int y_width = cell->parameters.at("\\Y_WIDTH", ndef).as_int();	// The width of the result
-			const bool a_signed = cell->parameters.at("\\A_SIGNED", ndef).as_bool();
-			const bool b_signed = cell->parameters.at("\\B_SIGNED", ndef).as_bool();
+			int a_width = cell->parameters.at(ID::A_WIDTH, ndef).as_int();	// The width of "A"
+			int b_width = cell->parameters.at(ID::B_WIDTH, ndef).as_int();	// The width of "A"
+			const int y_width = cell->parameters.at(ID::Y_WIDTH, ndef).as_int();	// The width of the result
+			const bool a_signed = cell->parameters.at(ID::A_SIGNED, ndef).as_bool();
+			const bool b_signed = cell->parameters.at(ID::B_SIGNED, ndef).as_bool();
 			bool firrtl_is_signed = a_signed;	// The result is signed (subsequent code may change this).
 			int firrtl_width = 0;
 			string primop;
@@ -456,9 +456,9 @@ struct FirrtlWorker
 			string y_id = make_id(cell->name);
 			std::string cellFileinfo = getFileinfo(cell);
 
-			if (cell->type.in("$not", "$logic_not", "$neg", "$reduce_and", "$reduce_or", "$reduce_xor", "$reduce_bool", "$reduce_xnor"))
+			if (cell->type.in(ID($not), ID($logic_not), ID($neg), ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_bool), ID($reduce_xnor)))
 			{
-				string a_expr = make_expr(cell->getPort("\\A"));
+				string a_expr = make_expr(cell->getPort(ID::A));
 				wire_decls.push_back(stringf("    wire %s: UInt<%d> %s\n", y_id.c_str(), y_width, cellFileinfo.c_str()));
 
 				if (a_signed) {
@@ -466,29 +466,29 @@ struct FirrtlWorker
 				}
 
 				// Don't use the results of logical operations (a single bit) to control padding
-				if (!(cell->type.in("$eq", "$eqx", "$gt", "$ge", "$lt", "$le", "$ne", "$nex", "$reduce_bool", "$logic_not") && y_width == 1) ) {
+				if (!(cell->type.in(ID($eq), ID($eqx), ID($gt), ID($ge), ID($lt), ID($le), ID($ne), ID($nex), ID($reduce_bool), ID($logic_not)) && y_width == 1) ) {
 					a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
 				}
 
 				// Assume the FIRRTL width is a single bit.
 				firrtl_width = 1;
-				if (cell->type == "$not") primop = "not";
-				else if (cell->type == "$neg") {
+				if (cell->type == ID($not)) primop = "not";
+				else if (cell->type == ID($neg)) {
 					primop = "neg";
 					firrtl_is_signed = true;	// Result of "neg" is signed (an SInt).
 					firrtl_width = a_width;
-				} else if (cell->type == "$logic_not") {
+				} else if (cell->type == ID($logic_not)) {
 					primop = "eq";
 					a_expr = stringf("%s, UInt(0)", a_expr.c_str());
 				}
-				else if (cell->type == "$reduce_and") primop = "andr";
-				else if (cell->type == "$reduce_or") primop = "orr";
-				else if (cell->type == "$reduce_xor") primop = "xorr";
-				else if (cell->type == "$reduce_xnor") {
+				else if (cell->type == ID($reduce_and)) primop = "andr";
+				else if (cell->type == ID($reduce_or)) primop = "orr";
+				else if (cell->type == ID($reduce_xor)) primop = "xorr";
+				else if (cell->type == ID($reduce_xnor)) {
 					primop = "not";
 					a_expr = stringf("xorr(%s)", a_expr.c_str());
 				}
-				else if (cell->type == "$reduce_bool") {
+				else if (cell->type == ID($reduce_bool)) {
 					primop = "neq";
 					// Use the sign of the a_expr and its width as the type (UInt/SInt) and width of the comparand.
 					a_expr = stringf("%s, %cInt<%d>(0)", a_expr.c_str(), a_signed ? 'S' : 'U', a_width);
@@ -500,16 +500,16 @@ struct FirrtlWorker
 					expr = stringf("asUInt(%s)", expr.c_str());
 
 				cell_exprs.push_back(stringf("    %s <= %s %s\n", y_id.c_str(), expr.c_str(), cellFileinfo.c_str()));
-				register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+				register_reverse_wire_map(y_id, cell->getPort(ID::Y));
 
 				continue;
 			}
-			if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$xnor", "$and", "$or", "$eq", "$eqx",
-				"$gt", "$ge", "$lt", "$le", "$ne", "$nex", "$shr", "$sshr", "$sshl", "$shl",
-				"$logic_and", "$logic_or", "$pow"))
+			if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($xnor), ID($and), ID($or), ID($eq), ID($eqx),
+												ID($gt), ID($ge), ID($lt), ID($le), ID($ne), ID($nex), ID($shr), ID($sshr), ID($sshl), ID($shl),
+												ID($logic_and), ID($logic_or), ID($pow)))
 			{
-				string a_expr = make_expr(cell->getPort("\\A"));
-				string b_expr = make_expr(cell->getPort("\\B"));
+				string a_expr = make_expr(cell->getPort(ID::A));
+				string b_expr = make_expr(cell->getPort(ID::B));
 				std::string cellFileinfo = getFileinfo(cell);
 				wire_decls.push_back(stringf("    wire %s: UInt<%d> %s\n", y_id.c_str(), y_width, cellFileinfo.c_str()));
 
@@ -523,7 +523,7 @@ struct FirrtlWorker
 				}
 				// Shift amount is always unsigned, and needn't be padded to result width,
 				//  otherwise, we need to cast the b_expr appropriately
-				if (b_signed && !cell->type.in("$shr", "$sshr", "$shl", "$sshl", "$pow")) {
+				if (b_signed && !cell->type.in(ID($shr), ID($sshr), ID($shl), ID($sshl), ID($pow))) {
 					b_expr = "asSInt(" + b_expr + ")";
 					// Expand the "B" operand to the result width
 					if (b_width < y_width) {
@@ -534,7 +534,7 @@ struct FirrtlWorker
 
 				// For the arithmetic ops, expand operand widths to result widths befor performing the operation.
 				// This corresponds (according to iverilog) to what verilog compilers implement.
-				if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$xnor", "$and", "$or"))
+				if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($xnor), ID($and), ID($or)))
 				{
 					if (a_width < y_width) {
 						a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
@@ -547,85 +547,85 @@ struct FirrtlWorker
 				}
 				// Assume the FIRRTL width is the width of "A"
 				firrtl_width = a_width;
-				auto a_sig = cell->getPort("\\A");
+				auto a_sig = cell->getPort(ID::A);
 
-				if (cell->type == "$add") {
+				if (cell->type == ID($add)) {
 					primop = "add";
 					firrtl_is_signed = a_signed | b_signed;
 					firrtl_width = max(a_width, b_width);
-				} else if (cell->type == "$sub") {
+				} else if (cell->type == ID($sub)) {
 					primop = "sub";
 					firrtl_is_signed = true;
 					int a_widthInc = (!a_signed && b_signed) ? 2 : (a_signed && !b_signed) ? 1 : 0;
 					int b_widthInc = (a_signed && !b_signed) ? 2 : (!a_signed && b_signed) ? 1 : 0;
 					firrtl_width = max(a_width + a_widthInc, b_width + b_widthInc);
-				} else if (cell->type == "$mul") {
+				} else if (cell->type == ID($mul)) {
 					primop = "mul";
 					firrtl_is_signed = a_signed | b_signed;
 					firrtl_width = a_width + b_width;
-				} else if (cell->type == "$div") {
+				} else if (cell->type == ID($div)) {
 					primop = "div";
 					firrtl_is_signed = a_signed | b_signed;
 					firrtl_width = a_width;
-				} else if (cell->type == "$mod") {
+				} else if (cell->type == ID($mod)) {
 					primop = "rem";
 					firrtl_width = min(a_width, b_width);
-				} else if (cell->type == "$and") {
+				} else if (cell->type == ID($and)) {
 					primop = "and";
 					always_uint = true;
 					firrtl_width = max(a_width, b_width);
 				}
-				else if (cell->type == "$or" ) {
+				else if (cell->type == ID($or) ) {
 					primop =  "or";
 					always_uint = true;
 					firrtl_width = max(a_width, b_width);
 				}
-				else if (cell->type == "$xor") {
+				else if (cell->type == ID($xor)) {
 					primop = "xor";
 					always_uint = true;
 					firrtl_width = max(a_width, b_width);
 				}
-				else if (cell->type == "$xnor") {
+				else if (cell->type == ID($xnor)) {
 					primop = "xnor";
 					always_uint = true;
 					firrtl_width = max(a_width, b_width);
 				}
-				else if ((cell->type == "$eq") | (cell->type == "$eqx")) {
+				else if ((cell->type == ID($eq)) | (cell->type == ID($eqx))) {
 					primop = "eq";
 					always_uint = true;
 					firrtl_width = 1;
-				}
-				else if ((cell->type == "$ne") | (cell->type == "$nex")) {
+			    }
+				else if ((cell->type == ID($ne)) | (cell->type == ID($nex))) {
 					primop = "neq";
 					always_uint = true;
 					firrtl_width = 1;
 				}
-				else if (cell->type == "$gt") {
+				else if (cell->type == ID($gt)) {
 					primop = "gt";
 					always_uint = true;
 					firrtl_width = 1;
 				}
-				else if (cell->type == "$ge") {
+				else if (cell->type == ID($ge)) {
 					primop = "geq";
 					always_uint = true;
 					firrtl_width = 1;
 				}
-				else if (cell->type == "$lt") {
+				else if (cell->type == ID($lt)) {
 					primop = "lt";
 					always_uint = true;
 					firrtl_width = 1;
 				}
-				else if (cell->type == "$le") {
+				else if (cell->type == ID($le)) {
 					primop = "leq";
 					always_uint = true;
 					firrtl_width = 1;
 				}
-				else if ((cell->type == "$shl") | (cell->type == "$sshl")) {
+				else if ((cell->type == ID($shl)) | (cell->type == ID($sshl))) {
 					// FIRRTL will widen the result (y) by the amount of the shift.
 					// We'll need to offset this by extracting the un-widened portion as Verilog would do.
 					extract_y_bits = true;
 					// Is the shift amount constant?
-					auto b_sig = cell->getPort("\\B");
+					auto b_sig = cell->getPort(ID::B);
 					if (b_sig.is_fully_const()) {
 						primop = "shl";
 						int shift_amount = b_sig.as_int();
@@ -638,11 +638,11 @@ struct FirrtlWorker
 						firrtl_width = a_width + (1 << b_width) - 1;
 					}
 				}
-				else if ((cell->type == "$shr") | (cell->type == "$sshr")) {
+				else if ((cell->type == ID($shr)) | (cell->type == ID($sshr))) {
 					// We don't need to extract a specific range of bits.
 					extract_y_bits = false;
 					// Is the shift amount constant?
-					auto b_sig = cell->getPort("\\B");
+					auto b_sig = cell->getPort(ID::B);
 					if (b_sig.is_fully_const()) {
 						primop = "shr";
 						int shift_amount = b_sig.as_int();
@@ -655,26 +655,26 @@ struct FirrtlWorker
 					// We'll need to do some special fixups if the source (and thus result) is signed.
 					if (firrtl_is_signed) {
 						// If this is a "logical" shift right, pretend the source is unsigned.
-						if (cell->type == "$shr") {
+						if (cell->type == ID($shr)) {
 							a_expr = "asUInt(" + a_expr + ")";
 						}
 					}
 				}
-				else if ((cell->type == "$logic_and")) {
+				else if ((cell->type == ID($logic_and))) {
 					primop = "and";
 					a_expr = "neq(" + a_expr + ", UInt(0))";
 					b_expr = "neq(" + b_expr + ", UInt(0))";
 					always_uint = true;
 					firrtl_width = 1;
 				}
-				else if ((cell->type == "$logic_or")) {
+				else if ((cell->type == ID($logic_or))) {
 					primop = "or";
 					a_expr = "neq(" + a_expr + ", UInt(0))";
 					b_expr = "neq(" + b_expr + ", UInt(0))";
 					always_uint = true;
 					firrtl_width = 1;
 				}
-				else if ((cell->type == "$pow")) {
+				else if ((cell->type == ID($pow))) {
 					if (a_sig.is_fully_const() && a_sig.as_int() == 2) {
 						// We'll convert this to a shift. To simplify things, change the a_expr to "1"
 						//	so we can use b_expr directly as a shift amount.
@@ -684,7 +684,7 @@ struct FirrtlWorker
 						a_expr = firrtl_is_signed ? "SInt(1)" : "UInt(1)";
 						extract_y_bits = true;
 						// Is the shift amount constant?
-						auto b_sig = cell->getPort("\\B");
+						auto b_sig = cell->getPort(ID::B);
 						if (b_sig.is_fully_const()) {
 							primop = "shl";
 							int shiftAmount = b_sig.as_int();
@@ -704,7 +704,7 @@ struct FirrtlWorker
 					}
 				}
 
-				if (!cell->parameters.at("\\B_SIGNED").as_bool()) {
+				if (!cell->parameters.at(ID::B_SIGNED).as_bool()) {
 					b_expr = "asUInt(" + b_expr + ")";
 				}
 
@@ -728,47 +728,47 @@ struct FirrtlWorker
 					expr = stringf("asUInt(%s)", expr.c_str());
 
 				cell_exprs.push_back(stringf("    %s <= %s %s\n", y_id.c_str(), expr.c_str(), cellFileinfo.c_str()));
-				register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+				register_reverse_wire_map(y_id, cell->getPort(ID::Y));
 
 				continue;
 			}
 
-			if (cell->type.in("$mux"))
+			if (cell->type.in(ID($mux)))
 			{
-				int width = cell->parameters.at("\\WIDTH").as_int();
-				string a_expr = make_expr(cell->getPort("\\A"));
-				string b_expr = make_expr(cell->getPort("\\B"));
-				string s_expr = make_expr(cell->getPort("\\S"));
+				int width = cell->parameters.at(ID::WIDTH).as_int();
+				string a_expr = make_expr(cell->getPort(ID::A));
+				string b_expr = make_expr(cell->getPort(ID::B));
+				string s_expr = make_expr(cell->getPort(ID::S));
 				wire_decls.push_back(stringf("    wire %s: UInt<%d> %s\n", y_id.c_str(), width, cellFileinfo.c_str()));
 
 				string expr = stringf("mux(%s, %s, %s)", s_expr.c_str(), b_expr.c_str(), a_expr.c_str());
 
 				cell_exprs.push_back(stringf("    %s <= %s %s\n", y_id.c_str(), expr.c_str(), cellFileinfo.c_str()));
-				register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+				register_reverse_wire_map(y_id, cell->getPort(ID::Y));
 
 				continue;
 			}
 
-			if (cell->type.in("$mem"))
+			if (cell->type.in(ID($mem)))
 			{
 				string mem_id = make_id(cell->name);
-				int abits = cell->parameters.at("\\ABITS").as_int();
-				int width = cell->parameters.at("\\WIDTH").as_int();
-				int size = cell->parameters.at("\\SIZE").as_int();
+				int abits = cell->parameters.at(ID::ABITS).as_int();
+				int width = cell->parameters.at(ID::WIDTH).as_int();
+				int size = cell->parameters.at(ID::SIZE).as_int();
 				memory m(cell, mem_id, abits, size, width);
-				int rd_ports = cell->parameters.at("\\RD_PORTS").as_int();
-				int wr_ports = cell->parameters.at("\\WR_PORTS").as_int();
+				int rd_ports = cell->parameters.at(ID::RD_PORTS).as_int();
+				int wr_ports = cell->parameters.at(ID::WR_PORTS).as_int();
 
-				Const initdata = cell->parameters.at("\\INIT");
+				Const initdata = cell->parameters.at(ID::INIT);
 				for (State bit : initdata.bits)
 					if (bit != State::Sx)
 						log_error("Memory with initialization data: %s.%s\n", log_id(module), log_id(cell));
 
-				Const rd_clk_enable = cell->parameters.at("\\RD_CLK_ENABLE");
-				Const wr_clk_enable = cell->parameters.at("\\WR_CLK_ENABLE");
-				Const wr_clk_polarity = cell->parameters.at("\\WR_CLK_POLARITY");
+				Const rd_clk_enable = cell->parameters.at(ID::RD_CLK_ENABLE);
+				Const wr_clk_enable = cell->parameters.at(ID::WR_CLK_ENABLE);
+				Const wr_clk_polarity = cell->parameters.at(ID::WR_CLK_POLARITY);
 
-				int offset = cell->parameters.at("\\OFFSET").as_int();
+				int offset = cell->parameters.at(ID::OFFSET).as_int();
 				if (offset != 0)
 					log_error("Memory with nonzero offset: %s.%s\n", log_id(module), log_id(cell));
 
@@ -777,8 +777,8 @@ struct FirrtlWorker
 					if (rd_clk_enable[i] != State::S0)
 						log_error("Clocked read port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
 
-					SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(i*abits, abits);
-					SigSpec data_sig = cell->getPort("\\RD_DATA").extract(i*width, width);
+					SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(i*abits, abits);
+					SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(i*width, width);
 					string addr_expr = make_expr(addr_sig);
 					string name(stringf("%s.r%d", m.name.c_str(), i));
 					bool clk_enable = false;
@@ -804,14 +804,14 @@ struct FirrtlWorker
 					bool clk_enable = true;
 					bool clk_parity = true;
 					bool transparency = false;
-					SigSpec addr_sig =cell->getPort("\\WR_ADDR").extract(i*abits, abits);
+					SigSpec addr_sig =cell->getPort(ID::WR_ADDR).extract(i*abits, abits);
 					string addr_expr = make_expr(addr_sig);
-					SigSpec data_sig =cell->getPort("\\WR_DATA").extract(i*width, width);
+					SigSpec data_sig =cell->getPort(ID::WR_DATA).extract(i*width, width);
 					string data_expr = make_expr(data_sig);
-					SigSpec clk_sig = cell->getPort("\\WR_CLK").extract(i);
+					SigSpec clk_sig = cell->getPort(ID::WR_CLK).extract(i);
 					string clk_expr = make_expr(clk_sig);
 
-					SigSpec wen_sig = cell->getPort("\\WR_EN").extract(i*width, width);
+					SigSpec wen_sig = cell->getPort(ID::WR_EN).extract(i*width, width);
 					string wen_expr = make_expr(wen_sig[0]);
 
 					for (int i = 1; i < GetSize(wen_sig); i++)
@@ -828,23 +828,23 @@ struct FirrtlWorker
 				continue;
 			}
 
-			if (cell->type.in("$memwr", "$memrd", "$meminit"))
+			if (cell->type.in(ID($memwr), ID($memrd), ID($meminit)))
 			{
 				std::string cell_type = fid(cell->type);
-				std::string mem_id = make_id(cell->parameters["\\MEMID"].decode_string());
-				int abits = cell->parameters.at("\\ABITS").as_int();
-				int width = cell->parameters.at("\\WIDTH").as_int();
+				std::string mem_id = make_id(cell->parameters[ID::MEMID].decode_string());
+				int abits = cell->parameters.at(ID::ABITS).as_int();
+				int width = cell->parameters.at(ID::WIDTH).as_int();
 				memory *mp = nullptr;
-				if (cell->type == "$meminit" ) {
+				if (cell->type == ID($meminit) ) {
 					log_error("$meminit (%s.%s.%s) currently unsupported\n", log_id(module), log_id(cell), mem_id.c_str());
 				} else {
 					// It's a $memwr or $memrd. Remember the read/write port parameters for the eventual FIRRTL memory definition.
-					auto addrSig = cell->getPort("\\ADDR");
-					auto dataSig = cell->getPort("\\DATA");
-					auto enableSig = cell->getPort("\\EN");
-					auto clockSig = cell->getPort("\\CLK");
-					Const clk_enable = cell->parameters.at("\\CLK_ENABLE");
-					Const clk_polarity = cell->parameters.at("\\CLK_POLARITY");
+					auto addrSig = cell->getPort(ID::ADDR);
+					auto dataSig = cell->getPort(ID::DATA);
+					auto enableSig = cell->getPort(ID::EN);
+					auto clockSig = cell->getPort(ID::CLK);
+					Const clk_enable = cell->parameters.at(ID::CLK_ENABLE);
+					Const clk_polarity = cell->parameters.at(ID::CLK_POLARITY);
 
 					// Do we already have an entry for this memory?
 					if (memories.count(mem_id) == 0) {
@@ -855,13 +855,13 @@ struct FirrtlWorker
 					int portNum = 0;
 					bool transparency = false;
 					string data_expr = make_expr(dataSig);
-					if (cell->type.in("$memwr")) {
+					if (cell->type.in(ID($memwr))) {
 						portNum = (int) mp->write_ports.size();
 						write_port wp(stringf("%s.w%d", mem_id.c_str(), portNum), clk_enable.as_bool(), clk_polarity.as_bool(),  transparency, clockSig, enableSig, addrSig, dataSig);
 						mp->add_memory_write_port(wp);
 						cell_exprs.push_back(stringf("%s%s.data <= %s\n", indent.c_str(), wp.name.c_str(), data_expr.c_str()));
 						cell_exprs.push_back(wp.gen_write(indent.c_str()));
-					} else if (cell->type.in("$memrd")) {
+					} else if (cell->type.in(ID($memrd))) {
 						portNum = (int) mp->read_ports.size();
 						read_port rp(stringf("%s.r%d", mem_id.c_str(), portNum), clk_enable.as_bool(), clk_polarity.as_bool(),  transparency, clockSig, enableSig, addrSig);
 						mp->add_memory_read_port(rp);
@@ -872,20 +872,20 @@ struct FirrtlWorker
 				continue;
 			}
 
-			if (cell->type.in("$dff"))
+			if (cell->type.in(ID($dff)))
 			{
-				bool clkpol = cell->parameters.at("\\CLK_POLARITY").as_bool();
+				bool clkpol = cell->parameters.at(ID::CLK_POLARITY).as_bool();
 				if (clkpol == false)
 					log_error("Negative edge clock on FF %s.%s.\n", log_id(module), log_id(cell));
 
-				int width = cell->parameters.at("\\WIDTH").as_int();
-				string expr = make_expr(cell->getPort("\\D"));
-				string clk_expr = "asClock(" + make_expr(cell->getPort("\\CLK")) + ")";
+				int width = cell->parameters.at(ID::WIDTH).as_int();
+				string expr = make_expr(cell->getPort(ID::D));
+				string clk_expr = "asClock(" + make_expr(cell->getPort(ID::CLK)) + ")";
 
 				wire_decls.push_back(stringf("    reg %s: UInt<%d>, %s %s\n", y_id.c_str(), width, clk_expr.c_str(), cellFileinfo.c_str()));
 
 				cell_exprs.push_back(stringf("    %s <= %s %s\n", y_id.c_str(), expr.c_str(), cellFileinfo.c_str()));
-				register_reverse_wire_map(y_id, cell->getPort("\\Q"));
+				register_reverse_wire_map(y_id, cell->getPort(ID::Q));
 
 				continue;
 			}
@@ -896,38 +896,38 @@ struct FirrtlWorker
 				process_instance(cell, wire_exprs);
 				continue;
 			}
-			if (cell->type == "$shiftx") {
+			if (cell->type == ID($shiftx)) {
 				// assign y = a[b +: y_width];
 				// We'll extract the correct bits as part of the primop.
 
-				string a_expr = make_expr(cell->getPort("\\A"));
+				string a_expr = make_expr(cell->getPort(ID::A));
 				// Get the initial bit selector
-				string b_expr = make_expr(cell->getPort("\\B"));
+				string b_expr = make_expr(cell->getPort(ID::B));
 				wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", y_id.c_str(), y_width));
 
-				if (cell->getParam("\\B_SIGNED").as_bool()) {
+				if (cell->getParam(ID::B_SIGNED).as_bool()) {
 					// Use validif to constrain the selection (test the sign bit)
 					auto b_string = b_expr.c_str();
-					int b_sign = cell->parameters.at("\\B_WIDTH").as_int() - 1;
+					int b_sign = cell->parameters.at(ID::B_WIDTH).as_int() - 1;
 					b_expr = stringf("validif(not(bits(%s, %d, %d)), %s)", b_string, b_sign, b_sign, b_string);
 				}
 				string expr = stringf("dshr(%s, %s)", a_expr.c_str(), b_expr.c_str());
 
 				cell_exprs.push_back(stringf("    %s <= %s\n", y_id.c_str(), expr.c_str()));
-				register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+				register_reverse_wire_map(y_id, cell->getPort(ID::Y));
 				continue;
 			}
-			if (cell->type == "$shift") {
+			if (cell->type == ID($shift)) {
 				// assign y = a >> b;
 				//  where b may be negative
 
-				string a_expr = make_expr(cell->getPort("\\A"));
-				string b_expr = make_expr(cell->getPort("\\B"));
+				string a_expr = make_expr(cell->getPort(ID::A));
+				string b_expr = make_expr(cell->getPort(ID::B));
 				auto b_string = b_expr.c_str();
 				string expr;
 				wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", y_id.c_str(), y_width));
 
-				if (cell->getParam("\\B_SIGNED").as_bool()) {
+				if (cell->getParam(ID::B_SIGNED).as_bool()) {
 					// We generate a left or right shift based on the sign of b.
 					std::string dshl = stringf("bits(dshl(%s, %s), 0, %d)", a_expr.c_str(), gen_dshl(b_expr, b_width).c_str(), y_width);
 					std::string dshr = stringf("dshr(%s, %s)", a_expr.c_str(), b_string);
@@ -940,13 +940,13 @@ struct FirrtlWorker
 					expr = stringf("dshr(%s, %s)", a_expr.c_str(), b_string);
 				}
 				cell_exprs.push_back(stringf("    %s <= %s\n", y_id.c_str(), expr.c_str()));
-				register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+				register_reverse_wire_map(y_id, cell->getPort(ID::Y));
 				continue;
 			}
-			if (cell->type == "$pos") {
+			if (cell->type == ID($pos)) {
 				// assign y = a;
 //				printCell(cell);
-				string a_expr = make_expr(cell->getPort("\\A"));
+				string a_expr = make_expr(cell->getPort(ID::A));
 				// Verilog appears to treat the result as signed, so if the result is wider than "A",
 				//  we need to pad.
 				if (a_width < y_width) {
@@ -954,7 +954,7 @@ struct FirrtlWorker
 				}
 				wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", y_id.c_str(), y_width));
 				cell_exprs.push_back(stringf("    %s <= %s\n", y_id.c_str(), a_expr.c_str()));
-				register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+				register_reverse_wire_map(y_id, cell->getPort(ID::Y));
 				continue;
 			}
 			log_error("Cell type not supported: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
@@ -1134,7 +1134,7 @@ struct FirrtlBackend : public Backend {
 		for (auto module : design->modules()) {
 			make_id(module->name);
 			last = module;
-			if (top == nullptr && module->get_bool_attribute("\\top")) {
+			if (top == nullptr && module->get_bool_attribute(ID::top)) {
 				top = module;
 			}
 			for (auto wire : module->wires())
diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index e06786220..5445fad90 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -358,10 +358,10 @@ void ILANG_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool onl
 
 	if (!flag_m) {
 		int count_selected_mods = 0;
-		for (auto it = design->modules_.begin(); it != design->modules_.end(); ++it) {
-			if (design->selected_whole_module(it->first))
+		for (auto module : design->modules()) {
+			if (design->selected_whole_module(module->name))
 				flag_m = true;
-			if (design->selected(it->second))
+			if (design->selected(module))
 				count_selected_mods++;
 		}
 		if (count_selected_mods > 1)
@@ -374,11 +374,11 @@ 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) {
-		if (!only_selected || design->selected(it->second)) {
+	for (auto module : design->modules()) {
+		if (!only_selected || design->selected(module)) {
 			if (only_selected)
 				f << stringf("\n");
-			dump_module(f, "", it->second, design, only_selected, flag_m, flag_n);
+			dump_module(f, "", module, design, only_selected, flag_m, flag_n);
 		}
 	}
 
diff --git a/backends/intersynth/intersynth.cc b/backends/intersynth/intersynth.cc
index 809a0fa09..31dce1cca 100644
--- a/backends/intersynth/intersynth.cc
+++ b/backends/intersynth/intersynth.cc
@@ -122,70 +122,67 @@ struct IntersynthBackend : public Backend {
 		for (auto lib : libs)
 			ct.setup_design(lib);
 
-		for (auto module_it : design->modules_)
+		for (auto module : design->modules())
 		{
-			RTLIL::Module *module = module_it.second;
 			SigMap sigmap(module);
 
 			if (module->get_blackbox_attribute())
 				continue;
-			if (module->memories.size() == 0 && module->processes.size() == 0 && module->cells_.size() == 0)
+			if (module->memories.size() == 0 && module->processes.size() == 0 && module->cells().size() == 0)
 				continue;
 
 			if (selected && !design->selected_whole_module(module->name)) {
 				if (design->selected_module(module->name))
-					log_cmd_error("Can't handle partially selected module %s!\n", RTLIL::id2cstr(module->name));
+					log_cmd_error("Can't handle partially selected module %s!\n", log_id(module->name));
 				continue;
 			}
 
-			log("Generating netlist %s.\n", RTLIL::id2cstr(module->name));
+			log("Generating netlist %s.\n", log_id(module->name));
 
 			if (module->memories.size() != 0 || module->processes.size() != 0)
 				log_error("Can't generate a netlist for a module with unprocessed memories or processes!\n");
 
 			std::set<std::string> constcells_code;
-			netlists_code += stringf("# Netlist of module %s\n", RTLIL::id2cstr(module->name));
-			netlists_code += stringf("netlist %s\n", RTLIL::id2cstr(module->name));
+			netlists_code += stringf("# Netlist of module %s\n", log_id(module->name));
+			netlists_code += stringf("netlist %s\n", log_id(module->name));
 
 			// Module Ports: "std::set<string> celltypes_code" prevents duplicate top level ports
-			for (auto wire_it : module->wires_) {
-				RTLIL::Wire *wire = wire_it.second;
+			for (auto wire : module->wires()) {
 				if (wire->port_input || wire->port_output) {
 					celltypes_code.insert(stringf("celltype !%s b%d %sPORT\n" "%s %s %d %s PORT\n",
-							RTLIL::id2cstr(wire->name), wire->width, wire->port_input ? "*" : "",
-							wire->port_input ? "input" : "output", RTLIL::id2cstr(wire->name), wire->width, RTLIL::id2cstr(wire->name)));
-					netlists_code += stringf("node %s %s PORT %s\n", RTLIL::id2cstr(wire->name), RTLIL::id2cstr(wire->name),
+							log_id(wire->name), wire->width, wire->port_input ? "*" : "",
+							wire->port_input ? "input" : "output", log_id(wire->name), wire->width, log_id(wire->name)));
+					netlists_code += stringf("node %s %s PORT %s\n", log_id(wire->name), log_id(wire->name),
 							netname(conntypes_code, celltypes_code, constcells_code, sigmap(wire)).c_str());
 				}
 			}
 
 			// Submodules: "std::set<string> celltypes_code" prevents duplicate cell types
-			for (auto cell_it : module->cells_)
+			for (auto cell : module->cells())
 			{
-				RTLIL::Cell *cell = cell_it.second;
 				std::string celltype_code, node_code;
 
 				if (!ct.cell_known(cell->type))
-					log_error("Found unknown cell type %s in module!\n", RTLIL::id2cstr(cell->type));
+					log_error("Found unknown cell type %s in module!\n", log_id(cell->type));
 
-				celltype_code = stringf("celltype %s", RTLIL::id2cstr(cell->type));
-				node_code = stringf("node %s %s", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
+				celltype_code = stringf("celltype %s", log_id(cell->type));
+				node_code = stringf("node %s %s", log_id(cell->name), log_id(cell->type));
 				for (auto &port : cell->connections()) {
 					RTLIL::SigSpec sig = sigmap(port.second);
 					if (sig.size() != 0) {
 						conntypes_code.insert(stringf("conntype b%d %d 2 %d\n", sig.size(), sig.size(), sig.size()));
-						celltype_code += stringf(" b%d %s%s", sig.size(), ct.cell_output(cell->type, port.first) ? "*" : "", RTLIL::id2cstr(port.first));
-						node_code += stringf(" %s %s", RTLIL::id2cstr(port.first), netname(conntypes_code, celltypes_code, constcells_code, sig).c_str());
+						celltype_code += stringf(" b%d %s%s", sig.size(), ct.cell_output(cell->type, port.first) ? "*" : "", log_id(port.first));
+						node_code += stringf(" %s %s", log_id(port.first), netname(conntypes_code, celltypes_code, constcells_code, sig).c_str());
 					}
 				}
 				for (auto &param : cell->parameters) {
-					celltype_code += stringf(" cfg:%d %s", int(param.second.bits.size()), RTLIL::id2cstr(param.first));
+					celltype_code += stringf(" cfg:%d %s", int(param.second.bits.size()), log_id(param.first));
 					if (param.second.bits.size() != 32) {
-						node_code += stringf(" %s '", RTLIL::id2cstr(param.first));
+						node_code += stringf(" %s '", log_id(param.first));
 						for (int i = param.second.bits.size()-1; i >= 0; i--)
 							node_code += param.second.bits[i] == State::S1 ? "1" : "0";
 					} else
-						node_code += stringf(" %s 0x%x", RTLIL::id2cstr(param.first), param.second.as_int());
+						node_code += stringf(" %s 0x%x", log_id(param.first), param.second.as_int());
 				}
 
 				celltypes_code.insert(celltype_code + "\n");
diff --git a/backends/simplec/simplec.cc b/backends/simplec/simplec.cc
index 54dbb84af..83ed5e6e0 100644
--- a/backends/simplec/simplec.cc
+++ b/backends/simplec/simplec.cc
@@ -378,16 +378,16 @@ struct SimplecWorker
 
 	void eval_cell(HierDirtyFlags *work, Cell *cell)
 	{
-		if (cell->type.in("$_BUF_", "$_NOT_"))
+		if (cell->type.in(ID($_BUF_), ID($_NOT_)))
 		{
-			SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
-			SigBit y = sigmaps.at(work->module)(cell->getPort("\\Y"));
+			SigBit a = sigmaps.at(work->module)(cell->getPort(ID::A));
+			SigBit y = sigmaps.at(work->module)(cell->getPort(ID::Y));
 
 			string a_expr = a.wire ? util_get_bit(work->prefix + cid(a.wire->name), a.wire->width, a.offset) : a.data ? "1" : "0";
 			string expr;
 
-			if (cell->type == "$_BUF_")  expr = a_expr;
-			if (cell->type == "$_NOT_")  expr = "!" + a_expr;
+			if (cell->type == ID($_BUF_))  expr = a_expr;
+			if (cell->type == ID($_NOT_))  expr = "!" + a_expr;
 
 			log_assert(y.wire);
 			funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
@@ -397,24 +397,24 @@ struct SimplecWorker
 			return;
 		}
 
-		if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_", "$_ANDNOT_", "$_ORNOT_"))
+		if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_)))
 		{
-			SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
-			SigBit b = sigmaps.at(work->module)(cell->getPort("\\B"));
-			SigBit y = sigmaps.at(work->module)(cell->getPort("\\Y"));
+			SigBit a = sigmaps.at(work->module)(cell->getPort(ID::A));
+			SigBit b = sigmaps.at(work->module)(cell->getPort(ID::B));
+			SigBit y = sigmaps.at(work->module)(cell->getPort(ID::Y));
 
 			string a_expr = a.wire ? util_get_bit(work->prefix + cid(a.wire->name), a.wire->width, a.offset) : a.data ? "1" : "0";
 			string b_expr = b.wire ? util_get_bit(work->prefix + cid(b.wire->name), b.wire->width, b.offset) : b.data ? "1" : "0";
 			string expr;
 
-			if (cell->type == "$_AND_")    expr = stringf("%s & %s",    a_expr.c_str(), b_expr.c_str());
-			if (cell->type == "$_NAND_")   expr = stringf("!(%s & %s)", a_expr.c_str(), b_expr.c_str());
-			if (cell->type == "$_OR_")     expr = stringf("%s | %s",    a_expr.c_str(), b_expr.c_str());
-			if (cell->type == "$_NOR_")    expr = stringf("!(%s | %s)", a_expr.c_str(), b_expr.c_str());
-			if (cell->type == "$_XOR_")    expr = stringf("%s ^ %s",    a_expr.c_str(), b_expr.c_str());
-			if (cell->type == "$_XNOR_")   expr = stringf("!(%s ^ %s)", a_expr.c_str(), b_expr.c_str());
-			if (cell->type == "$_ANDNOT_") expr = stringf("%s & (!%s)", a_expr.c_str(), b_expr.c_str());
-			if (cell->type == "$_ORNOT_")  expr = stringf("%s | (!%s)", a_expr.c_str(), b_expr.c_str());
+			if (cell->type == ID($_AND_))    expr = stringf("%s & %s",    a_expr.c_str(), b_expr.c_str());
+			if (cell->type == ID($_NAND_))   expr = stringf("!(%s & %s)", a_expr.c_str(), b_expr.c_str());
+			if (cell->type == ID($_OR_))     expr = stringf("%s | %s",    a_expr.c_str(), b_expr.c_str());
+			if (cell->type == ID($_NOR_))    expr = stringf("!(%s | %s)", a_expr.c_str(), b_expr.c_str());
+			if (cell->type == ID($_XOR_))    expr = stringf("%s ^ %s",    a_expr.c_str(), b_expr.c_str());
+			if (cell->type == ID($_XNOR_))   expr = stringf("!(%s ^ %s)", a_expr.c_str(), b_expr.c_str());
+			if (cell->type == ID($_ANDNOT_)) expr = stringf("%s & (!%s)", a_expr.c_str(), b_expr.c_str());
+			if (cell->type == ID($_ORNOT_))  expr = stringf("%s | (!%s)", a_expr.c_str(), b_expr.c_str());
 
 			log_assert(y.wire);
 			funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
@@ -424,20 +424,20 @@ struct SimplecWorker
 			return;
 		}
 
-		if (cell->type.in("$_AOI3_", "$_OAI3_"))
+		if (cell->type.in(ID($_AOI3_), ID($_OAI3_)))
 		{
-			SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
-			SigBit b = sigmaps.at(work->module)(cell->getPort("\\B"));
-			SigBit c = sigmaps.at(work->module)(cell->getPort("\\C"));
-			SigBit y = sigmaps.at(work->module)(cell->getPort("\\Y"));
+			SigBit a = sigmaps.at(work->module)(cell->getPort(ID::A));
+			SigBit b = sigmaps.at(work->module)(cell->getPort(ID::B));
+			SigBit c = sigmaps.at(work->module)(cell->getPort(ID::C));
+			SigBit y = sigmaps.at(work->module)(cell->getPort(ID::Y));
 
 			string a_expr = a.wire ? util_get_bit(work->prefix + cid(a.wire->name), a.wire->width, a.offset) : a.data ? "1" : "0";
 			string b_expr = b.wire ? util_get_bit(work->prefix + cid(b.wire->name), b.wire->width, b.offset) : b.data ? "1" : "0";
 			string c_expr = c.wire ? util_get_bit(work->prefix + cid(c.wire->name), c.wire->width, c.offset) : c.data ? "1" : "0";
 			string expr;
 
-			if (cell->type == "$_AOI3_") expr = stringf("!((%s & %s) | %s)", a_expr.c_str(), b_expr.c_str(), c_expr.c_str());
-			if (cell->type == "$_OAI3_") expr = stringf("!((%s | %s) & %s)", a_expr.c_str(), b_expr.c_str(), c_expr.c_str());
+			if (cell->type == ID($_AOI3_)) expr = stringf("!((%s & %s) | %s)", a_expr.c_str(), b_expr.c_str(), c_expr.c_str());
+			if (cell->type == ID($_OAI3_)) expr = stringf("!((%s | %s) & %s)", a_expr.c_str(), b_expr.c_str(), c_expr.c_str());
 
 			log_assert(y.wire);
 			funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
@@ -447,13 +447,13 @@ struct SimplecWorker
 			return;
 		}
 
-		if (cell->type.in("$_AOI4_", "$_OAI4_"))
+		if (cell->type.in(ID($_AOI4_), ID($_OAI4_)))
 		{
-			SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
-			SigBit b = sigmaps.at(work->module)(cell->getPort("\\B"));
-			SigBit c = sigmaps.at(work->module)(cell->getPort("\\C"));
-			SigBit d = sigmaps.at(work->module)(cell->getPort("\\D"));
-			SigBit y = sigmaps.at(work->module)(cell->getPort("\\Y"));
+			SigBit a = sigmaps.at(work->module)(cell->getPort(ID::A));
+			SigBit b = sigmaps.at(work->module)(cell->getPort(ID::B));
+			SigBit c = sigmaps.at(work->module)(cell->getPort(ID::C));
+			SigBit d = sigmaps.at(work->module)(cell->getPort(ID::D));
+			SigBit y = sigmaps.at(work->module)(cell->getPort(ID::Y));
 
 			string a_expr = a.wire ? util_get_bit(work->prefix + cid(a.wire->name), a.wire->width, a.offset) : a.data ? "1" : "0";
 			string b_expr = b.wire ? util_get_bit(work->prefix + cid(b.wire->name), b.wire->width, b.offset) : b.data ? "1" : "0";
@@ -461,8 +461,8 @@ struct SimplecWorker
 			string d_expr = d.wire ? util_get_bit(work->prefix + cid(d.wire->name), d.wire->width, d.offset) : d.data ? "1" : "0";
 			string expr;
 
-			if (cell->type == "$_AOI4_") expr = stringf("!((%s & %s) | (%s & %s))", a_expr.c_str(), b_expr.c_str(), c_expr.c_str(), d_expr.c_str());
-			if (cell->type == "$_OAI4_") expr = stringf("!((%s | %s) & (%s | %s))", a_expr.c_str(), b_expr.c_str(), c_expr.c_str(), d_expr.c_str());
+			if (cell->type == ID($_AOI4_)) expr = stringf("!((%s & %s) | (%s & %s))", a_expr.c_str(), b_expr.c_str(), c_expr.c_str(), d_expr.c_str());
+			if (cell->type == ID($_OAI4_)) expr = stringf("!((%s | %s) & (%s | %s))", a_expr.c_str(), b_expr.c_str(), c_expr.c_str(), d_expr.c_str());
 
 			log_assert(y.wire);
 			funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
@@ -472,12 +472,12 @@ struct SimplecWorker
 			return;
 		}
 
-		if (cell->type.in("$_MUX_", "$_NMUX_"))
+		if (cell->type.in(ID($_MUX_), ID($_NMUX_)))
 		{
-			SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
-			SigBit b = sigmaps.at(work->module)(cell->getPort("\\B"));
-			SigBit s = sigmaps.at(work->module)(cell->getPort("\\S"));
-			SigBit y = sigmaps.at(work->module)(cell->getPort("\\Y"));
+			SigBit a = sigmaps.at(work->module)(cell->getPort(ID::A));
+			SigBit b = sigmaps.at(work->module)(cell->getPort(ID::B));
+			SigBit s = sigmaps.at(work->module)(cell->getPort(ID::S));
+			SigBit y = sigmaps.at(work->module)(cell->getPort(ID::Y));
 
 			string a_expr = a.wire ? util_get_bit(work->prefix + cid(a.wire->name), a.wire->width, a.offset) : a.data ? "1" : "0";
 			string b_expr = b.wire ? util_get_bit(work->prefix + cid(b.wire->name), b.wire->width, b.offset) : b.data ? "1" : "0";
@@ -485,8 +485,8 @@ struct SimplecWorker
 
 			// casts to bool are a workaround for CBMC bug (https://github.com/diffblue/cbmc/issues/933)
 			string expr = stringf("%s ? %s(bool)%s : %s(bool)%s", s_expr.c_str(),
-					cell->type == "$_NMUX_" ? "!" : "", b_expr.c_str(),
-					cell->type == "$_NMUX_" ? "!" : "", a_expr.c_str());
+					cell->type == ID($_NMUX_) ? "!" : "", b_expr.c_str(),
+					cell->type == ID($_NMUX_) ? "!" : "", a_expr.c_str());
 
 			log_assert(y.wire);
 			funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
@@ -653,10 +653,10 @@ struct SimplecWorker
 
 		for (Wire *w : module->wires())
 		{
-			if (w->attributes.count("\\init"))
+			if (w->attributes.count(ID::init))
 			{
 				SigSpec sig = sigmaps.at(module)(w);
-				Const val = w->attributes.at("\\init");
+				Const val = w->attributes.at(ID::init);
 				val.bits.resize(GetSize(sig), State::Sx);
 
 				for (int i = 0; i < GetSize(sig); i++)
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index ea252b6b9..3e67e55f2 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -135,7 +135,7 @@ struct Smt2Worker
 				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));
 
-			if (cell->type.in("$mem") && conn.first.in("\\RD_CLK", "\\WR_CLK"))
+			if (cell->type.in(ID($mem)) && conn.first.in(ID::RD_CLK, ID::WR_CLK))
 			{
 				SigSpec clk = sigmap(conn.second);
 				for (int i = 0; i < GetSize(clk); i++)
@@ -143,19 +143,19 @@ struct Smt2Worker
 					if (clk[i].wire == nullptr)
 						continue;
 
-					if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_ENABLE" : "\\WR_CLK_ENABLE")[i] != State::S1)
+					if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_ENABLE : ID::WR_CLK_ENABLE)[i] != State::S1)
 						continue;
 
-					if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_POLARITY" : "\\WR_CLK_POLARITY")[i] == State::S1)
+					if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_POLARITY : ID::WR_CLK_POLARITY)[i] == State::S1)
 						clock_posedge.insert(clk[i]);
 					else
 						clock_negedge.insert(clk[i]);
 				}
 			}
 			else
-			if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_") && conn.first.in("\\CLK", "\\C"))
+			if (cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)) && conn.first.in(ID::CLK, ID::C))
 			{
-				bool posedge = (cell->type == "$_DFF_N_") || (cell->type == "$dff" && cell->getParam("\\CLK_POLARITY").as_bool());
+				bool posedge = (cell->type == ID($_DFF_N_)) || (cell->type == ID($dff) && cell->getParam(ID::CLK_POLARITY).as_bool());
 				for (auto bit : sigmap(conn.second)) {
 					if (posedge)
 						clock_posedge.insert(bit);
@@ -367,15 +367,15 @@ struct Smt2Worker
 
 	void export_gate(RTLIL::Cell *cell, std::string expr)
 	{
-		RTLIL::SigBit bit = sigmap(cell->getPort("\\Y").as_bit());
+		RTLIL::SigBit bit = sigmap(cell->getPort(ID::Y).as_bit());
 		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"));
+			if (ch == 'A') processed_expr += get_bool(cell->getPort(ID::A));
+			else if (ch == 'B') processed_expr += get_bool(cell->getPort(ID::B));
+			else if (ch == 'C') processed_expr += get_bool(cell->getPort(ID::C));
+			else if (ch == 'D') processed_expr += get_bool(cell->getPort(ID::D));
+			else if (ch == 'S') processed_expr += get_bool(cell->getPort(ID::S));
 			else processed_expr += ch;
 		}
 
@@ -391,23 +391,23 @@ struct Smt2Worker
 	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();
+		RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
+		bool is_signed = cell->getParam(ID::A_SIGNED).as_bool();
 		int width = GetSize(sig_y);
 
 		if (type == 's' || type == 'd' || type == 'b') {
-			width = max(width, GetSize(cell->getPort("\\A")));
-			if (cell->hasPort("\\B"))
-				width = max(width, GetSize(cell->getPort("\\B")));
+			width = max(width, GetSize(cell->getPort(ID::A)));
+			if (cell->hasPort(ID::B))
+				width = max(width, GetSize(cell->getPort(ID::B)));
 		}
 
-		if (cell->hasPort("\\A")) {
-			sig_a = cell->getPort("\\A");
+		if (cell->hasPort(ID::A)) {
+			sig_a = cell->getPort(ID::A);
 			sig_a.extend_u0(width, is_signed);
 		}
 
-		if (cell->hasPort("\\B")) {
-			sig_b = cell->getPort("\\B");
+		if (cell->hasPort(ID::B)) {
+			sig_b = cell->getPort(ID::B);
 			sig_b.extend_u0(width, is_signed && !(type == 's'));
 		}
 
@@ -416,7 +416,7 @@ struct Smt2Worker
 		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 == 'P') processed_expr += get_bv(cell->getPort("\\B"));
+			else if (ch == 'P') processed_expr += get_bv(cell->getPort(ID::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;
@@ -443,7 +443,7 @@ struct Smt2Worker
 
 	void export_reduce(RTLIL::Cell *cell, std::string expr, bool identity_val)
 	{
-		RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y"));
+		RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
 		std::string processed_expr;
 
 		for (char ch : expr)
@@ -480,9 +480,9 @@ struct Smt2Worker
 		exported_cells.insert(cell);
 		recursive_cells.insert(cell);
 
-		if (cell->type == "$initstate")
+		if (cell->type == ID($initstate))
 		{
-			SigBit bit = sigmap(cell->getPort("\\Y").as_bit());
+			SigBit bit = sigmap(cell->getPort(ID::Y).as_bit());
 			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (|%s_is| state)) ; %s\n",
 					get_id(module), idcounter, get_id(module), get_id(module), log_signal(bit)));
 			register_bool(bit, idcounter++);
@@ -490,132 +490,132 @@ struct Smt2Worker
 			return;
 		}
 
-		if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
+		if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_)))
 		{
 			registers.insert(cell);
-			makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort("\\Q")));
-			register_bool(cell->getPort("\\Q"), idcounter++);
+			makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q)));
+			register_bool(cell->getPort(ID::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 == "$_ANDNOT_") return export_gate(cell, "(and A (not B))");
-		if (cell->type == "$_ORNOT_") return export_gate(cell, "(or A (not B))");
-		if (cell->type == "$_MUX_") return export_gate(cell, "(ite S B A)");
-		if (cell->type == "$_NMUX_") return export_gate(cell, "(not (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)))");
+		if (cell->type == ID($_BUF_)) return export_gate(cell, "A");
+		if (cell->type == ID($_NOT_)) return export_gate(cell, "(not A)");
+		if (cell->type == ID($_AND_)) return export_gate(cell, "(and A B)");
+		if (cell->type == ID($_NAND_)) return export_gate(cell, "(not (and A B))");
+		if (cell->type == ID($_OR_)) return export_gate(cell, "(or A B)");
+		if (cell->type == ID($_NOR_)) return export_gate(cell, "(not (or A B))");
+		if (cell->type == ID($_XOR_)) return export_gate(cell, "(xor A B)");
+		if (cell->type == ID($_XNOR_)) return export_gate(cell, "(not (xor A B))");
+		if (cell->type == ID($_ANDNOT_)) return export_gate(cell, "(and A (not B))");
+		if (cell->type == ID($_ORNOT_)) return export_gate(cell, "(or A (not B))");
+		if (cell->type == ID($_MUX_)) return export_gate(cell, "(ite S B A)");
+		if (cell->type == ID($_NMUX_)) return export_gate(cell, "(not (ite S B A))");
+		if (cell->type == ID($_AOI3_)) return export_gate(cell, "(not (or (and A B) C))");
+		if (cell->type == ID($_OAI3_)) return export_gate(cell, "(not (and (or A B) C))");
+		if (cell->type == ID($_AOI4_)) return export_gate(cell, "(not (or (and A B) (and C D)))");
+		if (cell->type == ID($_OAI4_)) return export_gate(cell, "(not (and (or A B) (or C D)))");
 
 		// FIXME: $lut
 
 		if (bvmode)
 		{
-			if (cell->type.in("$ff", "$dff"))
+			if (cell->type.in(ID($ff), ID($dff)))
 			{
 				registers.insert(cell);
-				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q")));
-				register_bv(cell->getPort("\\Q"), idcounter++);
+				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q)));
+				register_bv(cell->getPort(ID::Q), idcounter++);
 				recursive_cells.erase(cell);
 				return;
 			}
 
-			if (cell->type.in("$anyconst", "$anyseq", "$allconst", "$allseq"))
+			if (cell->type.in(ID($anyconst), ID($anyseq), ID($allconst), ID($allseq)))
 			{
 				registers.insert(cell);
-				string infostr = cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell);
-				if (cell->attributes.count("\\reg"))
-					infostr += " " + cell->attributes.at("\\reg").decode_string();
-				decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort("\\Y")), infostr.c_str()));
-				if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\maximize")){
+				string infostr = cell->attributes.count(ID::src) ? cell->attributes.at(ID::src).decode_string().c_str() : get_id(cell);
+				if (cell->attributes.count(ID::reg))
+					infostr += " " + cell->attributes.at(ID::reg).decode_string();
+				decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(ID::Y)), infostr.c_str()));
+				if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::maximize)){
 					decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter));
-					log("Wire %s is maximized\n", cell->getPort("\\Y").as_wire()->name.str().c_str());
+					log("Wire %s is maximized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str());
 				}
-				else if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\minimize")){
+				else if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::minimize)){
 					decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter));
-					log("Wire %s is minimized\n", cell->getPort("\\Y").as_wire()->name.str().c_str());
+					log("Wire %s is minimized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str());
 				}
-				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
-				if (cell->type == "$anyseq")
+				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::Y)));
+				if (cell->type == ID($anyseq))
 					ex_input_eq.push_back(stringf("  (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));
-				register_bv(cell->getPort("\\Y"), idcounter++);
+				register_bv(cell->getPort(ID::Y), 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 == ID($and)) return export_bvop(cell, "(bvand A B)");
+			if (cell->type == ID($or)) return export_bvop(cell, "(bvor A B)");
+			if (cell->type == ID($xor)) return export_bvop(cell, "(bvxor A B)");
+			if (cell->type == ID($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');
+			if (cell->type == ID($shl)) return export_bvop(cell, "(bvshl A B)", 's');
+			if (cell->type == ID($shr)) return export_bvop(cell, "(bvlshr A B)", 's');
+			if (cell->type == ID($sshl)) return export_bvop(cell, "(bvshl A B)", 's');
+			if (cell->type == ID($sshr)) return export_bvop(cell, "(bvLshr A B)", 's');
 
-			if (cell->type.in("$shift", "$shiftx")) {
-				if (cell->getParam("\\B_SIGNED").as_bool()) {
+			if (cell->type.in(ID($shift), ID($shiftx))) {
+				if (cell->getParam(ID::B_SIGNED).as_bool()) {
 					return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
 							"(bvlshr A B) (bvlshr A (bvneg B)))",
-							GetSize(cell->getPort("\\B")), 0), 's');
+							GetSize(cell->getPort(ID::B)), 0), 's');
 				} else {
 					return export_bvop(cell, "(bvlshr A B)", 's');
 				}
 			}
 
-			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.in("$reduce_and", "$reduce_or", "$reduce_bool") &&
-					2*GetSize(cell->getPort("\\A").chunks()) < GetSize(cell->getPort("\\A"))) {
-				bool is_and = cell->type == "$reduce_and";
-				string bits(GetSize(cell->getPort("\\A")), is_and ? '1' : '0');
+			if (cell->type == ID($lt)) return export_bvop(cell, "(bvUlt A B)", 'b');
+			if (cell->type == ID($le)) return export_bvop(cell, "(bvUle A B)", 'b');
+			if (cell->type == ID($ge)) return export_bvop(cell, "(bvUge A B)", 'b');
+			if (cell->type == ID($gt)) return export_bvop(cell, "(bvUgt A B)", 'b');
+
+			if (cell->type == ID($ne)) return export_bvop(cell, "(distinct A B)", 'b');
+			if (cell->type == ID($nex)) return export_bvop(cell, "(distinct A B)", 'b');
+			if (cell->type == ID($eq)) return export_bvop(cell, "(= A B)", 'b');
+			if (cell->type == ID($eqx)) return export_bvop(cell, "(= A B)", 'b');
+
+			if (cell->type == ID($not)) return export_bvop(cell, "(bvnot A)");
+			if (cell->type == ID($pos)) return export_bvop(cell, "A");
+			if (cell->type == ID($neg)) return export_bvop(cell, "(bvneg A)");
+
+			if (cell->type == ID($add)) return export_bvop(cell, "(bvadd A B)");
+			if (cell->type == ID($sub)) return export_bvop(cell, "(bvsub A B)");
+			if (cell->type == ID($mul)) return export_bvop(cell, "(bvmul A B)");
+			if (cell->type == ID($div)) return export_bvop(cell, "(bvUdiv A B)", 'd');
+			if (cell->type == ID($mod)) return export_bvop(cell, "(bvUrem A B)", 'd');
+
+			if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)) &&
+					2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) {
+				bool is_and = cell->type == ID($reduce_and);
+				string bits(GetSize(cell->getPort(ID::A)), is_and ? '1' : '0');
 				return export_bvop(cell, stringf("(%s A #b%s)", is_and ? "=" : "distinct", bits.c_str()), 'b');
 			}
 
-			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 == ID($reduce_and)) return export_reduce(cell, "(and A)", true);
+			if (cell->type == ID($reduce_or)) return export_reduce(cell, "(or A)", false);
+			if (cell->type == ID($reduce_xor)) return export_reduce(cell, "(xor A)", false);
+			if (cell->type == ID($reduce_xnor)) return export_reduce(cell, "(not (xor A))", false);
+			if (cell->type == ID($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 == ID($logic_not)) return export_reduce(cell, "(not (or A))", false);
+			if (cell->type == ID($logic_and)) return export_reduce(cell, "(and (or A) (or B))", false);
+			if (cell->type == ID($logic_or)) return export_reduce(cell, "(or A B)", false);
 
-			if (cell->type.in("$mux", "$pmux"))
+			if (cell->type.in(ID($mux), ID($pmux)))
 			{
-				int width = GetSize(cell->getPort("\\Y"));
-				std::string processed_expr = get_bv(cell->getPort("\\A"));
+				int width = GetSize(cell->getPort(ID::Y));
+				std::string processed_expr = get_bv(cell->getPort(ID::A));
 
-				RTLIL::SigSpec sig_b = cell->getPort("\\B");
-				RTLIL::SigSpec sig_s = cell->getPort("\\S");
+				RTLIL::SigSpec sig_b = cell->getPort(ID::B);
+				RTLIL::SigSpec sig_s = cell->getPort(ID::S);
 				get_bv(sig_b);
 				get_bv(sig_s);
 
@@ -626,7 +626,7 @@ struct Smt2Worker
 				if (verbose)
 					log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
 
-				RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
+				RTLIL::SigSpec sig = sigmap(cell->getPort(ID::Y));
 				decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
 						get_id(module), idcounter, get_id(module), width, processed_expr.c_str(), log_signal(sig)));
 				register_bv(sig, idcounter++);
@@ -637,19 +637,19 @@ struct Smt2Worker
 			// FIXME: $slice $concat
 		}
 
-		if (memmode && cell->type == "$mem")
+		if (memmode && cell->type == ID($mem))
 		{
 			int arrayid = idcounter++;
 			memarrays[cell] = arrayid;
 
-			int abits = cell->getParam("\\ABITS").as_int();
-			int width = cell->getParam("\\WIDTH").as_int();
-			int rd_ports = cell->getParam("\\RD_PORTS").as_int();
-			int wr_ports = cell->getParam("\\WR_PORTS").as_int();
+			int abits = cell->getParam(ID::ABITS).as_int();
+			int width = cell->getParam(ID::WIDTH).as_int();
+			int rd_ports = cell->getParam(ID::RD_PORTS).as_int();
+			int wr_ports = cell->getParam(ID::WR_PORTS).as_int();
 
 			bool async_read = false;
-			if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
-				if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_zero())
+			if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) {
+				if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero())
 					log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
 				async_read = true;
 			}
@@ -665,8 +665,8 @@ struct Smt2Worker
 
 			if (statebv)
 			{
-				int mem_size = cell->getParam("\\SIZE").as_int();
-				int mem_offset = cell->getParam("\\OFFSET").as_int();
+				int mem_size = cell->getParam(ID::SIZE).as_int();
+				int mem_offset = cell->getParam(ID::OFFSET).as_int();
 
 				makebits(memstate, width*mem_size, get_id(cell));
 				decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n",
@@ -674,11 +674,11 @@ struct Smt2Worker
 
 				for (int i = 0; i < rd_ports; i++)
 				{
-					SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
-					SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
+					SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits);
+					SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width);
 					std::string addr = get_bv(addr_sig);
 
-					if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
+					if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool())
 						log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
 								"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
 
@@ -717,11 +717,11 @@ struct Smt2Worker
 
 				for (int i = 0; i < rd_ports; i++)
 				{
-					SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
-					SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
+					SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits);
+					SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width);
 					std::string addr = get_bv(addr_sig);
 
-					if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
+					if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool())
 						log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
 								"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
 
@@ -801,9 +801,9 @@ struct Smt2Worker
 
 		pool<SigBit> reg_bits;
 		for (auto cell : module->cells())
-			if (cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_P_", "$_DFF_N_")) {
+			if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) {
 				// not using sigmap -- we want the net directly at the dff output
-				for (auto bit : cell->getPort("\\Q"))
+				for (auto bit : cell->getPort(ID::Q))
 					reg_bits.insert(bit);
 			}
 
@@ -812,7 +812,7 @@ struct Smt2Worker
 			for (auto bit : SigSpec(wire))
 				if (reg_bits.count(bit))
 					is_register = true;
-			if (wire->port_id || is_register || wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) {
+			if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) {
 				RTLIL::SigSpec sig = sigmap(wire);
 				if (wire->port_input)
 					decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width));
@@ -820,7 +820,7 @@ struct Smt2Worker
 					decls.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
 				if (is_register)
 					decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
-				if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\'))
+				if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\'))
 					decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
 				if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
 					decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
@@ -854,9 +854,9 @@ struct Smt2Worker
 
 		vector<string> init_list;
 		for (auto wire : module->wires())
-			if (wire->attributes.count("\\init")) {
+			if (wire->attributes.count(ID::init)) {
 				RTLIL::SigSpec sig = sigmap(wire);
-				Const val = wire->attributes.at("\\init");
+				Const val = wire->attributes.at(ID::init);
 				val.bits.resize(GetSize(sig), State::Sx);
 				if (bvmode && GetSize(sig) > 1) {
 					Const mask(State::S1, GetSize(sig));
@@ -885,31 +885,31 @@ struct Smt2Worker
 
 		for (auto cell : module->cells())
 		{
-			if (cell->type.in("$assert", "$assume", "$cover"))
+			if (cell->type.in(ID($assert), ID($assume), ID($cover)))
 			{
-				int &id = cell->type == "$assert" ? assert_id :
-						cell->type == "$assume" ? assume_id :
-						cell->type == "$cover" ? cover_id : *(int*)nullptr;
+				int &id = cell->type == ID($assert) ? assert_id :
+						cell->type == ID($assume) ? assume_id :
+						cell->type == ID($cover) ? cover_id : *(int*)nullptr;
 
-				char postfix = cell->type == "$assert" ? 'a' :
-						cell->type == "$assume" ? 'u' :
-						cell->type == "$cover" ? 'c' : 0;
+				char postfix = cell->type == ID($assert) ? 'a' :
+						cell->type == ID($assume) ? 'u' :
+						cell->type == ID($cover) ? 'c' : 0;
 
-				string name_a = get_bool(cell->getPort("\\A"));
-				string name_en = get_bool(cell->getPort("\\EN"));
-				string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\src").decode_string() : get_id(cell);
+				string name_a = get_bool(cell->getPort(ID::A));
+				string name_en = get_bool(cell->getPort(ID::EN));
+				string infostr = (cell->name[0] == '$' && cell->attributes.count(ID::src)) ? cell->attributes.at(ID::src).decode_string() : get_id(cell);
 				decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str()));
 
-				if (cell->type == "$cover")
+				if (cell->type == ID($cover))
 					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
 							get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
 				else
 					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
 							get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
 
-				if (cell->type == "$assert")
+				if (cell->type == ID($assert))
 					assert_list.push_back(stringf("(|%s_a %d| state)", get_id(module), id));
-				else if (cell->type == "$assume")
+				else if (cell->type == ID($assume))
 					assume_list.push_back(stringf("(|%s_u %d| state)", get_id(module), id));
 
 				id++;
@@ -965,44 +965,44 @@ struct Smt2Worker
 
 			for (auto cell : this_regs)
 			{
-				if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
+				if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_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(), get_id(cell), log_signal(cell->getPort("\\Q"))));
-					ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort("\\Q")).c_str(), get_bool(cell->getPort("\\Q"), "other_state").c_str()));
+					std::string expr_d = get_bool(cell->getPort(ID::D));
+					std::string expr_q = get_bool(cell->getPort(ID::Q), "next_state");
+					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Q))));
+					ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort(ID::Q)).c_str(), get_bool(cell->getPort(ID::Q), "other_state").c_str()));
 				}
 
-				if (cell->type.in("$ff", "$dff"))
+				if (cell->type.in(ID($ff), ID($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(), get_id(cell), log_signal(cell->getPort("\\Q"))));
-					ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Q")).c_str(), get_bv(cell->getPort("\\Q"), "other_state").c_str()));
+					std::string expr_d = get_bv(cell->getPort(ID::D));
+					std::string expr_q = get_bv(cell->getPort(ID::Q), "next_state");
+					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Q))));
+					ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Q)).c_str(), get_bv(cell->getPort(ID::Q), "other_state").c_str()));
 				}
 
-				if (cell->type.in("$anyconst", "$allconst"))
+				if (cell->type.in(ID($anyconst), ID($allconst)))
 				{
-					std::string expr_d = get_bv(cell->getPort("\\Y"));
-					std::string expr_q = get_bv(cell->getPort("\\Y"), "next_state");
-					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Y"))));
-					if (cell->type == "$anyconst")
-						ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Y")).c_str(), get_bv(cell->getPort("\\Y"), "other_state").c_str()));
+					std::string expr_d = get_bv(cell->getPort(ID::Y));
+					std::string expr_q = get_bv(cell->getPort(ID::Y), "next_state");
+					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Y))));
+					if (cell->type == ID($anyconst))
+						ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Y)).c_str(), get_bv(cell->getPort(ID::Y), "other_state").c_str()));
 				}
 
-				if (cell->type == "$mem")
+				if (cell->type == ID($mem))
 				{
 					int arrayid = memarrays.at(cell);
 
-					int abits = cell->getParam("\\ABITS").as_int();
-					int width = cell->getParam("\\WIDTH").as_int();
-					int wr_ports = cell->getParam("\\WR_PORTS").as_int();
+					int abits = cell->getParam(ID::ABITS).as_int();
+					int width = cell->getParam(ID::WIDTH).as_int();
+					int wr_ports = cell->getParam(ID::WR_PORTS).as_int();
 
 					bool async_read = false;
 					string initial_memstate, final_memstate;
 
-					if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
-						log_assert(cell->getParam("\\WR_CLK_ENABLE").is_fully_zero());
+					if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) {
+						log_assert(cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero());
 						async_read = true;
 						initial_memstate = stringf("%s#%d#0", get_id(module), arrayid);
 						final_memstate = stringf("%s#%d#final", get_id(module), arrayid);
@@ -1010,8 +1010,8 @@ struct Smt2Worker
 
 					if (statebv)
 					{
-						int mem_size = cell->getParam("\\SIZE").as_int();
-						int mem_offset = cell->getParam("\\OFFSET").as_int();
+						int mem_size = cell->getParam(ID::SIZE).as_int();
+						int mem_offset = cell->getParam(ID::OFFSET).as_int();
 
 						if (async_read) {
 							makebits(final_memstate, width*mem_size, get_id(cell));
@@ -1019,9 +1019,9 @@ struct Smt2Worker
 
 						for (int i = 0; i < wr_ports; i++)
 						{
-							SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits);
-							SigSpec data_sig = cell->getPort("\\WR_DATA").extract(width*i, width);
-							SigSpec mask_sig = cell->getPort("\\WR_EN").extract(width*i, width);
+							SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits);
+							SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width);
+							SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width);
 
 							std::string addr = get_bv(addr_sig);
 							std::string data = get_bv(data_sig);
@@ -1066,9 +1066,9 @@ struct Smt2Worker
 
 						for (int i = 0; i < wr_ports; i++)
 						{
-							SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits);
-							SigSpec data_sig = cell->getPort("\\WR_DATA").extract(width*i, width);
-							SigSpec mask_sig = cell->getPort("\\WR_EN").extract(width*i, width);
+							SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits);
+							SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width);
+							SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width);
 
 							std::string addr = get_bv(addr_sig);
 							std::string data = get_bv(data_sig);
@@ -1104,8 +1104,8 @@ struct Smt2Worker
 					if (async_read)
 						hier.push_back(stringf("  (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell)));
 
-					Const init_data = cell->getParam("\\INIT");
-					int memsize = cell->getParam("\\SIZE").as_int();
+					Const init_data = cell->getParam(ID::INIT);
+					int memsize = cell->getParam(ID::SIZE).as_int();
 
 					for (int i = 0; i < memsize; i++)
 					{
@@ -1394,7 +1394,7 @@ struct Smt2Backend : public Backend {
 		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("        ; we need QF_UFBV for this proof\n");
 		log("        (set-logic QF_UFBV)\n");
 		log("\n");
 		log("        ; insert the auto-generated code here\n");
@@ -1523,12 +1523,12 @@ struct Smt2Backend : public Backend {
 				for (auto &dep : it.second)
 					if (module_deps.count(dep) > 0)
 						goto not_ready_yet;
-				// log("Next in topological sort: %s\n", RTLIL::id2cstr(it.first->name));
+				// log("Next in topological sort: %s\n", log_id(it.first->name));
 				sorted_modules.push_back(it.first);
 			not_ready_yet:;
 			}
 			if (sorted_modules_idx == sorted_modules.size())
-				log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", RTLIL::id2cstr(module_deps.begin()->first->name));
+				log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", log_id(module_deps.begin()->first->name));
 			while (sorted_modules_idx < sorted_modules.size())
 				module_deps.erase(sorted_modules.at(sorted_modules_idx++));
 		}
@@ -1540,7 +1540,7 @@ struct Smt2Backend : public Backend {
 
 		for (auto module : sorted_modules)
 			for (auto cell : module->cells())
-				if (cell->type.in("$allconst", "$allseq"))
+				if (cell->type.in(ID($allconst), ID($allseq)))
 					goto found_forall;
 		if (0) {
 	found_forall:
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 4c691716e..69f59df79 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -704,8 +704,12 @@ class SmtIo:
                     if msg is not None:
                         print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True)
 
-        result = ""
-        while result not in ["sat", "unsat"]:
+        if self.forall:
+            result = self.read()
+            while result not in ["sat", "unsat", "unknown"]:
+                print("%s %s: %s" % (self.timestamp(), self.solver, result))
+                result = self.read()
+        else:
             result = self.read()
 
         if self.debug_file:
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index f755307bf..7113ebc97 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -219,30 +219,30 @@ struct SmvWorker
 			if (wire->port_input)
 				inputvars.push_back(stringf("%s : unsigned word[%d]; -- %s", cid(wire->name), wire->width, log_id(wire)));
 
-			if (wire->attributes.count("\\init"))
-				assignments.push_back(stringf("init(%s) := %s;", lvalue(wire), rvalue(wire->attributes.at("\\init"))));
+			if (wire->attributes.count(ID::init))
+				assignments.push_back(stringf("init(%s) := %s;", lvalue(wire), rvalue(wire->attributes.at(ID::init))));
 		}
 
 		for (auto cell : module->cells())
 		{
 			// FIXME: $slice, $concat, $mem
 
-			if (cell->type.in("$assert"))
+			if (cell->type.in(ID($assert)))
 			{
-				SigSpec sig_a = cell->getPort("\\A");
-				SigSpec sig_en = cell->getPort("\\EN");
+				SigSpec sig_a = cell->getPort(ID::A);
+				SigSpec sig_en = cell->getPort(ID::EN);
 
 				invarspecs.push_back(stringf("!bool(%s) | bool(%s);", rvalue(sig_en), rvalue(sig_a)));
 
 				continue;
 			}
 
-			if (cell->type.in("$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx"))
+			if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)))
 			{
-				SigSpec sig_a = cell->getPort("\\A");
-				SigSpec sig_b = cell->getPort("\\B");
+				SigSpec sig_a = cell->getPort(ID::A);
+				SigSpec sig_b = cell->getPort(ID::B);
 
-				int width_y = GetSize(cell->getPort("\\Y"));
+				int width_y = GetSize(cell->getPort(ID::Y));
 				int shift_b_width = GetSize(sig_b);
 				int width_ay = max(GetSize(sig_a), width_y);
 				int width = width_ay;
@@ -254,12 +254,12 @@ struct SmvWorker
 						break;
 					}
 
-				bool signed_a = cell->getParam("\\A_SIGNED").as_bool();
-				bool signed_b = cell->getParam("\\B_SIGNED").as_bool();
-				string op = cell->type.in("$shl", "$sshl") ? "<<" : ">>";
+				bool signed_a = cell->getParam(ID::A_SIGNED).as_bool();
+				bool signed_b = cell->getParam(ID::B_SIGNED).as_bool();
+				string op = cell->type.in(ID($shl), ID($sshl)) ? "<<" : ">>";
 				string expr, expr_a;
 
-				if (cell->type == "$sshr" && signed_a)
+				if (cell->type == ID($sshr) && signed_a)
 				{
 					expr_a = rvalue_s(sig_a, width);
 					expr = stringf("resize(unsigned(%s %s %s), %d)", expr_a.c_str(), op.c_str(), rvalue(sig_b.extract(0, shift_b_width)), width_y);
@@ -268,7 +268,7 @@ struct SmvWorker
 								rvalue(sig_b.extract(shift_b_width, GetSize(sig_b) - shift_b_width)), GetSize(sig_b) - shift_b_width,
 								rvalue(sig_a[GetSize(sig_a)-1]), width_y, width_y, expr.c_str());
 				}
-				else if (cell->type.in("$shift", "$shiftx") && signed_b)
+				else if (cell->type.in(ID($shift), ID($shiftx)) && signed_b)
 				{
 					expr_a = rvalue_u(sig_a, width);
 
@@ -292,7 +292,7 @@ struct SmvWorker
 				}
 				else
 				{
-					if (cell->type.in("$shift", "$shiftx") || !signed_a)
+					if (cell->type.in(ID($shift), ID($shiftx)) || !signed_a)
 						expr_a = rvalue_u(sig_a, width);
 					else
 						expr_a = stringf("resize(unsigned(%s), %d)", rvalue_s(sig_a, width_ay), width);
@@ -303,272 +303,272 @@ struct SmvWorker
 								GetSize(sig_b)-shift_b_width, width_y, expr.c_str());
 				}
 
-				definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
+				definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort(ID::Y)), expr.c_str()));
 
 				continue;
 			}
 
-			if (cell->type.in("$not", "$pos", "$neg"))
+			if (cell->type.in(ID($not), ID($pos), ID($neg)))
 			{
-				int width = GetSize(cell->getPort("\\Y"));
+				int width = GetSize(cell->getPort(ID::Y));
 				string expr_a, op;
 
-				if (cell->type == "$not")  op = "!";
-				if (cell->type == "$pos")  op = "";
-				if (cell->type == "$neg")  op = "-";
+				if (cell->type == ID($not))  op = "!";
+				if (cell->type == ID($pos))  op = "";
+				if (cell->type == ID($neg))  op = "-";
 
-				if (cell->getParam("\\A_SIGNED").as_bool())
+				if (cell->getParam(ID::A_SIGNED).as_bool())
 				{
-					definitions.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort("\\Y")),
-							op.c_str(), rvalue_s(cell->getPort("\\A"), width)));
+					definitions.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort(ID::Y)),
+							op.c_str(), rvalue_s(cell->getPort(ID::A), width)));
 				}
 				else
 				{
-					definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")),
-							op.c_str(), rvalue_u(cell->getPort("\\A"), width)));
+					definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort(ID::Y)),
+							op.c_str(), rvalue_u(cell->getPort(ID::A), width)));
 				}
 
 				continue;
 			}
 
-			if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor"))
+			if (cell->type.in(ID($add), ID($sub), ID($mul), ID($and), ID($or), ID($xor), ID($xnor)))
 			{
-				int width = GetSize(cell->getPort("\\Y"));
+				int width = GetSize(cell->getPort(ID::Y));
 				string expr_a, expr_b, op;
 
-				if (cell->type == "$add")  op = "+";
-				if (cell->type == "$sub")  op = "-";
-				if (cell->type == "$mul")  op = "*";
-				if (cell->type == "$and")  op = "&";
-				if (cell->type == "$or")   op = "|";
-				if (cell->type == "$xor")  op = "xor";
-				if (cell->type == "$xnor") op = "xnor";
+				if (cell->type == ID($add))  op = "+";
+				if (cell->type == ID($sub))  op = "-";
+				if (cell->type == ID($mul))  op = "*";
+				if (cell->type == ID($and))  op = "&";
+				if (cell->type == ID($or))   op = "|";
+				if (cell->type == ID($xor))  op = "xor";
+				if (cell->type == ID($xnor)) op = "xnor";
 
-				if (cell->getParam("\\A_SIGNED").as_bool())
+				if (cell->getParam(ID::A_SIGNED).as_bool())
 				{
-					definitions.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort("\\Y")),
-							rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width)));
+					definitions.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort(ID::Y)),
+							rvalue_s(cell->getPort(ID::A), width), op.c_str(), rvalue_s(cell->getPort(ID::B), width)));
 				}
 				else
 				{
-					definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
-							rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width)));
+					definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort(ID::Y)),
+							rvalue_u(cell->getPort(ID::A), width), op.c_str(), rvalue_u(cell->getPort(ID::B), width)));
 				}
 
 				continue;
 			}
 
-			if (cell->type.in("$div", "$mod"))
+			if (cell->type.in(ID($div), ID($mod)))
 			{
-				int width_y = GetSize(cell->getPort("\\Y"));
-				int width = max(width_y, GetSize(cell->getPort("\\A")));
-				width = max(width, GetSize(cell->getPort("\\B")));
+				int width_y = GetSize(cell->getPort(ID::Y));
+				int width = max(width_y, GetSize(cell->getPort(ID::A)));
+				width = max(width, GetSize(cell->getPort(ID::B)));
 				string expr_a, expr_b, op;
 
-				if (cell->type == "$div")  op = "/";
-				if (cell->type == "$mod")  op = "mod";
+				if (cell->type == ID($div))  op = "/";
+				if (cell->type == ID($mod))  op = "mod";
 
-				if (cell->getParam("\\A_SIGNED").as_bool())
+				if (cell->getParam(ID::A_SIGNED).as_bool())
 				{
-					definitions.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
-							rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width), width_y));
+					definitions.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort(ID::Y)),
+							rvalue_s(cell->getPort(ID::A), width), op.c_str(), rvalue_s(cell->getPort(ID::B), width), width_y));
 				}
 				else
 				{
-					definitions.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort("\\Y")),
-							rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width), width_y));
+					definitions.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort(ID::Y)),
+							rvalue_u(cell->getPort(ID::A), width), op.c_str(), rvalue_u(cell->getPort(ID::B), width), width_y));
 				}
 
 				continue;
 			}
 
-			if (cell->type.in("$eq", "$ne", "$eqx", "$nex", "$lt", "$le", "$ge", "$gt"))
+			if (cell->type.in(ID($eq), ID($ne), ID($eqx), ID($nex), ID($lt), ID($le), ID($ge), ID($gt)))
 			{
-				int width = max(GetSize(cell->getPort("\\A")), GetSize(cell->getPort("\\B")));
+				int width = max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::B)));
 				string expr_a, expr_b, op;
 
-				if (cell->type == "$eq")  op = "=";
-				if (cell->type == "$ne")  op = "!=";
-				if (cell->type == "$eqx") op = "=";
-				if (cell->type == "$nex") op = "!=";
-				if (cell->type == "$lt")  op = "<";
-				if (cell->type == "$le")  op = "<=";
-				if (cell->type == "$ge")  op = ">=";
-				if (cell->type == "$gt")  op = ">";
+				if (cell->type == ID($eq))  op = "=";
+				if (cell->type == ID($ne))  op = "!=";
+				if (cell->type == ID($eqx)) op = "=";
+				if (cell->type == ID($nex)) op = "!=";
+				if (cell->type == ID($lt))  op = "<";
+				if (cell->type == ID($le))  op = "<=";
+				if (cell->type == ID($ge))  op = ">=";
+				if (cell->type == ID($gt))  op = ">";
 
-				if (cell->getParam("\\A_SIGNED").as_bool())
+				if (cell->getParam(ID::A_SIGNED).as_bool())
 				{
-					expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\A")), width);
-					expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\B")), width);
+					expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort(ID::A)), width);
+					expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort(ID::B)), width);
 				}
 				else
 				{
-					expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort("\\A")), width);
-					expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort("\\B")), width);
+					expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort(ID::A)), width);
+					expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort(ID::B)), width);
 				}
 
-				definitions.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
-						expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort("\\Y"))));
+				definitions.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort(ID::Y)),
+						expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort(ID::Y))));
 
 				continue;
 			}
 
-			if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool"))
+			if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)))
 			{
-				int width_a = GetSize(cell->getPort("\\A"));
-				int width_y = GetSize(cell->getPort("\\Y"));
-				const char *expr_a = rvalue(cell->getPort("\\A"));
-				const char *expr_y = lvalue(cell->getPort("\\Y"));
+				int width_a = GetSize(cell->getPort(ID::A));
+				int width_y = GetSize(cell->getPort(ID::Y));
+				const char *expr_a = rvalue(cell->getPort(ID::A));
+				const char *expr_y = lvalue(cell->getPort(ID::Y));
 				string expr;
 
-				if (cell->type == "$reduce_and")  expr = stringf("%s = !0ub%d_0", expr_a, width_a);
-				if (cell->type == "$reduce_or")   expr = stringf("%s != 0ub%d_0", expr_a, width_a);
-				if (cell->type == "$reduce_bool") expr = stringf("%s != 0ub%d_0", expr_a, width_a);
+				if (cell->type == ID($reduce_and))  expr = stringf("%s = !0ub%d_0", expr_a, width_a);
+				if (cell->type == ID($reduce_or))   expr = stringf("%s != 0ub%d_0", expr_a, width_a);
+				if (cell->type == ID($reduce_bool)) expr = stringf("%s != 0ub%d_0", expr_a, width_a);
 
 				definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
 				continue;
 			}
 
-			if (cell->type.in("$reduce_xor", "$reduce_xnor"))
+			if (cell->type.in(ID($reduce_xor), ID($reduce_xnor)))
 			{
-				int width_y = GetSize(cell->getPort("\\Y"));
-				const char *expr_y = lvalue(cell->getPort("\\Y"));
+				int width_y = GetSize(cell->getPort(ID::Y));
+				const char *expr_y = lvalue(cell->getPort(ID::Y));
 				string expr;
 
-				for (auto bit : cell->getPort("\\A")) {
+				for (auto bit : cell->getPort(ID::A)) {
 					if (!expr.empty())
 						expr += " xor ";
 					expr += rvalue(bit);
 				}
 
-				if (cell->type == "$reduce_xnor")
+				if (cell->type == ID($reduce_xnor))
 					expr = "!(" + expr + ")";
 
 				definitions.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y));
 				continue;
 			}
 
-			if (cell->type.in("$logic_and", "$logic_or"))
+			if (cell->type.in(ID($logic_and), ID($logic_or)))
 			{
-				int width_a = GetSize(cell->getPort("\\A"));
-				int width_b = GetSize(cell->getPort("\\B"));
-				int width_y = GetSize(cell->getPort("\\Y"));
+				int width_a = GetSize(cell->getPort(ID::A));
+				int width_b = GetSize(cell->getPort(ID::B));
+				int width_y = GetSize(cell->getPort(ID::Y));
 
-				string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
-				string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\B")), width_b);
-				const char *expr_y = lvalue(cell->getPort("\\Y"));
+				string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort(ID::A)), width_a);
+				string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort(ID::B)), width_b);
+				const char *expr_y = lvalue(cell->getPort(ID::Y));
 
 				string expr;
-				if (cell->type == "$logic_and") expr = expr_a + " & " + expr_b;
-				if (cell->type == "$logic_or")  expr = expr_a + " | " + expr_b;
+				if (cell->type == ID($logic_and)) expr = expr_a + " & " + expr_b;
+				if (cell->type == ID($logic_or))  expr = expr_a + " | " + expr_b;
 
 				definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
 				continue;
 			}
 
-			if (cell->type.in("$logic_not"))
+			if (cell->type.in(ID($logic_not)))
 			{
-				int width_a = GetSize(cell->getPort("\\A"));
-				int width_y = GetSize(cell->getPort("\\Y"));
+				int width_a = GetSize(cell->getPort(ID::A));
+				int width_y = GetSize(cell->getPort(ID::Y));
 
-				string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
-				const char *expr_y = lvalue(cell->getPort("\\Y"));
+				string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort(ID::A)), width_a);
+				const char *expr_y = lvalue(cell->getPort(ID::Y));
 
 				definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y));
 				continue;
 			}
 
-			if (cell->type.in("$mux", "$pmux"))
+			if (cell->type.in(ID($mux), ID($pmux)))
 			{
-				int width = GetSize(cell->getPort("\\Y"));
-				SigSpec sig_a = cell->getPort("\\A");
-				SigSpec sig_b = cell->getPort("\\B");
-				SigSpec sig_s = cell->getPort("\\S");
+				int width = GetSize(cell->getPort(ID::Y));
+				SigSpec sig_a = cell->getPort(ID::A);
+				SigSpec sig_b = cell->getPort(ID::B);
+				SigSpec sig_s = cell->getPort(ID::S);
 
 				string expr;
 				for (int i = 0; i < GetSize(sig_s); i++)
 					expr += stringf("bool(%s) ? %s : ", rvalue(sig_s[i]), rvalue(sig_b.extract(i*width, width)));
 				expr += rvalue(sig_a);
 
-				definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
+				definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort(ID::Y)), expr.c_str()));
 				continue;
 			}
 
-			if (cell->type == "$dff")
+			if (cell->type == ID($dff))
 			{
-				vars.push_back(stringf("%s : unsigned word[%d]; -- %s", lvalue(cell->getPort("\\Q")), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q"))));
-				assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort("\\Q")), rvalue(cell->getPort("\\D"))));
+				vars.push_back(stringf("%s : unsigned word[%d]; -- %s", lvalue(cell->getPort(ID::Q)), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q))));
+				assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort(ID::Q)), rvalue(cell->getPort(ID::D))));
 				continue;
 			}
 
-			if (cell->type.in("$_BUF_", "$_NOT_"))
+			if (cell->type.in(ID($_BUF_), ID($_NOT_)))
 			{
-				string op = cell->type == "$_NOT_" ? "!" : "";
-				definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue(cell->getPort("\\A"))));
+				string op = cell->type == ID($_NOT_) ? "!" : "";
+				definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort(ID::Y)), op.c_str(), rvalue(cell->getPort(ID::A))));
 				continue;
 			}
 
-			if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_", "$_ANDNOT_", "$_ORNOT_"))
+			if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_)))
 			{
 				string op;
 
-				if (cell->type.in("$_AND_", "$_NAND_", "$_ANDNOT_")) op = "&";
-				if (cell->type.in("$_OR_", "$_NOR_", "$_ORNOT_")) op = "|";
-				if (cell->type.in("$_XOR_"))  op = "xor";
-				if (cell->type.in("$_XNOR_"))  op = "xnor";
+				if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_ANDNOT_))) op = "&";
+				if (cell->type.in(ID($_OR_), ID($_NOR_), ID($_ORNOT_))) op = "|";
+				if (cell->type.in(ID($_XOR_)))  op = "xor";
+				if (cell->type.in(ID($_XNOR_)))  op = "xnor";
 
-				if (cell->type.in("$_ANDNOT_", "$_ORNOT_"))
-					definitions.push_back(stringf("%s := %s %s (!%s);", lvalue(cell->getPort("\\Y")),
-							rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
+				if (cell->type.in(ID($_ANDNOT_), ID($_ORNOT_)))
+					definitions.push_back(stringf("%s := %s %s (!%s);", lvalue(cell->getPort(ID::Y)),
+							rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B))));
 				else
-				if (cell->type.in("$_NAND_", "$_NOR_"))
-					definitions.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort("\\Y")),
-							rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
+				if (cell->type.in(ID($_NAND_), ID($_NOR_)))
+					definitions.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort(ID::Y)),
+							rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B))));
 				else
-					definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
-							rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
+					definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort(ID::Y)),
+							rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B))));
 				continue;
 			}
 
-			if (cell->type == "$_MUX_")
+			if (cell->type == ID($_MUX_))
 			{
-				definitions.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort("\\Y")),
-						rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A"))));
+				definitions.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort(ID::Y)),
+						rvalue(cell->getPort(ID::S)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::A))));
 				continue;
 			}
 
-			if (cell->type == "$_NMUX_")
+			if (cell->type == ID($_NMUX_))
 			{
-				definitions.push_back(stringf("%s := !(bool(%s) ? %s : %s);", lvalue(cell->getPort("\\Y")),
-						rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A"))));
+				definitions.push_back(stringf("%s := !(bool(%s) ? %s : %s);", lvalue(cell->getPort(ID::Y)),
+						rvalue(cell->getPort(ID::S)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::A))));
 				continue;
 			}
 
-			if (cell->type == "$_AOI3_")
+			if (cell->type == ID($_AOI3_))
 			{
-				definitions.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")),
-						rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
+				definitions.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort(ID::Y)),
+						rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C))));
 				continue;
 			}
 
-			if (cell->type == "$_OAI3_")
+			if (cell->type == ID($_OAI3_))
 			{
-				definitions.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort("\\Y")),
-						rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
+				definitions.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort(ID::Y)),
+						rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C))));
 				continue;
 			}
 
-			if (cell->type == "$_AOI4_")
+			if (cell->type == ID($_AOI4_))
 			{
-				definitions.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort("\\Y")),
-						rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
+				definitions.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort(ID::Y)),
+						rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C)), rvalue(cell->getPort(ID::D))));
 				continue;
 			}
 
-			if (cell->type == "$_OAI4_")
+			if (cell->type == ID($_OAI4_))
 			{
-				definitions.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort("\\Y")),
-						rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
+				definitions.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort(ID::Y)),
+						rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C)), rvalue(cell->getPort(ID::D))));
 				continue;
 			}
 
diff --git a/backends/spice/spice.cc b/backends/spice/spice.cc
index 6738a4bbd..84e93b61b 100644
--- a/backends/spice/spice.cc
+++ b/backends/spice/spice.cc
@@ -70,14 +70,13 @@ static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::De
 	idict<IdString, 1> inums;
 	int cell_counter = 0, conn_counter = 0, nc_counter = 0;
 
-	for (auto &cell_it : module->cells_)
+	for (auto cell : module->cells())
 	{
-		RTLIL::Cell *cell = cell_it.second;
 		f << stringf("X%d", cell_counter++);
 
 		std::vector<RTLIL::SigSpec> port_sigs;
 
-		if (design->modules_.count(cell->type) == 0)
+		if (design->module(cell->type) == nullptr)
 		{
 			log_warning("no (blackbox) module for cell type `%s' (%s.%s) found! Guessing order of ports.\n",
 					log_id(cell->type), log_id(module), log_id(cell));
@@ -88,11 +87,10 @@ static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::De
 		}
 		else
 		{
-			RTLIL::Module *mod = design->modules_.at(cell->type);
+			RTLIL::Module *mod = design->module(cell->type);
 
 			std::vector<RTLIL::Wire*> ports;
-			for (auto wire_it : mod->wires_) {
-				RTLIL::Wire *wire = wire_it.second;
+			for (auto wire : mod->wires()) {
 				if (wire->port_id == 0)
 					continue;
 				while (int(ports.size()) < wire->port_id)
@@ -202,16 +200,15 @@ struct SpiceBackend : public Backend {
 		extra_args(f, filename, args, argidx);
 
 		if (top_module_name.empty())
-			for (auto & mod_it:design->modules_)
-				if (mod_it.second->get_bool_attribute("\\top"))
-					top_module_name = mod_it.first.str();
+			for (auto module : design->modules())
+				if (module->get_bool_attribute(ID::top))
+					top_module_name = module->name.str();
 
 		*f << stringf("* SPICE netlist generated by %s\n", yosys_version_str);
 		*f << stringf("\n");
 
-		for (auto module_it : design->modules_)
+		for (auto module : design->modules())
 		{
-			RTLIL::Module *module = module_it.second;
 			if (module->get_blackbox_attribute())
 				continue;
 
@@ -226,8 +223,7 @@ struct SpiceBackend : public Backend {
 			}
 
 			std::vector<RTLIL::Wire*> ports;
-			for (auto wire_it : module->wires_) {
-				RTLIL::Wire *wire = wire_it.second;
+			for (auto wire : module->wires()) {
 				if (wire->port_id == 0)
 					continue;
 				while (int(ports.size()) < wire->port_id)
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 19541f1c4..5467e250b 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -73,12 +73,12 @@ 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)
-		reset_auto_counter_id(it->second->name, true);
+	for (auto w : module->wires())
+		reset_auto_counter_id(w->name, true);
 
-	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 cell : module->cells()) {
+		reset_auto_counter_id(cell->name, true);
+		reset_auto_counter_id(cell->type, false);
 	}
 
 	for (auto it = module->processes.begin(); it != module->processes.end(); ++it)
@@ -378,7 +378,7 @@ void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString,
 	if (attr2comment)
 		as_comment = true;
 	for (auto it = attributes.begin(); it != attributes.end(); ++it) {
-		if (it->first == "\\init" && regattr) continue;
+		if (it->first == ID::init && regattr) continue;
 		f << stringf("%s" "%s %s", indent.c_str(), as_comment ? "/*" : "(*", id(it->first).c_str());
 		f << stringf(" = ");
 		if (modattr && (it->second == State::S0 || it->second == Const(0)))
@@ -423,9 +423,9 @@ void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
 		f << stringf("%s" "inout%s %s;\n", indent.c_str(), range.c_str(), id(wire->name).c_str());
 	if (reg_wires.count(wire->name)) {
 		f << stringf("%s" "reg%s %s", indent.c_str(), range.c_str(), id(wire->name).c_str());
-		if (wire->attributes.count("\\init")) {
+		if (wire->attributes.count(ID::init)) {
 			f << stringf(" = ");
-			dump_const(f, wire->attributes.at("\\init"));
+			dump_const(f, wire->attributes.at(ID::init));
 		}
 		f << stringf(";\n");
 	} else if (!wire->port_input && !wire->port_output)
@@ -451,9 +451,9 @@ void dump_cell_expr_port(std::ostream &f, RTLIL::Cell *cell, std::string port, b
 
 std::string cellname(RTLIL::Cell *cell)
 {
-	if (!norename && cell->name[0] == '$' && reg_ct.count(cell->type) && cell->hasPort("\\Q"))
+	if (!norename && cell->name[0] == '$' && reg_ct.count(cell->type) && cell->hasPort(ID::Q))
 	{
-		RTLIL::SigSpec sig = cell->getPort("\\Q");
+		RTLIL::SigSpec sig = cell->getPort(ID::Q);
 		if (GetSize(sig) != 1 || sig.is_fully_const())
 			goto no_special_reg_name;
 
@@ -488,7 +488,7 @@ no_special_reg_name:
 void dump_cell_expr_uniop(std::ostream &f, std::string indent, RTLIL::Cell *cell, std::string op)
 {
 	f << stringf("%s" "assign ", indent.c_str());
-	dump_sigspec(f, cell->getPort("\\Y"));
+	dump_sigspec(f, cell->getPort(ID::Y));
 	f << stringf(" = %s ", op.c_str());
 	dump_attributes(f, "", cell->attributes, ' ');
 	dump_cell_expr_port(f, cell, "A", true);
@@ -498,7 +498,7 @@ void dump_cell_expr_uniop(std::ostream &f, std::string indent, RTLIL::Cell *cell
 void dump_cell_expr_binop(std::ostream &f, std::string indent, RTLIL::Cell *cell, std::string op)
 {
 	f << stringf("%s" "assign ", indent.c_str());
-	dump_sigspec(f, cell->getPort("\\Y"));
+	dump_sigspec(f, cell->getPort(ID::Y));
 	f << stringf(" = ");
 	dump_cell_expr_port(f, cell, "A", true);
 	f << stringf(" %s ", op.c_str());
@@ -509,9 +509,9 @@ void dump_cell_expr_binop(std::ostream &f, std::string indent, RTLIL::Cell *cell
 
 bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 {
-	if (cell->type == "$_NOT_") {
+	if (cell->type == ID($_NOT_)) {
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = ");
 		f << stringf("~");
 		dump_attributes(f, "", cell->attributes, ' ');
@@ -520,34 +520,34 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
-	if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_", "$_ANDNOT_", "$_ORNOT_")) {
+	if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_))) {
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = ");
-		if (cell->type.in("$_NAND_", "$_NOR_", "$_XNOR_"))
+		if (cell->type.in(ID($_NAND_), ID($_NOR_), ID($_XNOR_)))
 			f << stringf("~(");
 		dump_cell_expr_port(f, cell, "A", false);
 		f << stringf(" ");
-		if (cell->type.in("$_AND_", "$_NAND_", "$_ANDNOT_"))
+		if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_ANDNOT_)))
 			f << stringf("&");
-		if (cell->type.in("$_OR_", "$_NOR_", "$_ORNOT_"))
+		if (cell->type.in(ID($_OR_), ID($_NOR_), ID($_ORNOT_)))
 			f << stringf("|");
-		if (cell->type.in("$_XOR_", "$_XNOR_"))
+		if (cell->type.in(ID($_XOR_), ID($_XNOR_)))
 			f << stringf("^");
 		dump_attributes(f, "", cell->attributes, ' ');
 		f << stringf(" ");
-		if (cell->type.in("$_ANDNOT_", "$_ORNOT_"))
+		if (cell->type.in(ID($_ANDNOT_), ID($_ORNOT_)))
 			f << stringf("~(");
 		dump_cell_expr_port(f, cell, "B", false);
-		if (cell->type.in("$_NAND_", "$_NOR_", "$_XNOR_", "$_ANDNOT_", "$_ORNOT_"))
+		if (cell->type.in(ID($_NAND_), ID($_NOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_)))
 			f << stringf(")");
 		f << stringf(";\n");
 		return true;
 	}
 
-	if (cell->type == "$_MUX_") {
+	if (cell->type == ID($_MUX_)) {
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = ");
 		dump_cell_expr_port(f, cell, "S", false);
 		f << stringf(" ? ");
@@ -559,9 +559,9 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
-	if (cell->type == "$_NMUX_") {
+	if (cell->type == ID($_NMUX_)) {
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = !(");
 		dump_cell_expr_port(f, cell, "S", false);
 		f << stringf(" ? ");
@@ -573,14 +573,14 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
-	if (cell->type.in("$_AOI3_", "$_OAI3_")) {
+	if (cell->type.in(ID($_AOI3_), ID($_OAI3_))) {
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = ~((");
 		dump_cell_expr_port(f, cell, "A", false);
-		f << stringf(cell->type == "$_AOI3_" ? " & " : " | ");
+		f << stringf(cell->type == ID($_AOI3_) ? " & " : " | ");
 		dump_cell_expr_port(f, cell, "B", false);
-		f << stringf(cell->type == "$_AOI3_" ? ") |" : ") &");
+		f << stringf(cell->type == ID($_AOI3_) ? ") |" : ") &");
 		dump_attributes(f, "", cell->attributes, ' ');
 		f << stringf(" ");
 		dump_cell_expr_port(f, cell, "C", false);
@@ -588,18 +588,18 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
-	if (cell->type.in("$_AOI4_", "$_OAI4_")) {
+	if (cell->type.in(ID($_AOI4_), ID($_OAI4_))) {
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = ~((");
 		dump_cell_expr_port(f, cell, "A", false);
-		f << stringf(cell->type == "$_AOI4_" ? " & " : " | ");
+		f << stringf(cell->type == ID($_AOI4_) ? " & " : " | ");
 		dump_cell_expr_port(f, cell, "B", false);
-		f << stringf(cell->type == "$_AOI4_" ? ") |" : ") &");
+		f << stringf(cell->type == ID($_AOI4_) ? ") |" : ") &");
 		dump_attributes(f, "", cell->attributes, ' ');
 		f << stringf(" (");
 		dump_cell_expr_port(f, cell, "C", false);
-		f << stringf(cell->type == "$_AOI4_" ? " & " : " | ");
+		f << stringf(cell->type == ID($_AOI4_) ? " & " : " | ");
 		dump_cell_expr_port(f, cell, "D", false);
 		f << stringf("));\n");
 		return true;
@@ -608,26 +608,26 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 	if (cell->type.begins_with("$_DFF_"))
 	{
 		std::string reg_name = cellname(cell);
-		bool out_is_reg_wire = is_reg_wire(cell->getPort("\\Q"), reg_name);
+		bool out_is_reg_wire = is_reg_wire(cell->getPort(ID::Q), reg_name);
 
 		if (!out_is_reg_wire) {
 			f << stringf("%s" "reg %s", indent.c_str(), reg_name.c_str());
-			dump_reg_init(f, cell->getPort("\\Q"));
+			dump_reg_init(f, cell->getPort(ID::Q));
 			f << ";\n";
 		}
 
 		dump_attributes(f, indent, cell->attributes);
 		f << stringf("%s" "always @(%sedge ", indent.c_str(), cell->type[6] == 'P' ? "pos" : "neg");
-		dump_sigspec(f, cell->getPort("\\C"));
+		dump_sigspec(f, cell->getPort(ID::C));
 		if (cell->type[7] != '_') {
 			f << stringf(" or %sedge ", cell->type[7] == 'P' ? "pos" : "neg");
-			dump_sigspec(f, cell->getPort("\\R"));
+			dump_sigspec(f, cell->getPort(ID::R));
 		}
 		f << stringf(")\n");
 
 		if (cell->type[7] != '_') {
 			f << stringf("%s" "  if (%s", indent.c_str(), cell->type[7] == 'P' ? "" : "!");
-			dump_sigspec(f, cell->getPort("\\R"));
+			dump_sigspec(f, cell->getPort(ID::R));
 			f << stringf(")\n");
 			f << stringf("%s" "    %s <= %c;\n", indent.c_str(), reg_name.c_str(), cell->type[8]);
 			f << stringf("%s" "  else\n", indent.c_str());
@@ -639,7 +639,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 
 		if (!out_is_reg_wire) {
 			f << stringf("%s" "assign ", indent.c_str());
-			dump_sigspec(f, cell->getPort("\\Q"));
+			dump_sigspec(f, cell->getPort(ID::Q));
 			f << stringf(" = %s;\n", reg_name.c_str());
 		}
 
@@ -651,30 +651,30 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		char pol_c = cell->type[8], pol_s = cell->type[9], pol_r = cell->type[10];
 
 		std::string reg_name = cellname(cell);
-		bool out_is_reg_wire = is_reg_wire(cell->getPort("\\Q"), reg_name);
+		bool out_is_reg_wire = is_reg_wire(cell->getPort(ID::Q), reg_name);
 
 		if (!out_is_reg_wire) {
 			f << stringf("%s" "reg %s", indent.c_str(), reg_name.c_str());
-			dump_reg_init(f, cell->getPort("\\Q"));
+			dump_reg_init(f, cell->getPort(ID::Q));
 			f << ";\n";
 		}
 
 		dump_attributes(f, indent, cell->attributes);
 		f << stringf("%s" "always @(%sedge ", indent.c_str(), pol_c == 'P' ? "pos" : "neg");
-		dump_sigspec(f, cell->getPort("\\C"));
+		dump_sigspec(f, cell->getPort(ID::C));
 		f << stringf(" or %sedge ", pol_s == 'P' ? "pos" : "neg");
-		dump_sigspec(f, cell->getPort("\\S"));
+		dump_sigspec(f, cell->getPort(ID::S));
 		f << stringf(" or %sedge ", pol_r == 'P' ? "pos" : "neg");
-		dump_sigspec(f, cell->getPort("\\R"));
+		dump_sigspec(f, cell->getPort(ID::R));
 		f << stringf(")\n");
 
 		f << stringf("%s" "  if (%s", indent.c_str(), pol_r == 'P' ? "" : "!");
-		dump_sigspec(f, cell->getPort("\\R"));
+		dump_sigspec(f, cell->getPort(ID::R));
 		f << stringf(")\n");
 		f << stringf("%s" "    %s <= 0;\n", indent.c_str(), reg_name.c_str());
 
 		f << stringf("%s" "  else if (%s", indent.c_str(), pol_s == 'P' ? "" : "!");
-		dump_sigspec(f, cell->getPort("\\S"));
+		dump_sigspec(f, cell->getPort(ID::S));
 		f << stringf(")\n");
 		f << stringf("%s" "    %s <= 1;\n", indent.c_str(), reg_name.c_str());
 
@@ -685,7 +685,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 
 		if (!out_is_reg_wire) {
 			f << stringf("%s" "assign ", indent.c_str());
-			dump_sigspec(f, cell->getPort("\\Q"));
+			dump_sigspec(f, cell->getPort(ID::Q));
 			f << stringf(" = %s;\n", reg_name.c_str());
 		}
 
@@ -697,117 +697,117 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 #define HANDLE_BINOP(_type, _operator) \
 	if (cell->type ==_type) { dump_cell_expr_binop(f, indent, cell, _operator); return true; }
 
-	HANDLE_UNIOP("$not", "~")
-	HANDLE_UNIOP("$pos", "+")
-	HANDLE_UNIOP("$neg", "-")
-
-	HANDLE_BINOP("$and",  "&")
-	HANDLE_BINOP("$or",   "|")
-	HANDLE_BINOP("$xor",  "^")
-	HANDLE_BINOP("$xnor", "~^")
-
-	HANDLE_UNIOP("$reduce_and",  "&")
-	HANDLE_UNIOP("$reduce_or",   "|")
-	HANDLE_UNIOP("$reduce_xor",  "^")
-	HANDLE_UNIOP("$reduce_xnor", "~^")
-	HANDLE_UNIOP("$reduce_bool", "|")
-
-	HANDLE_BINOP("$shl",  "<<")
-	HANDLE_BINOP("$shr",  ">>")
-	HANDLE_BINOP("$sshl", "<<<")
-	HANDLE_BINOP("$sshr", ">>>")
-
-	HANDLE_BINOP("$lt",  "<")
-	HANDLE_BINOP("$le",  "<=")
-	HANDLE_BINOP("$eq",  "==")
-	HANDLE_BINOP("$ne",  "!=")
-	HANDLE_BINOP("$eqx", "===")
-	HANDLE_BINOP("$nex", "!==")
-	HANDLE_BINOP("$ge",  ">=")
-	HANDLE_BINOP("$gt",  ">")
-
-	HANDLE_BINOP("$add", "+")
-	HANDLE_BINOP("$sub", "-")
-	HANDLE_BINOP("$mul", "*")
-	HANDLE_BINOP("$div", "/")
-	HANDLE_BINOP("$mod", "%")
-	HANDLE_BINOP("$pow", "**")
-
-	HANDLE_UNIOP("$logic_not", "!")
-	HANDLE_BINOP("$logic_and", "&&")
-	HANDLE_BINOP("$logic_or",  "||")
+	HANDLE_UNIOP(ID($not), "~")
+	HANDLE_UNIOP(ID($pos), "+")
+	HANDLE_UNIOP(ID($neg), "-")
+
+	HANDLE_BINOP(ID($and),  "&")
+	HANDLE_BINOP(ID($or),   "|")
+	HANDLE_BINOP(ID($xor),  "^")
+	HANDLE_BINOP(ID($xnor), "~^")
+
+	HANDLE_UNIOP(ID($reduce_and),  "&")
+	HANDLE_UNIOP(ID($reduce_or),   "|")
+	HANDLE_UNIOP(ID($reduce_xor),  "^")
+	HANDLE_UNIOP(ID($reduce_xnor), "~^")
+	HANDLE_UNIOP(ID($reduce_bool), "|")
+
+	HANDLE_BINOP(ID($shl),  "<<")
+	HANDLE_BINOP(ID($shr),  ">>")
+	HANDLE_BINOP(ID($sshl), "<<<")
+	HANDLE_BINOP(ID($sshr), ">>>")
+
+	HANDLE_BINOP(ID($lt),  "<")
+	HANDLE_BINOP(ID($le),  "<=")
+	HANDLE_BINOP(ID($eq),  "==")
+	HANDLE_BINOP(ID($ne),  "!=")
+	HANDLE_BINOP(ID($eqx), "===")
+	HANDLE_BINOP(ID($nex), "!==")
+	HANDLE_BINOP(ID($ge),  ">=")
+	HANDLE_BINOP(ID($gt),  ">")
+
+	HANDLE_BINOP(ID($add), "+")
+	HANDLE_BINOP(ID($sub), "-")
+	HANDLE_BINOP(ID($mul), "*")
+	HANDLE_BINOP(ID($div), "/")
+	HANDLE_BINOP(ID($mod), "%")
+	HANDLE_BINOP(ID($pow), "**")
+
+	HANDLE_UNIOP(ID($logic_not), "!")
+	HANDLE_BINOP(ID($logic_and), "&&")
+	HANDLE_BINOP(ID($logic_or),  "||")
 
 #undef HANDLE_UNIOP
 #undef HANDLE_BINOP
 
-	if (cell->type == "$shift")
+	if (cell->type == ID($shift))
 	{
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = ");
-		if (cell->getParam("\\B_SIGNED").as_bool())
+		if (cell->getParam(ID::B_SIGNED).as_bool())
 		{
 			f << stringf("$signed(");
-			dump_sigspec(f, cell->getPort("\\B"));
+			dump_sigspec(f, cell->getPort(ID::B));
 			f << stringf(")");
 			f << stringf(" < 0 ? ");
-			dump_sigspec(f, cell->getPort("\\A"));
+			dump_sigspec(f, cell->getPort(ID::A));
 			f << stringf(" << - ");
-			dump_sigspec(f, cell->getPort("\\B"));
+			dump_sigspec(f, cell->getPort(ID::B));
 			f << stringf(" : ");
-			dump_sigspec(f, cell->getPort("\\A"));
+			dump_sigspec(f, cell->getPort(ID::A));
 			f << stringf(" >> ");
-			dump_sigspec(f, cell->getPort("\\B"));
+			dump_sigspec(f, cell->getPort(ID::B));
 		}
 		else
 		{
-			dump_sigspec(f, cell->getPort("\\A"));
+			dump_sigspec(f, cell->getPort(ID::A));
 			f << stringf(" >> ");
-			dump_sigspec(f, cell->getPort("\\B"));
+			dump_sigspec(f, cell->getPort(ID::B));
 		}
 		f << stringf(";\n");
 		return true;
 	}
 
-	if (cell->type == "$shiftx")
+	if (cell->type == ID($shiftx))
 	{
 		std::string temp_id = next_auto_id();
-		f << stringf("%s" "wire [%d:0] %s = ", indent.c_str(), GetSize(cell->getPort("\\A"))-1, temp_id.c_str());
-		dump_sigspec(f, cell->getPort("\\A"));
+		f << stringf("%s" "wire [%d:0] %s = ", indent.c_str(), GetSize(cell->getPort(ID::A))-1, temp_id.c_str());
+		dump_sigspec(f, cell->getPort(ID::A));
 		f << stringf(";\n");
 
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = %s[", temp_id.c_str());
-		if (cell->getParam("\\B_SIGNED").as_bool())
+		if (cell->getParam(ID::B_SIGNED).as_bool())
 			f << stringf("$signed(");
-		dump_sigspec(f, cell->getPort("\\B"));
-		if (cell->getParam("\\B_SIGNED").as_bool())
+		dump_sigspec(f, cell->getPort(ID::B));
+		if (cell->getParam(ID::B_SIGNED).as_bool())
 			f << stringf(")");
-		f << stringf(" +: %d", cell->getParam("\\Y_WIDTH").as_int());
+		f << stringf(" +: %d", cell->getParam(ID::Y_WIDTH).as_int());
 		f << stringf("];\n");
 		return true;
 	}
 
-	if (cell->type == "$mux")
+	if (cell->type == ID($mux))
 	{
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = ");
-		dump_sigspec(f, cell->getPort("\\S"));
+		dump_sigspec(f, cell->getPort(ID::S));
 		f << stringf(" ? ");
 		dump_attributes(f, "", cell->attributes, ' ');
-		dump_sigspec(f, cell->getPort("\\B"));
+		dump_sigspec(f, cell->getPort(ID::B));
 		f << stringf(" : ");
-		dump_sigspec(f, cell->getPort("\\A"));
+		dump_sigspec(f, cell->getPort(ID::A));
 		f << stringf(";\n");
 		return true;
 	}
 
-	if (cell->type == "$pmux")
+	if (cell->type == ID($pmux))
 	{
-		int width = cell->parameters["\\WIDTH"].as_int();
-		int s_width = cell->getPort("\\S").size();
+		int width = cell->parameters[ID::WIDTH].as_int();
+		int s_width = cell->getPort(ID::S).size();
 		std::string func_name = cellname(cell);
 
 		f << stringf("%s" "function [%d:0] %s;\n", indent.c_str(), width-1, func_name.c_str());
@@ -839,76 +839,76 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		f << stringf("%s" "endfunction\n", indent.c_str());
 
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = %s(", func_name.c_str());
-		dump_sigspec(f, cell->getPort("\\A"));
+		dump_sigspec(f, cell->getPort(ID::A));
 		f << stringf(", ");
-		dump_sigspec(f, cell->getPort("\\B"));
+		dump_sigspec(f, cell->getPort(ID::B));
 		f << stringf(", ");
-		dump_sigspec(f, cell->getPort("\\S"));
+		dump_sigspec(f, cell->getPort(ID::S));
 		f << stringf(");\n");
 		return true;
 	}
 
-	if (cell->type == "$tribuf")
+	if (cell->type == ID($tribuf))
 	{
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = ");
-		dump_sigspec(f, cell->getPort("\\EN"));
+		dump_sigspec(f, cell->getPort(ID::EN));
 		f << stringf(" ? ");
-		dump_sigspec(f, cell->getPort("\\A"));
-		f << stringf(" : %d'bz;\n", cell->parameters.at("\\WIDTH").as_int());
+		dump_sigspec(f, cell->getPort(ID::A));
+		f << stringf(" : %d'bz;\n", cell->parameters.at(ID::WIDTH).as_int());
 		return true;
 	}
 
-	if (cell->type == "$slice")
+	if (cell->type == ID($slice))
 	{
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = ");
-		dump_sigspec(f, cell->getPort("\\A"));
-		f << stringf(" >> %d;\n", cell->parameters.at("\\OFFSET").as_int());
+		dump_sigspec(f, cell->getPort(ID::A));
+		f << stringf(" >> %d;\n", cell->parameters.at(ID::OFFSET).as_int());
 		return true;
 	}
 
-	if (cell->type == "$concat")
+	if (cell->type == ID($concat))
 	{
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = { ");
-		dump_sigspec(f, cell->getPort("\\B"));
+		dump_sigspec(f, cell->getPort(ID::B));
 		f << stringf(" , ");
-		dump_sigspec(f, cell->getPort("\\A"));
+		dump_sigspec(f, cell->getPort(ID::A));
 		f << stringf(" };\n");
 		return true;
 	}
 
-	if (cell->type == "$lut")
+	if (cell->type == ID($lut))
 	{
 		f << stringf("%s" "assign ", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\Y"));
+		dump_sigspec(f, cell->getPort(ID::Y));
 		f << stringf(" = ");
-		dump_const(f, cell->parameters.at("\\LUT"));
+		dump_const(f, cell->parameters.at(ID::LUT));
 		f << stringf(" >> ");
 		dump_attributes(f, "", cell->attributes, ' ');
-		dump_sigspec(f, cell->getPort("\\A"));
+		dump_sigspec(f, cell->getPort(ID::A));
 		f << stringf(";\n");
 		return true;
 	}
 
-	if (cell->type == "$dffsr")
+	if (cell->type == ID($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");
+		SigSpec sig_clk = cell->getPort(ID::CLK);
+		SigSpec sig_set = cell->getPort(ID::SET);
+		SigSpec sig_clr = cell->getPort(ID::CLR);
+		SigSpec sig_d = cell->getPort(ID::D);
+		SigSpec sig_q = cell->getPort(ID::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();
+		int width = cell->parameters[ID::WIDTH].as_int();
+		bool pol_clk = cell->parameters[ID::CLK_POLARITY].as_bool();
+		bool pol_set = cell->parameters[ID::SET_POLARITY].as_bool();
+		bool pol_clr = cell->parameters[ID::CLR_POLARITY].as_bool();
 
 		std::string reg_name = cellname(cell);
 		bool out_is_reg_wire = is_reg_wire(sig_q, reg_name);
@@ -950,43 +950,43 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
-	if (cell->type.in("$dff", "$adff", "$dffe"))
+	if (cell->type.in(ID($dff), ID($adff), ID($dffe)))
 	{
 		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();
+		sig_clk = cell->getPort(ID::CLK);
+		pol_clk = cell->parameters[ID::CLK_POLARITY].as_bool();
 
-		if (cell->type == "$adff") {
-			sig_arst = cell->getPort("\\ARST");
-			pol_arst = cell->parameters["\\ARST_POLARITY"].as_bool();
-			val_arst = RTLIL::SigSpec(cell->parameters["\\ARST_VALUE"]);
+		if (cell->type == ID($adff)) {
+			sig_arst = cell->getPort(ID::ARST);
+			pol_arst = cell->parameters[ID::ARST_POLARITY].as_bool();
+			val_arst = RTLIL::SigSpec(cell->parameters[ID::ARST_VALUE]);
 		}
 
-		if (cell->type == "$dffe") {
-			sig_en = cell->getPort("\\EN");
-			pol_en = cell->parameters["\\EN_POLARITY"].as_bool();
+		if (cell->type == ID($dffe)) {
+			sig_en = cell->getPort(ID::EN);
+			pol_en = cell->parameters[ID::EN_POLARITY].as_bool();
 		}
 
 		std::string reg_name = cellname(cell);
-		bool out_is_reg_wire = is_reg_wire(cell->getPort("\\Q"), reg_name);
+		bool out_is_reg_wire = is_reg_wire(cell->getPort(ID::Q), reg_name);
 
 		if (!out_is_reg_wire) {
-			f << stringf("%s" "reg [%d:0] %s", indent.c_str(), cell->parameters["\\WIDTH"].as_int()-1, reg_name.c_str());
-			dump_reg_init(f, cell->getPort("\\Q"));
+			f << stringf("%s" "reg [%d:0] %s", indent.c_str(), cell->parameters[ID::WIDTH].as_int()-1, reg_name.c_str());
+			dump_reg_init(f, cell->getPort(ID::Q));
 			f << ";\n";
 		}
 
 		f << stringf("%s" "always @(%sedge ", indent.c_str(), pol_clk ? "pos" : "neg");
 		dump_sigspec(f, sig_clk);
-		if (cell->type == "$adff") {
+		if (cell->type == ID($adff)) {
 			f << stringf(" or %sedge ", pol_arst ? "pos" : "neg");
 			dump_sigspec(f, sig_arst);
 		}
 		f << stringf(")\n");
 
-		if (cell->type == "$adff") {
+		if (cell->type == ID($adff)) {
 			f << stringf("%s" "  if (%s", indent.c_str(), pol_arst ? "" : "!");
 			dump_sigspec(f, sig_arst);
 			f << stringf(")\n");
@@ -996,7 +996,7 @@ 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") {
+		if (cell->type == ID($dffe)) {
 			f << stringf("%s" "  if (%s", indent.c_str(), pol_en ? "" : "!");
 			dump_sigspec(f, sig_en);
 			f << stringf(")\n");
@@ -1008,27 +1008,27 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 
 		if (!out_is_reg_wire) {
 			f << stringf("%s" "assign ", indent.c_str());
-			dump_sigspec(f, cell->getPort("\\Q"));
+			dump_sigspec(f, cell->getPort(ID::Q));
 			f << stringf(" = %s;\n", reg_name.c_str());
 		}
 
 		return true;
 	}
 
-	if (cell->type == "$dlatch")
+	if (cell->type == ID($dlatch))
 	{
 		RTLIL::SigSpec sig_en;
 		bool pol_en = false;
 
-		sig_en = cell->getPort("\\EN");
-		pol_en = cell->parameters["\\EN_POLARITY"].as_bool();
+		sig_en = cell->getPort(ID::EN);
+		pol_en = cell->parameters[ID::EN_POLARITY].as_bool();
 
 		std::string reg_name = cellname(cell);
-		bool out_is_reg_wire = is_reg_wire(cell->getPort("\\Q"), reg_name);
+		bool out_is_reg_wire = is_reg_wire(cell->getPort(ID::Q), reg_name);
 
 		if (!out_is_reg_wire) {
-			f << stringf("%s" "reg [%d:0] %s", indent.c_str(), cell->parameters["\\WIDTH"].as_int()-1, reg_name.c_str());
-			dump_reg_init(f, cell->getPort("\\Q"));
+			f << stringf("%s" "reg [%d:0] %s", indent.c_str(), cell->parameters[ID::WIDTH].as_int()-1, reg_name.c_str());
+			dump_reg_init(f, cell->getPort(ID::Q));
 			f << ";\n";
 		}
 
@@ -1044,22 +1044,22 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 
 		if (!out_is_reg_wire) {
 			f << stringf("%s" "assign ", indent.c_str());
-			dump_sigspec(f, cell->getPort("\\Q"));
+			dump_sigspec(f, cell->getPort(ID::Q));
 			f << stringf(" = %s;\n", reg_name.c_str());
 		}
 
 		return true;
 	}
 
-	if (cell->type == "$mem")
+	if (cell->type == ID($mem))
 	{
-		RTLIL::IdString memid = cell->parameters["\\MEMID"].decode_string();
-		std::string mem_id = id(cell->parameters["\\MEMID"].decode_string());
-		int abits = cell->parameters["\\ABITS"].as_int();
-		int size = cell->parameters["\\SIZE"].as_int();
-		int offset = cell->parameters["\\OFFSET"].as_int();
-		int width = cell->parameters["\\WIDTH"].as_int();
-		bool use_init = !(RTLIL::SigSpec(cell->parameters["\\INIT"]).is_fully_undef());
+		RTLIL::IdString memid = cell->parameters[ID::MEMID].decode_string();
+		std::string mem_id = id(cell->parameters[ID::MEMID].decode_string());
+		int abits = cell->parameters[ID::ABITS].as_int();
+		int size = cell->parameters[ID::SIZE].as_int();
+		int offset = cell->parameters[ID::OFFSET].as_int();
+		int width = cell->parameters[ID::WIDTH].as_int();
+		bool use_init = !(RTLIL::SigSpec(cell->parameters[ID::INIT]).is_fully_undef());
 
 		// for memory block make something like:
 		//  reg [7:0] memid [3:0];
@@ -1099,7 +1099,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 				{
 					for (int i=0; i<size; i++)
 					{
-						RTLIL::Const element = cell->parameters["\\INIT"].extract(i*width, width);
+						RTLIL::Const element = cell->parameters[ID::INIT].extract(i*width, width);
 						for (int j=0; j<element.size(); j++)
 						{
 							switch (element[element.size()-j-1])
@@ -1123,7 +1123,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 				for (int i=0; i<size; i++)
 				{
 					f << stringf("%s" "  %s[%d] = ", indent.c_str(), mem_id.c_str(), i);
-					dump_const(f, cell->parameters["\\INIT"].extract(i*width, width));
+					dump_const(f, cell->parameters[ID::INIT].extract(i*width, width));
 					f << stringf(";\n");
 				}
 				f << stringf("%s" "end\n", indent.c_str());
@@ -1137,19 +1137,19 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		// create a list of reg declarations
 		std::vector<std::string> lof_reg_declarations;
 
-		int nread_ports = cell->parameters["\\RD_PORTS"].as_int();
+		int nread_ports = cell->parameters[ID::RD_PORTS].as_int();
 		RTLIL::SigSpec sig_rd_clk, sig_rd_en, sig_rd_data, sig_rd_addr;
 		bool use_rd_clk, rd_clk_posedge, rd_transparent;
 		// read ports
 		for (int i=0; i < nread_ports; i++)
 		{
-			sig_rd_clk = cell->getPort("\\RD_CLK").extract(i);
-			sig_rd_en = cell->getPort("\\RD_EN").extract(i);
-			sig_rd_data = cell->getPort("\\RD_DATA").extract(i*width, width);
-			sig_rd_addr = cell->getPort("\\RD_ADDR").extract(i*abits, abits);
-			use_rd_clk = cell->parameters["\\RD_CLK_ENABLE"].extract(i).as_bool();
-			rd_clk_posedge = cell->parameters["\\RD_CLK_POLARITY"].extract(i).as_bool();
-			rd_transparent = cell->parameters["\\RD_TRANSPARENT"].extract(i).as_bool();
+			sig_rd_clk = cell->getPort(ID::RD_CLK).extract(i);
+			sig_rd_en = cell->getPort(ID::RD_EN).extract(i);
+			sig_rd_data = cell->getPort(ID::RD_DATA).extract(i*width, width);
+			sig_rd_addr = cell->getPort(ID::RD_ADDR).extract(i*abits, abits);
+			use_rd_clk = cell->parameters[ID::RD_CLK_ENABLE].extract(i).as_bool();
+			rd_clk_posedge = cell->parameters[ID::RD_CLK_POLARITY].extract(i).as_bool();
+			rd_transparent = cell->parameters[ID::RD_TRANSPARENT].extract(i).as_bool();
 			if (use_rd_clk)
 			{
 				{
@@ -1221,18 +1221,18 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 			}
 		}
 
-		int nwrite_ports = cell->parameters["\\WR_PORTS"].as_int();
+		int nwrite_ports = cell->parameters[ID::WR_PORTS].as_int();
 		RTLIL::SigSpec sig_wr_clk, sig_wr_data, sig_wr_addr, sig_wr_en;
 		bool wr_clk_posedge;
 
 		// write ports
 		for (int i=0; i < nwrite_ports; i++)
 		{
-			sig_wr_clk = cell->getPort("\\WR_CLK").extract(i);
-			sig_wr_data = cell->getPort("\\WR_DATA").extract(i*width, width);
-			sig_wr_addr = cell->getPort("\\WR_ADDR").extract(i*abits, abits);
-			sig_wr_en = cell->getPort("\\WR_EN").extract(i*width, width);
-			wr_clk_posedge = cell->parameters["\\WR_CLK_POLARITY"].extract(i).as_bool();
+			sig_wr_clk = cell->getPort(ID::WR_CLK).extract(i);
+			sig_wr_data = cell->getPort(ID::WR_DATA).extract(i*width, width);
+			sig_wr_addr = cell->getPort(ID::WR_ADDR).extract(i*abits, abits);
+			sig_wr_en = cell->getPort(ID::WR_EN).extract(i*width, width);
+			wr_clk_posedge = cell->parameters[ID::WR_CLK_POLARITY].extract(i).as_bool();
 			{
 				std::ostringstream os;
 				dump_sigspec(os, sig_wr_clk);
@@ -1319,66 +1319,66 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
-	if (cell->type.in("$assert", "$assume", "$cover"))
+	if (cell->type.in(ID($assert), ID($assume), ID($cover)))
 	{
 		f << stringf("%s" "always @* if (", indent.c_str());
-		dump_sigspec(f, cell->getPort("\\EN"));
+		dump_sigspec(f, cell->getPort(ID::EN));
 		f << stringf(") %s(", cell->type.c_str()+1);
-		dump_sigspec(f, cell->getPort("\\A"));
+		dump_sigspec(f, cell->getPort(ID::A));
 		f << stringf(");\n");
 		return true;
 	}
 
-	if (cell->type.in("$specify2", "$specify3"))
+	if (cell->type.in(ID($specify2), ID($specify3)))
 	{
 		f << stringf("%s" "specify\n%s  ", indent.c_str(), indent.c_str());
 
-		SigSpec en = cell->getPort("\\EN");
+		SigSpec en = cell->getPort(ID::EN);
 		if (en != State::S1) {
 			f << stringf("if (");
-			dump_sigspec(f, cell->getPort("\\EN"));
+			dump_sigspec(f, cell->getPort(ID::EN));
 			f << stringf(") ");
 		}
 
 		f << "(";
-		if (cell->type == "$specify3" && cell->getParam("\\EDGE_EN").as_bool())
-			f << (cell->getParam("\\EDGE_POL").as_bool() ? "posedge ": "negedge ");
+		if (cell->type == ID($specify3) && cell->getParam(ID::EDGE_EN).as_bool())
+			f << (cell->getParam(ID::EDGE_POL).as_bool() ? "posedge ": "negedge ");
 
-		dump_sigspec(f, cell->getPort("\\SRC"));
+		dump_sigspec(f, cell->getPort(ID::SRC));
 
 		f << " ";
-		if (cell->getParam("\\SRC_DST_PEN").as_bool())
-			f << (cell->getParam("\\SRC_DST_POL").as_bool() ? "+": "-");
-		f << (cell->getParam("\\FULL").as_bool() ? "*> ": "=> ");
+		if (cell->getParam(ID::SRC_DST_PEN).as_bool())
+			f << (cell->getParam(ID::SRC_DST_POL).as_bool() ? "+": "-");
+		f << (cell->getParam(ID::FULL).as_bool() ? "*> ": "=> ");
 
-		if (cell->type == "$specify3") {
+		if (cell->type == ID($specify3)) {
 			f << "(";
-			dump_sigspec(f, cell->getPort("\\DST"));
+			dump_sigspec(f, cell->getPort(ID::DST));
 			f << " ";
-			if (cell->getParam("\\DAT_DST_PEN").as_bool())
-				f << (cell->getParam("\\DAT_DST_POL").as_bool() ? "+": "-");
+			if (cell->getParam(ID::DAT_DST_PEN).as_bool())
+				f << (cell->getParam(ID::DAT_DST_POL).as_bool() ? "+": "-");
 			f << ": ";
-			dump_sigspec(f, cell->getPort("\\DAT"));
+			dump_sigspec(f, cell->getPort(ID::DAT));
 			f << ")";
 		} else {
-			dump_sigspec(f, cell->getPort("\\DST"));
+			dump_sigspec(f, cell->getPort(ID::DST));
 		}
 
 		bool bak_decimal = decimal;
 		decimal = 1;
 
 		f << ") = (";
-		dump_const(f, cell->getParam("\\T_RISE_MIN"));
+		dump_const(f, cell->getParam(ID::T_RISE_MIN));
 		f << ":";
-		dump_const(f, cell->getParam("\\T_RISE_TYP"));
+		dump_const(f, cell->getParam(ID::T_RISE_TYP));
 		f << ":";
-		dump_const(f, cell->getParam("\\T_RISE_MAX"));
+		dump_const(f, cell->getParam(ID::T_RISE_MAX));
 		f << ", ";
-		dump_const(f, cell->getParam("\\T_FALL_MIN"));
+		dump_const(f, cell->getParam(ID::T_FALL_MIN));
 		f << ":";
-		dump_const(f, cell->getParam("\\T_FALL_TYP"));
+		dump_const(f, cell->getParam(ID::T_FALL_TYP));
 		f << ":";
-		dump_const(f, cell->getParam("\\T_FALL_MAX"));
+		dump_const(f, cell->getParam(ID::T_FALL_MAX));
 		f << ");\n";
 
 		decimal = bak_decimal;
@@ -1387,49 +1387,49 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
-	if (cell->type == "$specrule")
+	if (cell->type == ID($specrule))
 	{
 		f << stringf("%s" "specify\n%s  ", indent.c_str(), indent.c_str());
 
-		string spec_type = cell->getParam("\\TYPE").decode_string();
+		IdString spec_type = cell->getParam(ID::TYPE).decode_string();
 		f << stringf("%s(", spec_type.c_str());
 
-		if (cell->getParam("\\SRC_PEN").as_bool())
-			f << (cell->getParam("\\SRC_POL").as_bool() ? "posedge ": "negedge ");
-		dump_sigspec(f, cell->getPort("\\SRC"));
+		if (cell->getParam(ID::SRC_PEN).as_bool())
+			f << (cell->getParam(ID::SRC_POL).as_bool() ? "posedge ": "negedge ");
+		dump_sigspec(f, cell->getPort(ID::SRC));
 
-		if (cell->getPort("\\SRC_EN") != State::S1) {
+		if (cell->getPort(ID::SRC_EN) != State::S1) {
 			f << " &&& ";
-			dump_sigspec(f, cell->getPort("\\SRC_EN"));
+			dump_sigspec(f, cell->getPort(ID::SRC_EN));
 		}
 
 		f << ", ";
-		if (cell->getParam("\\DST_PEN").as_bool())
-			f << (cell->getParam("\\DST_POL").as_bool() ? "posedge ": "negedge ");
-		dump_sigspec(f, cell->getPort("\\DST"));
+		if (cell->getParam(ID::DST_PEN).as_bool())
+			f << (cell->getParam(ID::DST_POL).as_bool() ? "posedge ": "negedge ");
+		dump_sigspec(f, cell->getPort(ID::DST));
 
-		if (cell->getPort("\\DST_EN") != State::S1) {
+		if (cell->getPort(ID::DST_EN) != State::S1) {
 			f << " &&& ";
-			dump_sigspec(f, cell->getPort("\\DST_EN"));
+			dump_sigspec(f, cell->getPort(ID::DST_EN));
 		}
 
 		bool bak_decimal = decimal;
 		decimal = 1;
 
 		f << ", ";
-		dump_const(f, cell->getParam("\\T_LIMIT_MIN"));
+		dump_const(f, cell->getParam(ID::T_LIMIT_MIN));
 		f << ": ";
-		dump_const(f, cell->getParam("\\T_LIMIT_TYP"));
+		dump_const(f, cell->getParam(ID::T_LIMIT_TYP));
 		f << ": ";
-		dump_const(f, cell->getParam("\\T_LIMIT_MAX"));
+		dump_const(f, cell->getParam(ID::T_LIMIT_MAX));
 
-		if (spec_type == "$setuphold" || spec_type == "$recrem" || spec_type == "$fullskew") {
+		if (spec_type.in(ID($setuphold), ID($recrem), ID($fullskew))) {
 			f << ", ";
-			dump_const(f, cell->getParam("\\T_LIMIT2_MIN"));
+			dump_const(f, cell->getParam(ID::T_LIMIT2_MIN));
 			f << ": ";
-			dump_const(f, cell->getParam("\\T_LIMIT2_TYP"));
+			dump_const(f, cell->getParam(ID::T_LIMIT2_TYP));
 			f << ": ";
-			dump_const(f, cell->getParam("\\T_LIMIT2_MAX"));
+			dump_const(f, cell->getParam(ID::T_LIMIT2_MAX));
 		}
 
 		f << ");\n";
@@ -1513,9 +1513,9 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		}
 	}
 
-	if (siminit && reg_ct.count(cell->type) && cell->hasPort("\\Q")) {
+	if (siminit && reg_ct.count(cell->type) && cell->hasPort(ID::Q)) {
 		std::stringstream ss;
-		dump_reg_init(ss, cell->getPort("\\Q"));
+		dump_reg_init(ss, cell->getPort(ID::Q));
 		if (!ss.str().empty()) {
 			f << stringf("%sinitial %s.Q", indent.c_str(), cell_name.c_str());
 			f << ss.str();
@@ -1698,9 +1698,9 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 	active_initdata.clear();
 
 	for (auto wire : module->wires())
-		if (wire->attributes.count("\\init")) {
+		if (wire->attributes.count(ID::init)) {
 			SigSpec sig = active_sigmap(wire);
-			Const val = wire->attributes.at("\\init");
+			Const val = wire->attributes.at(ID::init);
 			for (int i = 0; i < GetSize(sig) && i < GetSize(val); i++)
 				if (val[i] == State::S0 || val[i] == State::S1)
 					active_initdata[sig[i]] = val[i];
@@ -1719,13 +1719,12 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 	if (!noexpr)
 	{
 		std::set<std::pair<RTLIL::Wire*,int>> reg_bits;
-		for (auto &it : module->cells_)
+		for (auto cell : module->cells())
 		{
-			RTLIL::Cell *cell = it.second;
-			if (!reg_ct.count(cell->type) || !cell->hasPort("\\Q"))
+			if (!reg_ct.count(cell->type) || !cell->hasPort(ID::Q))
 				continue;
 
-			RTLIL::SigSpec sig = cell->getPort("\\Q");
+			RTLIL::SigSpec sig = cell->getPort(ID::Q);
 
 			if (sig.is_chunk()) {
 				RTLIL::SigChunk chunk = sig.as_chunk();
@@ -1734,9 +1733,8 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 						reg_bits.insert(std::pair<RTLIL::Wire*,int>(chunk.wire, chunk.offset+i));
 			}
 		}
-		for (auto &it : module->wires_)
+		for (auto wire : module->wires())
 		{
-			RTLIL::Wire *wire = it.second;
 			for (int i = 0; i < wire->width; i++)
 				if (reg_bits.count(std::pair<RTLIL::Wire*,int>(wire, i)) == 0)
 					goto this_wire_aint_reg;
@@ -1751,8 +1749,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 	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) {
-			RTLIL::Wire *wire = it->second;
+		for (auto wire : module->wires()) {
 			if (wire->port_id == port_id) {
 				if (port_id != 1)
 					f << stringf(", ");
@@ -1764,14 +1761,14 @@ 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)
-		dump_wire(f, indent + "  ", it->second);
+	for (auto w : module->wires())
+		dump_wire(f, indent + "  ", w);
 
 	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)
-		dump_cell(f, indent + "  ", it->second);
+	for (auto cell : module->cells())
+		dump_cell(f, indent + "  ", cell);
 
 	for (auto it = module->processes.begin(); it != module->processes.end(); ++it)
 		dump_process(f, indent + "  ", it->second);
@@ -1892,31 +1889,31 @@ struct VerilogBackend : public Backend {
 		reg_wires.clear();
 		reg_ct.clear();
 
-		reg_ct.insert("$dff");
-		reg_ct.insert("$adff");
-		reg_ct.insert("$dffe");
-		reg_ct.insert("$dlatch");
-
-		reg_ct.insert("$_DFF_N_");
-		reg_ct.insert("$_DFF_P_");
-
-		reg_ct.insert("$_DFF_NN0_");
-		reg_ct.insert("$_DFF_NN1_");
-		reg_ct.insert("$_DFF_NP0_");
-		reg_ct.insert("$_DFF_NP1_");
-		reg_ct.insert("$_DFF_PN0_");
-		reg_ct.insert("$_DFF_PN1_");
-		reg_ct.insert("$_DFF_PP0_");
-		reg_ct.insert("$_DFF_PP1_");
-
-		reg_ct.insert("$_DFFSR_NNN_");
-		reg_ct.insert("$_DFFSR_NNP_");
-		reg_ct.insert("$_DFFSR_NPN_");
-		reg_ct.insert("$_DFFSR_NPP_");
-		reg_ct.insert("$_DFFSR_PNN_");
-		reg_ct.insert("$_DFFSR_PNP_");
-		reg_ct.insert("$_DFFSR_PPN_");
-		reg_ct.insert("$_DFFSR_PPP_");
+		reg_ct.insert(ID($dff));
+		reg_ct.insert(ID($adff));
+		reg_ct.insert(ID($dffe));
+		reg_ct.insert(ID($dlatch));
+
+		reg_ct.insert(ID($_DFF_N_));
+		reg_ct.insert(ID($_DFF_P_));
+
+		reg_ct.insert(ID($_DFF_NN0_));
+		reg_ct.insert(ID($_DFF_NN1_));
+		reg_ct.insert(ID($_DFF_NP0_));
+		reg_ct.insert(ID($_DFF_NP1_));
+		reg_ct.insert(ID($_DFF_PN0_));
+		reg_ct.insert(ID($_DFF_PN1_));
+		reg_ct.insert(ID($_DFF_PP0_));
+		reg_ct.insert(ID($_DFF_PP1_));
+
+		reg_ct.insert(ID($_DFFSR_NNN_));
+		reg_ct.insert(ID($_DFFSR_NNP_));
+		reg_ct.insert(ID($_DFFSR_NPN_));
+		reg_ct.insert(ID($_DFFSR_NPP_));
+		reg_ct.insert(ID($_DFFSR_PNN_));
+		reg_ct.insert(ID($_DFFSR_PNP_));
+		reg_ct.insert(ID($_DFFSR_PPN_));
+		reg_ct.insert(ID($_DFFSR_PPP_));
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++) {
@@ -1995,16 +1992,16 @@ struct VerilogBackend : public Backend {
 		design->sort();
 
 		*f << stringf("/* Generated by %s */\n", yosys_version_str);
-		for (auto it = design->modules_.begin(); it != design->modules_.end(); ++it) {
-			if (it->second->get_blackbox_attribute() != blackboxes)
+		for (auto module : design->modules()) {
+			if (module->get_blackbox_attribute() != blackboxes)
 				continue;
-			if (selected && !design->selected_whole_module(it->first)) {
-				if (design->selected_module(it->first))
-					log_cmd_error("Can't handle partially selected module %s!\n", RTLIL::id2cstr(it->first));
+			if (selected && !design->selected_whole_module(module->name)) {
+				if (design->selected_module(module->name))
+					log_cmd_error("Can't handle partially selected module %s!\n", log_id(module->name));
 				continue;
 			}
-			log("Dumping module `%s'.\n", it->first.c_str());
-			dump_module(*f, "", it->second);
+			log("Dumping module `%s'.\n", module->name.c_str());
+			dump_module(*f, "", module);
 		}
 
 		auto_name_map.clear();