diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 617d7d85f..5b07a7195 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -132,7 +132,7 @@ struct AigerWriter return a; } - AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode, bool lmode) : module(module), zinit_mode(zinit_mode), sigmap(module) + AigerWriter(Module *module, bool no_sort, bool zinit_mode, bool imode, bool omode, bool bmode, bool lmode) : module(module), zinit_mode(zinit_mode), sigmap(module) { pool undriven_bits; pool unused_bits; @@ -152,6 +152,37 @@ struct AigerWriter if (wire->port_input) sigmap.add(wire); + // handle ports + // provided the input_bits and output_bits don't get sorted they + // will be returned in reverse order, so add them in reverse to + // match + for (auto riter = module->ports.rbegin(); riter != module->ports.rend(); ++riter) { + auto *wire = module->wire(*riter); + for (int i = 0; i < GetSize(wire); i++) + { + SigBit wirebit(wire, i); + SigBit bit = sigmap(wirebit); + + if (bit.wire == nullptr) { + if (wire->port_output) { + aig_map[wirebit] = (bit == State::S1) ? 1 : 0; + output_bits.insert(wirebit); + } + continue; + } + + if (wire->port_input) + input_bits.insert(bit); + + if (wire->port_output) { + if (bit != wirebit) + alias_map[wirebit] = bit; + output_bits.insert(wirebit); + } + } + } + + // handle wires for (auto wire : module->wires()) { if (wire->attributes.count(ID::init)) { @@ -167,25 +198,13 @@ struct AigerWriter SigBit wirebit(wire, i); SigBit bit = sigmap(wirebit); - if (bit.wire == nullptr) { - if (wire->port_output) { - aig_map[wirebit] = (bit == State::S1) ? 1 : 0; - output_bits.insert(wirebit); - } + if (bit.wire == nullptr) + continue; + if (wire->port_input || wire->port_output) continue; - } undriven_bits.insert(bit); unused_bits.insert(bit); - - if (wire->port_input) - input_bits.insert(bit); - - if (wire->port_output) { - if (bit != wirebit) - alias_map[wirebit] = bit; - output_bits.insert(wirebit); - } } if (wire->width == 1) { @@ -200,12 +219,6 @@ struct AigerWriter } } - for (auto bit : input_bits) - undriven_bits.erase(bit); - - for (auto bit : output_bits) - unused_bits.erase(bit); - for (auto cell : module->cells()) { if (cell->type == ID($_NOT_)) @@ -343,8 +356,11 @@ struct AigerWriter } init_map.sort(); - input_bits.sort(); - output_bits.sort(); + // we are relying here on unsorted pools iterating last-in-first-out + if (!no_sort) { + input_bits.sort(); + output_bits.sort(); + } not_map.sort(); ff_map.sort(); and_map.sort(); @@ -901,6 +917,9 @@ struct AigerBackend : public Backend { log(" -symbols\n"); log(" include a symbol table in the generated AIGER file\n"); log("\n"); + log(" -no-sort\n"); + log(" don't sort input/output ports\n"); + log("\n"); log(" -map \n"); log(" write an extra file with port and latch symbols\n"); log("\n"); @@ -925,6 +944,7 @@ struct AigerBackend : public Backend { bool zinit_mode = false; bool miter_mode = false; bool symbols_mode = false; + bool no_sort = false; bool verbose_map = false; bool imode = false; bool omode = false; @@ -955,6 +975,10 @@ struct AigerBackend : public Backend { symbols_mode = true; continue; } + if (args[argidx] == "-no-sort") { + no_sort = true; + continue; + } if (map_filename.empty() && args[argidx] == "-map" && argidx+1 < args.size()) { map_filename = args[++argidx]; continue; @@ -1008,7 +1032,7 @@ struct AigerBackend : public Backend { if (!top_module->memories.empty()) log_error("Found unmapped memories in module %s: unmapped memories are not supported in AIGER backend!\n", log_id(top_module)); - AigerWriter writer(top_module, zinit_mode, imode, omode, bmode, lmode); + AigerWriter writer(top_module, no_sort, zinit_mode, imode, omode, bmode, lmode); writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode); if (!map_filename.empty()) {