CIRCT  19.0.0git
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 
18 using namespace mlir;
19 using namespace circt;
20 using namespace hw;
21 
22 namespace 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 
31 namespace {
32 struct 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 };
38 } // namespace
39 
40 static Value lookupOrCreateStringGlobal(OpBuilder &builder, ModuleOp moduleOp,
41  StringRef str) {
42  Location loc = moduleOp.getLoc();
43  auto global = moduleOp.lookupSymbol<LLVM::GlobalOp>(str);
44  if (!global) {
45  OpBuilder b = OpBuilder::atBlockEnd(moduleOp.getBody());
46  auto arrayTy = LLVM::LLVMArrayType::get(b.getI8Type(), str.size() + 1);
47  global = b.create<LLVM::GlobalOp>(
48  loc, arrayTy, /*isConstant=*/true, LLVM::linkage::Linkage::Private, str,
49  StringAttr::get(b.getContext(), Twine(str).concat(Twine('\00'))));
50  }
51 
52  // FIXME: sanity check the fetched global: do all the attributes match what
53  // we expect?
54 
55  return builder.create<LLVM::AddressOfOp>(loc, global);
56 }
57 
58 hw::HWModuleOp ConstructLECPass::lookupModule(StringRef name) {
59  Operation *expectedModule = SymbolTable::lookupNearestSymbolFrom(
60  getOperation(), StringAttr::get(&getContext(), name));
61  if (!expectedModule || !isa<hw::HWModuleOp>(expectedModule)) {
62  getOperation().emitError("module named '") << name << "' not found";
63  return {};
64  }
65  return cast<hw::HWModuleOp>(expectedModule);
66 }
67 
68 void ConstructLECPass::runOnOperation() {
69  // Create necessary function declarations and globals
70  OpBuilder builder = OpBuilder::atBlockEnd(getOperation().getBody());
71  Location loc = getOperation()->getLoc();
72  auto ptrTy = LLVM::LLVMPointerType::get(builder.getContext());
73  auto voidTy = LLVM::LLVMVoidType::get(&getContext());
74 
75  // Lookup or declare printf function.
76  auto printfFunc =
77  LLVM::lookupOrCreateFn(getOperation(), "printf", ptrTy, voidTy, true);
78 
79  // Lookup the modules.
80  auto moduleA = lookupModule(firstModule);
81  if (!moduleA)
82  return signalPassFailure();
83  auto moduleB = lookupModule(secondModule);
84  if (!moduleB)
85  return signalPassFailure();
86 
87  if (moduleA.getModuleType() != moduleB.getModuleType()) {
88  moduleA.emitError("module's IO types don't match second modules: ")
89  << moduleA.getModuleType() << " vs " << moduleB.getModuleType();
90  return signalPassFailure();
91  }
92 
93  // Reuse the name of the first module for the entry function, so we don't have
94  // to do any uniquing and the LEC driver also already knows this name.
95  FunctionType functionType = FunctionType::get(&getContext(), {}, {});
96  func::FuncOp entryFunc =
97  builder.create<func::FuncOp>(loc, firstModule, functionType);
98 
99  if (insertMainFunc) {
100  OpBuilder::InsertionGuard guard(builder);
101  auto i32Ty = builder.getI32Type();
102  auto mainFunc = builder.create<func::FuncOp>(
103  loc, "main", builder.getFunctionType({i32Ty, ptrTy}, {i32Ty}));
104  builder.createBlock(&mainFunc.getBody(), {}, {i32Ty, ptrTy}, {loc, loc});
105  builder.create<func::CallOp>(loc, entryFunc, ValueRange{});
106  // TODO: don't use LLVM here
107  Value constZero = builder.create<LLVM::ConstantOp>(loc, i32Ty, 0);
108  builder.create<func::ReturnOp>(loc, constZero);
109  }
110 
111  builder.createBlock(&entryFunc.getBody());
112 
113  auto lecOp = builder.create<verif::LogicEquivalenceCheckingOp>(loc);
114  Value areEquivalent = lecOp.getAreEquivalent();
115  builder.cloneRegionBefore(moduleA.getBody(), lecOp.getFirstCircuit(),
116  lecOp.getFirstCircuit().end());
117  builder.cloneRegionBefore(moduleB.getBody(), lecOp.getSecondCircuit(),
118  lecOp.getSecondCircuit().end());
119 
120  moduleA->erase();
121  if (moduleA != moduleB)
122  moduleB->erase();
123 
124  {
125  auto *term = lecOp.getFirstCircuit().front().getTerminator();
126  OpBuilder::InsertionGuard guard(builder);
127  builder.setInsertionPoint(term);
128  builder.create<verif::YieldOp>(loc, term->getOperands());
129  term->erase();
130  term = lecOp.getSecondCircuit().front().getTerminator();
131  builder.setInsertionPoint(term);
132  builder.create<verif::YieldOp>(loc, term->getOperands());
133  term->erase();
134  }
135 
136  sortTopologically(&lecOp.getFirstCircuit().front());
137  sortTopologically(&lecOp.getSecondCircuit().front());
138 
139  // TODO: we should find a more elegant way of reporting the result than
140  // already inserting some LLVM here
141  Value eqFormatString =
142  lookupOrCreateStringGlobal(builder, getOperation(), "c1 == c2\n");
143  Value neqFormatString =
144  lookupOrCreateStringGlobal(builder, getOperation(), "c1 != c2\n");
145  Value formatString = builder.create<LLVM::SelectOp>(
146  loc, areEquivalent, eqFormatString, neqFormatString);
147  builder.create<LLVM::CallOp>(loc, printfFunc, ValueRange{formatString});
148 
149  builder.create<func::ReturnOp>(loc, ValueRange{});
150 }
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:539
static Value lookupOrCreateStringGlobal(OpBuilder &builder, ModuleOp moduleOp, StringRef str)
Builder builder
Direction get(bool isOutput)
Returns an output direction if isOutput is true, otherwise returns an input direction.
Definition: CalyxOps.cpp:54
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
Definition: DebugAnalysis.h:21
Definition: hw.py:1