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

[HWToSMT] Add ArrayInject lowering to HWToSMT (#8765) 

This commit implements the lowering of hw.array_inject operations to SMT
expressions using smt.array.store operations. The lowering creates a new
array with the specified element injected at the given index, with proper
bounds checking to handle out-of-bounds accesses gracefully.

The implementation includes bounds checking that compares the index against
the maximum valid index (numElements - 1) and uses smt.ite to return either
the updated array (if in bounds) or the original array (if out of bounds).
This commit is contained in:
Hideto Ueno 2025-07-23 01:21:59 -07:00 committed by GitHub
parent 959e0f18e2
commit 186dcc8b0e
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 48 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
lib/Conversion/HWToSMT/HWToSMT.cpp
View File

@ -154,6 +154,40 @@ struct ArrayGetOpConversion : OpConversionPattern<ArrayGetOp> {
}
};
/// Lower a hw::ArrayInjectOp operation to smt::ArrayStoreOp.
struct ArrayInjectOpConversion : OpConversionPattern<ArrayInjectOp> {
using OpConversionPattern<ArrayInjectOp>::OpConversionPattern;
LogicalResult
matchAndRewrite(ArrayInjectOp op, OpAdaptor adaptor,
ConversionPatternRewriter &rewriter) const override {
Location loc = op.getLoc();
unsigned numElements =
cast<hw::ArrayType>(op.getInput().getType()).getNumElements();
Type arrType = typeConverter->convertType(op.getType());
if (!arrType)
return rewriter.notifyMatchFailure(op.getLoc(), "unsupported array type");
// Check if the index is within bounds
Value numElementsVal = rewriter.create<mlir::smt::BVConstantOp>(
loc, numElements - 1, llvm::Log2_64_Ceil(numElements));
Value inBounds =
rewriter.create<mlir::smt::BVCmpOp>(loc, mlir::smt::BVCmpPredicate::ule,
adaptor.getIndex(), numElementsVal);
// Store the element at the given index
Value stored = rewriter.create<mlir::smt::ArrayStoreOp>(
loc, adaptor.getInput(), adaptor.getIndex(), adaptor.getElement());
// Return the original array if out of bounds, otherwise return the new
// array
rewriter.replaceOpWithNewOp<mlir::smt::IteOp>(op, inBounds, stored,
adaptor.getInput());
return success();
}
};
/// Remove redundant (seq::FromClock and seq::ToClock) ops.
template <typename OpTy>
struct ReplaceWithInput : OpConversionPattern<OpTy> {
@ -291,7 +325,8 @@ void circt::populateHWToSMTConversionPatterns(TypeConverter &converter,
patterns.add<HWConstantOpConversion, HWModuleOpConversion, OutputOpConversion,
InstanceOpConversion, ReplaceWithInput<seq::ToClockOp>,
ReplaceWithInput<seq::FromClockOp>, ArrayCreateOpConversion,
ArrayGetOpConversion>(converter, patterns.getContext());
ArrayGetOpConversion, ArrayInjectOpConversion>(
converter, patterns.getContext());
}
void ConvertHWToSMTPass::runOnOperation() {

12
test/Conversion/HWToSMT/hw-to-smt.mlir
View File

@ -25,3 +25,15 @@ hw.module @modB(in %in: i32, out out: i32) {
// CHECK-NEXT: return [[V]] : !smt.bv<32>
hw.output %0 : i32
}
// CHECK-LABEL: func.func @inject
// CHECK-SAME: (%[[ARR:.+]]: !smt.array<[!smt.bv<2> -> !smt.bv<8>]>, %[[IDX:.+]]: !smt.bv<2>, %[[VAL:.+]]: !smt.bv<8>)
hw.module @inject(in %arr: !hw.array<3xi8>, in %index: i2, in %v: i8, out out: !hw.array<3xi8>) {
// CHECK-NEXT: %[[C2:.+]] = smt.bv.constant #smt.bv<-2> : !smt.bv<2>
// CHECK-NEXT: %[[CMP:.+]] = smt.bv.cmp ule %[[IDX]], %[[C2]] : !smt.bv<2>
// CHECK-NEXT: %[[STORED:.+]] = smt.array.store %[[ARR]][%[[IDX]]], %[[VAL]] : !smt.array<[!smt.bv<2> -> !smt.bv<8>]>
// CHECK-NEXT: %[[RESULT:.+]] = smt.ite %[[CMP]], %[[STORED]], %[[ARR]] : !smt.array<[!smt.bv<2> -> !smt.bv<8>]>
// CHECK-NEXT: return %[[RESULT]] : !smt.array<[!smt.bv<2> -> !smt.bv<8>]>
%arr_injected = hw.array_inject %arr[%index], %v : !hw.array<3xi8>, i2
hw.output %arr_injected : !hw.array<3xi8>
}