abc9: perform name preservation

backends/aiger/xaiger.cc

@@ -683,6 +683,7 @@ struct XAigerWriter
 	{
 		dict<int, string> input_lines;
 		dict<int, string> output_lines;
+		dict<int, string> node_lines;
 
 		for (auto wire : module->wires())
 		{
@@ -702,6 +703,14 @@ struct XAigerWriter
 			}
 		}
 
+		for (auto &it : aig_map) {
+			auto bit = it.first;
+			auto node = it.second;
+			if (bit.wire == nullptr || input_bits.count(bit) || output_bits.count(bit))
+				continue;
+			node_lines[node] += stringf("node %d %d %s\n", node - 2, bit.wire->start_offset + bit.offset, log_id(bit.wire));
+		}
+
 		input_lines.sort();
 		for (auto &it : input_lines)
 			f << it.second;
@@ -711,6 +720,10 @@ struct XAigerWriter
 		for (auto cell : box_list)
 			f << stringf("box %d %d %s\n", box_count++, 0, log_id(cell->name));
 
+		node_lines.sort();
+		for (auto &it : node_lines)
+			f << it.second;
+
 		output_lines.sort();
 		for (auto &it : output_lines)
 			f << it.second;

frontends/aiger/aigerparse.cc

@@ -907,6 +907,9 @@ void AigerReader::post_process()
 					log_debug("Box %d (%s) no longer exists.\n", variable, log_id(escaped_s));
 				else
 					module->rename(cell, escaped_s);
+			}
+			else if (type == "node") {
+				
 			}
 			else
 				log_error("Symbol type '%s' not recognised.\n", type);

passes/techmap/abc9_exe.cc

@@ -248,11 +248,11 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe
 	}
 
 	abc9_script += stringf("; &ps -l; &write -n %s/output.aig", tempdir_name);
-	if (design->scratchpad_get_bool("abc9.verify")) {
+	if (design->scratchpad_get_bool("abc9.verify", true)) {
 		if (dff_mode)
 			abc9_script += "; &verify -s";
 		else
-			abc9_script += "; &verify";
+			abc9_script += "; &verify -y";
 	}
 	abc9_script += "; time";
 	abc9_script = add_echos_to_abc9_cmd(abc9_script);

passes/techmap/aigmap.cc

@@ -17,8 +17,11 @@
  *
  */
 
+#include "kernel/rtlil.h"
 #include "kernel/yosys.h"
 #include "kernel/cellaigs.h"
+#include "kernel/yosys_common.h"
+#include <sstream>
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
@@ -93,6 +96,7 @@ struct AigmapPass : public Pass {
 
 				vector<SigBit> sigs;
 				dict<pair<int, int>, SigBit> and_cache;
+				dict<pair<int, int>, SigBit> not_cache;
 
 				for (int node_idx = 0; node_idx < GetSize(aig.nodes); node_idx++)
 				{
@@ -119,21 +123,37 @@ struct AigmapPass : public Pass {
 							if (and_cache.count(key))
 								bit = and_cache.at(key);
 							else {
-								bit = module->addWire(NEW_ID);
+								std::stringstream ss;
+								ss << log_id(cell->name) << "$" << node_idx;
+								bit = module->addWire(IdString(ss.str()));
 								auto gate = module->addAndGate(NEW_ID, A, B, bit);
 								if (select_mode)
 									new_sel.insert(gate->name);
+								and_cache.insert({key, bit});
 							}
 						}
 					}
 
 					if (node.inverter) {
-						SigBit new_bit = module->addWire(NEW_ID);
+						pair<int, int> key(node.left_parent, node.right_parent);
-						auto gate = module->addNotGate(NEW_ID, bit, new_bit);
+						if (not_cache.count(key))
-						bit = new_bit;
+							bit = not_cache.at(key);
-						if (select_mode)
+						else {
-							new_sel.insert(gate->name);
+							IdString name;
-
+							if (bit.wire != nullptr) {
+								std::stringstream ss;
+								ss << "\\~" << log_id(bit.wire) << "[" << bit.offset << "]" << "$" << (autoidx++);
+								name = IdString(ss.str());
+							} else {
+								name = NEW_ID;
+							}
+							SigBit new_bit = module->addWire(name);
+							auto gate = module->addNotGate(NEW_ID, bit, new_bit);
+							bit = new_bit;
+							if (select_mode)
+								new_sel.insert(gate->name);
+							not_cache.insert({key, bit});
+						}
 					}
 
 				skip_inverter: