diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 988bc558be7..a1f8dad583d 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -63,6 +63,12 @@ struct XAigerWriter vector box_list; + // Track which cell produced each AND-map or CI entry (for \src propagation) + dict and_cell; + dict ci_cell; + // Track \src strings for AIG objects (by object ID) + dict 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(&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(&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()); } }; diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index e55349aa79b..880657cde65 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -429,6 +429,7 @@ void AigerReader::parse_xaiger() log_assert(output_sig); uint32_t nodeID; RTLIL::SigSpec input_sig; + std::vector input_node_ids; for (unsigned j = 0; j < cutLeavesM; ++j) { nodeID = parse_xaiger_literal(f); log_debug2("\t%u\n", nodeID); @@ -439,6 +440,7 @@ void AigerReader::parse_xaiger() RTLIL::Wire *wire = module->wire(stringf("$aiger%d$%d", aiger_autoidx, nodeID)); log_assert(wire); input_sig.append(wire); + input_node_ids.push_back(nodeID); } // Reverse input order as fastest input is returned first input_sig.reverse(); @@ -458,7 +460,10 @@ 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; + lut_input_objs[rootNodeID] = std::move(input_node_ids); } } else if (c == 'r') { @@ -510,6 +515,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(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 +823,29 @@ void AigerReader::post_process() dict> wideports_cache; + // Map from input AIG object ID to \src attribute value + dict 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 " + 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(variable) < inputs.size()); @@ -983,6 +1014,52 @@ 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 origin mapping. + // Each LUT gets \src from its output object's origin plus the origins + // of its input objects, merged with '|' (Yosys multi-source convention). + if (!equiv_lit_ids.empty() && !obj_src.empty()) { + int applied = 0; + for (auto &[obj_id, lut] : lut_by_obj) { + pool src_values; + // Collect \src from the output object's origin + if (obj_id >= 0 && obj_id < (int) equiv_lit_ids.size()) { + int32_t equiv_lit = equiv_lit_ids[obj_id]; + if (equiv_lit >= 0) { + auto src_it = obj_src.find(equiv_lit >> 1); + if (src_it != obj_src.end()) + src_values.insert(src_it->second); + } + } + // Collect \src from each input object's origin + auto leaf_it = lut_input_objs.find(obj_id); + if (leaf_it != lut_input_objs.end()) { + for (int leaf_obj : leaf_it->second) { + if (leaf_obj >= 0 && leaf_obj < (int) equiv_lit_ids.size()) { + int32_t leaf_equiv = equiv_lit_ids[leaf_obj]; + if (leaf_equiv >= 0) { + auto src_it = obj_src.find(leaf_equiv >> 1); + if (src_it != obj_src.end()) + src_values.insert(src_it->second); + } + } + } + } + if (!src_values.empty()) { + std::string merged; + for (auto &s : src_values) { + if (!merged.empty()) merged += "|"; + merged += s; + } + lut->set_string_attribute(ID::src, merged); + applied++; + log_debug("Applied \\src '%s' to cell %s (obj %d)\n", + merged.c_str(), log_id(lut), obj_id); + } + } + if (applied > 0) + log("Applied \\src attributes to %d cells via origin mapping.\n", applied); + } } struct AigerFrontend : public Frontend { diff --git a/frontends/aiger/aigerparse.h b/frontends/aiger/aigerparse.h index 81b9559474f..89ef3be67d3 100644 --- a/frontends/aiger/aigerparse.h +++ b/frontends/aiger/aigerparse.h @@ -46,6 +46,9 @@ struct AigerReader std::vector bad_properties; std::vector boxes; std::vector mergeability, initial_state; + std::vector equiv_lit_ids; + dict lut_by_obj; + dict> lut_input_objs; AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name, std::string map_filename, bool wideports); void parse_aiger(); diff --git a/frontends/aiger2/xaiger.cc b/frontends/aiger2/xaiger.cc index 510da0be87f..958a6850013 100644 --- a/frontends/aiger2/xaiger.cc +++ b/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 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,10 @@ struct Xaiger2Frontend : public Frontend { log_debug("reading 'M' (second pass)\n"); + // Track output literal → Cell* for \src application + dict lit_to_instance; + dict> instance_input_lits; + f->seekg(extensions_start); bool read_mapping = false; uint32_t no_cells, no_instances; @@ -294,11 +311,13 @@ 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()); log_assert(bits[in_lit] != RTLIL::Sm); instance->setPort(in, bits[in_lit]); + instance_input_lits[out_lit].push_back(in_lit); } } } else if (c == '\n') { @@ -318,6 +337,70 @@ struct Xaiger2Frontend : public Frontend { log("Read %d instances with cell library of size %d.\n", no_instances, no_cells); + // Read 'y' extension (origin literal IDs from ABC origin tracking) + // and apply \src attributes to mapped cells. + // Each cell gets \src from its output object's origin plus the + // origins of its input objects, merged with '|'. + 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 equiv_lit_ids(n_entries); + f->read(reinterpret_cast(equiv_lit_ids.data()), len); + + for (auto &[out_lit, instance] : lit_to_instance) { + pool src_values; + // Collect \src from the output object's origin + uint32_t out_obj = out_lit >> 1; + if (out_obj < n_entries) { + int32_t equiv_lit = equiv_lit_ids[out_obj]; + if (equiv_lit >= 0) { + auto src_it = obj_src.find(equiv_lit >> 1); + if (src_it != obj_src.end()) + src_values.insert(src_it->second); + } + } + // Collect \src from each input object's origin + auto leaf_it = instance_input_lits.find(out_lit); + if (leaf_it != instance_input_lits.end()) { + for (uint32_t in_lit : leaf_it->second) { + uint32_t in_obj = in_lit >> 1; + if (in_obj < n_entries) { + int32_t leaf_equiv = equiv_lit_ids[in_obj]; + if (leaf_equiv >= 0) { + auto src_it = obj_src.find(leaf_equiv >> 1); + if (src_it != obj_src.end()) + src_values.insert(src_it->second); + } + } + } + } + if (!src_values.empty()) { + std::string merged; + for (auto &s : src_values) { + if (!merged.empty()) merged += "|"; + merged += s; + } + instance->set_string_attribute(ID::src, merged); + log_debug(" applied \\src '%s' to cell %s (out_obj=%d)\n", + merged.c_str(), log_id(instance), out_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; diff --git a/passes/techmap/abc9_exe.cc b/passes/techmap/abc9_exe.cc index 2baf53a024f..4449065f892 100644 --- a/passes/techmap/abc9_exe.cc +++ b/passes/techmap/abc9_exe.cc @@ -248,7 +248,7 @@ 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 (design->scratchpad_get_bool("abc9.verify")) { if (dff_mode) abc9_script += "; &verify -s"; else diff --git a/passes/techmap/abc9_ops.cc b/passes/techmap/abc9_ops.cc index 8d3869ececc..3990ea20a69 100644 --- a/passes/techmap/abc9_ops.cc +++ b/passes/techmap/abc9_ops.cc @@ -1553,6 +1553,7 @@ void reintegrate(RTLIL::Module *module, bool dff_mode) driver_lut->getPort(ID::A), y_bit, driver_mask); + cell->attributes = driver_lut->attributes; for (auto &bit : cell->connections_.at(ID::A)) { bit.wire = module->wires_.at(remap_name(bit.wire->name)); bit2sinks[bit].push_back(cell); diff --git a/passes/techmap/aigmap.cc b/passes/techmap/aigmap.cc index 19e568a6147..ff8bae3bb07 100644 --- a/passes/techmap/aigmap.cc +++ b/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); diff --git a/tests/techmap/abc9_src_retention.ys b/tests/techmap/abc9_src_retention.ys new file mode 100644 index 00000000000..e8772f875fd --- /dev/null +++ b/tests/techmap/abc9_src_retention.ys @@ -0,0 +1,29 @@ +# Test that \src attributes are preserved through ABC9 synthesis +# via the XAIGER "y" extension equivalence mapping. +# +# The Verilog frontend sets \src attributes based on source location. +# These must survive: simplemap -> aigmap -> write_xaiger -> ABC -> +# read_aiger -> reintegrate, via the "y" identity/equivalence mapping. +# +# Not all LUT cells may receive \src — only those ABC can prove equivalent +# to an input object via &verify -y get the mapping back. + +read_verilog < "$TMPDIR/simple.v" <<'EOF' +module test(input wire a, input wire b, input wire c, output wire o); + wire w; + assign w = a & b; + assign o = w | c; +endmodule +EOF + +run_test "simple" "$TMPDIR/simple.v" + +# Test 2: Amaranth-style design with Python source references +cat > "$TMPDIR/amaranth.v" <<'EOF' +(* \generator = "Amaranth" *) +(* src = "led_blinker.py:8.1-42.0" *) +module top( + (* src = "led_blinker.py:10.5-10.30" *) + input wire [3:0] i_data, + (* src = "led_blinker.py:11.5-11.30" *) + input wire [3:0] i_mask, + (* src = "led_blinker.py:12.5-12.30" *) + input wire i_mode, + (* src = "led_blinker.py:13.5-13.30" *) + output wire [3:0] o_result, + (* src = "led_blinker.py:14.5-14.30" *) + output wire o_any +); + (* src = "led_blinker.py:18.5-18.40" *) + wire [3:0] masked; + (* src = "led_blinker.py:19.5-19.40" *) + wire [3:0] inverted; + (* src = "led_blinker.py:20.5-20.40" *) + wire [3:0] selected; + + assign masked = i_data & i_mask; + assign inverted = i_data ^ i_mask; + assign selected = i_mode ? inverted : masked; + assign o_result = selected; + assign o_any = |selected; +endmodule +EOF + +# Note: \src on cells comes from the Verilog source location of the assign +# statements, not from (* src *) attributes on wires. So we check for the +# temp .v file, not the Python source. The wire-level (* src *) attributes +# from Amaranth are preserved separately on wires, not cells. +run_test "amaranth" "$TMPDIR/amaranth.v" + +# Test 3: Larger design (8-bit adder with mux) +cat > "$TMPDIR/large.v" <<'EOF' +module adder_mux( + input wire [7:0] a, + input wire [7:0] b, + input wire [7:0] c, + input wire sel, + output wire [8:0] sum, + output wire zero +); + wire [8:0] ab_sum; + wire [8:0] ac_sum; + assign ab_sum = a + b; + assign ac_sum = a + c; + assign sum = sel ? ac_sum : ab_sum; + assign zero = (sum == 9'd0); +endmodule +EOF + +run_test "large" "$TMPDIR/large.v" + +echo "=== All tests passed ===" diff --git a/tests/techmap/abc9_src_retention_large.ys b/tests/techmap/abc9_src_retention_large.ys new file mode 100644 index 00000000000..325c2f95e89 --- /dev/null +++ b/tests/techmap/abc9_src_retention_large.ys @@ -0,0 +1,30 @@ +# Test \src retention through ABC9 with a larger combinational design. +# An 8-bit adder with carry chain exercises many AIG nodes and LUTs. +# Verifies that \src attributes propagate through non-trivial optimization. + +read_verilog < [options] + +Options: + --expect-source PREFIX At least one \\src must reference this file prefix + --cell-type TYPE Only check cells of this type (e.g. $lut) + +Checks: +1. The JSON file is valid and contains modules +2. At least one matching cell exists in the design +3. At least one matching cell has a \\src attribute +4. The \\src attribute values look like valid source locations (file:line.col) +5. If --expect-source is given, at least one \\src value must reference that prefix +""" + +import json +import re +import sys + +SRC_PATTERN = re.compile(r'^[\w./\\-]+:\d+\.\d+(-\d+\.\d+)?$') + + +def validate(json_path, expect_source=None, cell_type=None): + with open(json_path) as f: + data = json.load(f) + + modules = data.get('modules', {}) + if not modules: + print("FAIL: No modules found in JSON output") + return False + + total_cells = 0 + cells_with_src = 0 + valid_src_values = 0 + matching_src_values = 0 + src_values = [] + type_label = f" (type={cell_type})" if cell_type else "" + + for mod_name, mod in modules.items(): + for cell_name, cell in mod.get('cells', {}).items(): + if cell_type and cell.get('type') != cell_type: + continue + total_cells += 1 + attrs = cell.get('attributes', {}) + if 'src' in attrs: + cells_with_src += 1 + src_val = attrs['src'] + src_values.append(src_val) + # src can be pipe-separated for multiple source locations + for part in src_val.split('|'): + part = part.strip() + if part and SRC_PATTERN.match(part): + valid_src_values += 1 + if expect_source and part.startswith(expect_source): + matching_src_values += 1 + + print(f"Total cells{type_label}: {total_cells}") + print(f"Cells with \\src: {cells_with_src}") + print(f"Valid \\src values: {valid_src_values}") + if expect_source: + print(f"\\src values matching '{expect_source}': {matching_src_values}") + + if total_cells == 0: + print(f"FAIL: No cells{type_label} found in design") + return False + + if cells_with_src == 0: + print(f"FAIL: No cells{type_label} have \\src attributes") + return False + + if valid_src_values == 0: + print("FAIL: No valid \\src location strings found") + print(f"Found src values: {src_values}") + return False + + if expect_source and matching_src_values == 0: + print(f"FAIL: No \\src values reference expected source '{expect_source}'") + print(f"Found src values: {src_values[:10]}") + return False + + pct = 100.0 * cells_with_src / total_cells + print(f"PASS: {pct:.0f}% of cells ({cells_with_src}/{total_cells}) have \\src attributes") + for sv in src_values[:5]: + print(f" Example: {sv}") + return True + + +if __name__ == '__main__': + expect_source = None + cell_type = None + positional = [] + argv = sys.argv[1:] + i = 0 + while i < len(argv): + if argv[i] == '--expect-source' and i + 1 < len(argv): + expect_source = argv[i + 1] + i += 2 + elif argv[i] == '--cell-type' and i + 1 < len(argv): + cell_type = argv[i + 1] + i += 2 + elif not argv[i].startswith('--'): + positional.append(argv[i]) + i += 1 + else: + i += 1 + + if not positional: + print(f"Usage: {sys.argv[0]} [--expect-source PREFIX] [--cell-type TYPE]") + sys.exit(1) + if not validate(positional[0], expect_source, cell_type): + sys.exit(1)