From 5610060faeb0c08bb35eee548570c18b42da2535 Mon Sep 17 00:00:00 2001
From: nella <simontupy64@gmail.com>
Date: Wed, 30 Sep 2026 16:23:12 +0200
Subject: [PATCH] Cut xaiger2 at barriers.

---
 backends/aiger2/aiger.cc          | 11 +++++++--
 tests/various/barrier_abc9.ys     | 38 +++++++++++++++++++++++++++++++
 tests/various/barrier_backends.ys |  5 ++++
 3 files changed, 52 insertions(+), 2 deletions(-)
 create mode 100644 tests/various/barrier_abc9.ys

diff --git a/backends/aiger2/aiger.cc b/backends/aiger2/aiger.cc
index 4e3ddb5ea..16856dbb6 100644
--- a/backends/aiger2/aiger.cc
+++ b/backends/aiger2/aiger.cc
@@ -115,6 +115,13 @@ struct Index {
 	bool inline_whiteboxes = false;
 	bool allow_blackboxes = false;
 
+	bool is_known_op(Cell *cell)
+	{
+		if (cell->type == ID($barrier))
+			return !allow_blackboxes;
+		return known_ops(cell->type);
+	}
+
 	int index_module(RTLIL::Module *m)
 	{
 		ModuleInfo &info = modules[m];
@@ -129,7 +136,7 @@ struct Index {
 		int pos = index_wires(info, m);
 
 		for (auto cell : m->cells()) {
-			if (known_ops(cell->type) || cell->type.in(ID($scopeinfo), ID($specify2), ID($specify3), ID($specrule), ID($input_port)))
+			if (is_known_op(cell) || cell->type.in(ID($scopeinfo), ID($specify2), ID($specify3), ID($specrule), ID($input_port)))
 				continue;
 
 			Module *submodule = cell_def(m->design, cell);
@@ -865,7 +872,7 @@ struct Index {
 			// an output of a cell
 			Cell *driver = bit.wire->driverCell();
 
-			if (known_ops(driver->type)) {
+			if (is_known_op(driver)) {
 				ret = impl_op(cursor, driver, bit.wire->driverPort(), bit.offset);
 			} else {
 				Module *def = cursor.enter(*this, driver);
diff --git a/tests/various/barrier_abc9.ys b/tests/various/barrier_abc9.ys
new file mode 100644
index 000000000..441222ac9
--- /dev/null
+++ b/tests/various/barrier_abc9.ys
@@ -0,0 +1,38 @@
+# ABC must not optimize through $barrier
+read_verilog -icells <<EOT
+module top(input [3:0] a, b, output [3:0] y);
+	wire [3:0] t;
+	\$barrier #(.WIDTH(4)) bar (.A(a & b), .Y(t));
+	assign y = t & a;
+endmodule
+EOT
+hierarchy -top top
+design -save orig
+optbarriers -remove
+design -stash gold
+
+design -load orig
+abc9 -lut 4
+select -assert-count 1 t:$barrier
+select -assert-count 8 t:$lut
+optbarriers -remove
+design -stash gate
+
+design -copy-from gold -as gold top
+design -copy-from gate -as gate top
+miter -equiv -flatten -make_assert gold gate miter
+sat -verify -prove-asserts -show-ports miter
+design -reset
+
+design -load orig
+abc_new -liberty ../liberty/normal.lib
+select -assert-count 1 t:$barrier
+select -assert-count 0 t:$and
+optbarriers -remove
+design -stash gate
+
+read_liberty ../liberty/normal.lib
+design -copy-from gold -as gold top
+design -copy-from gate -as gate top
+miter -equiv -flatten -make_assert gold gate miter
+sat -verify -prove-asserts -show-ports miter
diff --git a/tests/various/barrier_backends.ys b/tests/various/barrier_backends.ys
index 08dca072f..8db25bcb3 100644
--- a/tests/various/barrier_backends.ys
+++ b/tests/various/barrier_backends.ys
@@ -27,3 +27,8 @@ write_cxxrtl temp/barrier.cc
 
 write_btor temp/barrier.btor
 write_aiger2 temp/barrier.aig
+
+# write_xaiger2 cuts at barriers so the cell is kept by -mapping_prep
+write_xaiger2 -mapping_prep -map2 temp/barrier.map2 temp/barrier.xaig
+select -assert-count 1 t:$barrier
+select -assert-count 0 t:$and