[Verif][NFC] Use auto-generated constructors for all passes (#7754)

Drop the `let constructor` line from the Verif pass definitions. This
causes TableGen to automatically generate the constructors for these
passes, and also handle pass options if we ever decide to add them.

This requires adding a `...Pass` to the end of each pass def to produce
a constructor name of the form `create...Pass()`.

include/circt/Dialect/Verif/Passes.td

@@ -1,4 +1,4 @@
-//===-- Passes.td - Verif pass definition file ----------------*- tablegen -*-===//
+//===-- Passes.td - Verif pass definition file -------------*- tablegen -*-===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -15,40 +15,30 @@
 
 include "mlir/Pass/PassBase.td"
 
-/**
- * Performs preparation transformations for formal verification.
- * This includes things like flattening wires, removing unnecessary information
- * such as OM Classes, handles formal contracts and transforms module instances.
- */
- def PrepareForFormal : Pass<"prepare-for-formal", "hw::HWModuleOp"> {
-  let summary = "Prepares a given top-level circuit for formal verification.";
+def PrepareForFormalPass : Pass<"prepare-for-formal", "hw::HWModuleOp"> {
+  let summary = "Prepares a given top-level circuit for formal verification";
   let description = [{
     Prepares a circuit for formal verification. This performs semantic-retaining 
-    transformations that make model checking easier, e.g. flattening wires, handling 
-    formal contracts, removing unwanted information such as OM Classes, etc...
+    transformations that make model checking easier, e.g. flattening wires,
+    handling formal contracts, removing unwanted information such as OM Classes,
+    etc.
   }];
-  let constructor = "circt::verif::createPrepareForFormalPass()";
- }
-
-/**
- * Checks the validity of clocked assertions, assumptions, and cover ops.
- */
-def VerifyClockedAssertLike : Pass<"verify-clocked-assert-like", "hw::HWModuleOp"> {
-  let summary = "Check that clocked-assert-like are valid.";
-  let description = [{
-    Checks that every `clocked_assert`, `clocked_assume` or `clocked_cover` op does not contain 
-    a nested `ltl.clock` or `ltl.disable` operation in its operand tree.
-  }];
-  let constructor = "circt::verif::createVerifyClockedAssertLikePass()";
 }
 
-/**
- * Converts verif.formal ops into hw.module.
- */
-def LowerFormalToHW : Pass<"lower-formal-to-hw", "mlir::ModuleOp"> {
-  let summary = "Lower verif.formal ops to hw.module ops.";
+def VerifyClockedAssertLikePass : Pass<"verify-clocked-assert-like",
+                                       "hw::HWModuleOp"> {
+  let summary = "Check that clocked-assert-like are valid";
   let description = [{
-    Converts verif.formal ops into hw.module ops.
+    Checks that every `clocked_assert`, `clocked_assume` or `clocked_cover` op
+    does not contain a nested `ltl.clock` or `ltl.disable` operation in its
+    operand tree.
+  }];
+}
+
+def LowerFormalToHWPass : Pass<"lower-formal-to-hw", "mlir::ModuleOp"> {
+  let summary = "Lower verif.formal ops to hw.module ops";
+  let description = [{
+    Converts `verif.formal` ops into `hw.module` ops.
   }];
 }
 

include/circt/Dialect/Verif/VerifPasses.h

@@ -27,10 +27,7 @@ class FormalOp;
 namespace circt {
 namespace verif {
 
-std::unique_ptr<mlir::Pass> createVerifyClockedAssertLikePass();
-std::unique_ptr<mlir::Pass> createPrepareForFormalPass();
-std::unique_ptr<mlir::Pass> createLowerFormalToHW();
-
+#define GEN_PASS_DECL
 #define GEN_PASS_REGISTRATION
 #include "circt/Dialect/Verif/Passes.h.inc"
 

lib/Dialect/Verif/Transforms/LowerFormalToHW.cpp

@@ -17,7 +17,7 @@ using namespace circt;
 
 namespace circt {
 namespace verif {
-#define GEN_PASS_DEF_LOWERFORMALTOHW
+#define GEN_PASS_DEF_LOWERFORMALTOHWPASS
 #include "circt/Dialect/Verif/Passes.h.inc"
 } // namespace verif
 } // namespace circt
@@ -26,8 +26,8 @@ using namespace mlir;
 using namespace verif;
 
 namespace {
-struct LowerFormalToHW
-    : circt::verif::impl::LowerFormalToHWBase<LowerFormalToHW> {
+struct LowerFormalToHWPass
+    : verif::impl::LowerFormalToHWPassBase<LowerFormalToHWPass> {
   void runOnOperation() override;
 };
 
@@ -67,7 +67,7 @@ struct FormalOpRewritePattern : public OpRewritePattern<verif::FormalOp> {
 };
 } // namespace
 
-void LowerFormalToHW::runOnOperation() {
+void LowerFormalToHWPass::runOnOperation() {
   RewritePatternSet patterns(&getContext());
   patterns.add<FormalOpRewritePattern>(patterns.getContext());
 

lib/Dialect/Verif/Transforms/PrepareForFormal.cpp

@@ -24,7 +24,7 @@ using namespace circt;
 
 namespace circt {
 namespace verif {
-#define GEN_PASS_DEF_PREPAREFORFORMAL
+#define GEN_PASS_DEF_PREPAREFORFORMALPASS
 #include "circt/Dialect/Verif/Passes.h.inc"
 } // namespace verif
 } // namespace circt
@@ -51,7 +51,7 @@ struct WireOpConversionPattern : OpConversionPattern<hw::WireOp> {
 
 // Eagerly replace all wires with their inputs
 struct PrepareForFormalPass
-    : circt::verif::impl::PrepareForFormalBase<PrepareForFormalPass> {
+    : verif::impl::PrepareForFormalPassBase<PrepareForFormalPass> {
   void runOnOperation() override;
 };
 } // namespace
@@ -71,7 +71,3 @@ void PrepareForFormalPass::runOnOperation() {
           applyPartialConversion(getOperation(), target, std::move(patterns))))
     return signalPassFailure();
 }
-
-std::unique_ptr<mlir::Pass> circt::verif::createPrepareForFormalPass() {
-  return std::make_unique<PrepareForFormalPass>();
-}

lib/Dialect/Verif/Transforms/VerifyClockedAssertLike.cpp

@@ -24,7 +24,7 @@
 
 namespace circt {
 namespace verif {
-#define GEN_PASS_DEF_VERIFYCLOCKEDASSERTLIKE
+#define GEN_PASS_DEF_VERIFYCLOCKEDASSERTLIKEPASS
 #include "circt/Dialect/Verif/Passes.h.inc"
 } // namespace verif
 } // namespace circt
@@ -38,7 +38,7 @@ namespace {
 // Clocked assertlike ops are a simple form of assertions that only
 // contain one clock and one disable condition.
 struct VerifyClockedAssertLikePass
-    : circt::verif::impl::VerifyClockedAssertLikeBase<
+    : verif::impl::VerifyClockedAssertLikePassBase<
           VerifyClockedAssertLikePass> {
 private:
   // Used to perform a DFS search through the module to visit all operands
@@ -107,7 +107,3 @@ void VerifyClockedAssertLikePass::runOnOperation() {
         .Default([&](auto) {});
   });
 }
-
-std::unique_ptr<mlir::Pass> circt::verif::createVerifyClockedAssertLikePass() {
-  return std::make_unique<VerifyClockedAssertLikePass>();
-}