hw.module @foo(in %a : i1, in %b : i1, out out0 : i1, out out1 : i1) {
%0 = synth.aig.and_inv not %a, not %b : i1
%1 = comb.or %a, %b : i1
hw.output %0, %1 : i1, i1
}
hw.module @bar(in %a : i1, in %b : i1, out out0 : i1, out out1 : i1) {
%0 = synth.aig.and_inv not %a, not %b : i1
%1 = comb.or %a, %b : i1
%not = synth.aig.and_inv not %0 : i1
hw.output %not, %1 : i1, i1
}
$ circt-opt -synth-functional-reduction='conflict-limit=-1' foo.mlir
hw.module @foo(in %a : i1, in %b : i1, out out0 : i1, out out1 : i1) {
%0 = synth.aig.and_inv not %a, not %b : i1
%1 = comb.or %a, %b : i1
hw.output %0, %1 : i1, i1
}
hw.module @bar(in %a : i1, in %b : i1, out out0 : i1, out out1 : i1) {
%0 = synth.aig.and_inv not %a, not %b : i1
%1 = comb.or %a, %b : i1
%2 = synth.aig.and_inv not %0 : i1
%3 = synth.choice %1, %2 : i1
hw.output %3, %3 : i1, i1
}
Currently FunctionalReduction only introduces choice in bar. Since in synthesis we generally consider inversion as zero cost, we should be able to prove the equivalence in that case as well, e.g:
hw.module @foo(in %a : i1, in %b : i1, out out0 : i1, out out1 : i1) {
%0 = synth.aig.and_inv not %a, not %b : i1
%1 = comb.or %a, %b : i1
%2 = synth.aig.and_inv not %0: i1
%choice = synth.choice %1, %2: i1
hw.output %choice, %choice : i1, i1
}
Basically change:
|
for (auto value : allValues) |
|
sigGroups[simSignatures.at(value)].push_back(value); |
to
for (auto value : allValues) {
auto signature = simSignatures.at(value);
auto flipedSignature = ~signature;
// Use smaller one as canonicalization
bool inverted = signature > flipedSignature;
sigGroups[inverterd? flipedSignatuer: signature: ].push_back({value, inverted});
}
And update the rest.
Currently FunctionalReduction only introduces choice in
bar. Since in synthesis we generally consider inversion as zero cost, we should be able to prove the equivalence in that case as well, e.g:Basically change:
circt/lib/Dialect/Synth/Transforms/FunctionalReduction.cpp
Lines 530 to 531 in 7f79dac
to
And update the rest.