From 176746869a03fa37aa97bd9b5ef861a330b624e7 Mon Sep 17 00:00:00 2001 From: okekayode Date: Wed, 3 Jun 2026 17:36:18 -0700 Subject: [PATCH 1/5] [CombToSynth] Add a lowering for mod/div where rhs is constant --- lib/Conversion/CombToSynth/CombToSynth.cpp | 153 ++++++++++++++ .../CombToSynth/comb-to-aig-arith.mlir | 186 ++++++++++++++++++ test/Tools/circt-lec/comb-const-divmod.mlir | 125 ++++++++++++ 3 files changed, 464 insertions(+) create mode 100644 test/Tools/circt-lec/comb-const-divmod.mlir diff --git a/lib/Conversion/CombToSynth/CombToSynth.cpp b/lib/Conversion/CombToSynth/CombToSynth.cpp index 55c5ccb1e4cb..0075085dec91 100644 --- a/lib/Conversion/CombToSynth/CombToSynth.cpp +++ b/lib/Conversion/CombToSynth/CombToSynth.cpp @@ -33,6 +33,7 @@ #include "llvm/ADT/APInt.h" #include "llvm/ADT/PointerUnion.h" #include "llvm/Support/Debug.h" +#include "llvm/Support/DivisionByConstantInfo.h" #include #define DEBUG_TYPE "comb-to-synth" @@ -269,6 +270,74 @@ static LogicalResult emulateBinaryOpForUnknownBits( return success(); } +static Value createLShrByConstant(OpBuilder &builder, Location loc, Value value, + unsigned amount) { + if (amount == 0) + return value; + return builder.createOrFold( + loc, value, + hw::ConstantOp::create( + builder, loc, + APInt(value.getType().getIntOrFloatBitWidth(), amount))); +} + +static Value createAShrByConstant(OpBuilder &builder, Location loc, Value value, + unsigned amount) { + if (amount == 0) + return value; + return builder.createOrFold( + loc, value, + hw::ConstantOp::create( + builder, loc, + APInt(value.getType().getIntOrFloatBitWidth(), amount))); +} + +template +static Value createMulHigh(OpBuilder &builder, Location loc, Value lhs, + const APInt &rhs) { + unsigned width = lhs.getType().getIntOrFloatBitWidth(); + auto destTy = builder.getIntegerType(width << 1); + Value wideLhs = isSigned ? comb::createOrFoldSExt(builder, loc, lhs, destTy) + : comb::createZExt(builder, loc, lhs, width << 1); + Value wideRhs = hw::ConstantOp::create( + builder, loc, isSigned ? rhs.sext(width << 1) : rhs.zext(width << 1)); + Value product = builder.createOrFold( + loc, ValueRange{wideLhs, wideRhs}, true); + return builder.createOrFold(loc, product, width, width); +} + +static Value lowerUnsignedDivByConstant(OpBuilder &builder, Location loc, + Value lhs, const APInt &divisor) { + auto info = llvm::UnsignedDivisionByConstantInfo::get(divisor); + Value q = createLShrByConstant(builder, loc, lhs, info.PreShift); + q = createMulHigh(builder, loc, q, info.Magic); + if (info.IsAdd) { + Value diff = builder.createOrFold(loc, lhs, q); + diff = createLShrByConstant(builder, loc, diff, 1); + q = builder.createOrFold(loc, q, diff); + unsigned postShift = info.PostShift > 0 ? info.PostShift - 1 : 0; + q = createLShrByConstant(builder, loc, q, postShift); + } else { + q = createLShrByConstant(builder, loc, q, info.PostShift); + } + return q; +} + +static Value lowerSignedDivByConstant(OpBuilder &builder, Location loc, + Value lhs, const APInt &divisor) { + unsigned width = lhs.getType().getIntOrFloatBitWidth(); + auto info = llvm::SignedDivisionByConstantInfo::get(divisor); + Value q = createMulHigh(builder, loc, lhs, info.Magic); + if (divisor.isStrictlyPositive() && info.Magic.isNegative()) + q = builder.createOrFold(loc, q, lhs); + else if (divisor.isNegative() && info.Magic.isStrictlyPositive()) + q = builder.createOrFold(loc, q, lhs); + q = createAShrByConstant(builder, loc, q, info.ShiftAmount); + Value signBit = builder.createOrFold(loc, q, width - 1, 1); + Value signPadded = comb::createZExt(builder, loc, signBit, width); + return builder.createOrFold(loc, q, signPadded); +} + //===----------------------------------------------------------------------===// // Conversion patterns //===----------------------------------------------------------------------===// @@ -969,6 +1038,21 @@ struct CombDivUOpConversion : DivModOpConversionBase { if (llvm::succeeded(comb::convertDivUByPowerOfTwo(op, rewriter))) return success(); + // Lower div if rhs is a constant value + if (auto rhsConst = adaptor.getRhs().getDefiningOp()) { + APInt divisor = rhsConst.getValue(); + if (divisor.isZero()) { + replaceOpWithNewOpAndCopyNamehint(rewriter, op, + op.getType(), 0); + return success(); + } + replaceOpAndCopyNamehint(rewriter, op, + lowerUnsignedDivByConstant(rewriter, op.getLoc(), + adaptor.getLhs(), + divisor)); + return success(); + } + // When rhs is not power of two and the number of unknown bits are small, // create a mux tree that emulates all possible cases. return emulateBinaryOpForUnknownBits( @@ -991,6 +1075,26 @@ struct CombModUOpConversion : DivModOpConversionBase { if (llvm::succeeded(comb::convertModUByPowerOfTwo(op, rewriter))) return success(); + // Lower mod where rhs is constant value + if (auto rhsConst = adaptor.getRhs().getDefiningOp()) { + APInt divisor = rhsConst.getValue(); + if (divisor.isZero()) { + replaceOpWithNewOpAndCopyNamehint(rewriter, op, + op.getType(), 0); + return success(); + } + auto loc = op.getLoc(); + Value q = + lowerUnsignedDivByConstant(rewriter, loc, adaptor.getLhs(), divisor); + Value product = + rewriter.createOrFold(loc, q, adaptor.getRhs()); + Value remainder = + rewriter.createOrFold(loc, adaptor.getLhs(), product); + replaceOpAndCopyNamehint(rewriter, op, remainder); + + return success(); + } + // When rhs is not power of two and the number of unknown bits are small, // create a mux tree that emulates all possible cases. return emulateBinaryOpForUnknownBits( @@ -1012,6 +1116,36 @@ struct CombDivSOpConversion : DivModOpConversionBase { ConversionPatternRewriter &rewriter) const override { // Currently only lower with emulation. // TODO: Implement a signed division lowering at least for power of two. + + if (auto rhsConst = adaptor.getRhs().getDefiningOp()) { + APInt divisor = rhsConst.getValue(); + unsigned width = op.getType().getIntOrFloatBitWidth(); + if (divisor.isZero()) { + replaceOpWithNewOpAndCopyNamehint(rewriter, op, + op.getType(), 0); + return success(); + } + if (divisor.isOne()) { + replaceOpAndCopyNamehint(rewriter, op, adaptor.getLhs()); + return success(); + } + if (divisor.isAllOnes()) { + replaceOpAndCopyNamehint( + rewriter, op, + rewriter.createOrFold( + op.getLoc(), + hw::ConstantOp::create(rewriter, op.getLoc(), + APInt::getZero(width)), + adaptor.getLhs())); + return success(); + } + replaceOpAndCopyNamehint(rewriter, op, + lowerSignedDivByConstant(rewriter, op.getLoc(), + adaptor.getLhs(), + divisor)); + return success(); + } + return emulateBinaryOpForUnknownBits( rewriter, maxEmulationUnknownBits, op, [](const APInt &lhs, const APInt &rhs) { @@ -1030,6 +1164,25 @@ struct CombModSOpConversion : DivModOpConversionBase { ConversionPatternRewriter &rewriter) const override { // Currently only lower with emulation. // TODO: Implement a signed modulus lowering at least for power of two. + + if (auto rhsConst = adaptor.getRhs().getDefiningOp()) { + APInt divisor = rhsConst.getValue(); + if (divisor.isZero()) { + replaceOpWithNewOpAndCopyNamehint(rewriter, op, + op.getType(), 0); + return success(); + } + auto loc = op.getLoc(); + Value q = + lowerSignedDivByConstant(rewriter, loc, adaptor.getLhs(), divisor); + Value product = + rewriter.createOrFold(loc, q, adaptor.getRhs()); + Value remainder = + rewriter.createOrFold(loc, adaptor.getLhs(), product); + replaceOpAndCopyNamehint(rewriter, op, remainder); + return success(); + } + return emulateBinaryOpForUnknownBits( rewriter, maxEmulationUnknownBits, op, [](const APInt &lhs, const APInt &rhs) { diff --git a/test/Conversion/CombToSynth/comb-to-aig-arith.mlir b/test/Conversion/CombToSynth/comb-to-aig-arith.mlir index fcd76d113201..5e754e0311d5 100644 --- a/test/Conversion/CombToSynth/comb-to-aig-arith.mlir +++ b/test/Conversion/CombToSynth/comb-to-aig-arith.mlir @@ -1,6 +1,7 @@ // RUN: circt-opt %s --pass-pipeline="builtin.module(hw.module(convert-comb-to-synth{additional-legal-ops=comb.xor,comb.or,comb.and,comb.mux},cse))" | FileCheck %s // RUN: circt-opt %s --pass-pipeline="builtin.module(hw.module(convert-comb-to-synth{additional-legal-ops=comb.xor,comb.or,comb.and,comb.mux,comb.add},cse))" | FileCheck %s --check-prefix=ALLOW_ADD // RUN: circt-opt %s --pass-pipeline="builtin.module(hw.module(convert-comb-to-synth{additional-legal-ops=comb.xor,comb.or,comb.and,comb.mux,comb.icmp}))" | FileCheck %s --check-prefix=ALLOW_ICMP +// RUN: circt-opt %s --pass-pipeline="builtin.module(hw.module(convert-comb-to-synth{additional-legal-ops=comb.xor,comb.or,comb.and,comb.mux,comb.add,comb.mul,comb.sub},cse))" | FileCheck %s --check-prefix=ALLOW_ARITH // CHECK-LABEL: @parity hw.module @parity(in %arg0: i4, out out: i1) { @@ -463,3 +464,188 @@ hw.module @divmodu_power_of_two(in %lhs: i8, out out_divu: i8, out out_modu: i8) // ALLOW_ICMP-NEXT: hw.output %[[DIVU]], %[[MODU]] : i8, i8 hw.output %0, %1 : i8, i8 } + +// CHECK-LABEL: @divu_const_3 +// CHECK-NOT: comb.divu +// CHECK: comb.concat +// CHECK: comb.extract +// ALLOW_ARITH-LABEL: @divu_const_3 +// ALLOW_ARITH-NOT: comb.divu +// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: comb.mul +// ALLOW_ARITH: comb.extract +hw.module @divu_const_3(in %lhs: i8, out out: i8) { + %rhs = hw.constant 3 : i8 + %div = comb.divu %lhs, %rhs : i8 + hw.output %div : i8 +} + +// CHECK-LABEL: @divu_const_7 +// CHECK-NOT: comb.divu +// CHECK: comb.concat +// CHECK: comb.extract +// ALLOW_ARITH-LABEL: @divu_const_7 +// ALLOW_ARITH-NOT: comb.divu +// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: comb.mul +// ALLOW_ARITH: comb.sub +// ALLOW_ARITH: comb.add +// ALLOW_ARITH: comb.extract +hw.module @divu_const_7(in %lhs: i8, out out: i8) { + %rhs = hw.constant 7 : i8 + %div = comb.divu %lhs, %rhs : i8 + hw.output %div : i8 +} + +// CHECK-LABEL: @divu_const_10 +// CHECK-NOT: comb.divu +// CHECK: comb.concat +// CHECK: comb.extract +// ALLOW_ARITH-LABEL: @divu_const_10 +// ALLOW_ARITH-NOT: comb.divu +// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: comb.mul +// ALLOW_ARITH: comb.extract +hw.module @divu_const_10(in %lhs: i8, out out: i8) { + %rhs = hw.constant 10 : i8 + %div = comb.divu %lhs, %rhs : i8 + hw.output %div : i8 +} + +// CHECK-LABEL: @modu_const_3 +// CHECK-NOT: comb.modu +// CHECK: comb.concat +// CHECK: comb.extract +// ALLOW_ARITH-LABEL: @modu_const_3 +// ALLOW_ARITH-NOT: comb.modu +// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: comb.mul +// ALLOW_ARITH: comb.extract +// ALLOW_ARITH: comb.sub +hw.module @modu_const_3(in %lhs: i8, out out: i8) { + %rhs = hw.constant 3 : i8 + %mod = comb.modu %lhs, %rhs : i8 + hw.output %mod : i8 +} + +// CHECK-LABEL: @divs_const_3 +// CHECK-NOT: comb.divs +// CHECK: comb.replicate +// CHECK: comb.concat +// CHECK: comb.extract +// ALLOW_ARITH-LABEL: @divs_const_3 +// ALLOW_ARITH-NOT: comb.divs +// ALLOW_ARITH: comb.replicate +// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: comb.mul +// ALLOW_ARITH: comb.add +hw.module @divs_const_3(in %lhs: i8, out out: i8) { + %rhs = hw.constant 3 : i8 + %div = comb.divs %lhs, %rhs : i8 + hw.output %div : i8 +} + +// CHECK-LABEL: @divs_const_neg3 +// CHECK-NOT: comb.divs +// CHECK: comb.replicate +// CHECK: comb.concat +// CHECK: comb.extract +// ALLOW_ARITH-LABEL: @divs_const_neg3 +// ALLOW_ARITH-NOT: comb.divs +// ALLOW_ARITH: comb.replicate +// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: comb.mul +// ALLOW_ARITH: comb.sub +// ALLOW_ARITH: comb.add +hw.module @divs_const_neg3(in %lhs: i8, out out: i8) { + %rhs = hw.constant -3 : i8 + %div = comb.divs %lhs, %rhs : i8 + hw.output %div : i8 +} + +// CHECK-LABEL: @mods_const_3 +// CHECK-NOT: comb.mods +// CHECK: comb.replicate +// CHECK: comb.concat +// CHECK: comb.extract +// ALLOW_ARITH-LABEL: @mods_const_3 +// ALLOW_ARITH-NOT: comb.mods +// ALLOW_ARITH: comb.replicate +// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: comb.mul +// ALLOW_ARITH: comb.add +// ALLOW_ARITH: comb.sub +hw.module @mods_const_3(in %lhs: i8, out out: i8) { + %rhs = hw.constant 3 : i8 + %mod = comb.mods %lhs, %rhs : i8 + hw.output %mod : i8 +} + +// CHECK-LABEL: @mods_const_neg3 +// CHECK-NOT: comb.mods +// CHECK: comb.replicate +// CHECK: comb.concat +// CHECK: comb.extract +// ALLOW_ARITH-LABEL: @mods_const_neg3 +// ALLOW_ARITH-NOT: comb.mods +// ALLOW_ARITH: comb.replicate +// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: comb.mul +// ALLOW_ARITH: comb.sub +// ALLOW_ARITH: comb.add +hw.module @mods_const_neg3(in %lhs: i8, out out: i8) { + %rhs = hw.constant -3 : i8 + %mod = comb.mods %lhs, %rhs : i8 + hw.output %mod : i8 +} + + +// CHECK-LABEL: @divs_const_1 +// CHECK-NOT: comb.divs +// CHECK-NOT: comb.mul +// CHECK-NOT: comb.replicate +// CHECK: hw.output %lhs +// ALLOW_ARITH-LABEL: @divs_const_1 +// ALLOW_ARITH-NOT: comb.divs +// ALLOW_ARITH-NOT: comb.mul +// ALLOW_ARITH-NOT: comb.replicate +// ALLOW_ARITH: hw.output %lhs +hw.module @divs_const_1(in %lhs: i8, out out: i8) { + %rhs = hw.constant 1 : i8 + %div = comb.divs %lhs, %rhs : i8 + hw.output %div : i8 +} + +// CHECK-LABEL: @divs_const_neg1 +// CHECK-NOT: comb.divs +// CHECK-NOT: comb.replicate +// CHECK: comb.xor +// ALLOW_ARITH-LABEL: @divs_const_neg1 +// ALLOW_ARITH-NOT: comb.divs +// ALLOW_ARITH-NOT: comb.replicate +// ALLOW_ARITH: comb.sub +hw.module @divs_const_neg1(in %lhs: i8, out out: i8) { + %rhs = hw.constant -1 : i8 + %div = comb.divs %lhs, %rhs : i8 + hw.output %div : i8 +} + +// CHECK-LABEL: @divu_const_0 +// CHECK: hw.constant 0 +// ALLOW_ARITH-LABEL: @divu_const_0 +// ALLOW_ARITH: hw.constant 0 +hw.module @divu_const_0(in %lhs: i8, out out: i8) { + %rhs = hw.constant 0 : i8 + %div = comb.divu %lhs, %rhs : i8 + hw.output %div : i8 +} + +// CHECK-LABEL: @modu_const_0 +// CHECK: hw.constant 0 +// ALLOW_ARITH-LABEL: @modu_const_0 +// ALLOW_ARITH: hw.constant 0 +hw.module @modu_const_0(in %lhs: i8, out out: i8) { + %rhs = hw.constant 0 : i8 + %mod = comb.modu %lhs, %rhs : i8 + hw.output %mod : i8 +} diff --git a/test/Tools/circt-lec/comb-const-divmod.mlir b/test/Tools/circt-lec/comb-const-divmod.mlir new file mode 100644 index 000000000000..8a8a883e22af --- /dev/null +++ b/test/Tools/circt-lec/comb-const-divmod.mlir @@ -0,0 +1,125 @@ +// RUN: circt-lec %s --c1 divu_const_7 --c2 divu_const_7_lowered --emit-mlir | FileCheck %s --check-prefix=DIVU7 +// RUN: circt-lec %s --c1 modu_const_3 --c2 modu_const_3_lowered --emit-mlir | FileCheck %s --check-prefix=MODU3 +// RUN: circt-lec %s --c1 divs_const_neg3 --c2 divs_const_neg3_lowered --emit-mlir | FileCheck %s --check-prefix=DIVSNEG3 +// RUN: circt-lec %s --c1 mods_const_neg3 --c2 mods_const_neg3_lowered --emit-mlir | FileCheck %s --check-prefix=MODSNEG3 + +// DIVU7-LABEL: smt.solver() +// DIVU7: smt.bv.udiv +// DIVU7: smt.bv.mul +// DIVU7: smt.bv.add +// DIVU7: smt.distinct + +// MODU3-LABEL: smt.solver() +// MODU3: smt.bv.urem +// MODU3: smt.bv.mul +// MODU3: smt.bv.neg +// MODU3: smt.bv.add +// MODU3: smt.distinct + +// DIVSNEG3-LABEL: smt.solver() +// DIVSNEG3: smt.bv.sdiv +// DIVSNEG3: smt.bv.mul +// DIVSNEG3: smt.bv.add +// DIVSNEG3: smt.distinct + +// MODSNEG3-LABEL: smt.solver() +// MODSNEG3: smt.bv.srem +// MODSNEG3: smt.bv.mul +// MODSNEG3: smt.bv.add +// MODSNEG3: smt.distinct + +hw.module @divu_const_7(in %lhs: i4, out out: i4) { + %rhs = hw.constant 7 : i4 + %div = comb.divu %lhs, %rhs : i4 + hw.output %div : i4 +} + +hw.module @divu_const_7_lowered(in %lhs: i4, out out: i4) { + %c0_i4 = hw.constant 0 : i4 + %wide = comb.concat %c0_i4, %lhs : i4, i4 + %magic = hw.constant 3 : i8 + %product = comb.mul %wide, %magic : i8 + %q0 = comb.extract %product from 4 : (i8) -> i4 + %diff = comb.sub %lhs, %q0 : i4 + %diff_bits = comb.extract %diff from 1 : (i4) -> i3 + %false = hw.constant false + %diff_shifted = comb.concat %false, %diff_bits : i1, i3 + %q1 = comb.add %q0, %diff_shifted : i4 + %q_bits = comb.extract %q1 from 1 : (i4) -> i3 + %q = comb.concat %false, %q_bits : i1, i3 + hw.output %q : i4 +} + +hw.module @modu_const_3(in %lhs: i4, out out: i4) { + %rhs = hw.constant 3 : i4 + %mod = comb.modu %lhs, %rhs : i4 + hw.output %mod : i4 +} + +hw.module @modu_const_3_lowered(in %lhs: i4, out out: i4) { + %rhs = hw.constant 3 : i4 + %c0_i4 = hw.constant 0 : i4 + %wide = comb.concat %c0_i4, %lhs : i4, i4 + %magic = hw.constant 11 : i8 + %product = comb.mul %wide, %magic : i8 + %q0 = comb.extract %product from 4 : (i8) -> i4 + %q_bits = comb.extract %q0 from 1 : (i4) -> i3 + %false = hw.constant false + %q = comb.concat %false, %q_bits : i1, i3 + %mul = comb.mul %q, %rhs : i4 + %mod = comb.sub %lhs, %mul : i4 + hw.output %mod : i4 +} + +hw.module @divs_const_neg3(in %lhs: i4, out out: i4) { + %rhs = hw.constant -3 : i4 + %div = comb.divs %lhs, %rhs : i4 + hw.output %div : i4 +} + +hw.module @divs_const_neg3_lowered(in %lhs: i4, out out: i4) { + %sign = comb.extract %lhs from 3 : (i4) -> i1 + %sign_ext = comb.replicate %sign : (i1) -> i4 + %wide = comb.concat %sign_ext, %lhs : i4, i4 + %magic = hw.constant 5 : i8 + %product = comb.mul %wide, %magic : i8 + %mulhi = comb.extract %product from 4 : (i8) -> i4 + %adjusted = comb.sub %mulhi, %lhs : i4 + %shift_sign = comb.extract %adjusted from 3 : (i4) -> i1 + %shift_bits = comb.extract %adjusted from 1 : (i4) -> i2 + %shift_pad = comb.replicate %shift_sign : (i1) -> i2 + %shifted = comb.concat %shift_pad, %shift_bits : i2, i2 + %result_sign = comb.extract %shifted from 3 : (i4) -> i1 + %c0_i3 = hw.constant 0 : i3 + %sign_padded = comb.concat %c0_i3, %result_sign : i3, i1 + %result = comb.add %shifted, %sign_padded : i4 + hw.output %result : i4 +} + +hw.module @mods_const_neg3(in %lhs: i4, out out: i4) { + %rhs = hw.constant -3 : i4 + %mod = comb.mods %lhs, %rhs : i4 + hw.output %mod : i4 +} + +hw.module @mods_const_neg3_lowered(in %lhs: i4, out out: i4) { + %rhs = hw.constant -3 : i4 + %sign = comb.extract %lhs from 3 : (i4) -> i1 + %sign_ext = comb.replicate %sign : (i1) -> i4 + %wide = comb.concat %sign_ext, %lhs : i4, i4 + %magic = hw.constant 5 : i8 + %product = comb.mul %wide, %magic : i8 + %mulhi = comb.extract %product from 4 : (i8) -> i4 + %adjusted = comb.sub %mulhi, %lhs : i4 + %shift_sign = comb.extract %adjusted from 3 : (i4) -> i1 + %shift_bits = comb.extract %adjusted from 1 : (i4) -> i2 + %shift_pad = comb.replicate %shift_sign : (i1) -> i2 + %shifted = comb.concat %shift_pad, %shift_bits : i2, i2 + %result_sign = comb.extract %shifted from 3 : (i4) -> i1 + %c0_i3 = hw.constant 0 : i3 + %sign_padded = comb.concat %c0_i3, %result_sign : i3, i1 + %quotient = comb.add %shifted, %sign_padded : i4 + %mul = comb.mul %quotient, %rhs : i4 + %mod = comb.sub %lhs, %mul : i4 + hw.output %mod : i4 +} From 4bb59c4de1baab0d68cb89bc68ec9237cd67fc17 Mon Sep 17 00:00:00 2001 From: okekayode Date: Fri, 5 Jun 2026 15:13:50 -0700 Subject: [PATCH 2/5] verify lowering correctness and remove wrongly placed mlir file --- integration_test/circt-synth/divmod.mlir | 25 ++++ lib/Conversion/CombToSynth/CombToSynth.cpp | 6 +- test/Tools/circt-lec/comb-const-divmod.mlir | 125 -------------------- 3 files changed, 26 insertions(+), 130 deletions(-) delete mode 100644 test/Tools/circt-lec/comb-const-divmod.mlir diff --git a/integration_test/circt-synth/divmod.mlir b/integration_test/circt-synth/divmod.mlir index e951f7aebf0f..52ef3af588cf 100644 --- a/integration_test/circt-synth/divmod.mlir +++ b/integration_test/circt-synth/divmod.mlir @@ -51,3 +51,28 @@ hw.module @divmod_mix_constant(in %in: i1, in %lhs: i1, in %rhs: i1, out out_div hw.output %0, %1, %2, %3 : i4, i4, i4, i4 } +// RUN: circt-lec %t.mlir %s -c1=divmodu_constants -c2=divmodu_constants --shared-libs=%libz3 | FileCheck %s --check-prefix=COMB_DIVMODU_CONSTANTS +// COMB_DIVMODU_CONSTANTS: c1 == c2 +hw.module @divmodu_constants(in %lhs: i8, out out_divu_7: i8, out out_divu_10: i8, out out_modu_3: i8) { + %c7_i8 = hw.constant 7 : i8 + %c10_i8 = hw.constant 10 : i8 + %c3_i8 = hw.constant 3 : i8 + + %0 = comb.divu %lhs, %c7_i8 : i8 + %1 = comb.divu %lhs, %c10_i8 : i8 + %2 = comb.modu %lhs, %c3_i8 : i8 + hw.output %0, %1, %2 : i8, i8, i8 +} + +// RUN: circt-lec %t.mlir %s -c1=divmods_constants -c2=divmods_constants --shared-libs=%libz3 | FileCheck %s --check-prefix=COMB_DIVMODS_CONSTANTS +// COMB_DIVMODS_CONSTANTS: c1 == c2 +hw.module @divmods_constants(in %lhs: i8, out out_divs_3: i8, out out_divs_neg3: i8, out out_mods_3: i8, out out_mods_neg3: i8) { + %c3_i8 = hw.constant 3 : i8 + %c-3_i8 = hw.constant -3 : i8 + + %0 = comb.divs %lhs, %c3_i8 : i8 + %1 = comb.divs %lhs, %c-3_i8 : i8 + %2 = comb.mods %lhs, %c3_i8 : i8 + %3 = comb.mods %lhs, %c-3_i8 : i8 + hw.output %0, %1, %2, %3 : i8, i8, i8, i8 +} diff --git a/lib/Conversion/CombToSynth/CombToSynth.cpp b/lib/Conversion/CombToSynth/CombToSynth.cpp index 0075085dec91..d3783a2b6a0e 100644 --- a/lib/Conversion/CombToSynth/CombToSynth.cpp +++ b/lib/Conversion/CombToSynth/CombToSynth.cpp @@ -315,12 +315,8 @@ static Value lowerUnsignedDivByConstant(OpBuilder &builder, Location loc, Value diff = builder.createOrFold(loc, lhs, q); diff = createLShrByConstant(builder, loc, diff, 1); q = builder.createOrFold(loc, q, diff); - unsigned postShift = info.PostShift > 0 ? info.PostShift - 1 : 0; - q = createLShrByConstant(builder, loc, q, postShift); - } else { - q = createLShrByConstant(builder, loc, q, info.PostShift); } - return q; + return createLShrByConstant(builder, loc, q, info.PostShift); } static Value lowerSignedDivByConstant(OpBuilder &builder, Location loc, diff --git a/test/Tools/circt-lec/comb-const-divmod.mlir b/test/Tools/circt-lec/comb-const-divmod.mlir deleted file mode 100644 index 8a8a883e22af..000000000000 --- a/test/Tools/circt-lec/comb-const-divmod.mlir +++ /dev/null @@ -1,125 +0,0 @@ -// RUN: circt-lec %s --c1 divu_const_7 --c2 divu_const_7_lowered --emit-mlir | FileCheck %s --check-prefix=DIVU7 -// RUN: circt-lec %s --c1 modu_const_3 --c2 modu_const_3_lowered --emit-mlir | FileCheck %s --check-prefix=MODU3 -// RUN: circt-lec %s --c1 divs_const_neg3 --c2 divs_const_neg3_lowered --emit-mlir | FileCheck %s --check-prefix=DIVSNEG3 -// RUN: circt-lec %s --c1 mods_const_neg3 --c2 mods_const_neg3_lowered --emit-mlir | FileCheck %s --check-prefix=MODSNEG3 - -// DIVU7-LABEL: smt.solver() -// DIVU7: smt.bv.udiv -// DIVU7: smt.bv.mul -// DIVU7: smt.bv.add -// DIVU7: smt.distinct - -// MODU3-LABEL: smt.solver() -// MODU3: smt.bv.urem -// MODU3: smt.bv.mul -// MODU3: smt.bv.neg -// MODU3: smt.bv.add -// MODU3: smt.distinct - -// DIVSNEG3-LABEL: smt.solver() -// DIVSNEG3: smt.bv.sdiv -// DIVSNEG3: smt.bv.mul -// DIVSNEG3: smt.bv.add -// DIVSNEG3: smt.distinct - -// MODSNEG3-LABEL: smt.solver() -// MODSNEG3: smt.bv.srem -// MODSNEG3: smt.bv.mul -// MODSNEG3: smt.bv.add -// MODSNEG3: smt.distinct - -hw.module @divu_const_7(in %lhs: i4, out out: i4) { - %rhs = hw.constant 7 : i4 - %div = comb.divu %lhs, %rhs : i4 - hw.output %div : i4 -} - -hw.module @divu_const_7_lowered(in %lhs: i4, out out: i4) { - %c0_i4 = hw.constant 0 : i4 - %wide = comb.concat %c0_i4, %lhs : i4, i4 - %magic = hw.constant 3 : i8 - %product = comb.mul %wide, %magic : i8 - %q0 = comb.extract %product from 4 : (i8) -> i4 - %diff = comb.sub %lhs, %q0 : i4 - %diff_bits = comb.extract %diff from 1 : (i4) -> i3 - %false = hw.constant false - %diff_shifted = comb.concat %false, %diff_bits : i1, i3 - %q1 = comb.add %q0, %diff_shifted : i4 - %q_bits = comb.extract %q1 from 1 : (i4) -> i3 - %q = comb.concat %false, %q_bits : i1, i3 - hw.output %q : i4 -} - -hw.module @modu_const_3(in %lhs: i4, out out: i4) { - %rhs = hw.constant 3 : i4 - %mod = comb.modu %lhs, %rhs : i4 - hw.output %mod : i4 -} - -hw.module @modu_const_3_lowered(in %lhs: i4, out out: i4) { - %rhs = hw.constant 3 : i4 - %c0_i4 = hw.constant 0 : i4 - %wide = comb.concat %c0_i4, %lhs : i4, i4 - %magic = hw.constant 11 : i8 - %product = comb.mul %wide, %magic : i8 - %q0 = comb.extract %product from 4 : (i8) -> i4 - %q_bits = comb.extract %q0 from 1 : (i4) -> i3 - %false = hw.constant false - %q = comb.concat %false, %q_bits : i1, i3 - %mul = comb.mul %q, %rhs : i4 - %mod = comb.sub %lhs, %mul : i4 - hw.output %mod : i4 -} - -hw.module @divs_const_neg3(in %lhs: i4, out out: i4) { - %rhs = hw.constant -3 : i4 - %div = comb.divs %lhs, %rhs : i4 - hw.output %div : i4 -} - -hw.module @divs_const_neg3_lowered(in %lhs: i4, out out: i4) { - %sign = comb.extract %lhs from 3 : (i4) -> i1 - %sign_ext = comb.replicate %sign : (i1) -> i4 - %wide = comb.concat %sign_ext, %lhs : i4, i4 - %magic = hw.constant 5 : i8 - %product = comb.mul %wide, %magic : i8 - %mulhi = comb.extract %product from 4 : (i8) -> i4 - %adjusted = comb.sub %mulhi, %lhs : i4 - %shift_sign = comb.extract %adjusted from 3 : (i4) -> i1 - %shift_bits = comb.extract %adjusted from 1 : (i4) -> i2 - %shift_pad = comb.replicate %shift_sign : (i1) -> i2 - %shifted = comb.concat %shift_pad, %shift_bits : i2, i2 - %result_sign = comb.extract %shifted from 3 : (i4) -> i1 - %c0_i3 = hw.constant 0 : i3 - %sign_padded = comb.concat %c0_i3, %result_sign : i3, i1 - %result = comb.add %shifted, %sign_padded : i4 - hw.output %result : i4 -} - -hw.module @mods_const_neg3(in %lhs: i4, out out: i4) { - %rhs = hw.constant -3 : i4 - %mod = comb.mods %lhs, %rhs : i4 - hw.output %mod : i4 -} - -hw.module @mods_const_neg3_lowered(in %lhs: i4, out out: i4) { - %rhs = hw.constant -3 : i4 - %sign = comb.extract %lhs from 3 : (i4) -> i1 - %sign_ext = comb.replicate %sign : (i1) -> i4 - %wide = comb.concat %sign_ext, %lhs : i4, i4 - %magic = hw.constant 5 : i8 - %product = comb.mul %wide, %magic : i8 - %mulhi = comb.extract %product from 4 : (i8) -> i4 - %adjusted = comb.sub %mulhi, %lhs : i4 - %shift_sign = comb.extract %adjusted from 3 : (i4) -> i1 - %shift_bits = comb.extract %adjusted from 1 : (i4) -> i2 - %shift_pad = comb.replicate %shift_sign : (i1) -> i2 - %shifted = comb.concat %shift_pad, %shift_bits : i2, i2 - %result_sign = comb.extract %shifted from 3 : (i4) -> i1 - %c0_i3 = hw.constant 0 : i3 - %sign_padded = comb.concat %c0_i3, %result_sign : i3, i1 - %quotient = comb.add %shifted, %sign_padded : i4 - %mul = comb.mul %quotient, %rhs : i4 - %mod = comb.sub %lhs, %mul : i4 - hw.output %mod : i4 -} From 5a477929415761b52f6208b3a60b6274e51994fa Mon Sep 17 00:00:00 2001 From: okekayode Date: Fri, 5 Jun 2026 22:56:25 -0700 Subject: [PATCH 3/5] added mods edge cases --- integration_test/circt-synth/divmod.mlir | 8 ++++++++ lib/Conversion/CombToSynth/CombToSynth.cpp | 2 +- test/Conversion/CombToSynth/comb-to-aig-arith.mlir | 12 ++++++++++++ 3 files changed, 21 insertions(+), 1 deletion(-) diff --git a/integration_test/circt-synth/divmod.mlir b/integration_test/circt-synth/divmod.mlir index 52ef3af588cf..d71953328d4a 100644 --- a/integration_test/circt-synth/divmod.mlir +++ b/integration_test/circt-synth/divmod.mlir @@ -76,3 +76,11 @@ hw.module @divmods_constants(in %lhs: i8, out out_divs_3: i8, out out_divs_neg3: %3 = comb.mods %lhs, %c-3_i8 : i8 hw.output %0, %1, %2, %3 : i8, i8, i8, i8 } + +// RUN: circt-lec %t.mlir %s -c1=const_divmod_mods_neg1_i3 -c2=const_divmod_mods_neg1_i3 --shared-libs=%libz3 | FileCheck %s --check-prefix=COMB_MODS_NEG1_I3 +// COMB_MODS_NEG1_I3: c1 == c2 +hw.module @const_divmod_mods_neg1_i3(in %lhs: i3, out out: i3) { + %c_neg1_i3 = hw.constant -1 : i3 + %0 = comb.mods %lhs, %c_neg1_i3 : i3 + hw.output %0 : i3 +} diff --git a/lib/Conversion/CombToSynth/CombToSynth.cpp b/lib/Conversion/CombToSynth/CombToSynth.cpp index d3783a2b6a0e..be4f29b8ad8a 100644 --- a/lib/Conversion/CombToSynth/CombToSynth.cpp +++ b/lib/Conversion/CombToSynth/CombToSynth.cpp @@ -1163,7 +1163,7 @@ struct CombModSOpConversion : DivModOpConversionBase { if (auto rhsConst = adaptor.getRhs().getDefiningOp()) { APInt divisor = rhsConst.getValue(); - if (divisor.isZero()) { + if (divisor.isZero() || divisor.isOne() || divisor.isAllOnes()) { replaceOpWithNewOpAndCopyNamehint(rewriter, op, op.getType(), 0); return success(); diff --git a/test/Conversion/CombToSynth/comb-to-aig-arith.mlir b/test/Conversion/CombToSynth/comb-to-aig-arith.mlir index 5e754e0311d5..60eae71d834b 100644 --- a/test/Conversion/CombToSynth/comb-to-aig-arith.mlir +++ b/test/Conversion/CombToSynth/comb-to-aig-arith.mlir @@ -649,3 +649,15 @@ hw.module @modu_const_0(in %lhs: i8, out out: i8) { %mod = comb.modu %lhs, %rhs : i8 hw.output %mod : i8 } + +// CHECK-LABEL: @const_divmod_mods_neg1_i3 +// CHECK-NOT: comb.mods +// CHECK: hw.constant 0 : i3 +// ALLOW_ARITH-LABEL: @const_divmod_mods_neg1_i3 +// ALLOW_ARITH-NOT: comb.mods +// ALLOW_ARITH: hw.constant 0 : i3 +hw.module @const_divmod_mods_neg1_i3(in %lhs: i3, out out: i3) { + %c_neg1_i3 = hw.constant -1 : i3 + %0 = comb.mods %lhs, %c_neg1_i3 : i3 + hw.output %0 : i3 +} From 864167efed97cc4f7e5bb4dcff0ef494f000a007 Mon Sep 17 00:00:00 2001 From: okekayode Date: Sun, 7 Jun 2026 11:21:30 -0700 Subject: [PATCH 4/5] check rhs and remove comb.concat --- .../CombToSynth/comb-to-aig-arith.mlir | 58 ++++++------------- 1 file changed, 17 insertions(+), 41 deletions(-) diff --git a/test/Conversion/CombToSynth/comb-to-aig-arith.mlir b/test/Conversion/CombToSynth/comb-to-aig-arith.mlir index 60eae71d834b..4a4a7010216a 100644 --- a/test/Conversion/CombToSynth/comb-to-aig-arith.mlir +++ b/test/Conversion/CombToSynth/comb-to-aig-arith.mlir @@ -467,11 +467,9 @@ hw.module @divmodu_power_of_two(in %lhs: i8, out out_divu: i8, out out_modu: i8) // CHECK-LABEL: @divu_const_3 // CHECK-NOT: comb.divu -// CHECK: comb.concat -// CHECK: comb.extract // ALLOW_ARITH-LABEL: @divu_const_3 // ALLOW_ARITH-NOT: comb.divu -// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: hw.constant 171 : i16 // ALLOW_ARITH: comb.mul // ALLOW_ARITH: comb.extract hw.module @divu_const_3(in %lhs: i8, out out: i8) { @@ -482,11 +480,9 @@ hw.module @divu_const_3(in %lhs: i8, out out: i8) { // CHECK-LABEL: @divu_const_7 // CHECK-NOT: comb.divu -// CHECK: comb.concat -// CHECK: comb.extract // ALLOW_ARITH-LABEL: @divu_const_7 // ALLOW_ARITH-NOT: comb.divu -// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: hw.constant 37 : i16 // ALLOW_ARITH: comb.mul // ALLOW_ARITH: comb.sub // ALLOW_ARITH: comb.add @@ -499,11 +495,9 @@ hw.module @divu_const_7(in %lhs: i8, out out: i8) { // CHECK-LABEL: @divu_const_10 // CHECK-NOT: comb.divu -// CHECK: comb.concat -// CHECK: comb.extract // ALLOW_ARITH-LABEL: @divu_const_10 // ALLOW_ARITH-NOT: comb.divu -// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: hw.constant 205 : i16 // ALLOW_ARITH: comb.mul // ALLOW_ARITH: comb.extract hw.module @divu_const_10(in %lhs: i8, out out: i8) { @@ -514,13 +508,11 @@ hw.module @divu_const_10(in %lhs: i8, out out: i8) { // CHECK-LABEL: @modu_const_3 // CHECK-NOT: comb.modu -// CHECK: comb.concat -// CHECK: comb.extract // ALLOW_ARITH-LABEL: @modu_const_3 // ALLOW_ARITH-NOT: comb.modu -// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: hw.constant 3 : i8 +// ALLOW_ARITH: hw.constant 171 : i16 // ALLOW_ARITH: comb.mul -// ALLOW_ARITH: comb.extract // ALLOW_ARITH: comb.sub hw.module @modu_const_3(in %lhs: i8, out out: i8) { %rhs = hw.constant 3 : i8 @@ -530,13 +522,9 @@ hw.module @modu_const_3(in %lhs: i8, out out: i8) { // CHECK-LABEL: @divs_const_3 // CHECK-NOT: comb.divs -// CHECK: comb.replicate -// CHECK: comb.concat -// CHECK: comb.extract // ALLOW_ARITH-LABEL: @divs_const_3 // ALLOW_ARITH-NOT: comb.divs -// ALLOW_ARITH: comb.replicate -// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: hw.constant 86 : i16 // ALLOW_ARITH: comb.mul // ALLOW_ARITH: comb.add hw.module @divs_const_3(in %lhs: i8, out out: i8) { @@ -547,13 +535,9 @@ hw.module @divs_const_3(in %lhs: i8, out out: i8) { // CHECK-LABEL: @divs_const_neg3 // CHECK-NOT: comb.divs -// CHECK: comb.replicate -// CHECK: comb.concat -// CHECK: comb.extract // ALLOW_ARITH-LABEL: @divs_const_neg3 // ALLOW_ARITH-NOT: comb.divs -// ALLOW_ARITH: comb.replicate -// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: hw.constant 85 : i16 // ALLOW_ARITH: comb.mul // ALLOW_ARITH: comb.sub // ALLOW_ARITH: comb.add @@ -565,13 +549,10 @@ hw.module @divs_const_neg3(in %lhs: i8, out out: i8) { // CHECK-LABEL: @mods_const_3 // CHECK-NOT: comb.mods -// CHECK: comb.replicate -// CHECK: comb.concat -// CHECK: comb.extract // ALLOW_ARITH-LABEL: @mods_const_3 // ALLOW_ARITH-NOT: comb.mods -// ALLOW_ARITH: comb.replicate -// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: hw.constant 3 : i8 +// ALLOW_ARITH: hw.constant 86 : i16 // ALLOW_ARITH: comb.mul // ALLOW_ARITH: comb.add // ALLOW_ARITH: comb.sub @@ -583,13 +564,10 @@ hw.module @mods_const_3(in %lhs: i8, out out: i8) { // CHECK-LABEL: @mods_const_neg3 // CHECK-NOT: comb.mods -// CHECK: comb.replicate -// CHECK: comb.concat -// CHECK: comb.extract // ALLOW_ARITH-LABEL: @mods_const_neg3 // ALLOW_ARITH-NOT: comb.mods -// ALLOW_ARITH: comb.replicate -// ALLOW_ARITH: comb.concat +// ALLOW_ARITH: hw.constant -3 : i8 +// ALLOW_ARITH: hw.constant 85 : i16 // ALLOW_ARITH: comb.mul // ALLOW_ARITH: comb.sub // ALLOW_ARITH: comb.add @@ -599,7 +577,6 @@ hw.module @mods_const_neg3(in %lhs: i8, out out: i8) { hw.output %mod : i8 } - // CHECK-LABEL: @divs_const_1 // CHECK-NOT: comb.divs // CHECK-NOT: comb.mul @@ -618,11 +595,10 @@ hw.module @divs_const_1(in %lhs: i8, out out: i8) { // CHECK-LABEL: @divs_const_neg1 // CHECK-NOT: comb.divs -// CHECK-NOT: comb.replicate -// CHECK: comb.xor +// CHECK: hw.constant -1 : i8 // ALLOW_ARITH-LABEL: @divs_const_neg1 // ALLOW_ARITH-NOT: comb.divs -// ALLOW_ARITH-NOT: comb.replicate +// ALLOW_ARITH: hw.constant 0 : i8 // ALLOW_ARITH: comb.sub hw.module @divs_const_neg1(in %lhs: i8, out out: i8) { %rhs = hw.constant -1 : i8 @@ -631,9 +607,9 @@ hw.module @divs_const_neg1(in %lhs: i8, out out: i8) { } // CHECK-LABEL: @divu_const_0 -// CHECK: hw.constant 0 +// CHECK: hw.constant 0 : i8 // ALLOW_ARITH-LABEL: @divu_const_0 -// ALLOW_ARITH: hw.constant 0 +// ALLOW_ARITH: hw.constant 0 : i8 hw.module @divu_const_0(in %lhs: i8, out out: i8) { %rhs = hw.constant 0 : i8 %div = comb.divu %lhs, %rhs : i8 @@ -641,9 +617,9 @@ hw.module @divu_const_0(in %lhs: i8, out out: i8) { } // CHECK-LABEL: @modu_const_0 -// CHECK: hw.constant 0 +// CHECK: hw.constant 0 : i8 // ALLOW_ARITH-LABEL: @modu_const_0 -// ALLOW_ARITH: hw.constant 0 +// ALLOW_ARITH: hw.constant 0 : i8 hw.module @modu_const_0(in %lhs: i8, out out: i8) { %rhs = hw.constant 0 : i8 %mod = comb.modu %lhs, %rhs : i8 From 8738b11a694be753536f371f9f4c251177e21c5d Mon Sep 17 00:00:00 2001 From: okekayode Date: Sun, 7 Jun 2026 19:42:16 -0700 Subject: [PATCH 5/5] resolve .mlir conflicts --- test/Conversion/CombToSynth/comb-to-aig-arith.mlir | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/test/Conversion/CombToSynth/comb-to-aig-arith.mlir b/test/Conversion/CombToSynth/comb-to-aig-arith.mlir index 73544048d756..412054c62ab6 100644 --- a/test/Conversion/CombToSynth/comb-to-aig-arith.mlir +++ b/test/Conversion/CombToSynth/comb-to-aig-arith.mlir @@ -653,4 +653,5 @@ hw.module @modu_const_0(in %lhs: i8, out out: i8) { hw.module @const_divmod_mods_neg1_i3(in %lhs: i3, out out: i3) { %c_neg1_i3 = hw.constant -1 : i3 %0 = comb.mods %lhs, %c_neg1_i3 : i3 - hw.output %0 : i3 \ No newline at end of file + hw.output %0 : i3 +}