Loading [MathJax]/extensions/tex2jax.js
CIRCT 22.0.0git
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ConstructLEC.cpp
Go to the documentation of this file.
1//===- ConstructLEC.cpp ---------------------------------------------------===//
2//
3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4// See https://llvm.org/LICENSE.txt for license information.
5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6//
7//===----------------------------------------------------------------------===//
8
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"
17
18using namespace mlir;
19using namespace circt;
20using namespace hw;
21
22namespace circt {
23#define GEN_PASS_DEF_CONSTRUCTLEC
24#include "circt/Tools/circt-lec/Passes.h.inc"
25} // namespace circt
26
27//===----------------------------------------------------------------------===//
28// ConstructLEC pass
29//===----------------------------------------------------------------------===//
30
31namespace {
32struct ConstructLECPass
33 : public circt::impl::ConstructLECBase<ConstructLECPass> {
34 using circt::impl::ConstructLECBase<ConstructLECPass>::ConstructLECBase;
35 void runOnOperation() override;
36 hw::HWModuleOp lookupModule(StringRef name);
37 Value constructMiter(OpBuilder builder, Location loc, hw::HWModuleOp moduleA,
38 hw::HWModuleOp moduleB, bool withResult);
39};
40} // namespace
41
42static Value lookupOrCreateStringGlobal(OpBuilder &builder, ModuleOp moduleOp,
43 StringRef str) {
44 Location loc = moduleOp.getLoc();
45 auto global = moduleOp.lookupSymbol<LLVM::GlobalOp>(str);
46 if (!global) {
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, /*isConstant=*/true, LLVM::linkage::Linkage::Private,
51 str, StringAttr::get(b.getContext(), Twine(str).concat(Twine('\00'))));
52 }
53
54 // FIXME: sanity check the fetched global: do all the attributes match what
55 // we expect?
56
57 return LLVM::AddressOfOp::create(builder, loc, global);
58}
59
60hw::HWModuleOp ConstructLECPass::lookupModule(StringRef name) {
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";
65 return {};
66 }
67 return cast<hw::HWModuleOp>(expectedModule);
68}
69
70Value ConstructLECPass::constructMiter(OpBuilder builder, Location loc,
71 hw::HWModuleOp moduleA,
72 hw::HWModuleOp moduleB,
73 bool withResult) {
74
75 // Create the miter circuit that return equivalence result.
76 auto lecOp =
77 verif::LogicEquivalenceCheckingOp::create(builder, loc, withResult);
78
79 builder.cloneRegionBefore(moduleA.getBody(), lecOp.getFirstCircuit(),
80 lecOp.getFirstCircuit().end());
81 builder.cloneRegionBefore(moduleB.getBody(), lecOp.getSecondCircuit(),
82 lecOp.getSecondCircuit().end());
83
84 moduleA->erase();
85 if (moduleA != moduleB)
86 moduleB->erase();
87
88 {
89 auto *term = lecOp.getFirstCircuit().front().getTerminator();
90 OpBuilder::InsertionGuard guard(builder);
91 builder.setInsertionPoint(term);
92 verif::YieldOp::create(builder, loc, term->getOperands());
93 term->erase();
94 term = lecOp.getSecondCircuit().front().getTerminator();
95 builder.setInsertionPoint(term);
96 verif::YieldOp::create(builder, loc, term->getOperands());
97 term->erase();
98 }
99
100 sortTopologically(&lecOp.getFirstCircuit().front());
101 sortTopologically(&lecOp.getSecondCircuit().front());
102
103 return withResult ? lecOp.getIsProven() : Value{};
104}
105
106void ConstructLECPass::runOnOperation() {
107 // Create necessary function declarations and globals
108 OpBuilder builder = OpBuilder::atBlockEnd(getOperation().getBody());
109 Location loc = getOperation()->getLoc();
110
111 // Lookup the modules.
112 auto moduleA = lookupModule(firstModule);
113 if (!moduleA)
114 return signalPassFailure();
115 auto moduleB = lookupModule(secondModule);
116 if (!moduleB)
117 return signalPassFailure();
118
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();
123 }
124
125 // Only construct the miter with no additional insertions.
126 if (insertMode == lec::InsertAdditionalModeEnum::None) {
127 constructMiter(builder, loc, moduleA, moduleB, /*withResult*/ false);
128 return;
129 }
130
131 mlir::FailureOr<mlir::LLVM::LLVMFuncOp> printfFunc;
132 auto ptrTy = LLVM::LLVMPointerType::get(builder.getContext());
133 auto voidTy = LLVM::LLVMVoidType::get(&getContext());
134 // Lookup or declare printf function.
135 printfFunc = LLVM::lookupOrCreateFn(builder, getOperation(), "printf", ptrTy,
136 voidTy, true);
137 if (failed(printfFunc)) {
138 getOperation()->emitError("failed to lookup or create printf");
139 return signalPassFailure();
140 }
141
142 // Reuse the name of the first module for the entry function, so we don't
143 // have to do any uniquing and the LEC driver also already knows this name.
144 FunctionType functionType = FunctionType::get(&getContext(), {}, {});
145 func::FuncOp entryFunc =
146 func::FuncOp::create(builder, loc, firstModule, functionType);
147
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{});
155 // TODO: don't use LLVM here
156 Value constZero = LLVM::ConstantOp::create(builder, loc, i32Ty, 0);
157 func::ReturnOp::create(builder, loc, constZero);
158 }
159
160 builder.createBlock(&entryFunc.getBody());
161
162 // Create the miter circuit that returns equivalence result.
163 auto areEquivalent =
164 constructMiter(builder, loc, moduleA, moduleB, /*withResult*/ true);
165 assert(!!areEquivalent && "Expected LEC operation with result.");
166
167 // TODO: we should find a more elegant way of reporting the result than
168 // already inserting some LLVM here
169 Value eqFormatString =
170 lookupOrCreateStringGlobal(builder, getOperation(), "c1 == c2\n");
171 Value neqFormatString =
172 lookupOrCreateStringGlobal(builder, getOperation(), "c1 != c2\n");
173 Value formatString = LLVM::SelectOp::create(builder, loc, areEquivalent,
174 eqFormatString, neqFormatString);
175 LLVM::CallOp::create(builder, loc, printfFunc.value(),
176 ValueRange{formatString});
177
178 func::ReturnOp::create(builder, loc, ValueRange{});
179}
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.
Definition CalyxOps.cpp:540
static Value lookupOrCreateStringGlobal(OpBuilder &builder, ModuleOp moduleOp, StringRef str)
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
Definition hw.py:1