Skip to content

write_aiger: Add no-sort option #5150

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jun 2, 2025
Merged

write_aiger: Add no-sort option #5150

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0072a26
write_aiger: Add no-sort option
KrystalDelusion May 29, 2025
aac562d
aiger.cc: Explicit unsorted-pool-as-LIFO
KrystalDelusion May 30, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
70 changes: 47 additions & 23 deletions backends/aiger/aiger.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<SigBit> undriven_bits;
pool<SigBit> unused_bits;
Expand All @@ -152,16 +152,12 @@ struct AigerWriter
if (wire->port_input)
sigmap.add(wire);

for (auto wire : module->wires())
{
if (wire->attributes.count(ID::init)) {
SigSpec initsig = sigmap(wire);
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;
}

// 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);
Expand All @@ -175,9 +171,6 @@ struct AigerWriter
continue;
}

undriven_bits.insert(bit);
unused_bits.insert(bit);

if (wire->port_input)
input_bits.insert(bit);

Expand All @@ -187,6 +180,32 @@ struct AigerWriter
output_bits.insert(wirebit);
}
}
}

// handle wires
for (auto wire : module->wires())
{
if (wire->attributes.count(ID::init)) {
SigSpec initsig = sigmap(wire);
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;
}

for (int i = 0; i < GetSize(wire); i++)
{
SigBit wirebit(wire, i);
SigBit bit = sigmap(wirebit);

if (bit.wire == nullptr)
continue;
if (wire->port_input || wire->port_output)
continue;

undriven_bits.insert(bit);
unused_bits.insert(bit);
}

if (wire->width == 1) {
auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
Expand All @@ -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_))
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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 <filename>\n");
log(" write an extra file with port and latch symbols\n");
log("\n");
Expand All @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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()) {
Expand Down
Loading