12#include "mlir/Analysis/TopologicalSortUtils.h"
13#include "mlir/Dialect/Func/IR/FuncOps.h"
14#include "mlir/Dialect/LLVMIR/FunctionCallUtils.h"
15#include "mlir/Dialect/LLVMIR/LLVMDialect.h"
16#include "mlir/Transforms/DialectConversion.h"
23#define GEN_PASS_DEF_CONSTRUCTLEC
24#include "circt/Tools/circt-lec/Passes.h.inc"
32struct ConstructLECPass
33 :
public circt::impl::ConstructLECBase<ConstructLECPass> {
34 using circt::impl::ConstructLECBase<ConstructLECPass>::ConstructLECBase;
35 void runOnOperation()
override;
37 Value constructMiter(OpBuilder builder, Location loc,
hw::HWModuleOp moduleA,
44 Location loc = moduleOp.getLoc();
45 auto global = moduleOp.lookupSymbol<LLVM::GlobalOp>(str);
47 OpBuilder b = OpBuilder::atBlockEnd(moduleOp.getBody());
48 auto arrayTy = LLVM::LLVMArrayType::get(b.getI8Type(), str.size() + 1);
49 global = LLVM::GlobalOp::create(
50 b, loc, arrayTy,
true, LLVM::linkage::Linkage::Private,
51 str, StringAttr::get(b.getContext(), Twine(str).
concat(Twine(
'\00'))));
57 return LLVM::AddressOfOp::create(builder, loc, global);
61 Operation *expectedModule = SymbolTable::lookupNearestSymbolFrom(
62 getOperation(), StringAttr::get(&getContext(), name));
63 if (!expectedModule || !isa<hw::HWModuleOp>(expectedModule)) {
64 getOperation().emitError(
"module named '") << name <<
"' not found";
67 return cast<hw::HWModuleOp>(expectedModule);
70Value ConstructLECPass::constructMiter(OpBuilder builder, Location loc,
77 verif::LogicEquivalenceCheckingOp::create(builder, loc, withResult);
79 builder.cloneRegionBefore(moduleA.getBody(), lecOp.getFirstCircuit(),
80 lecOp.getFirstCircuit().end());
81 builder.cloneRegionBefore(moduleB.getBody(), lecOp.getSecondCircuit(),
82 lecOp.getSecondCircuit().end());
85 if (moduleA != moduleB)
89 auto *term = lecOp.getFirstCircuit().front().getTerminator();
90 OpBuilder::InsertionGuard guard(builder);
91 builder.setInsertionPoint(term);
92 verif::YieldOp::create(builder, loc, term->getOperands());
94 term = lecOp.getSecondCircuit().front().getTerminator();
95 builder.setInsertionPoint(term);
96 verif::YieldOp::create(builder, loc, term->getOperands());
100 sortTopologically(&lecOp.getFirstCircuit().front());
101 sortTopologically(&lecOp.getSecondCircuit().front());
103 return withResult ? lecOp.getIsProven() : Value{};
106void ConstructLECPass::runOnOperation() {
108 OpBuilder builder = OpBuilder::atBlockEnd(getOperation().getBody());
109 Location loc = getOperation()->getLoc();
112 auto moduleA = lookupModule(firstModule);
114 return signalPassFailure();
115 auto moduleB = lookupModule(secondModule);
117 return signalPassFailure();
119 if (moduleA.getModuleType() != moduleB.getModuleType()) {
120 moduleA.emitError(
"module's IO types don't match second modules: ")
121 << moduleA.getModuleType() <<
" vs " << moduleB.getModuleType();
122 return signalPassFailure();
126 if (insertMode == lec::InsertAdditionalModeEnum::None) {
127 constructMiter(builder, loc, moduleA, moduleB,
false);
131 mlir::FailureOr<mlir::LLVM::LLVMFuncOp> printfFunc;
132 auto ptrTy = LLVM::LLVMPointerType::get(builder.getContext());
133 auto voidTy = LLVM::LLVMVoidType::get(&getContext());
135 printfFunc = LLVM::lookupOrCreateFn(builder, getOperation(),
"printf", ptrTy,
137 if (failed(printfFunc)) {
138 getOperation()->emitError(
"failed to lookup or create printf");
139 return signalPassFailure();
144 FunctionType functionType = FunctionType::get(&getContext(), {}, {});
145 func::FuncOp entryFunc =
146 func::FuncOp::create(builder, loc, firstModule, functionType);
148 if (insertMode == lec::InsertAdditionalModeEnum::Main) {
149 OpBuilder::InsertionGuard guard(builder);
150 auto i32Ty = builder.getI32Type();
151 auto mainFunc = func::FuncOp::create(
152 builder, loc,
"main", builder.getFunctionType({i32Ty, ptrTy}, {i32Ty}));
153 builder.createBlock(&mainFunc.getBody(), {}, {i32Ty, ptrTy}, {loc, loc});
154 func::CallOp::create(builder, loc, entryFunc, ValueRange{});
156 Value constZero = LLVM::ConstantOp::create(builder, loc, i32Ty, 0);
157 func::ReturnOp::create(builder, loc, constZero);
160 builder.createBlock(&entryFunc.getBody());
164 constructMiter(builder, loc, moduleA, moduleB,
true);
165 assert(!!areEquivalent &&
"Expected LEC operation with result.");
169 Value eqFormatString =
171 Value neqFormatString =
173 Value formatString = LLVM::SelectOp::create(builder, loc, areEquivalent,
174 eqFormatString, neqFormatString);
175 LLVM::CallOp::create(builder, loc, printfFunc.value(),
176 ValueRange{formatString});
178 func::ReturnOp::create(builder, loc, ValueRange{});
assert(baseType &&"element must be base type")
static SmallVector< T > concat(const SmallVectorImpl< T > &a, const SmallVectorImpl< T > &b)
Returns a new vector containing the concatenation of vectors a and b.
static Value lookupOrCreateStringGlobal(OpBuilder &builder, ModuleOp moduleOp, StringRef str)
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.