Cut xaiger2 at barriers.

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);

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

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