Skip to content

Commit

Permalink
extract_fa: Fix handling inversion of an FA xor output
Browse files Browse the repository at this point in the history
Fixes what seems to be a missing inversion of the xor output when the
heueristic decides to use an inverted FA.

Fixes #3879
  • Loading branch information
jix committed Aug 7, 2023
1 parent 105c447 commit 1e3fe54
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 2 deletions.
4 changes: 2 additions & 2 deletions passes/techmap/extract_fa.cc
Original file line number Diff line number Diff line change
Expand Up @@ -413,13 +413,13 @@ struct ExtractFaWorker
}

if (func3.at(key).count(xor3_func)) {
SigBit YY = invert_xy ? module->NotGate(NEW_ID, Y) : Y;
SigBit YY = invert_xy != f3i.inv_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 != f3i.inv_y ? Y : module->NotGate(NEW_ID, Y);
for (auto bit : func3.at(key).at(xnor3_func))
assign_new_driver(bit, YY);
}
Expand Down
29 changes: 29 additions & 0 deletions tests/various/bug3879.ys
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 1e3fe54

Please sign in to comment.