Merge pull request #4691 from hovind/experiments/extract-fa-fix

extract_fa: Fix `xor3`/`xnor3` inversion bug
YosysHQ · Feb 6, 2025 · 772b9c0 · 772b9c0
2 parents ed5d9c8 + ed076bc
commit 772b9c0
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 2 deletions.
diff --git a/passes/techmap/extract_fa.cc b/passes/techmap/extract_fa.cc
@@ -412,14 +412,15 @@ struct ExtractFaWorker
 					facache[fakey] = make_tuple(X, Y, cell);
 				}
 
+				bool invert_y = f3i.inv_a ^ f3i.inv_b ^ f3i.inv_c;
 				if (func3.at(key).count(xor3_func)) {
-					SigBit YY = invert_xy ? module->NotGate(NEW_ID, Y) : Y;
+					SigBit YY = invert_xy ^ invert_y ? module->NotGate(NEW_ID, Y) : Y;
 					for (auto bit : func3.at(key).at(xor3_func))
 						assign_new_driver(bit, YY);
 				}
 
 				if (func3.at(key).count(xnor3_func)) {
-					SigBit YY = invert_xy ? Y : module->NotGate(NEW_ID, Y);
+					SigBit YY = invert_xy ^ invert_y ? Y : module->NotGate(NEW_ID, Y);
 					for (auto bit : func3.at(key).at(xnor3_func))
 						assign_new_driver(bit, YY);
 				}

diff --git a/tests/various/bug3879.ys b/tests/various/bug3879.ys
@@ -0,0 +1,29 @@
+read_verilog <<EOF
+module gcd(I, D);
+
+  output [2:0] I;
+  input [3:0] D;
+
+  assign I = D[0]+D[1]+D[2]+D[3];
+endmodule
+EOF
+design -save input
+
+prep
+
+design -stash gold
+
+design -load input
+
+synth  -top gcd -flatten
+
+extract_fa -v
+
+design -stash gate
+
+design -copy-from gold -as gold gcd
+design -copy-from gate -as gate gcd
+
+miter -equiv -make_assert -flatten gold gate miter
+
+sat -verify -prove-asserts -show-all miter