[Synth] Add MaximumAndCover Pass

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

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
+}

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

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<aig::AndInverterOp> {
+  using OpRewritePattern<aig::AndInverterOp>::OpRewritePattern;
+
+  LogicalResult matchAndRewrite(aig::AndInverterOp op,
+                                PatternRewriter &rewriter) const override {
+    // Check if any operand can be collapsed (single-fanout non-inverted AND)
+    llvm::SmallVector<Value> newFanins;
+    llvm::SmallVector<bool> newInverts;
+    bool changed = false;
+
+    for (auto [input, inverted] : llvm::zip(op.getInputs(), op.getInverted())) {
+      auto andOp = input.getDefiningOp<aig::AndInverterOp>();
+
+      // 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<aig::AndInverterOp>(op, newFanins, newInverts);
+    return success();
+  }
+};
+
+struct MaximumAndCoverPass
+    : public impl::MaximumAndCoverBase<MaximumAndCoverPass> {
+  void runOnOperation() override;
+};
+} // namespace
+
+void MaximumAndCoverPass::runOnOperation() {
+  RewritePatternSet patterns(&getContext());
+  patterns.add<MaximumAndCoverPattern>(&getContext());
+
+  mlir::FrozenRewritePatternSet frozenPatterns(std::move(patterns));
+  if (failed(mlir::applyPatternsGreedily(getOperation(), frozenPatterns)))
+    return signalPassFailure();
+}

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()) {

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
+}