Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

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

Merged
merged 1 commit into from
Oct 31, 2024
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 16 additions & 26 deletions include/circt/Dialect/Verif/Passes.td
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//===-- Passes.td - Verif pass definition file ----------------*- tablegen -*-===//
//===-- Passes.td - Verif pass definition file -------------*- tablegen -*-===//
//
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💯

// 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.";
def VerifyClockedAssertLikePass : 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.
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 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.
Converts `verif.formal` ops into `hw.module` ops.
}];
}

5 changes: 1 addition & 4 deletions include/circt/Dialect/Verif/VerifPasses.h
Original file line number Diff line number Diff line change
@@ -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"

8 changes: 4 additions & 4 deletions lib/Dialect/Verif/Transforms/LowerFormalToHW.cpp
Original file line number Diff line number Diff line change
@@ -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());

8 changes: 2 additions & 6 deletions lib/Dialect/Verif/Transforms/PrepareForFormal.cpp
Original file line number Diff line number Diff line change
@@ -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>();
}
8 changes: 2 additions & 6 deletions lib/Dialect/Verif/Transforms/VerifyClockedAssertLike.cpp
Original file line number Diff line number Diff line change
@@ -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>();
}
Loading