[Synth] Add MajorityInverterOp (synth.mig.maj_inv) to Synth dialect

include/circt/Dialect/AIG/AIGOps.td

@@ -56,9 +56,9 @@ def AndInverterOp : AIGOp<"and_inv", [SameOperandsAndResultType, Pure]> {
   let arguments = (ins Variadic<AnyType>:$inputs, DenseBoolArrayAttr:$inverted);
   let results = (outs AnyType:$result);
 
-  // NOTE: Custom assembly format is needed to pretty print the `inverted`
-  // attribute.
-  let hasCustomAssemblyFormat = 1;
+  let assemblyFormat = [{
+    custom<VariadicInvertibleOperands>($inputs, type($result), $inverted, attr-dict)
+  }];
 
   let builders = [
     OpBuilder<(ins "Value":$input, CArg<"bool", "false">:$invert), [{

include/circt/Dialect/Synth/SynthOps.h

@@ -15,7 +15,10 @@
 
 #include "circt/Dialect/Synth/SynthDialect.h"
 #include "circt/Support/LLVM.h"
-#include "mlir/IR/OpDefinition.h"
+#include "mlir/IR/Builders.h"
+#include "mlir/IR/BuiltinOps.h"
+#include "mlir/Interfaces/InferTypeOpInterface.h"
+#include "mlir/Interfaces/SideEffectInterfaces.h"
 
 #define GET_OP_CLASSES
 #include "circt/Dialect/Synth/Synth.h.inc"

include/circt/Dialect/Synth/SynthOps.td

@@ -15,9 +15,45 @@
 
 include "circt/Dialect/Synth/Synth.td"
 include "mlir/IR/OpBase.td"
+include "mlir/Interfaces/InferTypeOpInterface.td"
+include "mlir/Interfaces/SideEffectInterfaces.td"
 
 // Base class for the operations in this dialect.
 class SynthOp<string mnemonic, list<Trait> traits = []> :
     Op<Synth_Dialect, mnemonic, traits>;
 
+def MajorityInverterOp : SynthOp<"mig.maj_inv",
+                                 [SameOperandsAndResultType, Pure]> {
+  let summary = "Majority-Inverter operation";
+  let description = [{
+    The `synth.mig.maj_inv` operation represents a Majority-Inverter in the
+    Synth dialect. This is used to represent majority inverter graph in
+    synthesis. This operation computes the majority function of its inputs,
+    where operands can be inverted respectively.
+
+    The majority function returns 1 when more than half of the inputs are 1,
+    and 0 otherwise. For three inputs, it's equivalent to:
+    (a & b) | (a & c) | (b & c).
+
+    Example:
+    ```mlir
+      %r1 = synth.mig.maj_inv %a, %b, %c : i1
+      %r2 = synth.mig.maj_inv not %a, %b, not %c : i1
+      %r3 = synth.mig.maj_inv %a, %b, %c, %d, %e : i3
+    ```
+
+    The number of inputs must be odd to avoid ties.
+  }];
+  let arguments = (ins Variadic<AnyType>:$inputs,
+                       DenseBoolArrayAttr:$inverted);
+  let results = (outs AnyType:$result);
+  let hasVerifier = true;
+
+  let assemblyFormat = [{
+    custom<VariadicInvertibleOperands>($inputs, type($result), $inverted,
+                                       attr-dict)
+  }];
+  let cppNamespace = "::circt::synth::mig";
+}
+
 #endif // CIRCT_DIALECT_SYNTH_SYNTHOPS_TD

include/circt/Support/CustomDirectiveImpl.h

@@ -15,7 +15,11 @@
 
 #include "circt/Support/LLVM.h"
 #include "mlir/IR/Builders.h"
+#include "mlir/IR/BuiltinAttributes.h"
 #include "mlir/IR/OpImplementation.h"
+#include "mlir/IR/OperationSupport.h"
+#include "mlir/IR/TypeRange.h"
+#include "mlir/IR/Types.h"
 
 namespace circt {
 
@@ -86,6 +90,26 @@ ParseResult parseKeywordBool(OpAsmParser &parser, BoolAttr &attr,
 void printKeywordBool(OpAsmPrinter &printer, Operation *op, BoolAttr attr,
                       StringRef trueKeyword, StringRef falseKeyword);
 
+//===----------------------------------------------------------------------===//
+// Variadic Invertible Custom Directive
+//===----------------------------------------------------------------------===//
+
+/// Parse a variadic list of operands that may be prefixed with an optional
+/// `not` keyword. If the `not` keyword is present, the corresponding element
+/// in the `inverted` attribute is set to true; otherwise, it is set to false.
+ParseResult parseVariadicInvertibleOperands(
+    OpAsmParser &parser,
+    SmallVectorImpl<OpAsmParser::UnresolvedOperand> &operands, Type &resultType,
+    mlir::DenseBoolArrayAttr &inverted, NamedAttrList &attrDict);
+
+/// Print a variadic list of operands that may be prefixed with an optional
+/// `not` keyword. If the corresponding element in `isInverted` is true, the
+/// `not` keyword is printed before the operand; otherwise, it is omitted.
+void printVariadicInvertibleOperands(OpAsmPrinter &printer, Operation *op,
+                                     OperandRange operands, Type resultType,
+                                     mlir::DenseBoolArrayAttr inverted,
+                                     DictionaryAttr attrDict);
+
 } // namespace circt
 
 #endif // CIRCT_SUPPORT_CUSTOMDIRECTIVEIMPL_H

lib/Dialect/AIG/AIGOps.cpp

@@ -12,6 +12,7 @@
 
 #include "circt/Dialect/AIG/AIGOps.h"
 #include "circt/Dialect/HW/HWOps.h"
+#include "circt/Support/CustomDirectiveImpl.h"
 #include "circt/Support/Naming.h"
 #include "mlir/IR/PatternMatch.h"
 
@@ -104,48 +105,6 @@ LogicalResult AndInverterOp::canonicalize(AndInverterOp op,
   return success();
 }
 
-ParseResult AndInverterOp::parse(OpAsmParser &parser, OperationState &result) {
-  SmallVector<OpAsmParser::UnresolvedOperand> operands;
-  SmallVector<bool> inverts;
-  auto loc = parser.getCurrentLocation();
-
-  while (true) {
-    inverts.push_back(succeeded(parser.parseOptionalKeyword("not")));
-    operands.push_back(OpAsmParser::UnresolvedOperand());
-
-    if (parser.parseOperand(operands.back()))
-      return failure();
-    if (parser.parseOptionalComma())
-      break;
-  }
-
-  Type type;
-  if (parser.parseOptionalAttrDict(result.attributes) || parser.parseColon() ||
-      parser.parseCustomTypeWithFallback(type))
-    return failure();
-
-  result.addTypes({type});
-  result.addAttribute("inverted",
-                      parser.getBuilder().getDenseBoolArrayAttr(inverts));
-  if (parser.resolveOperands(operands, type, loc, result.operands))
-    return failure();
-  return success();
-}
-
-void AndInverterOp::print(OpAsmPrinter &odsPrinter) {
-  odsPrinter << ' ';
-  llvm::interleaveComma(llvm::zip(getInverted(), getInputs()), odsPrinter,
-                        [&](auto &&pair) {
-                          auto [invert, input] = pair;
-                          if (invert) {
-                            odsPrinter << "not ";
-                          }
-                          odsPrinter << input;
-                        });
-  odsPrinter.printOptionalAttrDict((*this)->getAttrs(), {"inverted"});
-  odsPrinter << " : " << getResult().getType();
-}
-
 APInt AndInverterOp::evaluate(ArrayRef<APInt> inputs) {
   assert(inputs.size() == getNumOperands() &&
          "Expected as many inputs as operands");

lib/Dialect/AIG/CMakeLists.txt

@@ -8,6 +8,7 @@ add_circt_dialect_library(CIRCTAIG
   LINK_LIBS PUBLIC
   MLIRIR
   CIRCTHW
+  CIRCTSupport
 
   DEPENDS
   MLIRAIGIncGen

lib/Dialect/Synth/CMakeLists.txt

@@ -19,6 +19,7 @@ add_circt_dialect_library(CIRCTSynth
 
   LINK_LIBS PUBLIC
   MLIRIR
+  CIRCTSupport
 )
 
 add_subdirectory(Transforms)

lib/Dialect/Synth/SynthOps.cpp

@@ -7,9 +7,17 @@
 //===----------------------------------------------------------------------===//
 
 #include "circt/Dialect/Synth/SynthOps.h"
+#include "circt/Support/CustomDirectiveImpl.h"
 
 using namespace circt;
-using namespace synth;
+using namespace circt::synth::mig;
 
 #define GET_OP_CLASSES
 #include "circt/Dialect/Synth/Synth.cpp.inc"
+
+LogicalResult MajorityInverterOp::verify() {
+  if (getNumOperands() % 2 != 1)
+    return emitOpError("requires an odd number of operands");
+
+  return success();
+}

lib/Support/CustomDirectiveImpl.cpp

@@ -138,3 +138,46 @@ void circt::printKeywordBool(OpAsmPrinter &printer, Operation *op,
   else
     printer << falseKeyword;
 }
+
+ParseResult circt::parseVariadicInvertibleOperands(
+    OpAsmParser &parser,
+    SmallVectorImpl<OpAsmParser::UnresolvedOperand> &operands, Type &resultType,
+    mlir::DenseBoolArrayAttr &inverted, NamedAttrList &attrDict) {
+  SmallVector<bool> inverts;
+
+  while (true) {
+    inverts.push_back(succeeded(parser.parseOptionalKeyword("not")));
+    operands.push_back(OpAsmParser::UnresolvedOperand());
+
+    if (parser.parseOperand(operands.back()))
+      return failure();
+    if (parser.parseOptionalComma())
+      break;
+  }
+
+  if (parser.parseOptionalAttrDict(attrDict) || parser.parseColon() ||
+      parser.parseCustomTypeWithFallback(resultType))
+    return failure();
+
+  inverted = parser.getBuilder().getDenseBoolArrayAttr(inverts);
+  return success();
+}
+
+void circt::printVariadicInvertibleOperands(OpAsmPrinter &printer,
+                                            Operation *op,
+                                            OperandRange operands,
+                                            Type resultType,
+                                            mlir::DenseBoolArrayAttr inverted,
+                                            DictionaryAttr attrDict) {
+
+  llvm::interleaveComma(llvm::zip(inverted.asArrayRef(), operands), printer,
+                        [&](auto &&pair) {
+                          auto [invert, input] = pair;
+                          if (invert)
+                            printer << "not ";
+                          printer << input;
+                        });
+  printer.printOptionalAttrDict(attrDict.getValue(), {"inverted"});
+  printer << " : ";
+  printer.printType(resultType);
+}

test/Dialect/Synth/errors.mlir

@@ -0,0 +1,7 @@
+// RUN: circt-opt %s --verify-diagnostics
+
+hw.module @test(in %a : i1, in %b : i1, out result : i1) {
+    // expected-error @+1 {{'synth.mig.maj_inv' op requires an odd number of operands}}
+    %0 = synth.mig.maj_inv %a, %b : i1
+    hw.output %0 : i1
+}

test/Dialect/Synth/round-trip.mlir

@@ -0,0 +1,7 @@
+// RUN: circt-opt --verify-roundtrip --verify-diagnostics %s | FileCheck %s
+// CHECK-LABEL: @basic
+// CHECK: synth.mig.maj_inv
+hw.module @basic(in %a : i4, out result : i4) {
+    %0 = synth.mig.maj_inv not %a, %a, %a {sv.namehint = "out0"} : i4
+    hw.output %0 : i4
+}