Skip to content

Commit 9f0ac86

Browse files
uenokuMax-astro
uenoku
and
Max-astro
committed
[Synth] Add MaximumAndCover Pass
This implementation is based on a tree-balancing algorithm described in this paper: "https://ieeexplore.ieee.org/abstract/document/6105357". Rebased from #8262. Co-authored-by: Max Zhou <[email protected]>
1 parent 26a6b6e commit 9f0ac86

File tree

6 files changed

+177
-0
lines changed

6 files changed

+177
-0
lines changed

‎include/circt/Dialect/Synth/Transforms/SynthPasses.td‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -189,4 +189,12 @@ def StructuralHash : Pass<"synth-structural-hash", "hw::HWModuleOp"> {
189189
}];
190190
}
191191

192+
def MaximumAndCover : Pass<"synth-maximum-and-cover", "hw::HWModuleOp"> {
193+
let summary = "Maximum And Cover for And-Inverter";
194+
let description = [{
195+
This pass performs maximum AND-cover optimization by collapsing single-fanout
196+
and-inverter ops into their users
197+
}];
198+
}
199+
192200
#endif // CIRCT_DIALECT_SYNTH_TRANSFORMS_PASSES_TD

‎integration_test/circt-synth/maximum-and-cover-lec.mlir‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
// REQUIRES: libz3
2+
// REQUIRES: circt-lec-jit
3+
4+
// RUN: circt-opt %s --convert-synth-to-comb -o %t1.mlir
5+
// RUN: circt-opt %s --synth-maximum-and-cover --convert-synth-to-comb -o %t2.mlir
6+
7+
// RUN: circt-lec %t1.mlir %t2.mlir -c1=MaxCover1 -c2=MaxCover1 --shared-libs=%libz3 | FileCheck %s --check-prefix=MAX_COVER_1
8+
// MAX_COVER_1: c1 == c2
9+
hw.module @MaxCover1(in %a: i1, in %b: i1, in %c: i1, in %d: i1, out o1: i1, out o2: i1, out o3: i1) {
10+
%0 = synth.aig.and_inv %a, %b : i1
11+
%1 = synth.aig.and_inv %0, %c : i1
12+
%2 = synth.aig.and_inv %b, %c : i1
13+
%3 = synth.aig.and_inv %2, %d : i1
14+
15+
%4 = synth.aig.and_inv %c, %d : i1
16+
%5 = synth.aig.and_inv %b, %4 : i1
17+
%6 = synth.aig.and_inv %a, %5 : i1
18+
19+
hw.output %1, %3, %6 : i1, i1, i1
20+
}
21+
22+
// RUN: circt-lec %t1.mlir %t2.mlir -c1=MaxCover2 -c2=MaxCover2 --shared-libs=%libz3 | FileCheck %s --check-prefix=MAX_COVER_2
23+
// MAX_COVER_2: c1 == c2
24+
hw.module @MaxCover2(in %a: i1, in %b: i1, in %c: i1, in %d: i1, in %e: i1, in %f: i1, in %g: i1, out o1: i1) {
25+
%1 = synth.aig.and_inv %a, not %b : i1
26+
%2 = synth.aig.and_inv %d, not %e : i1
27+
%3 = synth.aig.and_inv not %2, %f : i1
28+
%4 = synth.aig.and_inv not %c, %3 : i1
29+
%5 = synth.aig.and_inv %1, not %4 : i1
30+
%6 = synth.aig.and_inv %5, %g : i1
31+
32+
hw.output %6 : i1
33+
}

