riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

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

extract_fa: Fix `xor3`/`xnor3` inversion bug
This commit is contained in:
Martin Povišer 2025-02-06 21:12:32 +01:00 committed by GitHub
parent ed5d9c8687 ed076bc168
commit 772b9c0cfd
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 32 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
passes/techmap/extract_fa.cc
View File

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

29
tests/various/bug3879.ys Normal file
View File

@ -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