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

Merge 94215584e9 into 4b3c03dabc

This commit is contained in:
hovind 2024-11-25 14:22:25 +01:00 committed by GitHub
parent 4b3c03dabc 94215584e9
commit cb23a7e80c
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 35 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
passes/techmap/extract_fa.cc
View File

@ -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 {
@ -412,14 +405,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);
}
@ -516,14 +510,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);
}

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