‎lib/Dialect/Synth/Transforms/CMakeLists.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ add_circt_dialect_library(CIRCTSynthTransforms
1212
GenericLUTMapper.cpp
1313
LowerVariadic.cpp
1414
LowerWordToBits.cpp
15+
MaximumAndCover.cpp
1516
StructuralHash.cpp
1617
SynthesisPipeline.cpp
1718
TechMapper.cpp

‎lib/Dialect/Synth/Transforms/MaximumAndCover.cpp‎

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
//===----------------------------------------------------------------------===//
2+
//
3+
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4+
// See https://llvm.org/LICENSE.txt for license information.
5+
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6+
//
7+
//===----------------------------------------------------------------------===//
8+
//
9+
// This pass performs maximum AND-cover optimization by collapsing single-fanout
10+
// AND nodes into their consumers.
11+
//
12+
//===----------------------------------------------------------------------===//
13+
14+
#include "circt/Dialect/HW/HWOps.h"
15+
#include "circt/Dialect/Synth/SynthOps.h"
16+
#include "circt/Dialect/Synth/Transforms/SynthPasses.h"
17+
#include "mlir/Transforms/GreedyPatternRewriteDriver.h"
18+
19+
#define DEBUG_TYPE "synth-maximum-and-cover"
20+
21+
namespace circt {
22+
namespace synth {
23+
#define GEN_PASS_DEF_MAXIMUMANDCOVER
24+
#include "circt/Dialect/Synth/Transforms/SynthPasses.h.inc"
25+
} // namespace synth
26+
} // namespace circt
27+
28+
using namespace circt;
29+
using namespace synth;
30+
31+
namespace {
32+
struct MaximumAndCoverPattern : OpRewritePattern<aig::AndInverterOp> {
33+
using OpRewritePattern<aig::AndInverterOp>::OpRewritePattern;
34+
35+
LogicalResult matchAndRewrite(aig::AndInverterOp op,
36+
PatternRewriter &rewriter) const override {
37+
// Check if any operand can be collapsed (single-fanout non-inverted AND)
38+
llvm::SmallVector<Value> newFanins;
39+
llvm::SmallVector<bool> newInverts;
40+
bool changed = false;
41+
42+
for (auto [input, inverted] : llvm::zip(op.getInputs(), op.getInverted())) {
43+
auto andOp = input.getDefiningOp<aig::AndInverterOp>();
44+
45+
// Can only collapse if:
46+
// 1. Input is an AND operation
47+
// 2. Input is not inverted in current op
48+
// 3. AND operation has only one use (single fanout)
49+
if (!inverted && andOp && andOp->hasOneUse()) {
50+
// Collect fanin node's inputs into current node
51+
for (auto [fanin, faninInverted] :
52+
llvm::zip(andOp.getInputs(), andOp.getInverted())) {
53+
newFanins.push_back(fanin);
54+
newInverts.push_back(faninInverted);
55+
}
56+
changed = true;
57+
} else {
58+
// Keep the original input
59+
newFanins.push_back(input);
60+
newInverts.push_back(inverted);
61+
}
62+
}
63+
64+
if (!changed)
65+
return failure();
66+
67+
// Create new AND operation with collapsed inputs
68+
rewriter.replaceOpWithNewOp<aig::AndInverterOp>(op, newFanins, newInverts);
69+
return success();
70+
}
71+
};
72+
73+
struct MaximumAndCoverPass
74+
: public impl::MaximumAndCoverBase<MaximumAndCoverPass> {
75+
void runOnOperation() override;
76+
};
77+
} // namespace
78+
79+
void MaximumAndCoverPass::runOnOperation() {
80+
RewritePatternSet patterns(&getContext());
81+
patterns.add<MaximumAndCoverPattern>(&getContext());
82+
83+
mlir::FrozenRewritePatternSet frozenPatterns(std::move(patterns));
84+
if (failed(mlir::applyPatternsGreedily(getOperation(), frozenPatterns)))
85+
return signalPassFailure();
86+
}

‎lib/Dialect/Synth/Transforms/SynthesisPipeline.cpp‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -112,6 +112,8 @@ void circt::synth::buildSynthOptimizationPipeline(
112112
pm.addPass(createCSEPass());
113113
pm.addPass(createStructuralHash());
114114
pm.addPass(createSimpleCanonicalizerPass());
115+
pm.addPass(synth::createMaximumAndCover());
116+
pm.addPass(synth::createLowerVariadic());
115117
pm.addPass(createStructuralHash());
116118

117119
if (!options.abcCommands.empty()) {

‎test/Dialect/Synth/maximum-and-cover.mlir‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
// RUN: circt-opt %s --synth-maximum-and-cover | FileCheck %s
2+
3+
// CHECK-LABEL: @SingleFanoutCollapse
4+
hw.module @SingleFanoutCollapse(in %a: i1, in %b: i1, in %c: i1, in %d: i1, out o1: i1) {
5+
// CHECK-NEXT: %[[AND:.+]] = synth.aig.and_inv %a, %b, %c, %d : i1
6+
// CHECK-NEXT: hw.output %[[AND]] : i1
7+
%0 = synth.aig.and_inv %a, %b : i1
8+
%1 = synth.aig.and_inv %0, %c, %d : i1
9+
hw.output %1 : i1
10+
}
11+
12+
// CHECK-LABEL: @MultiFanoutNoCollapse
13+
hw.module @MultiFanoutNoCollapse(in %a: i1, in %b: i1, in %c: i1, out o1: i1, out o2: i1) {
14+
// CHECK-NEXT: %[[AND0:.+]] = synth.aig.and_inv %a, %b : i1
15+
// CHECK-NEXT: %[[AND1:.+]] = synth.aig.and_inv %[[AND0]], %c : i1
16+
// CHECK-NEXT: hw.output %[[AND0]], %[[AND1]] : i1, i1
17+
%0 = synth.aig.and_inv %a, %b : i1
18+
%1 = synth.aig.and_inv %0, %c : i1
19+
hw.output %0, %1 : i1, i1
20+
}
21+
22+
// CHECK-LABEL: @InvertedNoCollapse
23+
hw.module @InvertedNoCollapse(in %a: i1, in %b: i1, in %c: i1, out o1: i1) {
24+
// CHECK-NEXT: %[[AND0:.+]] = synth.aig.and_inv %a, %b : i1
25+
// CHECK-NEXT: %[[AND1:.+]] = synth.aig.and_inv not %[[AND0]], %c : i1
26+
// CHECK-NEXT: hw.output %[[AND1]] : i1
27+
%0 = synth.aig.and_inv %a, %b : i1
28+
%1 = synth.aig.and_inv not %0, %c : i1
29+
hw.output %1 : i1
30+
}
31+
32+
// CHECK-LABEL: @ComplexTree
33+
hw.module @ComplexTree(in %a: i1, in %b: i1, in %c: i1, in %d: i1, in %e: i1, in %f: i1, in %g: i1, out o1: i1) {
34+
// CHECK-NEXT: %[[AND0:.+]] = synth.aig.and_inv %d, not %e : i1
35+
// CHECK-NEXT: %[[AND1:.+]] = synth.aig.and_inv not %c, not %[[AND0]], %f : i1
36+
// CHECK-NEXT: %[[AND2:.+]] = synth.aig.and_inv %a, not %b, not %[[AND1]], %g : i1
37+
// CHECK-NEXT: hw.output %[[AND2]] : i1
38+
39+
%1 = synth.aig.and_inv %a, not %b : i1
40+
%2 = synth.aig.and_inv %d, not %e : i1
41+
%3 = synth.aig.and_inv not %2, %f : i1
42+
%4 = synth.aig.and_inv not %c, %3 : i1
43+
%5 = synth.aig.and_inv %1, not %4 : i1
44+
%6 = synth.aig.and_inv %5, %g : i1
45+
46+
hw.output %6 : i1
47+
}

0 commit comments

Comments
 (0)