CIRCT  19.0.0git
LTLToCore.cpp
Go to the documentation of this file.
1 //===- LTLToCore.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 //
9 // Converts LTL and Verif operations to Core operations
10 //
11 //===----------------------------------------------------------------------===//
12 
16 #include "circt/Dialect/HW/HWOps.h"
20 #include "circt/Dialect/SV/SVOps.h"
25 #include "mlir/Dialect/Func/IR/FuncOps.h"
26 #include "mlir/Dialect/LLVMIR/LLVMDialect.h"
27 #include "mlir/Dialect/SCF/IR/SCF.h"
28 #include "mlir/Pass/Pass.h"
29 #include "mlir/Transforms/DialectConversion.h"
30 #include "llvm/Support/MathExtras.h"
31 
32 namespace circt {
33 #define GEN_PASS_DEF_LOWERLTLTOCORE
34 #include "circt/Conversion/Passes.h.inc"
35 } // namespace circt
36 
37 using namespace mlir;
38 using namespace circt;
39 using namespace hw;
40 
41 //===----------------------------------------------------------------------===//
42 // Conversion patterns
43 //===----------------------------------------------------------------------===//
44 
45 namespace {
46 struct HasBeenResetOpConversion : OpConversionPattern<verif::HasBeenResetOp> {
48 
49  // HasBeenReset generates a 1 bit register that is set to one once the reset
50  // has been raised and lowered at at least once.
51  LogicalResult
52  matchAndRewrite(verif::HasBeenResetOp op, OpAdaptor adaptor,
53  ConversionPatternRewriter &rewriter) const override {
54  auto i1 = rewriter.getI1Type();
55  // Generate the constant used to set the register value
56  Value constZero = rewriter.create<hw::ConstantOp>(op.getLoc(), i1, 0);
57 
58  // Generate the constant used to enegate the
59  Value constOne = rewriter.create<hw::ConstantOp>(op.getLoc(), i1, 1);
60 
61  // Create a backedge for the register to be used in the OrOp
62  circt::BackedgeBuilder bb(rewriter, op.getLoc());
63  circt::Backedge reg = bb.get(rewriter.getI1Type());
64 
65  // Generate an or between the reset and the register's value to store
66  // whether or not the reset has been active at least once
67  Value orReset =
68  rewriter.create<comb::OrOp>(op.getLoc(), adaptor.getReset(), reg);
69 
70  // This register should not be reset, so we give it dummy reset and resetval
71  // operands to fit the build signature
72  Value reset, resetval;
73 
74  // Finally generate the register to set the backedge
75  reg.setValue(rewriter.create<seq::CompRegOp>(
76  op.getLoc(), orReset,
77  rewriter.createOrFold<seq::ToClockOp>(op.getLoc(), adaptor.getClock()),
78  rewriter.getStringAttr("hbr"), reset, resetval, constZero,
79  InnerSymAttr{} // inner_sym
80  ));
81 
82  // We also need to consider the case where we are currently in a reset cycle
83  // in which case our hbr register should be down-
84  // Practically this means converting it to (and hbr (not reset))
85  Value notReset =
86  rewriter.create<comb::XorOp>(op.getLoc(), adaptor.getReset(), constOne);
87  rewriter.replaceOpWithNewOp<comb::AndOp>(op, reg, notReset);
88 
89  return success();
90  }
91 };
92 
93 } // namespace
94 
95 //===----------------------------------------------------------------------===//
96 // Lower LTL To Core pass
97 //===----------------------------------------------------------------------===//
98 
99 namespace {
100 struct LowerLTLToCorePass
101  : public circt::impl::LowerLTLToCoreBase<LowerLTLToCorePass> {
102  LowerLTLToCorePass() = default;
103  void runOnOperation() override;
104 };
105 } // namespace
106 
107 // Simply applies the conversion patterns defined above
108 void LowerLTLToCorePass::runOnOperation() {
109 
110  // Set target dialects: We don't want to see any ltl or verif that might
111  // come from an AssertProperty left in the result
112  ConversionTarget target(getContext());
113  target.addLegalDialect<hw::HWDialect>();
114  target.addLegalDialect<comb::CombDialect>();
115  target.addLegalDialect<sv::SVDialect>();
116  target.addLegalDialect<seq::SeqDialect>();
117  target.addLegalDialect<ltl::LTLDialect>();
118  target.addLegalDialect<verif::VerifDialect>();
119  target.addIllegalOp<verif::HasBeenResetOp>();
120 
121  // Create type converters, mostly just to convert an ltl property to a bool
122  mlir::TypeConverter converter;
123 
124  // Convert the ltl property type to a built-in type
125  converter.addConversion([](IntegerType type) { return type; });
126  converter.addConversion([](ltl::PropertyType type) {
127  return IntegerType::get(type.getContext(), 1);
128  });
129  converter.addConversion([](ltl::SequenceType type) {
130  return IntegerType::get(type.getContext(), 1);
131  });
132 
133  // Basic materializations
134  converter.addTargetMaterialization(
135  [&](mlir::OpBuilder &builder, mlir::Type resultType,
136  mlir::ValueRange inputs,
137  mlir::Location loc) -> std::optional<mlir::Value> {
138  if (inputs.size() != 1)
139  return std::nullopt;
140  return inputs[0];
141  });
142 
143  converter.addSourceMaterialization(
144  [&](mlir::OpBuilder &builder, mlir::Type resultType,
145  mlir::ValueRange inputs,
146  mlir::Location loc) -> std::optional<mlir::Value> {
147  if (inputs.size() != 1)
148  return std::nullopt;
149  return inputs[0];
150  });
151 
152  // Create the operation rewrite patters
153  RewritePatternSet patterns(&getContext());
154  patterns.add<HasBeenResetOpConversion>(converter, patterns.getContext());
155 
156  // Apply the conversions
157  if (failed(
158  applyPartialConversion(getOperation(), target, std::move(patterns))))
159  return signalPassFailure();
160 }
161 
162 // Basic default constructor
163 std::unique_ptr<mlir::Pass> circt::createLowerLTLToCorePass() {
164  return std::make_unique<LowerLTLToCorePass>();
165 }
llvm::SmallVector< StringAttr > inputs
Builder builder
Instantiate one of these and use it to build typed backedges.
Backedge is a wrapper class around a Value.
def create(data_type, value)
Definition: hw.py:393
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
std::unique_ptr< mlir::Pass > createLowerLTLToCorePass()
Definition: LTLToCore.cpp:163
Definition: hw.py:1
def reg(value, clock, reset=None, reset_value=None, name=None, sym_name=None)
Definition: seq.py:20