[AIG] Add CutOp (#7743)

The `aig.cut` operation represents a cut in the And-Inverter-Graph.
This operation is variadic and can take multiple inputs and outputs,
which corresponds to the input and output edges in AIG conceptually.

include/circt/Dialect/AIG/AIGOps.td

@@ -15,6 +15,7 @@
 
 include "circt/Dialect/AIG/AIG.td"
 include "mlir/IR/OpBase.td"
+include "mlir/Interfaces/ControlFlowInterfaces.td"
 include "mlir/Interfaces/InferTypeOpInterface.td"
 include "mlir/Interfaces/SideEffectInterfaces.td"
 
@@ -84,4 +85,49 @@ def AndInverterOp : AIGOp<"and_inv", [SameOperandsAndResultType, Pure]> {
   let hasCanonicalizeMethod = 1;
 }
 
+def CutOp : AIGOp<"cut", [IsolatedFromAbove, SingleBlock]> {
+  let summary = "AIG dialect Cut operation";
+  let description = [{
+    The `aig.cut` operation represents a cut in the And-Inverter-Graph.
+    This operation is variadic and can take multiple inputs and outputs,
+    which corresponds to the input and output edges in AIG conceptually.
+
+    ```mlir
+    %0, %1 = aig.cut %a, %b, %c, %d : (i1, i1, i1, i1) -> (i1, i1) {
+    ^bb0(%arg0: i1, %arg1: i1, %arg2: i1, %arg3: i1):
+      %0 = aig.and_inv not %arg0, %arg1 : i1
+      %1 = aig.and_inv %arg1, %arg3 : i1
+      aig.output %0, %1 : i1 }
+    ```
+
+    This operation is designed to be particularly useful for progressive LUT
+    mapping. For instance, a k-input cut can be readily mapped to a k-input LUT.
+    Consequently, the subsequent stages of the pipeline can concentrate on
+    replacing combinational logic with k-input Cut operations, simplifying the
+    overall process.
+  }];
+
+  // TODO: Restrict to HWIntegerType.
+  let arguments = (ins Variadic<AnyType>:$inputs);
+  let results = (outs Variadic<AnyType>:$results);
+  let regions = (region SizedRegion<1>:$bodyRegion);
+  let assemblyFormat = [{
+    $inputs attr-dict `:` functional-type($inputs, $results) $bodyRegion
+  }];
+
+  let hasVerifier = 1;
+}
+
+def OutputOp : AIGOp<"output", [Terminator,
+                                ReturnLike, ParentOneOf<["CutOp"]>]> {
+  let summary = "AIG dialect Output operation";
+  let description = [{
+    The `aig.output` operation represents out edges of a cut.
+  }];
+  let arguments = (ins Variadic<AnyType>:$outputs);
+  let assemblyFormat = [{
+    attr-dict ($outputs^ `:` qualified(type($outputs)))?
+  }];
+}
+
 #endif // CIRCT_DIALECT_AIG_OPS_TD

lib/Dialect/AIG/AIGOps.cpp

@@ -149,3 +149,44 @@ APInt AndInverterOp::evaluate(ArrayRef<APInt> inputs) {
   }
   return result;
 }
+
+LogicalResult CutOp::verify() {
+  auto *block = getBody();
+  // NOTE: Currently input and output types of the block must be exactly the
+  // same. We might want to relax this in the future as a way to represent
+  // "vectorized" cuts. For example in the following cut, the block arguments
+  // types are i1, but the cut is batch-applied over 8-bit lanes.
+  // %0 = aig.cut %a, %b : (i8, i8) -> (i8) {
+  //   ^bb0(%arg0: i1, %arg1: i1):
+  //     %c = aig.and_inv %arg0, not %arg1 : i1
+  //     aig.output %c : i1
+  // }
+
+  if (getInputs().size() != block->getNumArguments())
+    return emitOpError("the number of inputs and the number of block arguments "
+                       "do not match. Expected ")
+           << getInputs().size() << " but got " << block->getNumArguments();
+
+  // Check input types.
+  for (auto [input, arg] : llvm::zip(getInputs(), block->getArguments()))
+    if (input.getType() != arg.getType())
+      return emitOpError("input type ")
+             << input.getType() << " does not match "
+             << "block argument type " << arg.getType();
+
+  if (getNumResults() != block->getTerminator()->getNumOperands())
+    return emitOpError("the number of results and the number of terminator "
+                       "operands do not match. Expected ")
+           << getNumResults() << " but got "
+           << block->getTerminator()->getNumOperands();
+
+  // Check output types.
+  for (auto [result, arg] :
+       llvm::zip(getResults(), block->getTerminator()->getOperands()))
+    if (result.getType() != arg.getType())
+      return emitOpError("result type ")
+             << result.getType() << " does not match "
+             << "terminator operand type " << arg.getType();
+
+  return success();
+}

