CIRCT  19.0.0git
PrepareForFormal.cpp
Go to the documentation of this file.
1 //===- PrepareForFormal.cpp - Formal Preparations --------------*- C++ -*--===//
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 // Prepare a circuit for the formal verification back-ends.
9 //
10 //===----------------------------------------------------------------------===//
11 
12 #include "circt/Dialect/HW/HWOps.h"
18 #include "circt/Support/Naming.h"
19 #include "mlir/Transforms/DialectConversion.h"
20 
21 #include "mlir/Pass/Pass.h"
22 
23 using namespace circt;
24 
25 namespace circt {
26 namespace verif {
27 #define GEN_PASS_DEF_PREPAREFORFORMAL
28 #include "circt/Dialect/Verif/Passes.h.inc"
29 } // namespace verif
30 } // namespace circt
31 
32 using namespace mlir;
33 using namespace verif;
34 
35 namespace {
36 /// Inline wires by unconditionally replacing them with their inputs
37 /// Wires create an alias for a set of operations, they are usually removed
38 /// through canonicalization at some point. Some wires are however
39 /// maintained.This pass unconditionally replaces all wires with their inputs,
40 /// making it easier to reason about in contexts where wires don't exist.
41 struct WireOpConversionPattern : OpConversionPattern<hw::WireOp> {
43 
44  LogicalResult
45  matchAndRewrite(hw::WireOp wire, OpAdaptor adaptor,
46  ConversionPatternRewriter &rewriter) const override {
47  rewriter.replaceOp(wire, adaptor.getInput());
48  return success();
49  }
50 };
51 
52 // Eagerly replace all wires with their inputs
53 struct PrepareForFormalPass
54  : circt::verif::impl::PrepareForFormalBase<PrepareForFormalPass> {
55  void runOnOperation() override;
56 };
57 } // namespace
58 
59 void PrepareForFormalPass::runOnOperation() {
60  // Set target: We don't want any wires left in our output
61  ConversionTarget target(getContext());
62  target.addLegalDialect<hw::HWDialect>();
63  target.addIllegalOp<hw::WireOp>();
64 
65  // Create the operation rewrite patters
66  RewritePatternSet patterns(&getContext());
67  patterns.add<WireOpConversionPattern>(patterns.getContext());
68 
69  // Apply the conversions
70  if (failed(
71  applyPartialConversion(getOperation(), target, std::move(patterns))))
72  return signalPassFailure();
73 }
74 
75 std::unique_ptr<mlir::Pass> circt::verif::createPrepareForFormalPass() {
76  return std::make_unique<PrepareForFormalPass>();
77 }
std::unique_ptr< mlir::Pass > createPrepareForFormalPass()
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
Definition: DebugAnalysis.h:21
Definition: verif.py:1