Loading [MathJax]/extensions/tex2jax.js
CIRCT 22.0.0git
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
CombToSMT.cpp
Go to the documentation of this file.
1//===- CombToSMT.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
13#include "mlir/Dialect/Func/IR/FuncOps.h"
14#include "mlir/Dialect/SMT/IR/SMTOps.h"
15#include "mlir/Pass/Pass.h"
16#include "mlir/Transforms/DialectConversion.h"
17
18namespace circt {
19#define GEN_PASS_DEF_CONVERTCOMBTOSMT
20#include "circt/Conversion/Passes.h.inc"
21} // namespace circt
22
23using namespace mlir;
24using namespace circt;
25using namespace comb;
26
27//===----------------------------------------------------------------------===//
28// Conversion patterns
29//===----------------------------------------------------------------------===//
30
31namespace {
32/// Lower a comb::ReplicateOp operation to smt::RepeatOp
33struct CombReplicateOpConversion : OpConversionPattern<ReplicateOp> {
35
36 LogicalResult
37 matchAndRewrite(ReplicateOp op, OpAdaptor adaptor,
38 ConversionPatternRewriter &rewriter) const override {
39 rewriter.replaceOpWithNewOp<smt::RepeatOp>(op, op.getMultiple(),
40 adaptor.getInput());
41 return success();
42 }
43};
44
45/// Lower a comb::ICmpOp operation to a smt::BVCmpOp, smt::EqOp or
46/// smt::DistinctOp
47struct IcmpOpConversion : OpConversionPattern<ICmpOp> {
49
50 LogicalResult
51 matchAndRewrite(ICmpOp op, OpAdaptor adaptor,
52 ConversionPatternRewriter &rewriter) const override {
53 if (adaptor.getPredicate() == ICmpPredicate::weq ||
54 adaptor.getPredicate() == ICmpPredicate::ceq ||
55 adaptor.getPredicate() == ICmpPredicate::wne ||
56 adaptor.getPredicate() == ICmpPredicate::cne)
57 return rewriter.notifyMatchFailure(op,
58 "comparison predicate not supported");
59
60 Value result;
61 if (adaptor.getPredicate() == ICmpPredicate::eq) {
62 result = rewriter.create<smt::EqOp>(op.getLoc(), adaptor.getLhs(),
63 adaptor.getRhs());
64 } else if (adaptor.getPredicate() == ICmpPredicate::ne) {
65 result = rewriter.create<smt::DistinctOp>(op.getLoc(), adaptor.getLhs(),
66 adaptor.getRhs());
67 } else {
68 smt::BVCmpPredicate pred;
69 switch (adaptor.getPredicate()) {
70 case ICmpPredicate::sge:
71 pred = smt::BVCmpPredicate::sge;
72 break;
73 case ICmpPredicate::sgt:
74 pred = smt::BVCmpPredicate::sgt;
75 break;
76 case ICmpPredicate::sle:
77 pred = smt::BVCmpPredicate::sle;
78 break;
79 case ICmpPredicate::slt:
80 pred = smt::BVCmpPredicate::slt;
81 break;
82 case ICmpPredicate::uge:
83 pred = smt::BVCmpPredicate::uge;
84 break;
85 case ICmpPredicate::ugt:
86 pred = smt::BVCmpPredicate::ugt;
87 break;
88 case ICmpPredicate::ule:
89 pred = smt::BVCmpPredicate::ule;
90 break;
91 case ICmpPredicate::ult:
92 pred = smt::BVCmpPredicate::ult;
93 break;
94 default:
95 llvm_unreachable("all cases handled above");
96 }
97
98 result = rewriter.create<smt::BVCmpOp>(
99 op.getLoc(), pred, adaptor.getLhs(), adaptor.getRhs());
100 }
101
102 Value convVal = typeConverter->materializeTargetConversion(
103 rewriter, op.getLoc(), typeConverter->convertType(op.getType()),
104 result);
105 if (!convVal)
106 return failure();
107
108 rewriter.replaceOp(op, convVal);
109 return success();
110 }
111};
112
113/// Lower a comb::ExtractOp operation to an smt::ExtractOp
114struct ExtractOpConversion : OpConversionPattern<ExtractOp> {
116
117 LogicalResult
118 matchAndRewrite(ExtractOp op, OpAdaptor adaptor,
119 ConversionPatternRewriter &rewriter) const override {
120
121 rewriter.replaceOpWithNewOp<smt::ExtractOp>(
122 op, typeConverter->convertType(op.getResult().getType()),
123 adaptor.getLowBitAttr(), adaptor.getInput());
124 return success();
125 }
126};
127
128/// Lower a comb::MuxOp operation to an smt::IteOp
129struct MuxOpConversion : OpConversionPattern<MuxOp> {
131
132 LogicalResult
133 matchAndRewrite(MuxOp op, OpAdaptor adaptor,
134 ConversionPatternRewriter &rewriter) const override {
135 Value condition = typeConverter->materializeTargetConversion(
136 rewriter, op.getLoc(), smt::BoolType::get(getContext()),
137 adaptor.getCond());
138 rewriter.replaceOpWithNewOp<smt::IteOp>(
139 op, condition, adaptor.getTrueValue(), adaptor.getFalseValue());
140 return success();
141 }
142};
143
144/// Lower a comb::SubOp operation to an smt::BVNegOp + smt::BVAddOp
145struct SubOpConversion : OpConversionPattern<SubOp> {
147
148 LogicalResult
149 matchAndRewrite(SubOp op, OpAdaptor adaptor,
150 ConversionPatternRewriter &rewriter) const override {
151 Value negRhs = rewriter.create<smt::BVNegOp>(op.getLoc(), adaptor.getRhs());
152 rewriter.replaceOpWithNewOp<smt::BVAddOp>(op, adaptor.getLhs(), negRhs);
153 return success();
154 }
155};
156
157/// Lower a comb::ParityOp operation to a chain of smt::Extract + XOr ops
158struct ParityOpConversion : OpConversionPattern<ParityOp> {
160
161 LogicalResult
162 matchAndRewrite(ParityOp op, OpAdaptor adaptor,
163 ConversionPatternRewriter &rewriter) const override {
164 Location loc = op.getLoc();
165 unsigned bitwidth =
166 cast<smt::BitVectorType>(adaptor.getInput().getType()).getWidth();
167
168 // Note: the SMT bitvector type does not support 0 bitwidth vectors and thus
169 // the type conversion should already fail.
170 Type oneBitTy = smt::BitVectorType::get(getContext(), 1);
171 Value runner =
172 rewriter.create<smt::ExtractOp>(loc, oneBitTy, 0, adaptor.getInput());
173 for (unsigned i = 1; i < bitwidth; ++i) {
174 Value ext =
175 rewriter.create<smt::ExtractOp>(loc, oneBitTy, i, adaptor.getInput());
176 runner = rewriter.create<smt::BVXOrOp>(loc, runner, ext);
177 }
178
179 rewriter.replaceOp(op, runner);
180 return success();
181 }
182};
183
184/// Lower the SourceOp to the TargetOp one-to-one.
185template <typename SourceOp, typename TargetOp>
186struct OneToOneOpConversion : OpConversionPattern<SourceOp> {
188 using OpAdaptor = typename SourceOp::Adaptor;
189
190 LogicalResult
191 matchAndRewrite(SourceOp op, OpAdaptor adaptor,
192 ConversionPatternRewriter &rewriter) const override {
193
194 rewriter.replaceOpWithNewOp<TargetOp>(
195 op,
197 op.getResult().getType()),
198 adaptor.getOperands());
199 return success();
200 }
201};
202
203/// Lower the SourceOp to the TargetOp special-casing if the second operand is
204/// zero to return a new symbolic value.
205template <typename SourceOp, typename TargetOp>
206struct DivisionOpConversion : OpConversionPattern<SourceOp> {
208 using OpAdaptor = typename SourceOp::Adaptor;
209
210 LogicalResult
211 matchAndRewrite(SourceOp op, OpAdaptor adaptor,
212 ConversionPatternRewriter &rewriter) const override {
213 Location loc = op.getLoc();
214 auto type = dyn_cast<smt::BitVectorType>(adaptor.getRhs().getType());
215 if (!type)
216 return failure();
217
218 auto resultType = OpConversionPattern<SourceOp>::typeConverter->convertType(
219 op.getResult().getType());
220 Value zero =
221 rewriter.create<smt::BVConstantOp>(loc, APInt(type.getWidth(), 0));
222 Value isZero = rewriter.create<smt::EqOp>(loc, adaptor.getRhs(), zero);
223 Value symbolicVal = rewriter.create<smt::DeclareFunOp>(loc, resultType);
224 Value division =
225 rewriter.create<TargetOp>(loc, resultType, adaptor.getOperands());
226 rewriter.replaceOpWithNewOp<smt::IteOp>(op, isZero, symbolicVal, division);
227 return success();
228 }
229};
230
231/// Converts an operation with a variadic number of operands to a chain of
232/// binary operations assuming left-associativity of the operation.
233template <typename SourceOp, typename TargetOp>
234struct VariadicToBinaryOpConversion : OpConversionPattern<SourceOp> {
236 using OpAdaptor = typename SourceOp::Adaptor;
237
238 LogicalResult
239 matchAndRewrite(SourceOp op, OpAdaptor adaptor,
240 ConversionPatternRewriter &rewriter) const override {
241
242 ValueRange operands = adaptor.getOperands();
243 if (operands.size() < 2)
244 return failure();
245
246 Value runner = operands[0];
247 for (Value operand : operands.drop_front())
248 runner = rewriter.create<TargetOp>(op.getLoc(), runner, operand);
249
250 rewriter.replaceOp(op, runner);
251 return success();
252 }
253};
254
255} // namespace
256
257//===----------------------------------------------------------------------===//
258// Convert Comb to SMT pass
259//===----------------------------------------------------------------------===//
260
261namespace {
262struct ConvertCombToSMTPass
263 : public circt::impl::ConvertCombToSMTBase<ConvertCombToSMTPass> {
264 void runOnOperation() override;
265};
266} // namespace
267
268void circt::populateCombToSMTConversionPatterns(TypeConverter &converter,
269 RewritePatternSet &patterns) {
270 patterns.add<CombReplicateOpConversion, IcmpOpConversion, ExtractOpConversion,
271 SubOpConversion, MuxOpConversion, ParityOpConversion,
272 OneToOneOpConversion<ShlOp, smt::BVShlOp>,
273 OneToOneOpConversion<ShrUOp, smt::BVLShrOp>,
274 OneToOneOpConversion<ShrSOp, smt::BVAShrOp>,
275 DivisionOpConversion<DivSOp, smt::BVSDivOp>,
276 DivisionOpConversion<DivUOp, smt::BVUDivOp>,
277 DivisionOpConversion<ModSOp, smt::BVSRemOp>,
278 DivisionOpConversion<ModUOp, smt::BVURemOp>,
279 VariadicToBinaryOpConversion<ConcatOp, smt::ConcatOp>,
280 VariadicToBinaryOpConversion<AddOp, smt::BVAddOp>,
281 VariadicToBinaryOpConversion<MulOp, smt::BVMulOp>,
282 VariadicToBinaryOpConversion<AndOp, smt::BVAndOp>,
283 VariadicToBinaryOpConversion<OrOp, smt::BVOrOp>,
284 VariadicToBinaryOpConversion<XorOp, smt::BVXOrOp>>(
285 converter, patterns.getContext());
286
287 // TODO: there are two unsupported operations in the comb dialect: 'parity'
288 // and 'truth_table'.
289}
290
291void ConvertCombToSMTPass::runOnOperation() {
292 ConversionTarget target(getContext());
293 target.addIllegalDialect<hw::HWDialect>();
294 target.addIllegalOp<seq::FromClockOp>();
295 target.addIllegalOp<seq::ToClockOp>();
296 target.addIllegalDialect<comb::CombDialect>();
297 target.addLegalDialect<smt::SMTDialect>();
298 target.addLegalDialect<mlir::func::FuncDialect>();
299
300 RewritePatternSet patterns(&getContext());
301 TypeConverter converter;
303 // Also add HW patterns because some 'comb' canonicalizers produce constant
304 // operations, i.e., even if there is absolutely no HW operation present
305 // initially, we might have to convert one.
308
309 if (failed(mlir::applyPartialConversion(getOperation(), target,
310 std::move(patterns))))
311 return signalPassFailure();
312}
static Location getLoc(DefSlot slot)
Definition Mem2Reg.cpp:217
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
void populateHWToSMTConversionPatterns(TypeConverter &converter, RewritePatternSet &patterns)
Get the HW to SMT conversion patterns.
Definition HWToSMT.cpp:289
void populateCombToSMTConversionPatterns(TypeConverter &converter, RewritePatternSet &patterns)
Get the HW to SMT conversion patterns.
void populateHWToSMTTypeConverter(TypeConverter &converter)
Get the HW to SMT type conversions.
Definition HWToSMT.cpp:184
Definition comb.py:1