diff --git a/include/circt/Dialect/AIG/AIGOps.td b/include/circt/Dialect/AIG/AIGOps.td index 9c805f1f053d..b2b668ee9fd4 100644 --- a/include/circt/Dialect/AIG/AIGOps.td +++ b/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:$inputs); + let results = (outs Variadic:$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:$outputs); + let assemblyFormat = [{ + attr-dict ($outputs^ `:` qualified(type($outputs)))? + }]; +} + #endif // CIRCT_DIALECT_AIG_OPS_TD diff --git a/lib/Dialect/AIG/AIGOps.cpp b/lib/Dialect/AIG/AIGOps.cpp index 0d49ab8a638d..0b26856a3f22 100644 --- a/lib/Dialect/AIG/AIGOps.cpp +++ b/lib/Dialect/AIG/AIGOps.cpp @@ -149,3 +149,44 @@ APInt AndInverterOp::evaluate(ArrayRef 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(); +} diff --git a/test/Dialect/AIG/errors.mlir b/test/Dialect/AIG/errors.mlir new file mode 100644 index 000000000000..af41c3ccb0ca --- /dev/null +++ b/test/Dialect/AIG/errors.mlir @@ -0,0 +1,40 @@ +// 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: i1, in %b: i1) { + // expected-error @+1 {{'aig.cut' op result type 'i1' does not match terminator operand type 'i2'}} + %0 = aig.cut %a, %b : (i1, i1) -> (i1) { + ^bb0(%arg0: i1, %arg1: i1): + %c = builtin.unrealized_conversion_cast %arg0 : i1 to i2 + aig.output %c : i2 + } +} diff --git a/test/Dialect/AIG/round-trip.mlir b/test/Dialect/AIG/round-trip.mlir index 5279f865735f..1cce29084a3e 100644 --- a/test/Dialect/AIG/round-trip.mlir +++ b/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 +}