Loading [MathJax]/extensions/tex2jax.js
CIRCT 21.0.0git
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
VerifToSMT.cpp
Go to the documentation of this file.
1//===- VerifToSMT.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
14#include "mlir/Conversion/ReconcileUnrealizedCasts/ReconcileUnrealizedCasts.h"
15#include "mlir/Dialect/Arith/IR/Arith.h"
16#include "mlir/Dialect/Func/IR/FuncOps.h"
17#include "mlir/Dialect/SCF/IR/SCF.h"
18#include "mlir/Dialect/SMT/IR/SMTOps.h"
19#include "mlir/Dialect/SMT/IR/SMTTypes.h"
20#include "mlir/IR/ValueRange.h"
21#include "mlir/Pass/Pass.h"
22#include "mlir/Transforms/DialectConversion.h"
23#include "llvm/ADT/SmallVector.h"
24
25namespace circt {
26#define GEN_PASS_DEF_CONVERTVERIFTOSMT
27#include "circt/Conversion/Passes.h.inc"
28} // namespace circt
29
30using namespace mlir;
31using namespace circt;
32using namespace hw;
33
34//===----------------------------------------------------------------------===//
35// Conversion patterns
36//===----------------------------------------------------------------------===//
37
38namespace {
39/// Lower a verif::AssertOp operation with an i1 operand to a smt::AssertOp,
40/// negated to check for unsatisfiability.
41struct VerifAssertOpConversion : OpConversionPattern<verif::AssertOp> {
42 using OpConversionPattern<verif::AssertOp>::OpConversionPattern;
43
44 LogicalResult
45 matchAndRewrite(verif::AssertOp op, OpAdaptor adaptor,
46 ConversionPatternRewriter &rewriter) const override {
47 Value cond = typeConverter->materializeTargetConversion(
48 rewriter, op.getLoc(), smt::BoolType::get(getContext()),
49 adaptor.getProperty());
50 Value notCond = rewriter.create<smt::NotOp>(op.getLoc(), cond);
51 rewriter.replaceOpWithNewOp<smt::AssertOp>(op, notCond);
52 return success();
53 }
54};
55
56/// Lower a verif::AssumeOp operation with an i1 operand to a smt::AssertOp
57struct VerifAssumeOpConversion : OpConversionPattern<verif::AssumeOp> {
58 using OpConversionPattern<verif::AssumeOp>::OpConversionPattern;
59
60 LogicalResult
61 matchAndRewrite(verif::AssumeOp op, OpAdaptor adaptor,
62 ConversionPatternRewriter &rewriter) const override {
63 Value cond = typeConverter->materializeTargetConversion(
64 rewriter, op.getLoc(), smt::BoolType::get(getContext()),
65 adaptor.getProperty());
66 rewriter.replaceOpWithNewOp<smt::AssertOp>(op, cond);
67 return success();
68 }
69};
70
71/// Lower a verif::LecOp operation to a miter circuit encoded in SMT.
72/// More information on miter circuits can be found, e.g., in this paper:
73/// Brand, D., 1993, November. Verification of large synthesized designs. In
74/// Proceedings of 1993 International Conference on Computer Aided Design
75/// (ICCAD) (pp. 534-537). IEEE.
76struct LogicEquivalenceCheckingOpConversion
77 : OpConversionPattern<verif::LogicEquivalenceCheckingOp> {
79 verif::LogicEquivalenceCheckingOp>::OpConversionPattern;
80
81 LogicalResult
82 matchAndRewrite(verif::LogicEquivalenceCheckingOp op, OpAdaptor adaptor,
83 ConversionPatternRewriter &rewriter) const override {
84 Location loc = op.getLoc();
85 auto *firstOutputs = adaptor.getFirstCircuit().front().getTerminator();
86 auto *secondOutputs = adaptor.getSecondCircuit().front().getTerminator();
87
88 if (firstOutputs->getNumOperands() == 0) {
89 // Trivially equivalent
90 Value trueVal =
91 rewriter.create<arith::ConstantOp>(loc, rewriter.getBoolAttr(true));
92 rewriter.replaceOp(op, trueVal);
93 return success();
94 }
95
96 auto unusedResult = op.use_empty();
97
98 // Solver will only return a result when it is used to check the returned
99 // value.
100 smt::SolverOp solver;
101 if (unusedResult)
102 solver = rewriter.create<smt::SolverOp>(loc, TypeRange{}, ValueRange{});
103 else
104 solver = rewriter.create<smt::SolverOp>(loc, rewriter.getI1Type(),
105 ValueRange{});
106
107 rewriter.createBlock(&solver.getBodyRegion());
108
109 // First, convert the block arguments of the miter bodies.
110 if (failed(rewriter.convertRegionTypes(&adaptor.getFirstCircuit(),
111 *typeConverter)))
112 return failure();
113 if (failed(rewriter.convertRegionTypes(&adaptor.getSecondCircuit(),
114 *typeConverter)))
115 return failure();
116
117 // Second, create the symbolic values we replace the block arguments with
118 SmallVector<Value> inputs;
119 for (auto arg : adaptor.getFirstCircuit().getArguments())
120 inputs.push_back(rewriter.create<smt::DeclareFunOp>(loc, arg.getType()));
121
122 // Third, inline the blocks
123 // Note: the argument value replacement does not happen immediately, but
124 // only after all the operations are already legalized.
125 // Also, it has to be ensured that the original argument type and the type
126 // of the value with which is is to be replaced match. The value is looked
127 // up (transitively) in the replacement map at the time the replacement
128 // pattern is committed.
129 rewriter.mergeBlocks(&adaptor.getFirstCircuit().front(), solver.getBody(),
130 inputs);
131 rewriter.mergeBlocks(&adaptor.getSecondCircuit().front(), solver.getBody(),
132 inputs);
133 rewriter.setInsertionPointToEnd(solver.getBody());
134
135 // Fourth, convert the yielded values back to the source type system (since
136 // the operations of the inlined blocks will be converted by other patterns
137 // later on and we should make sure the IR is well-typed after each pattern
138 // application), and build the 'assert'.
139 SmallVector<Value> outputsDifferent;
140 for (auto [out1, out2] :
141 llvm::zip(firstOutputs->getOperands(), secondOutputs->getOperands())) {
142 Value o1 = typeConverter->materializeTargetConversion(
143 rewriter, loc, typeConverter->convertType(out1.getType()), out1);
144 Value o2 = typeConverter->materializeTargetConversion(
145 rewriter, loc, typeConverter->convertType(out1.getType()), out2);
146 outputsDifferent.emplace_back(
147 rewriter.create<smt::DistinctOp>(loc, o1, o2));
148 }
149
150 rewriter.eraseOp(firstOutputs);
151 rewriter.eraseOp(secondOutputs);
152
153 Value toAssert;
154 if (outputsDifferent.size() == 1)
155 toAssert = outputsDifferent[0];
156 else
157 toAssert = rewriter.create<smt::OrOp>(loc, outputsDifferent);
158
159 rewriter.create<smt::AssertOp>(loc, toAssert);
160
161 // Fifth, check for satisfiablility and report the result back.
162 // If no operation uses the result of this solver, we leave our check
163 // operations empty. If the result is used, we create a check operation with
164 // the result type of the operation and yield the result of the check
165 // operation.
166 if (unusedResult) {
167 auto checkOp = rewriter.create<smt::CheckOp>(loc, TypeRange{});
168 rewriter.createBlock(&checkOp.getSatRegion());
169 rewriter.create<smt::YieldOp>(loc);
170 rewriter.createBlock(&checkOp.getUnknownRegion());
171 rewriter.create<smt::YieldOp>(loc);
172 rewriter.createBlock(&checkOp.getUnsatRegion());
173 rewriter.create<smt::YieldOp>(loc);
174 rewriter.setInsertionPointAfter(checkOp);
175 rewriter.create<smt::YieldOp>(loc);
176
177 // Erase as operation is replaced by an operator without a return value.
178 rewriter.eraseOp(op);
179 } else {
180 Value falseVal =
181 rewriter.create<arith::ConstantOp>(loc, rewriter.getBoolAttr(false));
182 Value trueVal =
183 rewriter.create<arith::ConstantOp>(loc, rewriter.getBoolAttr(true));
184 auto checkOp = rewriter.create<smt::CheckOp>(loc, rewriter.getI1Type());
185 rewriter.createBlock(&checkOp.getSatRegion());
186 rewriter.create<smt::YieldOp>(loc, falseVal);
187 rewriter.createBlock(&checkOp.getUnknownRegion());
188 rewriter.create<smt::YieldOp>(loc, falseVal);
189 rewriter.createBlock(&checkOp.getUnsatRegion());
190 rewriter.create<smt::YieldOp>(loc, trueVal);
191 rewriter.setInsertionPointAfter(checkOp);
192 rewriter.create<smt::YieldOp>(loc, checkOp->getResults());
193
194 rewriter.replaceOp(op, solver->getResults());
195 }
196
197 return success();
198 }
199};
200
201/// Lower a verif::BMCOp operation to an MLIR program that performs the bounded
202/// model check
203struct VerifBoundedModelCheckingOpConversion
204 : OpConversionPattern<verif::BoundedModelCheckingOp> {
205 using OpConversionPattern<verif::BoundedModelCheckingOp>::OpConversionPattern;
206
207 VerifBoundedModelCheckingOpConversion(TypeConverter &converter,
208 MLIRContext *context, Namespace &names,
209 bool risingClocksOnly)
210 : OpConversionPattern(converter, context), names(names),
211 risingClocksOnly(risingClocksOnly) {}
212 LogicalResult
213 matchAndRewrite(verif::BoundedModelCheckingOp op, OpAdaptor adaptor,
214 ConversionPatternRewriter &rewriter) const override {
215 Location loc = op.getLoc();
216 SmallVector<Type> oldLoopInputTy(op.getLoop().getArgumentTypes());
217 SmallVector<Type> oldCircuitInputTy(op.getCircuit().getArgumentTypes());
218 // TODO: the init and loop regions should be able to be concrete instead of
219 // symbolic which is probably preferable - just need to convert back and
220 // forth
221 SmallVector<Type> loopInputTy, circuitInputTy, initOutputTy,
222 circuitOutputTy;
223 if (failed(typeConverter->convertTypes(oldLoopInputTy, loopInputTy)))
224 return failure();
225 if (failed(typeConverter->convertTypes(oldCircuitInputTy, circuitInputTy)))
226 return failure();
227 if (failed(typeConverter->convertTypes(
228 op.getInit().front().back().getOperandTypes(), initOutputTy)))
229 return failure();
230 if (failed(typeConverter->convertTypes(
231 op.getCircuit().front().back().getOperandTypes(), circuitOutputTy)))
232 return failure();
233 if (failed(rewriter.convertRegionTypes(&op.getInit(), *typeConverter)))
234 return failure();
235 if (failed(rewriter.convertRegionTypes(&op.getLoop(), *typeConverter)))
236 return failure();
237 if (failed(rewriter.convertRegionTypes(&op.getCircuit(), *typeConverter)))
238 return failure();
239
240 unsigned numRegs = op.getNumRegs();
241 auto initialValues = op.getInitialValues();
242
243 auto initFuncTy = rewriter.getFunctionType({}, initOutputTy);
244 // Loop and init output types are necessarily the same, so just use init
245 // output types
246 auto loopFuncTy = rewriter.getFunctionType(loopInputTy, initOutputTy);
247 auto circuitFuncTy =
248 rewriter.getFunctionType(circuitInputTy, circuitOutputTy);
249
250 func::FuncOp initFuncOp, loopFuncOp, circuitFuncOp;
251
252 {
253 OpBuilder::InsertionGuard guard(rewriter);
254 rewriter.setInsertionPointToEnd(
255 op->getParentOfType<ModuleOp>().getBody());
256 initFuncOp = rewriter.create<func::FuncOp>(loc, names.newName("bmc_init"),
257 initFuncTy);
258 rewriter.inlineRegionBefore(op.getInit(), initFuncOp.getFunctionBody(),
259 initFuncOp.end());
260 loopFuncOp = rewriter.create<func::FuncOp>(loc, names.newName("bmc_loop"),
261 loopFuncTy);
262 rewriter.inlineRegionBefore(op.getLoop(), loopFuncOp.getFunctionBody(),
263 loopFuncOp.end());
264 circuitFuncOp = rewriter.create<func::FuncOp>(
265 loc, names.newName("bmc_circuit"), circuitFuncTy);
266 rewriter.inlineRegionBefore(op.getCircuit(),
267 circuitFuncOp.getFunctionBody(),
268 circuitFuncOp.end());
269 auto funcOps = {&initFuncOp, &loopFuncOp, &circuitFuncOp};
270 // initOutputTy is the same as loop output types
271 auto outputTys = {initOutputTy, initOutputTy, circuitOutputTy};
272 for (auto [funcOp, outputTy] : llvm::zip(funcOps, outputTys)) {
273 auto operands = funcOp->getBody().front().back().getOperands();
274 rewriter.eraseOp(&funcOp->getFunctionBody().front().back());
275 rewriter.setInsertionPointToEnd(&funcOp->getBody().front());
276 SmallVector<Value> toReturn;
277 for (unsigned i = 0; i < outputTy.size(); ++i)
278 toReturn.push_back(typeConverter->materializeTargetConversion(
279 rewriter, loc, outputTy[i], operands[i]));
280 rewriter.create<func::ReturnOp>(loc, toReturn);
281 }
282 }
283
284 auto solver =
285 rewriter.create<smt::SolverOp>(loc, rewriter.getI1Type(), ValueRange{});
286 rewriter.createBlock(&solver.getBodyRegion());
287
288 // Call init func to get initial clock values
289 ValueRange initVals =
290 rewriter.create<func::CallOp>(loc, initFuncOp)->getResults();
291
292 // Initial push
293 rewriter.create<smt::PushOp>(loc, 1);
294
295 // InputDecls order should be <circuit arguments> <state arguments>
296 // <wasViolated>
297 // Get list of clock indexes in circuit args
298 size_t initIndex = 0;
299 SmallVector<Value> inputDecls;
300 SmallVector<int> clockIndexes;
301 for (auto [curIndex, oldTy, newTy] :
302 llvm::enumerate(oldCircuitInputTy, circuitInputTy)) {
303 if (isa<seq::ClockType>(oldTy)) {
304 inputDecls.push_back(initVals[initIndex++]);
305 clockIndexes.push_back(curIndex);
306 continue;
307 }
308 if (curIndex >= oldCircuitInputTy.size() - numRegs) {
309 auto initVal =
310 initialValues[curIndex - oldCircuitInputTy.size() + numRegs];
311 if (auto initIntAttr = dyn_cast<IntegerAttr>(initVal)) {
312 inputDecls.push_back(rewriter.create<smt::BVConstantOp>(
313 loc, initIntAttr.getValue().getSExtValue(),
314 cast<smt::BitVectorType>(newTy).getWidth()));
315 continue;
316 }
317 }
318 inputDecls.push_back(rewriter.create<smt::DeclareFunOp>(loc, newTy));
319 }
320
321 auto numStateArgs = initVals.size() - initIndex;
322 // Add the rest of the init vals (state args)
323 for (; initIndex < initVals.size(); ++initIndex)
324 inputDecls.push_back(initVals[initIndex]);
325
326 Value lowerBound =
327 rewriter.create<arith::ConstantOp>(loc, rewriter.getI32IntegerAttr(0));
328 Value step =
329 rewriter.create<arith::ConstantOp>(loc, rewriter.getI32IntegerAttr(1));
330 Value upperBound =
331 rewriter.create<arith::ConstantOp>(loc, adaptor.getBoundAttr());
332 Value constFalse =
333 rewriter.create<arith::ConstantOp>(loc, rewriter.getBoolAttr(false));
334 Value constTrue =
335 rewriter.create<arith::ConstantOp>(loc, rewriter.getBoolAttr(true));
336 inputDecls.push_back(constFalse); // wasViolated?
337
338 // TODO: swapping to a whileOp here would allow early exit once the property
339 // is violated
340 // Perform model check up to the provided bound
341 auto forOp = rewriter.create<scf::ForOp>(
342 loc, lowerBound, upperBound, step, inputDecls,
343 [&](OpBuilder &builder, Location loc, Value i, ValueRange iterArgs) {
344 // Drop existing assertions
345 builder.create<smt::PopOp>(loc, 1);
346 builder.create<smt::PushOp>(loc, 1);
347
348 // Execute the circuit
349 ValueRange circuitCallOuts =
350 builder
351 .create<func::CallOp>(
352 loc, circuitFuncOp,
353 iterArgs.take_front(circuitFuncOp.getNumArguments()))
354 ->getResults();
355 auto checkOp =
356 rewriter.create<smt::CheckOp>(loc, builder.getI1Type());
357 {
358 OpBuilder::InsertionGuard guard(builder);
359 builder.createBlock(&checkOp.getSatRegion());
360 builder.create<smt::YieldOp>(loc, constTrue);
361 builder.createBlock(&checkOp.getUnknownRegion());
362 builder.create<smt::YieldOp>(loc, constTrue);
363 builder.createBlock(&checkOp.getUnsatRegion());
364 builder.create<smt::YieldOp>(loc, constFalse);
365 }
366
367 Value violated = builder.create<arith::OrIOp>(
368 loc, checkOp.getResult(0), iterArgs.back());
369
370 // Call loop func to update clock & state arg values
371 SmallVector<Value> loopCallInputs;
372 // Fetch clock values to feed to loop
373 for (auto index : clockIndexes)
374 loopCallInputs.push_back(iterArgs[index]);
375 // Fetch state args to feed to loop
376 for (auto stateArg : iterArgs.drop_back().take_back(numStateArgs))
377 loopCallInputs.push_back(stateArg);
378 ValueRange loopVals =
379 builder.create<func::CallOp>(loc, loopFuncOp, loopCallInputs)
380 ->getResults();
381
382 size_t loopIndex = 0;
383 // Collect decls to yield at end of iteration
384 SmallVector<Value> newDecls;
385 for (auto [oldTy, newTy] :
386 llvm::zip(TypeRange(oldCircuitInputTy).drop_back(numRegs),
387 TypeRange(circuitInputTy).drop_back(numRegs))) {
388 if (isa<seq::ClockType>(oldTy))
389 newDecls.push_back(loopVals[loopIndex++]);
390 else
391 newDecls.push_back(builder.create<smt::DeclareFunOp>(loc, newTy));
392 }
393
394 // Only update the registers on a clock posedge unless in rising
395 // clocks only mode
396 // TODO: this will also need changing with multiple clocks - currently
397 // it only accounts for the one clock case.
398 if (clockIndexes.size() == 1) {
399 SmallVector<Value> regInputs = circuitCallOuts.take_back(numRegs);
400 if (risingClocksOnly) {
401 // In rising clocks only mode we don't need to worry about whether
402 // there was a posedge
403 newDecls.append(regInputs);
404 } else {
405 auto clockIndex = clockIndexes[0];
406 auto oldClock = iterArgs[clockIndex];
407 // The clock is necessarily the first value returned by the loop
408 // region
409 auto newClock = loopVals[0];
410 auto oldClockLow = builder.create<smt::BVNotOp>(loc, oldClock);
411 auto isPosedgeBV =
412 builder.create<smt::BVAndOp>(loc, oldClockLow, newClock);
413 // Convert posedge bv<1> to bool
414 auto trueBV = builder.create<smt::BVConstantOp>(loc, 1, 1);
415 auto isPosedge =
416 builder.create<smt::EqOp>(loc, isPosedgeBV, trueBV);
417 auto regStates =
418 iterArgs.take_front(circuitFuncOp.getNumArguments())
419 .take_back(numRegs);
420 SmallVector<Value> nextRegStates;
421 for (auto [regState, regInput] :
422 llvm::zip(regStates, regInputs)) {
423 // Create an ITE to calculate the next reg state
424 // TODO: we create a lot of ITEs here that will slow things down
425 // - these could be avoided by making init/loop regions concrete
426 nextRegStates.push_back(builder.create<smt::IteOp>(
427 loc, isPosedge, regInput, regState));
428 }
429 newDecls.append(nextRegStates);
430 }
431 }
432
433 // Add the rest of the loop state args
434 for (; loopIndex < loopVals.size(); ++loopIndex)
435 newDecls.push_back(loopVals[loopIndex]);
436
437 newDecls.push_back(violated);
438
439 builder.create<scf::YieldOp>(loc, newDecls);
440 });
441
442 Value res = rewriter.create<arith::XOrIOp>(loc, forOp->getResults().back(),
443 constTrue);
444 rewriter.create<smt::YieldOp>(loc, res);
445 rewriter.replaceOp(op, solver.getResults());
446 return success();
447 }
448
449 Namespace &names;
450 bool risingClocksOnly;
451};
452
453} // namespace
454
455//===----------------------------------------------------------------------===//
456// Convert Verif to SMT pass
457//===----------------------------------------------------------------------===//
458
459namespace {
460struct ConvertVerifToSMTPass
461 : public circt::impl::ConvertVerifToSMTBase<ConvertVerifToSMTPass> {
462 using Base::Base;
463 void runOnOperation() override;
464};
465} // namespace
466
468 RewritePatternSet &patterns,
469 Namespace &names,
470 bool risingClocksOnly) {
471 patterns.add<VerifAssertOpConversion, VerifAssumeOpConversion,
472 LogicEquivalenceCheckingOpConversion>(converter,
473 patterns.getContext());
474 patterns.add<VerifBoundedModelCheckingOpConversion>(
475 converter, patterns.getContext(), names, risingClocksOnly);
476}
477
478void ConvertVerifToSMTPass::runOnOperation() {
479 ConversionTarget target(getContext());
480 target.addIllegalDialect<verif::VerifDialect>();
481 target.addLegalDialect<smt::SMTDialect, arith::ArithDialect, scf::SCFDialect,
482 func::FuncDialect>();
483 target.addLegalOp<UnrealizedConversionCastOp>();
484
485 // Check BMC ops contain only one assertion (done outside pattern to avoid
486 // issues with whether assertions are/aren't lowered yet)
487 SymbolTable symbolTable(getOperation());
488 WalkResult assertionCheck = getOperation().walk(
489 [&](Operation *op) { // Check there is exactly one assertion and clock
490 if (auto bmcOp = dyn_cast<verif::BoundedModelCheckingOp>(op)) {
491 // We also currently don't support initial values on registers that
492 // don't have integer inputs.
493 auto regTypes = TypeRange(bmcOp.getCircuit().getArgumentTypes())
494 .take_back(bmcOp.getNumRegs());
495 for (auto [regType, initVal] :
496 llvm::zip(regTypes, bmcOp.getInitialValues())) {
497 if (!isa<IntegerType>(regType) && !isa<UnitAttr>(initVal)) {
498 op->emitError("initial values are currently only supported for "
499 "registers with integer types");
500 signalPassFailure();
501 return WalkResult::interrupt();
502 }
503 }
504 // Check only one clock is present in the circuit inputs
505 auto numClockArgs = 0;
506 for (auto argType : bmcOp.getCircuit().getArgumentTypes())
507 if (isa<seq::ClockType>(argType))
508 numClockArgs++;
509 // TODO: this can be removed once we have a way to associate reg
510 // ins/outs with clocks
511 if (numClockArgs > 1) {
512 op->emitError(
513 "only modules with one or zero clocks are currently supported");
514 return WalkResult::interrupt();
515 }
516 SmallVector<mlir::Operation *> worklist;
517 int numAssertions = 0;
518 op->walk([&](Operation *curOp) {
519 if (isa<verif::AssertOp>(curOp))
520 numAssertions++;
521 if (auto inst = dyn_cast<InstanceOp>(curOp))
522 worklist.push_back(symbolTable.lookup(inst.getModuleName()));
523 });
524 // TODO: probably negligible compared to actual model checking time
525 // but cacheing the assertion count of modules would speed this up
526 while (!worklist.empty()) {
527 auto *module = worklist.pop_back_val();
528 module->walk([&](Operation *curOp) {
529 if (isa<verif::AssertOp>(curOp))
530 numAssertions++;
531 if (auto inst = dyn_cast<InstanceOp>(curOp))
532 worklist.push_back(symbolTable.lookup(inst.getModuleName()));
533 });
534 if (numAssertions > 1)
535 break;
536 }
537 if (numAssertions > 1) {
538 op->emitError(
539 "bounded model checking problems with multiple assertions are "
540 "not yet "
541 "correctly handled - instead, you can assert the "
542 "conjunction of your assertions");
543 return WalkResult::interrupt();
544 }
545 }
546 return WalkResult::advance();
547 });
548 if (assertionCheck.wasInterrupted())
549 return signalPassFailure();
550 RewritePatternSet patterns(&getContext());
551 TypeConverter converter;
553
554 SymbolCache symCache;
555 symCache.addDefinitions(getOperation());
556 Namespace names;
557 names.add(symCache);
558
560 risingClocksOnly);
561
562 if (failed(mlir::applyPartialConversion(getOperation(), target,
563 std::move(patterns))))
564 return signalPassFailure();
565}
A namespace that is used to store existing names and generate new names in some scope within the IR.
Definition Namespace.h:30
void add(mlir::ModuleOp module)
Definition Namespace.h:48
void addDefinitions(mlir::Operation *top)
Populate the symbol cache with all symbol-defining operations within the 'top' operation.
Definition SymCache.cpp:23
Default symbol cache implementation; stores associations between names (StringAttr's) to mlir::Operat...
Definition SymCache.h:85
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
void populateVerifToSMTConversionPatterns(TypeConverter &converter, RewritePatternSet &patterns, Namespace &names, bool risingClocksOnly)
Get the Verif to SMT conversion patterns.
void populateHWToSMTTypeConverter(TypeConverter &converter)
Get the HW to SMT type conversions.
Definition HWToSMT.cpp:184
Definition hw.py:1
Definition seq.py:1