mirror of https://github.com/llvm/circt.git
Add passes to strip OM and Emit dialect ops (#8121)
Several tools in CIRCT do not process the OM and Emit dialects at all, for example, arcilator, circt-bmc, and circt-lec. Since these tools do a full lowering to LLVM internally, they have to discard all OM and Emit ops at some point in the pipeline. Arcilator currently does this in its StripSV pass; circt-bmc and circt-lec simply error out. This commit adds a `StripOM` pass to the OM dialect and a `StripEmit` pass to the Emit dialect which remove any OM and Emit ops from the IR, respectively. These passes are added to the arcilator, circt-bmc, and circt-lec pipelines in order to discard OM and Emit from the input. The commit also includes a few boilerplate changes and alphabetical ordering of dialects and dependencies.
This commit is contained in:
parent
1c70fcec53
commit
ce67b00a52
|
@ -5,9 +5,6 @@
|
|||
## SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
##
|
||||
##===----------------------------------------------------------------------===//
|
||||
##
|
||||
##
|
||||
##===----------------------------------------------------------------------===//
|
||||
|
||||
add_circt_dialect(Emit emit)
|
||||
add_circt_dialect_doc(Emit emit)
|
||||
|
@ -18,3 +15,8 @@ mlir_tablegen(EmitOpInterfaces.h.inc -gen-op-interface-decls)
|
|||
mlir_tablegen(EmitOpInterfaces.cpp.inc -gen-op-interface-defs)
|
||||
add_public_tablegen_target(CIRCTEmitOpInterfacesIncGen)
|
||||
add_dependencies(circt-headers CIRCTEmitOpInterfacesIncGen)
|
||||
|
||||
set(LLVM_TARGET_DEFINITIONS EmitPasses.td)
|
||||
mlir_tablegen(EmitPasses.h.inc -gen-pass-decls)
|
||||
add_public_tablegen_target(CIRCTEmitTransformsIncGen)
|
||||
add_circt_doc(EmitPasses EmitPasses -gen-pass-doc)
|
||||
|
|
|
@ -0,0 +1,30 @@
|
|||
//===- EmitPasses.h - Emit dialect passes ---------------------------------===//
|
||||
//
|
||||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
||||
// See https://llvm.org/LICENSE.txt for license information.
|
||||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#ifndef CIRCT_DIALECT_EMIT_EMITPASSES_H
|
||||
#define CIRCT_DIALECT_EMIT_EMITPASSES_H
|
||||
|
||||
#include "circt/Support/LLVM.h"
|
||||
#include "mlir/Pass/Pass.h"
|
||||
#include <memory>
|
||||
|
||||
namespace mlir {
|
||||
class Pass;
|
||||
} // namespace mlir
|
||||
|
||||
namespace circt {
|
||||
namespace emit {
|
||||
|
||||
#define GEN_PASS_DECL
|
||||
#define GEN_PASS_REGISTRATION
|
||||
#include "circt/Dialect/Emit/EmitPasses.h.inc"
|
||||
|
||||
} // namespace emit
|
||||
} // namespace circt
|
||||
|
||||
#endif // CIRCT_DIALECT_EMIT_EMITPASSES_H
|
|
@ -0,0 +1,17 @@
|
|||
//===- EmitPasses.td - Emit dialect passes -----------------*- tablegen -*-===//
|
||||
//
|
||||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
||||
// See https://llvm.org/LICENSE.txt for license information.
|
||||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
include "mlir/Pass/PassBase.td"
|
||||
|
||||
def StripEmitPass : Pass<"strip-emit", "mlir::ModuleOp"> {
|
||||
let summary = "Remove Emit dialect ops";
|
||||
let description = [{
|
||||
Removes all Emit dialect operations from the IR. Useful as a prepass in
|
||||
pipelines that have to discard Emit operations.
|
||||
}];
|
||||
}
|
|
@ -1,4 +1,4 @@
|
|||
//===- Passes.h - OM dialect passes --------------------------------------===//
|
||||
//===- OMPasses.h - OM dialect passes -------------------------------------===//
|
||||
//
|
||||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
||||
// See https://llvm.org/LICENSE.txt for license information.
|
||||
|
@ -25,6 +25,7 @@ std::unique_ptr<mlir::Pass> createFreezePathsPass(
|
|||
std::function<StringAttr(Operation *)> getOpNameFallback = {});
|
||||
std::unique_ptr<mlir::Pass> createVerifyObjectFieldsPass();
|
||||
|
||||
#define GEN_PASS_DECL
|
||||
#define GEN_PASS_REGISTRATION
|
||||
#include "circt/Dialect/OM/OMPasses.h.inc"
|
||||
|
||||
|
|
|
@ -33,3 +33,11 @@ def VerifyObjectFields: Pass<"om-verify-object-fields"> {
|
|||
}];
|
||||
let constructor = "circt::om::createVerifyObjectFieldsPass()";
|
||||
}
|
||||
|
||||
def StripOMPass : Pass<"strip-om", "mlir::ModuleOp"> {
|
||||
let summary = "Remove OM information";
|
||||
let description = [{
|
||||
Removes all OM operations from the IR. Useful as a prepass in pipelines that
|
||||
have to discard OM.
|
||||
}];
|
||||
}
|
||||
|
|
|
@ -22,6 +22,7 @@
|
|||
#include "circt/Dialect/Comb/CombPasses.h"
|
||||
#include "circt/Dialect/DC/DCPasses.h"
|
||||
#include "circt/Dialect/ESI/ESIDialect.h"
|
||||
#include "circt/Dialect/Emit/EmitPasses.h"
|
||||
#include "circt/Dialect/FIRRTL/Passes.h"
|
||||
#include "circt/Dialect/FSM/FSMPasses.h"
|
||||
#include "circt/Dialect/HW/HWPasses.h"
|
||||
|
@ -64,24 +65,25 @@ inline void registerAllPasses() {
|
|||
calyx::registerPasses();
|
||||
comb::registerPasses();
|
||||
dc::registerPasses();
|
||||
emit::registerPasses();
|
||||
esi::registerESIPasses();
|
||||
firrtl::registerPasses();
|
||||
fsm::registerPasses();
|
||||
handshake::registerPasses();
|
||||
hw::registerPasses();
|
||||
kanagawa::registerPasses();
|
||||
llhd::registerPasses();
|
||||
moore::registerPasses();
|
||||
msft::registerPasses();
|
||||
om::registerPasses();
|
||||
seq::registerPasses();
|
||||
sv::registerPasses();
|
||||
handshake::registerPasses();
|
||||
kanagawa::registerPasses();
|
||||
rtg::registerPasses();
|
||||
hw::registerPasses();
|
||||
pipeline::registerPasses();
|
||||
rtg::registerPasses();
|
||||
seq::registerPasses();
|
||||
sim::registerPasses();
|
||||
ssp::registerPasses();
|
||||
sv::registerPasses();
|
||||
systemc::registerPasses();
|
||||
verif::registerPasses();
|
||||
moore::registerPasses();
|
||||
}
|
||||
|
||||
} // namespace circt
|
||||
|
|
|
@ -9,8 +9,6 @@
|
|||
#include "circt/Dialect/Arc/ArcOps.h"
|
||||
#include "circt/Dialect/Arc/ArcPasses.h"
|
||||
#include "circt/Dialect/Comb/CombOps.h"
|
||||
#include "circt/Dialect/Emit/EmitDialect.h"
|
||||
#include "circt/Dialect/OM/OMDialect.h"
|
||||
#include "circt/Dialect/SV/SVOps.h"
|
||||
#include "circt/Dialect/Seq/SeqOps.h"
|
||||
#include "mlir/IR/ImplicitLocOpBuilder.h"
|
||||
|
@ -76,11 +74,6 @@ void StripSVPass::runOnOperation() {
|
|||
LLVM_DEBUG(llvm::dbgs() << "Found " << clockGateModuleNames.size()
|
||||
<< " clock gates\n");
|
||||
|
||||
// Remove OM and Emit dialect nodes.
|
||||
for (auto &op : llvm::make_early_inc_range(*mlirModule.getBody()))
|
||||
if (isa<emit::EmitDialect, om::OMDialect>(op.getDialect()))
|
||||
op.erase();
|
||||
|
||||
// Remove `sv.*` operation attributes.
|
||||
mlirModule.walk([](Operation *op) {
|
||||
auto isSVAttr = [](NamedAttribute attr) {
|
||||
|
|
|
@ -1,13 +1,10 @@
|
|||
##===- CMakeLists.txt - build definitions for Emit ------------*- cmake -*-===//
|
||||
##===- CMakeLists.txt - Emit dialect build definitions --------------------===//
|
||||
##
|
||||
## Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
||||
## See https://llvm.org/LICENSE.txt for license information.
|
||||
## SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
##
|
||||
##===----------------------------------------------------------------------===//
|
||||
##
|
||||
##
|
||||
##===----------------------------------------------------------------------===//
|
||||
|
||||
add_circt_dialect_library(CIRCTEmit
|
||||
EmitDialect.cpp
|
||||
|
@ -29,3 +26,5 @@ add_circt_dialect_library(CIRCTEmit
|
|||
MLIRPass
|
||||
MLIRTransforms
|
||||
)
|
||||
|
||||
add_subdirectory(Transforms)
|
||||
|
|
|
@ -0,0 +1,13 @@
|
|||
add_circt_dialect_library(CIRCTEmitTransforms
|
||||
StripEmit.cpp
|
||||
|
||||
DEPENDS
|
||||
CIRCTEmitTransformsIncGen
|
||||
|
||||
LINK_LIBS PUBLIC
|
||||
CIRCTEmit
|
||||
CIRCTSupport
|
||||
MLIRIR
|
||||
MLIRPass
|
||||
MLIRTransformUtils
|
||||
)
|
|
@ -0,0 +1,36 @@
|
|||
//===- StripEmit.cpp ------------------------------------------------------===//
|
||||
//
|
||||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
||||
// See https://llvm.org/LICENSE.txt for license information.
|
||||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "circt/Dialect/Emit/EmitOps.h"
|
||||
#include "circt/Dialect/Emit/EmitPasses.h"
|
||||
#include "mlir/Pass/Pass.h"
|
||||
#include "llvm/Support/Debug.h"
|
||||
|
||||
namespace circt {
|
||||
namespace emit {
|
||||
#define GEN_PASS_DEF_STRIPEMITPASS
|
||||
#include "circt/Dialect/Emit/EmitPasses.h.inc"
|
||||
} // namespace emit
|
||||
} // namespace circt
|
||||
|
||||
using namespace mlir;
|
||||
using namespace circt;
|
||||
|
||||
namespace {
|
||||
struct StripEmitPass : public emit::impl::StripEmitPassBase<StripEmitPass> {
|
||||
void runOnOperation() override {
|
||||
for (auto &op : llvm::make_early_inc_range(getOperation().getOps())) {
|
||||
if (isa_and_nonnull<emit::EmitDialect>(op.getDialect())) {
|
||||
op.erase();
|
||||
continue;
|
||||
}
|
||||
op.removeAttr("emit.fragments");
|
||||
}
|
||||
}
|
||||
};
|
||||
} // namespace
|
|
@ -1,6 +1,7 @@
|
|||
add_circt_dialect_library(CIRCTOMTransforms
|
||||
FreezePaths.cpp
|
||||
LinkModules.cpp
|
||||
StripOM.cpp
|
||||
VerifyObjectFields.cpp
|
||||
|
||||
DEPENDS
|
||||
|
|
|
@ -0,0 +1,32 @@
|
|||
//===- StripOM.cpp --------------------------------------------------------===//
|
||||
//
|
||||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
||||
// See https://llvm.org/LICENSE.txt for license information.
|
||||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "circt/Dialect/OM/OMOps.h"
|
||||
#include "circt/Dialect/OM/OMPasses.h"
|
||||
#include "mlir/Pass/Pass.h"
|
||||
#include "llvm/Support/Debug.h"
|
||||
|
||||
namespace circt {
|
||||
namespace om {
|
||||
#define GEN_PASS_DEF_STRIPOMPASS
|
||||
#include "circt/Dialect/OM/OMPasses.h.inc"
|
||||
} // namespace om
|
||||
} // namespace circt
|
||||
|
||||
using namespace mlir;
|
||||
using namespace circt;
|
||||
|
||||
namespace {
|
||||
struct StripOMPass : public om::impl::StripOMPassBase<StripOMPass> {
|
||||
void runOnOperation() override {
|
||||
for (auto &op : llvm::make_early_inc_range(getOperation().getOps()))
|
||||
if (isa_and_nonnull<om::OMDialect>(op.getDialect()))
|
||||
op.erase();
|
||||
}
|
||||
};
|
||||
} // namespace
|
|
@ -26,6 +26,7 @@ set(CIRCT_TEST_DEPENDS
|
|||
circt-capi-rtg-test
|
||||
circt-capi-rtgtest-test
|
||||
circt-as
|
||||
circt-bmc
|
||||
circt-dis
|
||||
circt-lec
|
||||
circt-opt
|
||||
|
|
|
@ -0,0 +1,19 @@
|
|||
// RUN: circt-opt --strip-emit --allow-unregistered-dialect %s | FileCheck %s
|
||||
|
||||
// CHECK-NOT: emit.file
|
||||
emit.file "foo.sv" {}
|
||||
|
||||
// CHECK-NOT: emit.fragment
|
||||
emit.fragment @Bar {}
|
||||
|
||||
// CHECK-NOT: emit.file_list
|
||||
emit.file_list "baz.f", []
|
||||
|
||||
// CHECK: "some_unknown_dialect.op"
|
||||
"some_unknown_dialect.op"() {} : () -> ()
|
||||
|
||||
// CHECK: hw.module @Baz
|
||||
// CHECK-NOT: emit.fragments
|
||||
hw.module @Baz() attributes {emit.fragments = [@Bar]} {
|
||||
hw.output
|
||||
}
|
|
@ -0,0 +1,12 @@
|
|||
// RUN: circt-opt --strip-om --allow-unregistered-dialect %s | FileCheck %s
|
||||
|
||||
// CHECK-NOT: om.class
|
||||
om.class @Foo() {
|
||||
om.class.fields
|
||||
}
|
||||
|
||||
// CHECK-NOT: om.class.extern
|
||||
om.class.extern @Bar() {}
|
||||
|
||||
// CHECK: "some_unknown_dialect.op"
|
||||
"some_unknown_dialect.op"() {} : () -> ()
|
|
@ -0,0 +1,3 @@
|
|||
// RUN: circt-bmc --help | FileCheck %s
|
||||
|
||||
// CHECK: OVERVIEW: circt-bmc - bounded model checker
|
|
@ -0,0 +1,3 @@
|
|||
// RUN: circt-lec --help | FileCheck %s
|
||||
|
||||
// CHECK: OVERVIEW: circt-lec - logical equivalence checker
|
|
@ -9,21 +9,21 @@ set(LLVM_LINK_COMPONENTS Support ${ARCILATOR_JIT_LLVM_COMPONENTS})
|
|||
|
||||
set(libs
|
||||
CIRCTArc
|
||||
CIRCTHWTransforms
|
||||
CIRCTArcToLLVM
|
||||
CIRCTArcTransforms
|
||||
CIRCTCombToArith
|
||||
CIRCTConvertToArcs
|
||||
CIRCTEmit
|
||||
CIRCTEmitTransforms
|
||||
CIRCTExportArc
|
||||
CIRCTOM
|
||||
CIRCTHWTransforms
|
||||
CIRCTLLHD
|
||||
CIRCTVerif
|
||||
CIRCTOMTransforms
|
||||
CIRCTSeqToSV
|
||||
CIRCTSeqTransforms
|
||||
CIRCTSimTransforms
|
||||
CIRCTSupport
|
||||
CIRCTTransforms
|
||||
CIRCTVerif
|
||||
MLIRArithDialect
|
||||
MLIRBuiltinToLLVMIRTranslation
|
||||
MLIRControlFlowDialect
|
||||
|
|
|
@ -23,9 +23,11 @@
|
|||
#include "circt/Dialect/Arc/ModelInfoExport.h"
|
||||
#include "circt/Dialect/Comb/CombDialect.h"
|
||||
#include "circt/Dialect/Emit/EmitDialect.h"
|
||||
#include "circt/Dialect/Emit/EmitPasses.h"
|
||||
#include "circt/Dialect/HW/HWPasses.h"
|
||||
#include "circt/Dialect/LLHD/IR/LLHDDialect.h"
|
||||
#include "circt/Dialect/OM/OMDialect.h"
|
||||
#include "circt/Dialect/OM/OMPasses.h"
|
||||
#include "circt/Dialect/SV/SVDialect.h"
|
||||
#include "circt/Dialect/Seq/SeqPasses.h"
|
||||
#include "circt/Dialect/Sim/SimDialect.h"
|
||||
|
@ -252,6 +254,8 @@ static void populateHwModuleToArcPipeline(PassManager &pm) {
|
|||
// represented as intrinsic ops.
|
||||
if (untilReached(UntilPreprocessing))
|
||||
return;
|
||||
pm.addPass(om::createStripOMPass());
|
||||
pm.addPass(emit::createStripEmitPass());
|
||||
pm.addPass(createLowerFirMemPass());
|
||||
{
|
||||
arc::AddTapsOptions opts;
|
||||
|
|
|
@ -13,25 +13,27 @@ add_circt_tool(circt-bmc circt-bmc.cpp)
|
|||
target_link_libraries(circt-bmc
|
||||
PRIVATE
|
||||
CIRCTBMCTransforms
|
||||
CIRCTSMTToZ3LLVM
|
||||
CIRCTHWToSMT
|
||||
CIRCTCombToSMT
|
||||
CIRCTVerifToSMT
|
||||
CIRCTComb
|
||||
CIRCTCombToSMT
|
||||
CIRCTEmitTransforms
|
||||
CIRCTHW
|
||||
CIRCTHWToSMT
|
||||
CIRCTOMTransforms
|
||||
CIRCTSeq
|
||||
CIRCTSMT
|
||||
CIRCTVerif
|
||||
CIRCTSMTToZ3LLVM
|
||||
CIRCTSupport
|
||||
MLIRIR
|
||||
MLIRFuncDialect
|
||||
CIRCTVerif
|
||||
CIRCTVerifToSMT
|
||||
LLVMSupport
|
||||
MLIRArithDialect
|
||||
MLIRBuiltinToLLVMIRTranslation
|
||||
MLIRFuncDialect
|
||||
MLIRFuncInlinerExtension
|
||||
MLIRIR
|
||||
MLIRLLVMIRTransforms
|
||||
MLIRLLVMToLLVMIRTranslation
|
||||
MLIRTargetLLVMIRExport
|
||||
MLIRFuncInlinerExtension
|
||||
MLIRBuiltinToLLVMIRTranslation
|
||||
LLVMSupport
|
||||
|
||||
${CIRCT_BMC_JIT_DEPS}
|
||||
)
|
||||
|
|
|
@ -15,7 +15,11 @@
|
|||
#include "circt/Conversion/SMTToZ3LLVM.h"
|
||||
#include "circt/Conversion/VerifToSMT.h"
|
||||
#include "circt/Dialect/Comb/CombDialect.h"
|
||||
#include "circt/Dialect/Emit/EmitDialect.h"
|
||||
#include "circt/Dialect/Emit/EmitPasses.h"
|
||||
#include "circt/Dialect/HW/HWDialect.h"
|
||||
#include "circt/Dialect/OM/OMDialect.h"
|
||||
#include "circt/Dialect/OM/OMPasses.h"
|
||||
#include "circt/Dialect/SMT/SMTDialect.h"
|
||||
#include "circt/Dialect/Seq/SeqDialect.h"
|
||||
#include "circt/Dialect/Verif/VerifDialect.h"
|
||||
|
@ -168,6 +172,8 @@ static LogicalResult executeBMC(MLIRContext &context) {
|
|||
std::make_unique<VerbosePassInstrumentation<mlir::ModuleOp>>(
|
||||
"circt-bmc"));
|
||||
|
||||
pm.addPass(om::createStripOMPass());
|
||||
pm.addPass(emit::createStripEmitPass());
|
||||
pm.addPass(createExternalizeRegisters());
|
||||
LowerToBMCOptions lowerToBMCOptions;
|
||||
lowerToBMCOptions.bound = clockBound;
|
||||
|
@ -307,11 +313,21 @@ int main(int argc, char **argv) {
|
|||
|
||||
// Register the supported CIRCT dialects and create a context to work with.
|
||||
DialectRegistry registry;
|
||||
registry.insert<circt::comb::CombDialect, circt::hw::HWDialect,
|
||||
circt::seq::SeqDialect, circt::smt::SMTDialect,
|
||||
mlir::func::FuncDialect, circt::verif::VerifDialect,
|
||||
mlir::LLVM::LLVMDialect, mlir::arith::ArithDialect,
|
||||
mlir::BuiltinDialect>();
|
||||
// clang-format off
|
||||
registry.insert<
|
||||
circt::comb::CombDialect,
|
||||
circt::emit::EmitDialect,
|
||||
circt::hw::HWDialect,
|
||||
circt::om::OMDialect,
|
||||
circt::seq::SeqDialect,
|
||||
circt::smt::SMTDialect,
|
||||
circt::verif::VerifDialect,
|
||||
mlir::arith::ArithDialect,
|
||||
mlir::BuiltinDialect,
|
||||
mlir::func::FuncDialect,
|
||||
mlir::LLVM::LLVMDialect
|
||||
>();
|
||||
// clang-format on
|
||||
mlir::func::registerInlinerExtension(registry);
|
||||
mlir::registerBuiltinDialectTranslation(registry);
|
||||
mlir::registerLLVMDialectTranslation(registry);
|
||||
|
|
|
@ -12,26 +12,28 @@ set(LLVM_LINK_COMPONENTS Support ${CIRCT_LEC_JIT_LLVM_COMPONENTS})
|
|||
add_circt_tool(circt-lec circt-lec.cpp)
|
||||
target_link_libraries(circt-lec
|
||||
PRIVATE
|
||||
CIRCTLECTransforms
|
||||
CIRCTSMTToZ3LLVM
|
||||
CIRCTHWToSMT
|
||||
CIRCTCombToSMT
|
||||
CIRCTVerifToSMT
|
||||
CIRCTComb
|
||||
CIRCTCombToSMT
|
||||
CIRCTEmitTransforms
|
||||
CIRCTHW
|
||||
CIRCTHWToSMT
|
||||
CIRCTLECTransforms
|
||||
CIRCTOMTransforms
|
||||
CIRCTSMT
|
||||
CIRCTSMTToZ3LLVM
|
||||
CIRCTSupport
|
||||
CIRCTVerif
|
||||
MLIRIR
|
||||
MLIRFuncDialect
|
||||
CIRCTVerifToSMT
|
||||
LLVMSupport
|
||||
MLIRArithDialect
|
||||
MLIRBuiltinToLLVMIRTranslation
|
||||
MLIRFuncDialect
|
||||
MLIRFuncInlinerExtension
|
||||
MLIRIR
|
||||
MLIRLLVMIRTransforms
|
||||
MLIRLLVMToLLVMIRTranslation
|
||||
MLIRTargetLLVMIRExport
|
||||
MLIRFuncInlinerExtension
|
||||
MLIRBuiltinToLLVMIRTranslation
|
||||
MLIRLLVMToLLVMIRTranslation
|
||||
LLVMSupport
|
||||
MLIRTargetLLVMIRExport
|
||||
|
||||
${CIRCT_LEC_JIT_DEPS}
|
||||
)
|
||||
|
|
|
@ -17,7 +17,11 @@
|
|||
#include "circt/Conversion/SMTToZ3LLVM.h"
|
||||
#include "circt/Conversion/VerifToSMT.h"
|
||||
#include "circt/Dialect/Comb/CombDialect.h"
|
||||
#include "circt/Dialect/Emit/EmitDialect.h"
|
||||
#include "circt/Dialect/Emit/EmitPasses.h"
|
||||
#include "circt/Dialect/HW/HWDialect.h"
|
||||
#include "circt/Dialect/OM/OMDialect.h"
|
||||
#include "circt/Dialect/OM/OMPasses.h"
|
||||
#include "circt/Dialect/SMT/SMTDialect.h"
|
||||
#include "circt/Dialect/Verif/VerifDialect.h"
|
||||
#include "circt/Support/Passes.h"
|
||||
|
@ -217,10 +221,14 @@ static LogicalResult executeLEC(MLIRContext &context) {
|
|||
std::make_unique<VerbosePassInstrumentation<mlir::ModuleOp>>(
|
||||
"circt-lec"));
|
||||
|
||||
ConstructLECOptions constructLECOptions;
|
||||
constructLECOptions.firstModule = firstModuleName;
|
||||
constructLECOptions.secondModule = secondModuleName;
|
||||
pm.addPass(createConstructLEC(constructLECOptions));
|
||||
pm.addPass(om::createStripOMPass());
|
||||
pm.addPass(emit::createStripEmitPass());
|
||||
{
|
||||
ConstructLECOptions opts;
|
||||
opts.firstModule = firstModuleName;
|
||||
opts.secondModule = secondModuleName;
|
||||
pm.addPass(createConstructLEC(opts));
|
||||
}
|
||||
pm.addPass(createConvertHWToSMT());
|
||||
pm.addPass(createConvertCombToSMT());
|
||||
pm.addPass(createConvertVerifToSMT());
|
||||
|
@ -352,10 +360,20 @@ int main(int argc, char **argv) {
|
|||
|
||||
// Register the supported CIRCT dialects and create a context to work with.
|
||||
DialectRegistry registry;
|
||||
registry.insert<circt::comb::CombDialect, circt::hw::HWDialect,
|
||||
circt::smt::SMTDialect, circt::verif::VerifDialect,
|
||||
mlir::func::FuncDialect, mlir::LLVM::LLVMDialect,
|
||||
mlir::arith::ArithDialect, mlir::BuiltinDialect>();
|
||||
// clang-format off
|
||||
registry.insert<
|
||||
circt::comb::CombDialect,
|
||||
circt::emit::EmitDialect,
|
||||
circt::hw::HWDialect,
|
||||
circt::om::OMDialect,
|
||||
circt::smt::SMTDialect,
|
||||
circt::verif::VerifDialect,
|
||||
mlir::arith::ArithDialect,
|
||||
mlir::BuiltinDialect,
|
||||
mlir::func::FuncDialect,
|
||||
mlir::LLVM::LLVMDialect
|
||||
>();
|
||||
// clang-format on
|
||||
mlir::func::registerInlinerExtension(registry);
|
||||
mlir::registerBuiltinDialectTranslation(registry);
|
||||
mlir::registerLLVMDialectTranslation(registry);
|
||||
|
|
Loading…
Reference in New Issue