Preserve \src attributes through ABC9 via XAIGER "y" extension

Use ABC's &verify -y mechanism to compute output-to-input object
equivalence mappings during optimization. The XAIGER writer emits
a "y" identity extension and src map entries in the map file. After
ABC optimizes and rewrites the AIG, the XAIGER readers use the "y"
mapping to trace output objects back to input objects, recovering
the original \src attributes for mapped LUT cells.

Changes:
- xaiger writer: emit "y" identity extension + "src" map file entries
- abc9_exe: use &verify -y (combinational) + second &write
- aiger/aiger2 readers: parse "y" extension + src map, apply \src
- aigmap: propagate \src to AND/NOT/NAND gates during AIG mapping

Enabled via: scratchpad -set abc9.verify true

Co-developed-by: Claude Code v2.1.44 (claude-opus-4-6)

Author: robtaylor

backends/aiger/xaiger.cc

@@ -63,6 +63,12 @@ struct XAigerWriter
 
 	vector<Cell*> box_list;
 
+	// Track which cell produced each AND-map or CI entry (for \src propagation)
+	dict<SigBit, Cell*> and_cell;
+	dict<SigBit, Cell*> ci_cell;
+	// Track \src strings for AIG objects (by object ID)
+	dict<int, std::string> aig_obj_src;
+
 	int mkgate(int a0, int a1)
 	{
 		aig_m++, aig_a++;
@@ -108,6 +114,13 @@ struct XAigerWriter
 			int a0 = bit2aig(args.first);
 			int a1 = bit2aig(args.second);
 			a = mkgate(a0, a1);
+			// Record \src for this AIG object if the source cell has one
+			auto cell_it = and_cell.find(bit);
+			if (cell_it != and_cell.end()) {
+				auto src = cell_it->second->get_string_attribute(ID::src);
+				if (!src.empty())
+					aig_obj_src[a >> 1] = src;
+			}
 		} else
 		if (alias_map.count(bit)) {
 			a = bit2aig(alias_map.at(bit));
@@ -207,6 +220,7 @@ struct XAigerWriter
 					unused_bits.erase(B);
 					undriven_bits.erase(Y);
 					and_map[Y] = make_pair(A, B);
+					and_cell[Y] = cell;
 					continue;
 				}
 
@@ -373,6 +387,7 @@ struct XAigerWriter
 						if (O != b)
 							alias_map[O] = b;
 						ci_bits.emplace_back(b);
+						ci_cell[b] = cell;
 						undriven_bits.erase(O);
 					}
 			}
@@ -425,6 +440,13 @@ struct XAigerWriter
 			if (aig_map.count(bit))
 				log_error("Visited AIG node more than once; this could be a combinatorial loop that has not been broken\n");
 			aig_map[bit] = 2*aig_m;
+			// Record \src for box CI objects
+			auto ci_it = ci_cell.find(bit);
+			if (ci_it != ci_cell.end()) {
+				auto src = ci_it->second->get_string_attribute(ID::src);
+				if (!src.empty())
+					aig_obj_src[aig_m] = src;
+			}
 		}
 
 		for (auto bit : co_bits) {
@@ -671,6 +693,20 @@ struct XAigerWriter
 		//f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
 		//f.write(buffer_str.data(), buffer_str.size());
 
+		// Write "y" extension: identity mapping for \src preservation
+		// ABC's &verify -y will use this to map output objects back to input objects
+		{
+			int n_objs = aig_m + 1;  // objects 0 through aig_m
+			f << "y";
+			write_buffer(f, 4 * n_objs);  // length in bytes (BE32)
+			for (int i = 0; i < n_objs; i++) {
+				// Identity mapping: each object maps to itself (literal = 2*i)
+				// Written as native-endian 32-bit int (matches ABC's fwrite of Vec_IntArray)
+				uint32_t lit = 2 * i;
+				f.write(reinterpret_cast<const char*>(&lit), sizeof(lit));
+			}
+		}
+
 		f << stringf("Generated by %s\n", yosys_maybe_version());
 
 		design->scratchpad_set_int("write_xaiger.num_ands", and_map.size());
@@ -715,6 +751,10 @@ struct XAigerWriter
 		for (auto &it : output_lines)
 			f << it.second;
 		log_assert(output_lines.size() == output_bits.size());
+
+		// Write src lines mapping AIG object IDs to \src attribute values
+		for (auto &it : aig_obj_src)
+			f << stringf("src %d %s\n", it.first, it.second.c_str());
 	}
 };
 

