CIRCT  19.0.0git
HWToSMT.cpp
Go to the documentation of this file.
1 //===- HWToSMT.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 
10 #include "circt/Dialect/HW/HWOps.h"
12 #include "mlir/Analysis/TopologicalSortUtils.h"
13 #include "mlir/Dialect/Func/IR/FuncOps.h"
14 #include "mlir/Pass/Pass.h"
15 #include "mlir/Transforms/DialectConversion.h"
16 
17 namespace circt {
18 #define GEN_PASS_DEF_CONVERTHWTOSMT
19 #include "circt/Conversion/Passes.h.inc"
20 } // namespace circt
21 
22 using namespace circt;
23 using namespace hw;
24 
25 //===----------------------------------------------------------------------===//
26 // Conversion patterns
27 //===----------------------------------------------------------------------===//
28 
29 namespace {
30 /// Lower a hw::ConstantOp operation to smt::BVConstantOp
31 struct HWConstantOpConversion : OpConversionPattern<ConstantOp> {
33 
34  LogicalResult
35  matchAndRewrite(ConstantOp op, OpAdaptor adaptor,
36  ConversionPatternRewriter &rewriter) const override {
37  rewriter.replaceOpWithNewOp<smt::BVConstantOp>(op, adaptor.getValue());
38  return success();
39  }
40 };
41 
42 /// Lower a hw::HWModuleOp operation to func::FuncOp.
43 struct HWModuleOpConversion : OpConversionPattern<HWModuleOp> {
45 
46  LogicalResult
47  matchAndRewrite(HWModuleOp op, OpAdaptor adaptor,
48  ConversionPatternRewriter &rewriter) const override {
49  auto funcTy = op.getModuleType().getFuncType();
50  SmallVector<Type> inputTypes, resultTypes;
51  if (failed(typeConverter->convertTypes(funcTy.getInputs(), inputTypes)))
52  return failure();
53  if (failed(typeConverter->convertTypes(funcTy.getResults(), resultTypes)))
54  return failure();
55  if (failed(rewriter.convertRegionTypes(&op.getBody(), *typeConverter)))
56  return failure();
57  auto funcOp = rewriter.create<mlir::func::FuncOp>(
58  op.getLoc(), adaptor.getSymNameAttr(),
59  rewriter.getFunctionType(inputTypes, resultTypes));
60  rewriter.inlineRegionBefore(op.getBody(), funcOp.getBody(), funcOp.end());
61  rewriter.eraseOp(op);
62  return success();
63  }
64 };
65 
66 /// Lower a hw::OutputOp operation to func::ReturnOp.
67 struct OutputOpConversion : OpConversionPattern<OutputOp> {
69 
70  LogicalResult
71  matchAndRewrite(OutputOp op, OpAdaptor adaptor,
72  ConversionPatternRewriter &rewriter) const override {
73  rewriter.replaceOpWithNewOp<mlir::func::ReturnOp>(op, adaptor.getOutputs());
74  return success();
75  }
76 };
77 
78 /// Lower a hw::InstanceOp operation to func::CallOp.
79 struct InstanceOpConversion : OpConversionPattern<InstanceOp> {
81 
82  LogicalResult
83  matchAndRewrite(InstanceOp op, OpAdaptor adaptor,
84  ConversionPatternRewriter &rewriter) const override {
85  SmallVector<Type> resultTypes;
86  if (failed(typeConverter->convertTypes(op->getResultTypes(), resultTypes)))
87  return failure();
88 
89  rewriter.replaceOpWithNewOp<mlir::func::CallOp>(
90  op, adaptor.getModuleNameAttr(), resultTypes, adaptor.getInputs());
91  return success();
92  }
93 };
94 
95 } // namespace
96 
97 //===----------------------------------------------------------------------===//
98 // Convert HW to SMT pass
99 //===----------------------------------------------------------------------===//
100 
101 namespace {
102 struct ConvertHWToSMTPass
103  : public impl::ConvertHWToSMTBase<ConvertHWToSMTPass> {
104  void runOnOperation() override;
105 };
106 } // namespace
107 
108 void circt::populateHWToSMTTypeConverter(TypeConverter &converter) {
109  // The semantics of the builtin integer at the CIRCT core level is currently
110  // not very well defined. It is used for two-valued, four-valued, and possible
111  // other multi-valued logic. Here, we interpret it as two-valued for now.
112  // From a formal perspective, CIRCT would ideally define its own types for
113  // two-valued, four-valued, nine-valued (etc.) logic each. In MLIR upstream
114  // the integer type also carries poison information (which we don't have in
115  // CIRCT?).
116  converter.addConversion([](IntegerType type) -> std::optional<Type> {
117  if (type.getWidth() <= 0)
118  return std::nullopt;
119  return smt::BitVectorType::get(type.getContext(), type.getWidth());
120  });
121 
122  // Default target materialization to convert from illegal types to legal
123  // types, e.g., at the boundary of an inlined child block.
124  converter.addTargetMaterialization([&](OpBuilder &builder, Type resultType,
125  ValueRange inputs,
126  Location loc) -> std::optional<Value> {
127  return builder
128  .create<mlir::UnrealizedConversionCastOp>(loc, resultType, inputs)
129  ->getResult(0);
130  });
131 
132  // Convert a 'smt.bool'-typed value to a 'smt.bv<N>'-typed value
133  converter.addTargetMaterialization(
134  [&](OpBuilder &builder, smt::BitVectorType resultType, ValueRange inputs,
135  Location loc) -> std::optional<Value> {
136  if (inputs.size() != 1)
137  return std::nullopt;
138 
139  if (!isa<smt::BoolType>(inputs[0].getType()))
140  return std::nullopt;
141 
142  unsigned width = resultType.getWidth();
143  Value constZero = builder.create<smt::BVConstantOp>(loc, 0, width);
144  Value constOne = builder.create<smt::BVConstantOp>(loc, 1, width);
145  return builder.create<smt::IteOp>(loc, inputs[0], constOne, constZero);
146  });
147 
148  // Convert an unrealized conversion cast from 'smt.bool' to i1
149  // into a direct conversion from 'smt.bool' to 'smt.bv<1>'.
150  converter.addTargetMaterialization(
151  [&](OpBuilder &builder, smt::BitVectorType resultType, ValueRange inputs,
152  Location loc) -> std::optional<Value> {
153  if (inputs.size() != 1 || resultType.getWidth() != 1)
154  return std::nullopt;
155 
156  auto intType = dyn_cast<IntegerType>(inputs[0].getType());
157  if (!intType || intType.getWidth() != 1)
158  return std::nullopt;
159 
160  auto castOp =
161  inputs[0].getDefiningOp<mlir::UnrealizedConversionCastOp>();
162  if (!castOp || castOp.getInputs().size() != 1)
163  return std::nullopt;
164 
165  if (!isa<smt::BoolType>(castOp.getInputs()[0].getType()))
166  return std::nullopt;
167 
168  Value constZero = builder.create<smt::BVConstantOp>(loc, 0, 1);
169  Value constOne = builder.create<smt::BVConstantOp>(loc, 1, 1);
170  return builder.create<smt::IteOp>(loc, castOp.getInputs()[0], constOne,
171  constZero);
172  });
173 
174  // Convert a 'smt.bv<1>'-typed value to a 'smt.bool'-typed value
175  converter.addTargetMaterialization(
176  [&](OpBuilder &builder, smt::BoolType resultType, ValueRange inputs,
177  Location loc) -> std::optional<Value> {
178  if (inputs.size() != 1)
179  return std::nullopt;
180 
181  auto bvType = dyn_cast<smt::BitVectorType>(inputs[0].getType());
182  if (!bvType || bvType.getWidth() != 1)
183  return std::nullopt;
184 
185  Value constOne = builder.create<smt::BVConstantOp>(loc, 1, 1);
186  return builder.create<smt::EqOp>(loc, inputs[0], constOne);
187  });
188 
189  // Default source materialization to convert from illegal types to legal
190  // types, e.g., at the boundary of an inlined child block.
191  converter.addSourceMaterialization([&](OpBuilder &builder, Type resultType,
192  ValueRange inputs,
193  Location loc) -> std::optional<Value> {
194  return builder
195  .create<mlir::UnrealizedConversionCastOp>(loc, resultType, inputs)
196  ->getResult(0);
197  });
198 }
199 
200 void circt::populateHWToSMTConversionPatterns(TypeConverter &converter,
201  RewritePatternSet &patterns) {
202  patterns.add<HWConstantOpConversion, HWModuleOpConversion, OutputOpConversion,
203  InstanceOpConversion>(converter, patterns.getContext());
204 }
205 
206 void ConvertHWToSMTPass::runOnOperation() {
207  ConversionTarget target(getContext());
208  target.addIllegalDialect<hw::HWDialect>();
209  target.addLegalDialect<smt::SMTDialect>();
210  target.addLegalDialect<mlir::func::FuncDialect>();
211 
212  RewritePatternSet patterns(&getContext());
213  TypeConverter converter;
214  populateHWToSMTTypeConverter(converter);
216 
217  if (failed(mlir::applyPartialConversion(getOperation(), target,
218  std::move(patterns))))
219  return signalPassFailure();
220 
221  // Sort the functions topologically because 'hw.module' has a graph region
222  // while 'func.func' is a regular SSACFG region. Real combinational cycles or
223  // pseudo cycles through module instances are not supported yet.
224  for (auto func : getOperation().getOps<mlir::func::FuncOp>()) {
225  // Skip functions that are definitely not the result of lowering from
226  // 'hw.module'
227  if (func.getBody().getBlocks().size() != 1)
228  continue;
229 
230  mlir::sortTopologically(&func.getBody().front());
231  }
232 }
int32_t width
Definition: FIRRTL.cpp:36
llvm::SmallVector< StringAttr > inputs
Builder builder
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
void populateHWToSMTConversionPatterns(TypeConverter &converter, RewritePatternSet &patterns)
Get the HW to SMT conversion patterns.
Definition: HWToSMT.cpp:200
void populateHWToSMTTypeConverter(TypeConverter &converter)
Get the HW to SMT type conversions.
Definition: HWToSMT.cpp:108
Definition: hw.py:1