terapines
/
circt
mirror of https://github.com/llvm/circt.git
2
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[SMT] Add HWToSMT and CombToSMT conversion passes (#6815)

This commit is contained in:
Martin Erhart 2024-03-17 18:19:48 +01:00 committed by GitHub
parent 110e610b35
commit cfb9792f48
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
16 changed files with 637 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
include/circt/Conversion/CombToSMT.h Normal file
View File

@ -0,0 +1,26 @@
//===- CombToSMT.h - Comb to SMT dialect conversion ---------*- C++ -*-===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
#ifndef CIRCT_CONVERSION_COMBTOSMT_H
#define CIRCT_CONVERSION_COMBTOSMT_H
#include "circt/Support/LLVM.h"
#include <memory>
namespace circt {
/// Get the HW to SMT conversion patterns.
void populateCombToSMTConversionPatterns(TypeConverter &converter,
RewritePatternSet &patterns);
#define GEN_PASS_DECL_CONVERTCOMBTOSMT
#include "circt/Conversion/Passes.h.inc"
} // namespace circt
#endif // CIRCT_CONVERSION_COMBTOSMT_H

29
include/circt/Conversion/HWToSMT.h Normal file
View File

@ -0,0 +1,29 @@
//===- HWToSMT.h - HW to SMT dialect conversion -----------------*- C++ -*-===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
#ifndef CIRCT_CONVERSION_HWTOSMT_H
#define CIRCT_CONVERSION_HWTOSMT_H
#include "circt/Support/LLVM.h"
#include <memory>
namespace circt {
/// Get the HW to SMT conversion patterns.
void populateHWToSMTConversionPatterns(TypeConverter &converter,
RewritePatternSet &patterns);
/// Get the HW to SMT type conversions.
void populateHWToSMTTypeConverter(TypeConverter &converter);
#define GEN_PASS_DECL_CONVERTHWTOSMT
#include "circt/Conversion/Passes.h.inc"
} // namespace circt
#endif // CIRCT_CONVERSION_HWTOSMT_H

2
include/circt/Conversion/Passes.h
View File

@ -20,6 +20,7 @@
#include "circt/Conversion/CalyxToFSM.h"
#include "circt/Conversion/CalyxToHW.h"
#include "circt/Conversion/CombToArith.h"
#include "circt/Conversion/CombToSMT.h"
#include "circt/Conversion/ConvertToArcs.h"
#include "circt/Conversion/DCToHW.h"
#include "circt/Conversion/ExportChiselInterface.h"
@ -30,6 +31,7 @@
#include "circt/Conversion/HWToBTOR2.h"
#include "circt/Conversion/HWToLLHD.h"
#include "circt/Conversion/HWToLLVM.h"
#include "circt/Conversion/HWToSMT.h"
#include "circt/Conversion/HWToSV.h"
#include "circt/Conversion/HWToSystemC.h"
#include "circt/Conversion/HandshakeToDC.h"

20
include/circt/Conversion/Passes.td
View File

@ -667,6 +667,26 @@ def ConvertCombToArith : Pass<"convert-comb-to-arith", "mlir::ModuleOp"> {
let dependentDialects = ["mlir::arith::ArithDialect"];
}
//===----------------------------------------------------------------------===//
// ConvertCombToSMT
//===----------------------------------------------------------------------===//
def ConvertCombToSMT : Pass<"convert-comb-to-smt", "mlir::ModuleOp"> {
let summary = "Convert combinational ops and constants to SMT ops";
// Need to depend on HWDialect because some 'comb' canonicalization patterns
// build 'hw.constant' operations.
let dependentDialects = ["smt::SMTDialect", "hw::HWDialect"];
}
//===----------------------------------------------------------------------===//
// ConvertHWToSMT
//===----------------------------------------------------------------------===//
def ConvertHWToSMT : Pass<"convert-hw-to-smt", "mlir::ModuleOp"> {
let summary = "Convert HW ops and constants to SMT ops";
let dependentDialects = ["smt::SMTDialect"];
}
//===----------------------------------------------------------------------===//
// ConvertArcToLLVM
//===----------------------------------------------------------------------===//

18
include/circt/Dialect/SMT/SMTOps.td
View File

@ -183,6 +183,12 @@ def EqOp : SMTOp<"eq", [Pure, SameTypeOperands]> {
let arguments = (ins Variadic<AnySMTType>:$inputs);
let results = (outs BoolType:$result);
let builders = [
OpBuilder<(ins "mlir::Value":$lhs, "mlir::Value":$rhs), [{
build($_builder, $_state, ValueRange{lhs, rhs});
}]>
];
let hasCustomAssemblyFormat = true;
let hasVerifier = true;
}
@ -218,6 +224,12 @@ def DistinctOp : SMTOp<"distinct", [Pure, SameTypeOperands]> {
let arguments = (ins Variadic<AnySMTType>:$inputs);
let results = (outs BoolType:$result);
let builders = [
OpBuilder<(ins "mlir::Value":$lhs, "mlir::Value":$rhs), [{
build($_builder, $_state, ValueRange{lhs, rhs});
}]>
];
let hasCustomAssemblyFormat = true;
let hasVerifier = true;
}
@ -274,6 +286,12 @@ class VariadicBoolOp<string mnemonic, string desc> : SMTOp<mnemonic, [Pure]> {
let arguments = (ins Variadic<BoolType>:$inputs);
let results = (outs BoolType:$result);
let assemblyFormat = "$inputs attr-dict";
let builders = [
OpBuilder<(ins "mlir::Value":$lhs, "mlir::Value":$rhs), [{
build($_builder, $_state, ValueRange{lhs, rhs});
}]>
];
}
def AndOp : VariadicBoolOp<"and", "a boolean conjunction">;

2
lib/CAPI/Conversion/CMakeLists.txt
View File

@ -9,6 +9,7 @@ add_mlir_public_c_api_library(CIRCTCAPIConversion
CIRCTCalyxNative
CIRCTCombToArith
CIRCTCombToLLVM
CIRCTCombToSMT
CIRCTConvertToArcs
CIRCTDCToHW
CIRCTExportChiselInterface
@ -21,6 +22,7 @@ add_mlir_public_c_api_library(CIRCTCAPIConversion
CIRCTHWToLLHD
CIRCTHWToLLVM
CIRCTHWToBTOR2
CIRCTHWToSMT
CIRCTHWToSV
CIRCTHWToSystemC
CIRCTLLHDToLLVM

2
lib/Conversion/CMakeLists.txt
View File

@ -4,6 +4,7 @@ add_subdirectory(CalyxToFSM)
add_subdirectory(CalyxToHW)
add_subdirectory(CombToArith)
add_subdirectory(CombToLLVM)
add_subdirectory(CombToSMT)
add_subdirectory(ConvertToArcs)
add_subdirectory(DCToHW)
add_subdirectory(ExportChiselInterface)
@ -16,6 +17,7 @@ add_subdirectory(HWArithToHW)
add_subdirectory(HWToBTOR2)
add_subdirectory(HWToLLHD)
add_subdirectory(HWToLLVM)
add_subdirectory(HWToSMT)
add_subdirectory(HWToSV)
add_subdirectory(HWToSystemC)
add_subdirectory(LLHDToLLVM)

15
lib/Conversion/CombToSMT/CMakeLists.txt Normal file
View File

@ -0,0 +1,15 @@
add_circt_conversion_library(CIRCTCombToSMT
CombToSMT.cpp
DEPENDS
CIRCTConversionPassIncGen
LINK_COMPONENTS
Core
LINK_LIBS PUBLIC
CIRCTComb
CIRCTHWToSMT
CIRCTSMT
MLIRTransforms
)

245
lib/Conversion/CombToSMT/CombToSMT.cpp Normal file
View File

@ -0,0 +1,245 @@
//===- CombToSMT.cpp ------------------------------------------------------===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
#include "circt/Conversion/CombToSMT.h"
#include "circt/Conversion/HWToSMT.h"
#include "circt/Dialect/Comb/CombOps.h"
#include "circt/Dialect/SMT/SMTOps.h"
#include "mlir/Pass/Pass.h"
#include "mlir/Transforms/DialectConversion.h"
namespace circt {
#define GEN_PASS_DEF_CONVERTCOMBTOSMT
#include "circt/Conversion/Passes.h.inc"
} // namespace circt
using namespace circt;
using namespace comb;
//===----------------------------------------------------------------------===//
// Conversion patterns
//===----------------------------------------------------------------------===//
namespace {
/// Lower a comb::ReplicateOp operation to smt::RepeatOp
struct CombReplicateOpConversion : OpConversionPattern<ReplicateOp> {
using OpConversionPattern<ReplicateOp>::OpConversionPattern;
LogicalResult
matchAndRewrite(ReplicateOp op, OpAdaptor adaptor,
ConversionPatternRewriter &rewriter) const override {
rewriter.replaceOpWithNewOp<smt::RepeatOp>(op, op.getMultiple(),
adaptor.getInput());
return success();
}
};
/// Lower a comb::ICmpOp operation to a smt::BVCmpOp, smt::EqOp or
/// smt::DistinctOp
struct IcmpOpConversion : OpConversionPattern<ICmpOp> {
using OpConversionPattern<ICmpOp>::OpConversionPattern;
LogicalResult
matchAndRewrite(ICmpOp op, OpAdaptor adaptor,
ConversionPatternRewriter &rewriter) const override {
if (adaptor.getPredicate() == ICmpPredicate::weq ||
adaptor.getPredicate() == ICmpPredicate::ceq ||
adaptor.getPredicate() == ICmpPredicate::wne ||
adaptor.getPredicate() == ICmpPredicate::cne)
return rewriter.notifyMatchFailure(op,
"comparison predicate not supported");
if (adaptor.getPredicate() == ICmpPredicate::eq) {
rewriter.replaceOpWithNewOp<smt::EqOp>(op, adaptor.getLhs(),
adaptor.getRhs());
return success();
}
if (adaptor.getPredicate() == ICmpPredicate::ne) {
rewriter.replaceOpWithNewOp<smt::DistinctOp>(op, adaptor.getLhs(),
adaptor.getRhs());
return success();
}
smt::BVCmpPredicate pred;
switch (adaptor.getPredicate()) {
case ICmpPredicate::sge:
pred = smt::BVCmpPredicate::sge;
break;
case ICmpPredicate::sgt:
pred = smt::BVCmpPredicate::sgt;
break;
case ICmpPredicate::sle:
pred = smt::BVCmpPredicate::sle;
break;
case ICmpPredicate::slt:
pred = smt::BVCmpPredicate::slt;
break;
case ICmpPredicate::uge:
pred = smt::BVCmpPredicate::uge;
break;
case ICmpPredicate::ugt:
pred = smt::BVCmpPredicate::ugt;
break;
case ICmpPredicate::ule:
pred = smt::BVCmpPredicate::ule;
break;
case ICmpPredicate::ult:
pred = smt::BVCmpPredicate::ult;
break;
default:
llvm_unreachable("all cases handled above");
}
rewriter.replaceOpWithNewOp<smt::BVCmpOp>(op, pred, adaptor.getLhs(),
adaptor.getRhs());
return success();
}
};
/// Lower a comb::ExtractOp operation to an smt::ExtractOp
struct ExtractOpConversion : OpConversionPattern<ExtractOp> {
using OpConversionPattern<ExtractOp>::OpConversionPattern;
LogicalResult
matchAndRewrite(ExtractOp op, OpAdaptor adaptor,
ConversionPatternRewriter &rewriter) const override {
rewriter.replaceOpWithNewOp<smt::ExtractOp>(
op, typeConverter->convertType(op.getResult().getType()),
adaptor.getLowBitAttr(), adaptor.getInput());
return success();
}
};
/// Lower a comb::MuxOp operation to an smt::IteOp
struct MuxOpConversion : OpConversionPattern<MuxOp> {
using OpConversionPattern<MuxOp>::OpConversionPattern;
LogicalResult
matchAndRewrite(MuxOp op, OpAdaptor adaptor,
ConversionPatternRewriter &rewriter) const override {
Value condition = typeConverter->materializeTargetConversion(
rewriter, op.getLoc(), smt::BoolType::get(getContext()),
adaptor.getCond());
rewriter.replaceOpWithNewOp<smt::IteOp>(
op, condition, adaptor.getTrueValue(), adaptor.getFalseValue());
return success();
}
};
/// Lower a comb::SubOp operation to an smt::BVNegOp + smt::BVAddOp
struct SubOpConversion : OpConversionPattern<SubOp> {
using OpConversionPattern<SubOp>::OpConversionPattern;
LogicalResult
matchAndRewrite(SubOp op, OpAdaptor adaptor,
ConversionPatternRewriter &rewriter) const override {
Value negRhs = rewriter.create<smt::BVNegOp>(op.getLoc(), adaptor.getRhs());
rewriter.replaceOpWithNewOp<smt::BVAddOp>(op, adaptor.getLhs(), negRhs);
return success();
}
};
/// Lower the SourceOp to the TargetOp one-to-one.
template <typename SourceOp, typename TargetOp>
struct OneToOneOpConversion : OpConversionPattern<SourceOp> {
using OpConversionPattern<SourceOp>::OpConversionPattern;
using OpAdaptor = typename SourceOp::Adaptor;
LogicalResult
matchAndRewrite(SourceOp op, OpAdaptor adaptor,
ConversionPatternRewriter &rewriter) const override {
rewriter.replaceOpWithNewOp<TargetOp>(
op,
OpConversionPattern<SourceOp>::typeConverter->convertType(
op.getResult().getType()),
adaptor.getOperands());
return success();
}
};
/// Converts an operation with a variadic number of operands to a chain of
/// binary operations assuming left-associativity of the operation.
template <typename SourceOp, typename TargetOp>
struct VariadicToBinaryOpConversion : OpConversionPattern<SourceOp> {
using OpConversionPattern<SourceOp>::OpConversionPattern;
using OpAdaptor = typename SourceOp::Adaptor;
LogicalResult
matchAndRewrite(SourceOp op, OpAdaptor adaptor,
ConversionPatternRewriter &rewriter) const override {
ValueRange operands = adaptor.getOperands();
if (operands.size() < 2)
return failure();
Value runner = operands[0];
for (Value operand : operands.drop_front())
runner = rewriter.create<TargetOp>(op.getLoc(), runner, operand);
rewriter.replaceOp(op, runner);
return success();
}
};
} // namespace
//===----------------------------------------------------------------------===//
// Convert Comb to SMT pass
//===----------------------------------------------------------------------===//
namespace {
struct ConvertCombToSMTPass
: public impl::ConvertCombToSMTBase<ConvertCombToSMTPass> {
void runOnOperation() override;
};
} // namespace
void circt::populateCombToSMTConversionPatterns(TypeConverter &converter,
RewritePatternSet &patterns) {
patterns.add<CombReplicateOpConversion, IcmpOpConversion, ExtractOpConversion,
SubOpConversion, MuxOpConversion,
OneToOneOpConversion<ShlOp, smt::BVShlOp>,
OneToOneOpConversion<ShrUOp, smt::BVLShrOp>,
OneToOneOpConversion<ShrSOp, smt::BVAShrOp>,
OneToOneOpConversion<DivSOp, smt::BVSDivOp>,
OneToOneOpConversion<DivUOp, smt::BVUDivOp>,
OneToOneOpConversion<ModSOp, smt::BVSRemOp>,
OneToOneOpConversion<ModUOp, smt::BVURemOp>,
VariadicToBinaryOpConversion<ConcatOp, smt::ConcatOp>,
VariadicToBinaryOpConversion<AddOp, smt::BVAddOp>,
VariadicToBinaryOpConversion<MulOp, smt::BVMulOp>,
VariadicToBinaryOpConversion<AndOp, smt::BVAndOp>,
VariadicToBinaryOpConversion<OrOp, smt::BVOrOp>,
VariadicToBinaryOpConversion<XorOp, smt::BVXOrOp>>(
converter, patterns.getContext());
// TODO: there are two unsupported operations in the comb dialect: 'parity'
// and 'truth_table'.
}
void ConvertCombToSMTPass::runOnOperation() {
ConversionTarget target(getContext());
target.addIllegalDialect<comb::CombDialect>();
target.addLegalDialect<smt::SMTDialect>();
RewritePatternSet patterns(&getContext());
TypeConverter converter;
populateHWToSMTTypeConverter(converter);
// Also add HW patterns because some 'comb' canonicalizers produce constant
// operations, i.e., even if there is absolutely no HW operation present
// initially, we might have to convert one.
populateHWToSMTConversionPatterns(converter, patterns);
populateCombToSMTConversionPatterns(converter, patterns);
if (failed(mlir::applyPartialConversion(getOperation(), target,
std::move(patterns))))
return signalPassFailure();
}

14
lib/Conversion/HWToSMT/CMakeLists.txt Normal file
View File

@ -0,0 +1,14 @@
add_circt_conversion_library(CIRCTHWToSMT
HWToSMT.cpp
DEPENDS
CIRCTConversionPassIncGen
LINK_COMPONENTS
Core
LINK_LIBS PUBLIC
CIRCTHW
CIRCTSMT
MLIRTransforms
)

114
lib/Conversion/HWToSMT/HWToSMT.cpp Normal file
View File

@ -0,0 +1,114 @@
//===- HWToSMT.cpp --------------------------------------------------------===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
#include "circt/Conversion/HWToSMT.h"
#include "circt/Dialect/HW/HWOps.h"
#include "circt/Dialect/SMT/SMTOps.h"
#include "mlir/Pass/Pass.h"
#include "mlir/Transforms/DialectConversion.h"
namespace circt {
#define GEN_PASS_DEF_CONVERTHWTOSMT
#include "circt/Conversion/Passes.h.inc"
} // namespace circt
using namespace circt;
using namespace hw;
//===----------------------------------------------------------------------===//
// Conversion patterns
//===----------------------------------------------------------------------===//
namespace {
/// Lower a hw::ConstantOp operation to smt::BVConstantOp
struct HWConstantOpConversion : OpConversionPattern<ConstantOp> {
using OpConversionPattern<ConstantOp>::OpConversionPattern;
LogicalResult
matchAndRewrite(ConstantOp op, OpAdaptor adaptor,
ConversionPatternRewriter &rewriter) const override {
rewriter.replaceOpWithNewOp<smt::BVConstantOp>(op, adaptor.getValue());
return success();
}
};
} // namespace
//===----------------------------------------------------------------------===//
// Convert HW to SMT pass
//===----------------------------------------------------------------------===//
namespace {
struct ConvertHWToSMTPass
: public impl::ConvertHWToSMTBase<ConvertHWToSMTPass> {
void runOnOperation() override;
};
} // namespace
void circt::populateHWToSMTTypeConverter(TypeConverter &converter) {
// The semantics of the builtin integer at the CIRCT core level is currently
// not very well defined. It is used for two-valued, four-valued, and possible
// other multi-valued logic. Here, we interpret it as two-valued for now.
// From a formal perspective, CIRCT would ideally define its own types for
// two-valued, four-valued, nine-valued (etc.) logic each. In MLIR upstream
// the integer type also carries poison information (which we don't have in
// CIRCT?).
converter.addConversion([](IntegerType type) {
return smt::BitVectorType::get(type.getContext(), type.getWidth());
});
// Convert a 'smt.bool'-typed value to a 'smt.bv<N>'-typed value
converter.addTargetMaterialization(
[&](OpBuilder &builder, smt::BitVectorType resultType, ValueRange inputs,
Location loc) -> std::optional<Value> {
if (inputs.size() != 1)
return std::nullopt;
if (!isa<smt::BoolType>(inputs[0].getType()))
return std::nullopt;
unsigned width = resultType.getWidth();
Value constZero = builder.create<smt::BVConstantOp>(loc, 0, width);
Value constOne = builder.create<smt::BVConstantOp>(loc, 1, width);
return builder.create<smt::IteOp>(loc, inputs[0], constOne, constZero);
});
// Convert a 'smt.bv<1>'-typed value to a 'smt.bool'-typed value
converter.addTargetMaterialization(
[&](OpBuilder &builder, smt::BoolType resultType, ValueRange inputs,
Location loc) -> std::optional<Value> {
if (inputs.size() != 1)
return std::nullopt;
auto bvType = dyn_cast<smt::BitVectorType>(inputs[0].getType());
if (!bvType || bvType.getWidth() != 1)
return std::nullopt;
Value constOne = builder.create<smt::BVConstantOp>(loc, 1, 1);
return builder.create<smt::EqOp>(loc, inputs[0], constOne);
});
}
void circt::populateHWToSMTConversionPatterns(TypeConverter &converter,
RewritePatternSet &patterns) {
patterns.add<HWConstantOpConversion>(converter, patterns.getContext());
}
void ConvertHWToSMTPass::runOnOperation() {
ConversionTarget target(getContext());
target.addIllegalDialect<hw::HWDialect>();
target.addLegalDialect<smt::SMTDialect>();
RewritePatternSet patterns(&getContext());
TypeConverter converter;
populateHWToSMTTypeConverter(converter);
populateHWToSMTConversionPatterns(converter, patterns);
if (failed(mlir::applyPartialConversion(getOperation(), target,
std::move(patterns))))
return signalPassFailure();
}

4
lib/Conversion/PassDetail.h
View File

@ -133,6 +133,10 @@ namespace fsm {
class FSMDialect;
} // namespace fsm
namespace smt {
class SMTDialect;
} // namespace smt
namespace systemc {
class SystemCDialect;
} // namespace systemc

39
test/Conversion/CombToSMT/comb-to-smt-error.mlir Normal file
View File

@ -0,0 +1,39 @@
// RUN: circt-opt %s --convert-comb-to-smt --split-input-file --verify-diagnostics
func.func @test(%a0: !smt.bv<32>, %a1: !smt.bv<32>) {
%arg0 = builtin.unrealized_conversion_cast %a0 : !smt.bv<32> to i32
%arg1 = builtin.unrealized_conversion_cast %a0 : !smt.bv<32> to i32
// expected-error @below {{failed to legalize operation 'comb.icmp' that was explicitly marked illegal}}
%14 = comb.icmp weq %arg0, %arg1 : i32
return
}
// -----
func.func @test(%a0: !smt.bv<32>, %a1: !smt.bv<32>) {
%arg0 = builtin.unrealized_conversion_cast %a0 : !smt.bv<32> to i32
%arg1 = builtin.unrealized_conversion_cast %a0 : !smt.bv<32> to i32
// expected-error @below {{failed to legalize operation 'comb.icmp' that was explicitly marked illegal}}
%14 = comb.icmp ceq %arg0, %arg1 : i32
return
}
// -----
func.func @test(%a0: !smt.bv<32>, %a1: !smt.bv<32>) {
%arg0 = builtin.unrealized_conversion_cast %a0 : !smt.bv<32> to i32
%arg1 = builtin.unrealized_conversion_cast %a0 : !smt.bv<32> to i32
// expected-error @below {{failed to legalize operation 'comb.icmp' that was explicitly marked illegal}}
%14 = comb.icmp wne %arg0, %arg1 : i32
return
}
// -----
func.func @test(%a0: !smt.bv<32>, %a1: !smt.bv<32>) {
%arg0 = builtin.unrealized_conversion_cast %a0 : !smt.bv<32> to i32
%arg1 = builtin.unrealized_conversion_cast %a0 : !smt.bv<32> to i32
// expected-error @below {{failed to legalize operation 'comb.icmp' that was explicitly marked illegal}}
%14 = comb.icmp cne %arg0, %arg1 : i32
return
}

92
test/Conversion/CombToSMT/comb-to-smt.mlir Normal file
View File

@ -0,0 +1,92 @@
// RUN: circt-opt %s --convert-comb-to-smt | FileCheck %s
// CHECK-LABEL: func @test
// CHECK-SAME: ([[A0:%.+]]: !smt.bv<32>, [[A1:%.+]]: !smt.bv<32>, [[A2:%.+]]: !smt.bv<32>, [[A3:%.+]]: !smt.bv<32>, [[A4:%.+]]: !smt.bv<1>)
func.func @test(%a0: !smt.bv<32>, %a1: !smt.bv<32>, %a2: !smt.bv<32>, %a3: !smt.bv<32>, %a4: !smt.bv<1>) {
%arg0 = builtin.unrealized_conversion_cast %a0 : !smt.bv<32> to i32
%arg1 = builtin.unrealized_conversion_cast %a1 : !smt.bv<32> to i32
%arg2 = builtin.unrealized_conversion_cast %a2 : !smt.bv<32> to i32
%arg3 = builtin.unrealized_conversion_cast %a3 : !smt.bv<32> to i32
%arg4 = builtin.unrealized_conversion_cast %a4 : !smt.bv<1> to i1
// CHECK: smt.bv.sdiv [[A0]], [[A1]] : !smt.bv<32>
%0 = comb.divs %arg0, %arg1 : i32
// CHECK-NEXT: smt.bv.udiv [[A0]], [[A1]] : !smt.bv<32>
%1 = comb.divu %arg0, %arg1 : i32
// CHECK-NEXT: smt.bv.srem [[A0]], [[A1]] : !smt.bv<32>
%2 = comb.mods %arg0, %arg1 : i32
// CHECK-NEXT: smt.bv.urem [[A0]], [[A1]] : !smt.bv<32>
%3 = comb.modu %arg0, %arg1 : i32
// CHECK-NEXT: [[NEG:%.+]] = smt.bv.neg [[A1]] : !smt.bv<32>
// CHECK-NEXT: smt.bv.add [[A0]], [[NEG]] : !smt.bv<32>
%7 = comb.sub %arg0, %arg1 : i32
// CHECK-NEXT: [[A5:%.+]] = smt.bv.add [[A0]], [[A1]] : !smt.bv<32>
// CHECK-NEXT: [[A6:%.+]] = smt.bv.add [[A5]], [[A2]] : !smt.bv<32>
// CHECK-NEXT: smt.bv.add [[A6]], [[A3]] : !smt.bv<32>
%8 = comb.add %arg0, %arg1, %arg2, %arg3 : i32
// CHECK-NEXT: [[B1:%.+]] = smt.bv.mul [[A0]], [[A1]] : !smt.bv<32>
// CHECK-NEXT: [[B2:%.+]] = smt.bv.mul [[B1]], [[A2]] : !smt.bv<32>
// CHECK-NEXT: smt.bv.mul [[B2]], [[A3]] : !smt.bv<32>
%9 = comb.mul %arg0, %arg1, %arg2, %arg3 : i32
// CHECK-NEXT: [[C1:%.+]] = smt.bv.and [[A0]], [[A1]] : !smt.bv<32>
// CHECK-NEXT: [[C2:%.+]] = smt.bv.and [[C1]], [[A2]] : !smt.bv<32>
// CHECK-NEXT: smt.bv.and [[C2]], [[A3]] : !smt.bv<32>
%10 = comb.and %arg0, %arg1, %arg2, %arg3 : i32
// CHECK-NEXT: [[D1:%.+]] = smt.bv.or [[A0]], [[A1]] : !smt.bv<32>
// CHECK-NEXT: [[D2:%.+]] = smt.bv.or [[D1]], [[A2]] : !smt.bv<32>
// CHECK-NEXT: smt.bv.or [[D2]], [[A3]] : !smt.bv<32>
%11 = comb.or %arg0, %arg1, %arg2, %arg3 : i32
// CHECK-NEXT: [[E1:%.+]] = smt.bv.xor [[A0]], [[A1]] : !smt.bv<32>
// CHECK-NEXT: [[E2:%.+]] = smt.bv.xor [[E1]], [[A2]] : !smt.bv<32>
// CHECK-NEXT: smt.bv.xor [[E2]], [[A3]] : !smt.bv<32>
%12 = comb.xor %arg0, %arg1, %arg2, %arg3 : i32
// CHECK-NEXT: [[CONST1:%.+]] = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
// CHECK-NEXT: [[COND:%.+]] = smt.eq [[A4]], [[CONST1]] : !smt.bv<1>
// CHECK-NEXT: smt.ite [[COND]], [[A0]], [[A1]] : !smt.bv<32>
%13 = comb.mux %arg4, %arg0, %arg1 : i32
// CHECK-NEXT: smt.eq [[A0]], [[A1]] : !smt.bv<32>
%14 = comb.icmp eq %arg0, %arg1 : i32
// CHECK-NEXT: smt.distinct [[A0]], [[A1]] : !smt.bv<32>
%15 = comb.icmp ne %arg0, %arg1 : i32
// CHECK-NEXT: smt.bv.cmp sle [[A0]], [[A1]] : !smt.bv<32>
%20 = comb.icmp sle %arg0, %arg1 : i32
// CHECK-NEXT: smt.bv.cmp slt [[A0]], [[A1]] : !smt.bv<32>
%21 = comb.icmp slt %arg0, %arg1 : i32
// CHECK-NEXT: smt.bv.cmp ule [[A0]], [[A1]] : !smt.bv<32>
%22 = comb.icmp ule %arg0, %arg1 : i32
// CHECK-NEXT: smt.bv.cmp ult [[A0]], [[A1]] : !smt.bv<32>
%23 = comb.icmp ult %arg0, %arg1 : i32
// CHECK-NEXT: smt.bv.cmp sge [[A0]], [[A1]] : !smt.bv<32>
%24 = comb.icmp sge %arg0, %arg1 : i32
// CHECK-NEXT: smt.bv.cmp sgt [[A0]], [[A1]] : !smt.bv<32>
%25 = comb.icmp sgt %arg0, %arg1 : i32
// CHECK-NEXT: smt.bv.cmp uge [[A0]], [[A1]] : !smt.bv<32>
%26 = comb.icmp uge %arg0, %arg1 : i32
// CHECK-NEXT: smt.bv.cmp ugt [[A0]], [[A1]] : !smt.bv<32>
%27 = comb.icmp ugt %arg0, %arg1 : i32
// CHECK-NEXT: smt.bv.extract [[A0]] from 5 : (!smt.bv<32>) -> !smt.bv<16>
%28 = comb.extract %arg0 from 5 : (i32) -> i16
// CHECK-NEXT: smt.bv.concat [[A0]], [[A1]] : !smt.bv<32>, !smt.bv<32>
%29 = comb.concat %arg0, %arg1 : i32, i32
// CHECK-NEXT: smt.bv.repeat 32 times [[A4]] : !smt.bv<1>
%30 = comb.replicate %arg4 : (i1) -> i32
// CHECK-NEXT: %{{.*}} = smt.bv.shl [[A0]], [[A1]] : !smt.bv<32>
%32 = comb.shl %arg0, %arg1 : i32
// CHECK-NEXT: %{{.*}} = smt.bv.ashr [[A0]], [[A1]] : !smt.bv<32>
%33 = comb.shrs %arg0, %arg1 : i32
// CHECK-NEXT: %{{.*}} = smt.bv.lshr [[A0]], [[A1]] : !smt.bv<32>
%34 = comb.shru %arg0, %arg1 : i32
// The comb.icmp folder is called before the conversion patterns and produces
// a `hw.constant` operation.
// CHECK-NEXT: smt.bv.constant #smt.bv<-1> : !smt.bv<1>
%35 = comb.icmp eq %arg0, %arg0 : i32
return
}

13
test/Conversion/HWToSMT/hw-to-smt.mlir Normal file
View File

@ -0,0 +1,13 @@
// RUN: circt-opt %s --convert-hw-to-smt | FileCheck %s
// CHECK-LABEL: func @test
func.func @test() {
// CHECK: smt.bv.constant #smt.bv<42> : !smt.bv<32>
%c42_i32 = hw.constant 42 : i32
// CHECK: smt.bv.constant #smt.bv<-1> : !smt.bv<3>
%c-1_i32 = hw.constant -1 : i3
// CHECK: smt.bv.constant #smt.bv<0> : !smt.bv<1>
%false = hw.constant false
return
}

2
tools/circt-opt/CMakeLists.txt
View File

@ -22,6 +22,7 @@ target_link_libraries(circt-opt
CIRCTCalyxToFSM
CIRCTCalyxTransforms
CIRCTComb
CIRCTCombToSMT
CIRCTCombTransforms
CIRCTConvertToArcs
CIRCTDC
@ -60,6 +61,7 @@ target_link_libraries(circt-opt
CIRCTIbisTransforms
CIRCTInteropDialect
CIRCTHWToLLHD
CIRCTHWToSMT
CIRCTHWToSystemC
CIRCTHWToSV
CIRCTHWTransforms