From 0072a267cc5380963917fa2971b8198cbc54b635 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 29 May 2025 16:20:16 +1200
Subject: [PATCH 1/2] write_aiger: Add no-sort option

Prevents sorting input/output bits so that they remain in the same order they were read in.
---
 backends/aiger/aiger.cc | 70 ++++++++++++++++++++++++++---------------
 1 file changed, 45 insertions(+), 25 deletions(-)

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 617d7d85f..3da98d79d 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<SigBit> undriven_bits;
 		pool<SigBit> unused_bits;
@@ -152,6 +152,34 @@ struct AigerWriter
 			if (wire->port_input)
 				sigmap.add(wire);
 
+		// handle ports
+		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 +195,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 +216,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 +353,10 @@ struct AigerWriter
 		}
 
 		init_map.sort();
-		input_bits.sort();
-		output_bits.sort();
+		if (!no_sort) {
+			input_bits.sort();
+			output_bits.sort();
+		}
 		not_map.sort();
 		ff_map.sort();
 		and_map.sort();
@@ -901,6 +913,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");
@@ -925,6 +940,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 +971,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 +1028,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()) {

From aac562d36af6c8bf16072c2cc8ed0a2f778a3413 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Sat, 31 May 2025 09:55:00 +1200
Subject: [PATCH 2/2] aiger.cc: Explicit unsorted-pool-as-LIFO

---
 backends/aiger/aiger.cc | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 3da98d79d..5b07a7195 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -153,6 +153,9 @@ struct AigerWriter
 				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++)
@@ -353,6 +356,7 @@ struct AigerWriter
 		}
 
 		init_map.sort();
+		// we are relying here on unsorted pools iterating last-in-first-out
 		if (!no_sort) {
 			input_bits.sort();
 			output_bits.sort();