frontends/aiger/aigerparse.cc

@@ -458,7 +458,9 @@ void AigerReader::parse_xaiger()
 				RTLIL::Cell *output_cell = module->cell(stringf("$and$aiger%d$%d", aiger_autoidx, rootNodeID));
 				log_assert(output_cell);
 				module->remove(output_cell);
-				module->addLut(stringf("$lut$aiger%d$%d", aiger_autoidx, rootNodeID), input_sig, output_sig, std::move(lut_mask));
+				auto *lut = module->addLut(stringf("$lut$aiger%d$%d", aiger_autoidx, rootNodeID), input_sig, output_sig, std::move(lut_mask));
+				// Track for \src application via "y" mapping
+				lut_by_obj[rootNodeID] = lut;
 			}
 		}
 		else if (c == 'r') {
@@ -510,6 +512,14 @@ void AigerReader::parse_xaiger()
 				boxes.emplace_back(cell);
 			}
 		}
+		else if (c == 'y') {
+			uint32_t dataSize = parse_xaiger_literal(f);
+			uint32_t n_entries = dataSize / 4;
+			log_debug("y: dataSize=%u n_entries=%u\n", dataSize, n_entries);
+			equiv_lit_ids.resize(n_entries);
+			// Data is written as native-endian 32-bit ints by ABC
+			f.read(reinterpret_cast<char*>(equiv_lit_ids.data()), dataSize);
+		}
 		else if (c == 'a' || c == 'i' || c == 'o' || c == 's') {
 			uint32_t dataSize = parse_xaiger_literal(f);
 			f.ignore(dataSize);
@@ -810,11 +820,29 @@ void AigerReader::post_process()
 
 	dict<RTLIL::IdString, std::pair<int,int>> wideports_cache;
 
+	// Map from input AIG object ID to \src attribute value
+	dict<int, std::string> obj_src;
+
 	if (!map_filename.empty()) {
 		std::ifstream mf(map_filename);
 		std::string type, symbol;
 		int variable, index;
-		while (mf >> type >> variable >> index >> symbol) {
+		while (mf >> type) {
+			if (type == "src") {
+				// Parse src lines: "src <obj_id> <src_value>"
+				int obj_id;
+				std::string src_value;
+				if (!(mf >> obj_id))
+					log_error("Bad map file: malformed src line\n");
+				std::getline(mf, src_value);
+				// Trim leading whitespace
+				size_t start = src_value.find_first_not_of(" \t");
+				if (start != std::string::npos)
+					obj_src[obj_id] = src_value.substr(start);
+				continue;
+			}
+			if (!(mf >> variable >> index >> symbol))
+				break;
 			RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
 			if (type == "input") {
 				log_assert(static_cast<unsigned>(variable) < inputs.size());
@@ -983,6 +1011,28 @@ void AigerReader::post_process()
 		else
 			module->rename(cell, stringf("$lut%s[%d]", y_port.wire->name, y_port.offset));
 	}
+
+	// Apply \src attributes using "y" extension equivalence mapping
+	if (!equiv_lit_ids.empty() && !obj_src.empty()) {
+		int applied = 0;
+		for (auto &[obj_id, lut] : lut_by_obj) {
+			if (obj_id < 0 || obj_id >= (int) equiv_lit_ids.size())
+				continue;
+			int32_t equiv_lit = equiv_lit_ids[obj_id];
+			if (equiv_lit < 0)
+				continue;
+			int input_obj = equiv_lit >> 1;
+			auto src_it = obj_src.find(input_obj);
+			if (src_it != obj_src.end()) {
+				lut->set_string_attribute(ID::src, src_it->second);
+				applied++;
+				log_debug("Applied \\src '%s' to cell %s (obj %d -> input obj %d)\n",
+						  src_it->second.c_str(), log_id(lut), obj_id, input_obj);
+			}
+		}
+		if (applied > 0)
+			log("Applied \\src attributes to %d cells via equivalence mapping.\n", applied);
+	}
 }
 
 struct AigerFrontend : public Frontend {

frontends/aiger/aigerparse.h

@@ -46,6 +46,8 @@ struct AigerReader
     std::vector<RTLIL::Wire*> bad_properties;
     std::vector<RTLIL::Cell*> boxes;
     std::vector<int> mergeability, initial_state;
+    std::vector<int32_t> equiv_lit_ids;
+    dict<int, RTLIL::Cell*> lut_by_obj;
 
     AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name, std::string map_filename, bool wideports);
     void parse_aiger();

frontends/aiger2/xaiger.cc

@@ -121,6 +121,9 @@ struct Xaiger2Frontend : public Frontend {
 		bits[0] = RTLIL::S0;
 		bits[1] = RTLIL::S1;
 
+		// Map from input AIG object ID to \src attribute value
+		dict<int, std::string> obj_src;
+
 		std::string type;
 		while (map_file >> type) {
 			if (type == "pi") {
@@ -165,6 +168,16 @@ struct Xaiger2Frontend : public Frontend {
 					retained_boxes.resize(box_seq + 1);
 				}
 				boxes[box_seq] = std::make_pair(box, def);
+			} else if (type == "src") {
+				int obj_id;
+				std::string src_value;
+				if (!(map_file >> obj_id))
+					log_error("Bad map file (30)\n");
+				std::getline(map_file, src_value);
+				// Trim leading whitespace
+				size_t start = src_value.find_first_not_of(" \t");
+				if (start != std::string::npos)
+					obj_src[obj_id] = src_value.substr(start);
 			} else {
 				std::string scratch;
 				std::getline(map_file, scratch);
@@ -248,6 +261,9 @@ struct Xaiger2Frontend : public Frontend {
 
 		log_debug("reading 'M' (second pass)\n");
 
+		// Track output literal → Cell* for \src application
+		dict<uint32_t, Cell*> lit_to_instance;
+
 		f->seekg(extensions_start);
 		bool read_mapping = false;
 		uint32_t no_cells, no_instances;
@@ -294,6 +310,7 @@ struct Xaiger2Frontend : public Frontend {
 					auto out_w = module->addWire(module->uniquify(stringf("$lit%d", out_lit)));
 					instance->setPort(cell.out, out_w);
 					bits[out_lit] = out_w;
+					lit_to_instance[out_lit] = instance;
 					for (auto in : cell.ins) {
 						uint32_t in_lit = read_be32(*f);
 						log_assert(out_lit < bits.size());
@@ -318,6 +335,49 @@ struct Xaiger2Frontend : public Frontend {
 		log("Read %d instances with cell library of size %d.\n",
 			no_instances, no_cells);
 
+		// Read 'y' extension (equivalence literal IDs from &verify -y)
+		// and apply \src attributes to mapped cells
+		f->seekg(extensions_start);
+		log_debug("reading 'y' (third pass)\n");
+		for (int c = f->get(); c != EOF; c = f->get()) {
+			if (c == 'y') {
+				uint32_t len = read_be32(*f);
+				uint32_t n_entries = len / 4;
+				log_debug("y: len=%u n_entries=%u\n", len, n_entries);
+
+				std::vector<int32_t> equiv_lit_ids(n_entries);
+				// Data is written as native-endian 32-bit ints by ABC
+				f->read(reinterpret_cast<char*>(equiv_lit_ids.data()), len);
+
+				// Apply \src: for each mapped cell, look up its equivalent
+				// input object via the "y" mapping, then look up the \src
+				// from the input map file
+				for (auto &[out_lit, instance] : lit_to_instance) {
+					uint32_t out_obj = out_lit >> 1;
+					if (out_obj >= n_entries)
+						continue;
+					int32_t equiv_lit = equiv_lit_ids[out_obj];
+					if (equiv_lit < 0)
+						continue;  // no mapping for this object
+					int input_obj = equiv_lit >> 1;
+					auto src_it = obj_src.find(input_obj);
+					if (src_it != obj_src.end()) {
+						instance->set_string_attribute(ID::src, src_it->second);
+						log_debug("  applied \\src '%s' to cell %s (out_obj=%d -> input_obj=%d)\n",
+								  src_it->second.c_str(), log_id(instance), out_obj, input_obj);
+					}
+				}
+				break;
+			} else if (c == '\n') {
+				break;
+			} else if (c == 'c') {
+				break;
+			} else {
+				uint32_t len = read_be32(*f);
+				f->ignore(len);
+			}
+		}
+
 		f->seekg(extensions_start);
 		log_debug("reading 'h' (second pass)\n");
 		int co_counter = 0;

passes/techmap/abc9_exe.cc

@@ -248,11 +248,14 @@ 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", true)) {
-		if (dff_mode)
+	if (design->scratchpad_get_bool("abc9.verify")) {
+		if (dff_mode) {
 			abc9_script += "; &verify -s";
-		else
-			abc9_script += "; &verify";
+		} else {
+			abc9_script += "; &verify -y";
+			// Rewrite output to include "y" extension from verification
+			abc9_script += stringf("; &write -n %s/output.aig", tempdir_name);
+		}
 	}
 	abc9_script += "; time";
 	abc9_script = add_echos_to_abc9_cmd(abc9_script);

passes/techmap/aigmap.cc

@@ -110,6 +110,7 @@ struct AigmapPass : public Pass {
 						if (nand_mode && node.inverter) {
 							bit = module->addWire(NEW_ID);
 							auto gate = module->addNandGate(NEW_ID, A, B, bit);
+							gate->set_src_attribute(cell->get_src_attribute());
 							if (select_mode)
 								new_sel.insert(gate->name);
 
@@ -121,6 +122,7 @@ struct AigmapPass : public Pass {
 							else {
 								bit = module->addWire(NEW_ID);
 								auto gate = module->addAndGate(NEW_ID, A, B, bit);
+								gate->set_src_attribute(cell->get_src_attribute());
 								if (select_mode)
 									new_sel.insert(gate->name);
 							}
@@ -130,6 +132,7 @@ struct AigmapPass : public Pass {
 					if (node.inverter) {
 						SigBit new_bit = module->addWire(NEW_ID);
 						auto gate = module->addNotGate(NEW_ID, bit, new_bit);
+						gate->set_src_attribute(cell->get_src_attribute());
 						bit = new_bit;
 						if (select_mode)
 							new_sel.insert(gate->name);

tests/techmap/abc9_src_retention.ys

@@ -0,0 +1,22 @@
+read_verilog <<EOT
+module top(input a, b, c, output o);
+assign o = (a & b) | c;
+endmodule
+EOT
+
+# src attributes are set by the Verilog frontend based on source location
+# After simplemap, the $_AND_/$_OR_ cells should have \src attributes
+simplemap
+
+# Check that cells have \src attributes before abc9
+select -assert-any a:src
+
+# Enable verification with -y flag for src attribute propagation
+scratchpad -set abc9.verify true
+
+# Run abc9
+abc9 -lut 4
+
+# After abc9, the mapped LUT cells should have \src attributes
+# propagated via the "y" extension equivalence mapping
+select -assert-any t:$lut a:src