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"
32#define GEN_PASS_DEF_LOWERTOBMC
33#include "circt/Tools/circt-bmc/Passes.h.inc"
41struct LowerToBMCPass :
public circt::impl::LowerToBMCBase<LowerToBMCPass> {
42 using LowerToBMCBase::LowerToBMCBase;
43 void runOnOperation()
override;
47void LowerToBMCPass::runOnOperation() {
50 auto moduleOp = getOperation();
53 moduleOp.emitError(
"hw.module named '") << topModule <<
"' not found";
54 return signalPassFailure();
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();
64 if (!sortTopologically(&hwModule.getBodyRegion().front())) {
65 hwModule->emitError(
"could not resolve cycles in module");
66 return signalPassFailure();
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);
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();
86 auto entryFunc = builder.create<func::FuncOp>(
87 loc, topModule, builder.getFunctionType({}, {}));
88 builder.createBlock(&entryFunc.getBody());
91 OpBuilder::InsertionGuard guard(builder);
92 auto *terminator = hwModule.getBody().front().getTerminator();
93 builder.setInsertionPoint(terminator);
94 builder.create<verif::YieldOp>(loc, terminator->getOperands());
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();
111 bmcOp = builder.create<verif::BoundedModelCheckingOp>(
112 loc, risingClocksOnly ? bound : 2 * bound,
113 cast<IntegerAttr>(numRegs).getValue().getZExtValue(), initialValues);
115 hwModule->emitOpError(
"no num_regs or initial_values attribute found - "
116 "please run externalize "
117 "registers pass first");
118 return signalPassFailure();
125 for (
auto input : hwModule.getInputTypes()) {
126 if (isa<seq::ClockType>(input)) {
128 hwModule.emitError(
"designs with multiple clocks not yet supported");
129 return signalPassFailure();
133 if (
auto hwStruct = dyn_cast<hw::StructType>(input)) {
134 for (
auto field : hwStruct.getElements()) {
135 if (isa<seq::ClockType>(field.type)) {
138 "designs with multiple clocks not yet supported");
139 return signalPassFailure();
147 OpBuilder::InsertionGuard guard(builder);
150 auto *initBlock = builder.createBlock(&bmcOp.getInit());
151 builder.setInsertionPointToStart(initBlock);
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});
158 builder.create<verif::YieldOp>(loc, ValueRange{});
162 auto *loopBlock = builder.createBlock(&bmcOp.getLoop());
163 builder.setInsertionPointToStart(loopBlock);
165 loopBlock->addArgument(seq::ClockType::get(ctx), loc);
166 if (risingClocksOnly) {
168 builder.create<verif::YieldOp>(loc,
169 ValueRange{loopBlock->getArgument(0)});
172 builder.create<seq::FromClockOp>(loc, loopBlock->getArgument(0));
176 auto toClk = builder.create<seq::ToClockOp>(loc, nClk);
178 builder.create<verif::YieldOp>(loc, ValueRange{toClk});
181 builder.create<verif::YieldOp>(loc, ValueRange{});
184 bmcOp.getCircuit().takeBody(hwModule.getBody());
188 auto createUniqueStringGlobal = [&](StringRef str) -> FailureOr<Value> {
189 Location loc = moduleOp.getLoc();
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,
true, LLVM::linkage::Linkage::Private,
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();
203 builder.create<LLVM::AddressOfOp>(loc, global)->getResult(0));
206 auto successStrAddr =
207 createUniqueStringGlobal(
"Bound reached with no violations!\n");
208 auto failureStrAddr =
209 createUniqueStringGlobal(
"Assertion can be violated!\n");
211 if (failed(successStrAddr) || failed(failureStrAddr)) {
212 moduleOp->emitOpError(
"could not create result message strings");
213 return signalPassFailure();
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);
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{});
230 Value constZero = builder.create<LLVM::ConstantOp>(loc, i32Ty, 0);
231 builder.create<func::ReturnOp>(loc, constZero);
static SmallVector< T > concat(const SmallVectorImpl< T > &a, const SmallVectorImpl< T > &b)
Returns a new vector containing the concatenation of vectors a and b.
A namespace that is used to store existing names and generate new names in some scope within the IR.
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.