diff --git a/include/circt/Dialect/Synth/Transforms/SynthPasses.td b/include/circt/Dialect/Synth/Transforms/SynthPasses.td index 7585e25391f3..d3de1111654a 100644 --- a/include/circt/Dialect/Synth/Transforms/SynthPasses.td +++ b/include/circt/Dialect/Synth/Transforms/SynthPasses.td @@ -189,4 +189,12 @@ def StructuralHash : Pass<"synth-structural-hash", "hw::HWModuleOp"> { }]; } +def MaximumAndCover : Pass<"synth-maximum-and-cover", "hw::HWModuleOp"> { + let summary = "Maximum And Cover for And-Inverter"; + let description = [{ + This pass performs maximum AND-cover optimization by collapsing single-fanout + and-inverter ops into their users + }]; +} + #endif // CIRCT_DIALECT_SYNTH_TRANSFORMS_PASSES_TD diff --git a/integration_test/circt-synth/maximum-and-cover-lec.mlir b/integration_test/circt-synth/maximum-and-cover-lec.mlir new file mode 100644 index 000000000000..296d94313e78 --- /dev/null +++ b/integration_test/circt-synth/maximum-and-cover-lec.mlir @@ -0,0 +1,33 @@ +// REQUIRES: libz3 +// REQUIRES: circt-lec-jit + +// RUN: circt-opt %s --convert-synth-to-comb -o %t1.mlir +// RUN: circt-opt %s --synth-maximum-and-cover --convert-synth-to-comb -o %t2.mlir + +// RUN: circt-lec %t1.mlir %t2.mlir -c1=MaxCover1 -c2=MaxCover1 --shared-libs=%libz3 | FileCheck %s --check-prefix=MAX_COVER_1 +// MAX_COVER_1: c1 == c2 +hw.module @MaxCover1(in %a: i1, in %b: i1, in %c: i1, in %d: i1, out o1: i1, out o2: i1, out o3: i1) { + %0 = synth.aig.and_inv %a, %b : i1 + %1 = synth.aig.and_inv %0, %c : i1 + %2 = synth.aig.and_inv %b, %c : i1 + %3 = synth.aig.and_inv %2, %d : i1 + + %4 = synth.aig.and_inv %c, %d : i1 + %5 = synth.aig.and_inv %b, %4 : i1 + %6 = synth.aig.and_inv %a, %5 : i1 + + hw.output %1, %3, %6 : i1, i1, i1 +} + +// RUN: circt-lec %t1.mlir %t2.mlir -c1=MaxCover2 -c2=MaxCover2 --shared-libs=%libz3 | FileCheck %s --check-prefix=MAX_COVER_2 +// MAX_COVER_2: c1 == c2 +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) { + %1 = synth.aig.and_inv %a, not %b : i1 + %2 = synth.aig.and_inv %d, not %e : i1 + %3 = synth.aig.and_inv not %2, %f : i1 + %4 = synth.aig.and_inv not %c, %3 : i1 + %5 = synth.aig.and_inv %1, not %4 : i1 + %6 = synth.aig.and_inv %5, %g : i1 + + hw.output %6 : i1 +} diff --git a/lib/Dialect/Synth/Transforms/CMakeLists.txt b/lib/Dialect/Synth/Transforms/CMakeLists.txt index 160a006b6d5c..6ba1d9fb6415 100644 --- a/lib/Dialect/Synth/Transforms/CMakeLists.txt +++ b/lib/Dialect/Synth/Transforms/CMakeLists.txt @@ -12,6 +12,7 @@ add_circt_dialect_library(CIRCTSynthTransforms GenericLUTMapper.cpp LowerVariadic.cpp LowerWordToBits.cpp + MaximumAndCover.cpp StructuralHash.cpp SynthesisPipeline.cpp TechMapper.cpp diff --git a/lib/Dialect/Synth/Transforms/MaximumAndCover.cpp b/lib/Dialect/Synth/Transforms/MaximumAndCover.cpp new file mode 100644 index 000000000000..724607d70d05 --- /dev/null +++ b/lib/Dialect/Synth/Transforms/MaximumAndCover.cpp @@ -0,0 +1,86 @@ +//===----------------------------------------------------------------------===// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// +// +// This pass performs maximum AND-cover optimization by collapsing single-fanout +// AND nodes into their consumers. +// +//===----------------------------------------------------------------------===// + +#include "circt/Dialect/HW/HWOps.h" +#include "circt/Dialect/Synth/SynthOps.h" +#include "circt/Dialect/Synth/Transforms/SynthPasses.h" +#include "mlir/Transforms/GreedyPatternRewriteDriver.h" + +#define DEBUG_TYPE "synth-maximum-and-cover" + +namespace circt { +namespace synth { +#define GEN_PASS_DEF_MAXIMUMANDCOVER +#include "circt/Dialect/Synth/Transforms/SynthPasses.h.inc" +} // namespace synth +} // namespace circt + +using namespace circt; +using namespace synth; + +namespace { +struct MaximumAndCoverPattern : OpRewritePattern { + using OpRewritePattern::OpRewritePattern; + + LogicalResult matchAndRewrite(aig::AndInverterOp op, + PatternRewriter &rewriter) const override { + // Check if any operand can be collapsed (single-fanout non-inverted AND) + llvm::SmallVector newFanins; + llvm::SmallVector newInverts; + bool changed = false; + + for (auto [input, inverted] : llvm::zip(op.getInputs(), op.getInverted())) { + auto andOp = input.getDefiningOp(); + + // Can only collapse if: + // 1. Input is an AND operation + // 2. Input is not inverted in current op + // 3. AND operation has only one use (single fanout) + if (!inverted && andOp && andOp->hasOneUse()) { + // Collect fanin node's inputs into current node + for (auto [fanin, faninInverted] : + llvm::zip(andOp.getInputs(), andOp.getInverted())) { + newFanins.push_back(fanin); + newInverts.push_back(faninInverted); + } + changed = true; + } else { + // Keep the original input + newFanins.push_back(input); + newInverts.push_back(inverted); + } + } + + if (!changed) + return failure(); + + // Create new AND operation with collapsed inputs + rewriter.replaceOpWithNewOp(op, newFanins, newInverts); + return success(); + } +}; + +struct MaximumAndCoverPass + : public impl::MaximumAndCoverBase { + void runOnOperation() override; +}; +} // namespace + +void MaximumAndCoverPass::runOnOperation() { + RewritePatternSet patterns(&getContext()); + patterns.add(&getContext()); + + mlir::FrozenRewritePatternSet frozenPatterns(std::move(patterns)); + if (failed(mlir::applyPatternsGreedily(getOperation(), frozenPatterns))) + return signalPassFailure(); +} diff --git a/lib/Dialect/Synth/Transforms/SynthesisPipeline.cpp b/lib/Dialect/Synth/Transforms/SynthesisPipeline.cpp index b50d911daf41..116ca2022fe2 100644 --- a/lib/Dialect/Synth/Transforms/SynthesisPipeline.cpp +++ b/lib/Dialect/Synth/Transforms/SynthesisPipeline.cpp @@ -112,6 +112,8 @@ void circt::synth::buildSynthOptimizationPipeline( pm.addPass(createCSEPass()); pm.addPass(createStructuralHash()); pm.addPass(createSimpleCanonicalizerPass()); + pm.addPass(synth::createMaximumAndCover()); + pm.addPass(synth::createLowerVariadic()); pm.addPass(createStructuralHash()); if (!options.abcCommands.empty()) { diff --git a/test/Dialect/Synth/maximum-and-cover.mlir b/test/Dialect/Synth/maximum-and-cover.mlir new file mode 100644 index 000000000000..c90e7357db61 --- /dev/null +++ b/test/Dialect/Synth/maximum-and-cover.mlir @@ -0,0 +1,47 @@ +// RUN: circt-opt %s --synth-maximum-and-cover | FileCheck %s + +// CHECK-LABEL: @SingleFanoutCollapse +hw.module @SingleFanoutCollapse(in %a: i1, in %b: i1, in %c: i1, in %d: i1, out o1: i1) { + // CHECK-NEXT: %[[AND:.+]] = synth.aig.and_inv %a, %b, %c, %d : i1 + // CHECK-NEXT: hw.output %[[AND]] : i1 + %0 = synth.aig.and_inv %a, %b : i1 + %1 = synth.aig.and_inv %0, %c, %d : i1 + hw.output %1 : i1 +} + +// CHECK-LABEL: @MultiFanoutNoCollapse +hw.module @MultiFanoutNoCollapse(in %a: i1, in %b: i1, in %c: i1, out o1: i1, out o2: i1) { + // CHECK-NEXT: %[[AND0:.+]] = synth.aig.and_inv %a, %b : i1 + // CHECK-NEXT: %[[AND1:.+]] = synth.aig.and_inv %[[AND0]], %c : i1 + // CHECK-NEXT: hw.output %[[AND0]], %[[AND1]] : i1, i1 + %0 = synth.aig.and_inv %a, %b : i1 + %1 = synth.aig.and_inv %0, %c : i1 + hw.output %0, %1 : i1, i1 +} + +// CHECK-LABEL: @InvertedNoCollapse +hw.module @InvertedNoCollapse(in %a: i1, in %b: i1, in %c: i1, out o1: i1) { + // CHECK-NEXT: %[[AND0:.+]] = synth.aig.and_inv %a, %b : i1 + // CHECK-NEXT: %[[AND1:.+]] = synth.aig.and_inv not %[[AND0]], %c : i1 + // CHECK-NEXT: hw.output %[[AND1]] : i1 + %0 = synth.aig.and_inv %a, %b : i1 + %1 = synth.aig.and_inv not %0, %c : i1 + hw.output %1 : i1 +} + +// CHECK-LABEL: @ComplexTree +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) { + // CHECK-NEXT: %[[AND0:.+]] = synth.aig.and_inv %d, not %e : i1 + // CHECK-NEXT: %[[AND1:.+]] = synth.aig.and_inv not %c, not %[[AND0]], %f : i1 + // CHECK-NEXT: %[[AND2:.+]] = synth.aig.and_inv %a, not %b, not %[[AND1]], %g : i1 + // CHECK-NEXT: hw.output %[[AND2]] : i1 + + %1 = synth.aig.and_inv %a, not %b : i1 + %2 = synth.aig.and_inv %d, not %e : i1 + %3 = synth.aig.and_inv not %2, %f : i1 + %4 = synth.aig.and_inv not %c, %3 : i1 + %5 = synth.aig.and_inv %1, not %4 : i1 + %6 = synth.aig.and_inv %5, %g : i1 + + hw.output %6 : i1 +}