Loading [MathJax]/extensions/tex2jax.js
CIRCT 21.0.0git
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
LowerToBMC.cpp
Go to the documentation of this file.
1//===- LowerToBMC.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
15#include "circt/Support/LLVM.h"
18#include "mlir/Analysis/TopologicalSortUtils.h"
19#include "mlir/Dialect/Func/IR/FuncOps.h"
20#include "mlir/Dialect/LLVMIR/FunctionCallUtils.h"
21#include "mlir/Dialect/LLVMIR/LLVMDialect.h"
22#include "mlir/IR/Builders.h"
23#include "mlir/IR/Location.h"
24#include "mlir/IR/SymbolTable.h"
25#include "llvm/Support/LogicalResult.h"
26
27using namespace mlir;
28using namespace circt;
29using namespace hw;
30
31namespace circt {
32#define GEN_PASS_DEF_LOWERTOBMC
33#include "circt/Tools/circt-bmc/Passes.h.inc"
34} // namespace circt
35
36//===----------------------------------------------------------------------===//
37// Convert Lower To BMC pass
38//===----------------------------------------------------------------------===//
39
40namespace {
41struct LowerToBMCPass : public circt::impl::LowerToBMCBase<LowerToBMCPass> {
42 using LowerToBMCBase::LowerToBMCBase;
43 void runOnOperation() override;
44};
45} // namespace
46
47void LowerToBMCPass::runOnOperation() {
48 Namespace names;
49 // Fetch the 'hw.module' operation to model check.
50 auto moduleOp = getOperation();
51 auto hwModule = moduleOp.lookupSymbol<hw::HWModuleOp>(topModule);
52 if (!hwModule) {
53 moduleOp.emitError("hw.module named '") << topModule << "' not found";
54 return signalPassFailure();
55 }
56
57 // TODO: Check whether instances contain properties to check
58 if (hwModule.getOps<verif::AssertOp>().empty() &&
59 hwModule.getOps<hw::InstanceOp>().empty()) {
60 hwModule.emitError("no property provided to check in module");
61 return signalPassFailure();
62 }
63
64 if (!sortTopologically(&hwModule.getBodyRegion().front())) {
65 hwModule->emitError("could not resolve cycles in module");
66 return signalPassFailure();
67 }
68
69 // Create necessary function declarations and globals
70 auto *ctx = &getContext();
71 OpBuilder builder(ctx);
72 Location loc = moduleOp->getLoc();
73 builder.setInsertionPointToEnd(moduleOp.getBody());
74 auto ptrTy = LLVM::LLVMPointerType::get(ctx);
75 auto voidTy = LLVM::LLVMVoidType::get(ctx);
76
77 // Lookup or declare printf function.
78 auto printfFunc =
79 LLVM::lookupOrCreateFn(builder, moduleOp, "printf", ptrTy, voidTy, true);
80 if (failed(printfFunc)) {
81 moduleOp->emitError("failed to lookup or create printf");
82 return signalPassFailure();
83 }
84
85 // Replace the top-module with a function performing the BMC
86 auto entryFunc = builder.create<func::FuncOp>(
87 loc, topModule, builder.getFunctionType({}, {}));
88 builder.createBlock(&entryFunc.getBody());
89
90 {
91 OpBuilder::InsertionGuard guard(builder);
92 auto *terminator = hwModule.getBody().front().getTerminator();
93 builder.setInsertionPoint(terminator);
94 builder.create<verif::YieldOp>(loc, terminator->getOperands());
95 terminator->erase();
96 }
97
98 // Double the bound given to the BMC op unless in rising clocks only mode, as
99 // a clock cycle involves two negations
100 verif::BoundedModelCheckingOp bmcOp;
101 auto numRegs = hwModule->getAttrOfType<IntegerAttr>("num_regs");
102 auto initialValues = hwModule->getAttrOfType<ArrayAttr>("initial_values");
103 if (numRegs && initialValues) {
104 for (auto value : initialValues) {
105 if (!isa<IntegerAttr, UnitAttr>(value)) {
106 hwModule->emitError("initial_values attribute must contain only "
107 "integer or unit attributes");
108 return signalPassFailure();
109 }
110 }
111 bmcOp = builder.create<verif::BoundedModelCheckingOp>(
112 loc, risingClocksOnly ? bound : 2 * bound,
113 cast<IntegerAttr>(numRegs).getValue().getZExtValue(), initialValues);
114 } else {
115 hwModule->emitOpError("no num_regs or initial_values attribute found - "
116 "please run externalize "
117 "registers pass first");
118 return signalPassFailure();
119 }
120
121 // Check that there's only one clock input to the module
122 // TODO: supporting multiple clocks isn't too hard, an interleaving of clock
123 // toggles just needs to be generated
124 bool hasClk = false;
125 for (auto input : hwModule.getInputTypes()) {
126 if (isa<seq::ClockType>(input)) {
127 if (hasClk) {
128 hwModule.emitError("designs with multiple clocks not yet supported");
129 return signalPassFailure();
130 }
131 hasClk = true;
132 }
133 if (auto hwStruct = dyn_cast<hw::StructType>(input)) {
134 for (auto field : hwStruct.getElements()) {
135 if (isa<seq::ClockType>(field.type)) {
136 if (hasClk) {
137 hwModule.emitError(
138 "designs with multiple clocks not yet supported");
139 return signalPassFailure();
140 }
141 hasClk = true;
142 }
143 }
144 }
145 }
146 {
147 OpBuilder::InsertionGuard guard(builder);
148 // Initialize clock to 0 if it exists, otherwise just yield nothing
149 // We initialize to 1 if we're in rising clocks only mode
150 auto *initBlock = builder.createBlock(&bmcOp.getInit());
151 builder.setInsertionPointToStart(initBlock);
152 if (hasClk) {
153 auto initVal = builder.create<hw::ConstantOp>(loc, builder.getI1Type(),
154 risingClocksOnly ? 1 : 0);
155 auto toClk = builder.create<seq::ToClockOp>(loc, initVal);
156 builder.create<verif::YieldOp>(loc, ValueRange{toClk});
157 } else {
158 builder.create<verif::YieldOp>(loc, ValueRange{});
159 }
160
161 // Toggle clock in loop region if it exists, otherwise just yield nothing
162 auto *loopBlock = builder.createBlock(&bmcOp.getLoop());
163 builder.setInsertionPointToStart(loopBlock);
164 if (hasClk) {
165 loopBlock->addArgument(seq::ClockType::get(ctx), loc);
166 if (risingClocksOnly) {
167 // In rising clocks only mode we don't need to toggle the clock
168 builder.create<verif::YieldOp>(loc,
169 ValueRange{loopBlock->getArgument(0)});
170 } else {
171 auto fromClk =
172 builder.create<seq::FromClockOp>(loc, loopBlock->getArgument(0));
173 auto cNeg1 =
174 builder.create<hw::ConstantOp>(loc, builder.getI1Type(), -1);
175 auto nClk = builder.create<comb::XorOp>(loc, fromClk, cNeg1);
176 auto toClk = builder.create<seq::ToClockOp>(loc, nClk);
177 // Only yield clock value
178 builder.create<verif::YieldOp>(loc, ValueRange{toClk});
179 }
180 } else {
181 builder.create<verif::YieldOp>(loc, ValueRange{});
182 }
183 }
184 bmcOp.getCircuit().takeBody(hwModule.getBody());
185 hwModule->erase();
186
187 // Define global string constants to print on success/failure
188 auto createUniqueStringGlobal = [&](StringRef str) -> FailureOr<Value> {
189 Location loc = moduleOp.getLoc();
190
191 OpBuilder b = OpBuilder::atBlockEnd(moduleOp.getBody());
192 auto arrayTy = LLVM::LLVMArrayType::get(b.getI8Type(), str.size() + 1);
193 auto global = b.create<LLVM::GlobalOp>(
194 loc, arrayTy, /*isConstant=*/true, LLVM::linkage::Linkage::Private,
195 "resultString",
196 StringAttr::get(b.getContext(), Twine(str).concat(Twine('\00'))));
197 SymbolTable symTable(moduleOp);
198 if (failed(symTable.renameToUnique(global, {&symTable}))) {
199 return mlir::failure();
200 }
201
202 return success(
203 builder.create<LLVM::AddressOfOp>(loc, global)->getResult(0));
204 };
205
206 auto successStrAddr =
207 createUniqueStringGlobal("Bound reached with no violations!\n");
208 auto failureStrAddr =
209 createUniqueStringGlobal("Assertion can be violated!\n");
210
211 if (failed(successStrAddr) || failed(failureStrAddr)) {
212 moduleOp->emitOpError("could not create result message strings");
213 return signalPassFailure();
214 }
215
216 auto formatString = builder.create<LLVM::SelectOp>(
217 loc, bmcOp.getResult(), successStrAddr.value(), failureStrAddr.value());
218 builder.create<LLVM::CallOp>(loc, printfFunc.value(),
219 ValueRange{formatString});
220 builder.create<func::ReturnOp>(loc);
221
222 if (insertMainFunc) {
223 builder.setInsertionPointToEnd(getOperation().getBody());
224 Type i32Ty = builder.getI32Type();
225 auto mainFunc = builder.create<func::FuncOp>(
226 loc, "main", builder.getFunctionType({i32Ty, ptrTy}, {i32Ty}));
227 builder.createBlock(&mainFunc.getBody(), {}, {i32Ty, ptrTy}, {loc, loc});
228 builder.create<func::CallOp>(loc, entryFunc, ValueRange{});
229 // TODO: don't use LLVM here
230 Value constZero = builder.create<LLVM::ConstantOp>(loc, i32Ty, 0);
231 builder.create<func::ReturnOp>(loc, constZero);
232 }
233}
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
A namespace that is used to store existing names and generate new names in some scope within the IR.
Definition Namespace.h:30
create(data_type, value)
Definition hw.py:433
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
Definition hw.py:1