test/Dialect/AIG/errors.mlir

@@ -0,0 +1,39 @@
+// RUN: circt-opt %s -split-input-file -verify-diagnostics
+
+hw.module @InputNum(in %a: i1, in %b: i1) {
+  // expected-error @+1 {{the number of inputs and the number of block arguments do not match. Expected 2 but got 1}}
+  %0 = aig.cut %a, %b : (i1, i1) -> (i1) {
+  ^bb0(%arg0: i1):
+    aig.output %arg0 : i1
+  }
+}
+
+// -----
+
+hw.module @InputType(in %a: i1, in %b: i1) {
+  // expected-error @+1 {{'aig.cut' op input type 'i1' does not match block argument type 'i2'}}
+  %0 = aig.cut %a, %b : (i1, i1) -> (i1) {
+  ^bb0(%arg0: i2, %arg1: i1):
+    aig.output %arg1 : i1
+  }
+}
+
+// -----
+
+hw.module @OutputNum(in %a: i1, in %b: i1) {
+  // expected-error @+1 {{the number of results and the number of terminator operands do not match. Expected 1 but got 2}}
+  %0 = aig.cut %a, %b : (i1, i1) -> (i1) {
+  ^bb0(%arg0: i1, %arg1: i1):
+    aig.output %arg0, %arg1 : i1, i1
+  }
+}
+
+// -----
+
+hw.module @OutputType(in %a: i2, in %b: i1) {
+  // expected-error @+1 {{'aig.cut' op result type 'i1' does not match terminator operand type 'i2'}}
+  %0 = aig.cut %a, %b : (i2, i1) -> (i1) {
+  ^bb0(%arg0: i2, %arg1: i1):
+    aig.output %arg0 : i2
+  }
+}

test/Dialect/AIG/round-trip.mlir

@@ -9,3 +9,22 @@ hw.module @And(in %a: i1, in %b: i4) {
   %1 = aig.and_inv %b, not %b : i4
   %2 = aig.and_inv not %a, not %a : i1
 }
+
+// CHECK-LABEL: @Cut
+// CHECK-NEXT: %[[RES:.+]]:2 = aig.cut %a, %b : (i1, i1) -> (i1, i1) {
+// CHECK-NEXT: ^bb0(%arg0: i1, %arg1: i1):
+// CHECK-NEXT:   %[[C:.+]] = aig.and_inv %arg0, not %arg1 : i1
+// CHECK-NEXT:   %[[D:.+]] = aig.and_inv %arg0, %arg1 : i1
+// CHECK-NEXT:   aig.output %[[C]], %[[D]] : i1, i1
+// CHECK-NEXT: }
+// CHECK-NEXT: hw.output %[[RES]]#0, %[[RES]]#1 : i1, i1
+
+hw.module @Cut(in %a: i1, in %b: i1, out c: i1, out d: i1) {
+  %0, %1 = aig.cut %a, %b : (i1, i1) -> (i1, i1) {
+  ^bb0(%arg0: i1, %arg1: i1):
+    %c = aig.and_inv %arg0, not %arg1 : i1
+    %d = aig.and_inv %arg0, %arg1 : i1
+    aig.output %c, %d : i1, i1
+  }
+  hw.output %0, %1 : i1, i1
+}