From d8863e427f46584d9e87c0f120658ab87fb466ff Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Wed, 30 Oct 2024 17:30:44 +0100
Subject: [PATCH 1/4] extract_fa: Add test case

---
 tests/various/bug3879.ys | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 tests/various/bug3879.ys

diff --git a/tests/various/bug3879.ys b/tests/various/bug3879.ys
new file mode 100644
index 00000000000..7163a1f567f
--- /dev/null
+++ 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

From 64d298e2e9ae2467ec589b6b0310d92f17136dd0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98ystein=20Hovind?= <oystein@ascenium.com>
Date: Wed, 30 Oct 2024 17:30:56 +0100
Subject: [PATCH 2/4] extract_fa: Invert xor3/xnor3 output when inverting
 majority3 input

---
 passes/techmap/extract_fa.cc | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/passes/techmap/extract_fa.cc b/passes/techmap/extract_fa.cc
index ec1979f3b6d..1984f82f51e 100644
--- 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);
 				}

From 84d0c8fbfc66bcd2a5ff54bd00a9cfba500ed248 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98ystein=20Hovind?= <oystein@ascenium.com>
Date: Wed, 30 Oct 2024 17:31:00 +0100
Subject: [PATCH 3/4] extract_fa: Simplify xor2/xnor2 negation

---
 passes/techmap/extract_fa.cc | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/passes/techmap/extract_fa.cc b/passes/techmap/extract_fa.cc
index 1984f82f51e..12bed78279f 100644
--- a/passes/techmap/extract_fa.cc
+++ b/passes/techmap/extract_fa.cc
@@ -517,14 +517,15 @@ struct ExtractFaWorker
 					cell->setPort(ID::Y, Y);
 				}
 
+				auto invert_y = f2i.inv_a ^ f2i.inv_b;
 				if (func2.at(key).count(xor2_func)) {
-					SigBit YY = invert_xy || (f2i.inv_a && !f2i.inv_b) || (!f2i.inv_a && f2i.inv_b) ? module->NotGate(NEW_ID, Y) : Y;
+					SigBit YY = invert_xy ^ invert_y ? module->NotGate(NEW_ID, Y) : Y;
 					for (auto bit : func2.at(key).at(xor2_func))
 						assign_new_driver(bit, YY);
 				}
 
 				if (func2.at(key).count(xnor2_func)) {
-					SigBit YY = invert_xy || (f2i.inv_a && !f2i.inv_b) || (!f2i.inv_a && f2i.inv_b) ? Y : module->NotGate(NEW_ID, Y);
+					SigBit YY = invert_xy ^ invert_y ? Y : module->NotGate(NEW_ID, Y);
 					for (auto bit : func2.at(key).at(xnor2_func))
 						assign_new_driver(bit, YY);
 				}

From 94215584e9bbc648c7c6184a4239d3be7df65db3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=98ystein=20Hovind?= <oystein@ascenium.com>
Date: Wed, 30 Oct 2024 17:31:05 +0100
Subject: [PATCH 4/4] extract_fa: Remove redundant code

---
 passes/techmap/extract_fa.cc | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/passes/techmap/extract_fa.cc b/passes/techmap/extract_fa.cc
index 12bed78279f..7314233c18f 100644
--- a/passes/techmap/extract_fa.cc
+++ b/passes/techmap/extract_fa.cc
@@ -344,13 +344,6 @@ struct ExtractFaWorker
 				if (func3.at(key).count(func) == 0)
 					continue;
 
-				if (func3.at(key).count(xor3_func) == 0 && func3.at(key).count(xnor3_func) != 0) {
-					f3i.inv_a = !f3i.inv_a;
-					f3i.inv_b = !f3i.inv_b;
-					f3i.inv_c = !f3i.inv_c;
-					f3i.inv_y = !f3i.inv_y;
-				}
-
 				if (!f3i.inv_a && !f3i.inv_b && !f3i.inv_c && !f3i.inv_y) {
 					log("    Majority without inversions:\n");
 				} else {