diff --git a/docs/Dialects/LTL.md b/docs/Dialects/LTL.md index 13aa900bcbf0..ffed29acf095 100644 --- a/docs/Dialects/LTL.md +++ b/docs/Dialects/LTL.md @@ -315,8 +315,31 @@ lowering above on the coerced 2-state value: %onehot = comb.mux %isunknown, %zero, %onehot_2state : i1 ``` -> The following functions are not yet supported by CIRCT: -> - **`$countones(a)`** +- **`$countones(a)`**: +For 2-state input `%a` (where `%a` has type `iN`): +The popcount is computed by extracting each bit, zero-extending to +`iM` (where `M = ceil(log2(N+1))`), and summing them: + +```mlir +// For an 8-bit input, M=4 and padding is i3: +%b0 = comb.extract %a from 0 : (i8) -> i1 +%ext0 = comb.concat %zeros3, %b0 : i3, i1 +%b1 = comb.extract %a from 1 : (i8) -> i1 +%ext1 = comb.concat %zeros3, %b1 : i3, i1 +%sum = comb.add %ext0, %ext1 : i4 +// ... for each bit +``` + +For 4-state input `%a` (where `%a` has type `!moore.lN`): +x/z bits do not match logic value 1 and are excluded from the count. The value +is coerced to 2-state (`logic_to_int` maps x/z to 0) and then the 2-state +lowering is applied: + +```mlir +%coerced_a = moore.logic_to_int %a +%int_a = moore.to_builtin_int %coerced_a +%countones = ... // 2-state lowering on %int_a +``` - **`a ##n b`**: diff --git a/lib/Conversion/ImportVerilog/AssertionExpr.cpp b/lib/Conversion/ImportVerilog/AssertionExpr.cpp index 18cf88b6876e..eaaae6f44c6f 100644 --- a/lib/Conversion/ImportVerilog/AssertionExpr.cpp +++ b/lib/Conversion/ImportVerilog/AssertionExpr.cpp @@ -9,11 +9,9 @@ #include "slang/ast/expressions/AssertionExpr.h" #include "ImportVerilogInternals.h" -#include "circt/Dialect/Comb/CombDialect.h" #include "circt/Dialect/Comb/CombOps.h" #include "circt/Dialect/LTL/LTLOps.h" #include "circt/Dialect/Moore/MooreOps.h" -#include "circt/Support/FVInt.h" #include "circt/Support/LLVM.h" #include "mlir/IR/BuiltinAttributes.h" #include "mlir/Support/LLVM.h" @@ -318,6 +316,11 @@ FailureOr Context::convertAssertionSystemCallArity1( return v; }; + // Helper to cast a builtin integer result to a two-valued Moore integer type. + auto castToTwoValued = [&](Value v) -> Value { + return moore::FromBuiltinIntOp::create(builder, loc, v); + }; + switch (nameId) { case ksn::Sampled: return castToMoore(ltl::SampledOp::create(builder, loc, value)); @@ -326,7 +329,7 @@ FailureOr Context::convertAssertionSystemCallArity1( case ksn::Fell: { auto past = ltl::PastOp::create(builder, loc, value, 1, clockVal).getResult(); - return castToMoore(comb::ICmpOp::create( + return castToTwoValued(comb::ICmpOp::create( builder, loc, comb::ICmpPredicate::ugt, past, value, false)); } @@ -334,7 +337,7 @@ FailureOr Context::convertAssertionSystemCallArity1( case ksn::Rose: { auto past = ltl::PastOp::create(builder, loc, value, 1, clockVal).getResult(); - return castToMoore(comb::ICmpOp::create( + return castToTwoValued(comb::ICmpOp::create( builder, loc, comb::ICmpPredicate::ult, past, value, false)); } @@ -342,7 +345,7 @@ FailureOr Context::convertAssertionSystemCallArity1( case ksn::Changed: { auto past = ltl::PastOp::create(builder, loc, value, 1, clockVal).getResult(); - return castToMoore(comb::ICmpOp::create( + return castToTwoValued(comb::ICmpOp::create( builder, loc, comb::ICmpPredicate::ne, past, value, false)); } @@ -350,55 +353,18 @@ FailureOr Context::convertAssertionSystemCallArity1( case ksn::Stable: { auto past = ltl::PastOp::create(builder, loc, value, 1, clockVal).getResult(); - return castToMoore(comb::ICmpOp::create( + return castToTwoValued(comb::ICmpOp::create( builder, loc, comb::ICmpPredicate::eq, past, value, false)); } case ksn::Past: return castToMoore(ltl::PastOp::create(builder, loc, value, 1, clockVal)); - case ksn::OneHot0: { - auto one = hw::ConstantOp::create(builder, loc, value.getType(), 1); - auto minusOne = comb::SubOp::create(builder, loc, value, one); - auto anded = comb::AndOp::create(builder, loc, value, minusOne); - auto zero = hw::ConstantOp::create(builder, loc, value.getType(), 0); - return castToMoore(comb::ICmpOp::create( - builder, loc, comb::ICmpPredicate::eq, anded, zero, false)); - } - - case ksn::OneHot: { - auto one = hw::ConstantOp::create(builder, loc, value.getType(), 1); - auto minusOne = comb::SubOp::create(builder, loc, value, one); - auto anded = comb::AndOp::create(builder, loc, value, minusOne); - auto zero = hw::ConstantOp::create(builder, loc, value.getType(), 0); - auto isOneHot0 = comb::ICmpOp::create(builder, loc, comb::ICmpPredicate::eq, - anded, zero, false); - auto isNotZero = comb::ICmpOp::create(builder, loc, comb::ICmpPredicate::ne, - value, zero, false); - auto result = comb::AndOp::create(builder, loc, isOneHot0, isNotZero); - return castToMoore(result); - } - default: return Value{}; } } -static Value getIsUnknown(OpBuilder &builder, Location loc, Value value, - moore::IntType valTy, MLIRContext *ctx) { - Value bitVal = value; - if (valTy.getWidth() > 1) { - auto mooreI1Type = moore::IntType::get(ctx, 1, valTy.getDomain()); - bitVal = moore::ReduceXorOp::create(builder, loc, mooreI1Type, value); - } - - auto xType = moore::IntType::get(ctx, 1, moore::Domain::FourValued); - auto xValue = FVInt::getAllX(1); - auto xConst = moore::ConstantOp::create(builder, loc, xType, xValue); - - return moore::CaseEqOp::create(builder, loc, bitVal, xConst).getResult(); -} - Value Context::convertAssertionCallExpression( const slang::ast::CallExpression &expr, const slang::ast::CallExpression::SystemCallInfo &info, Location loc) { @@ -454,51 +420,6 @@ Value Context::convertAssertionCallExpression( return {}; } - // IsUnknown is handled here rather than below with the others as below it - // would have already been converted to an integer type rather than bool - // type as here. - if (subroutine.knownNameId == slang::parsing::KnownSystemName::IsUnknown) { - return getIsUnknown(builder, loc, value, valTy, getContext()); - } - - // OneHot/OneHot0 are handled both here and below. - if ((subroutine.knownNameId == slang::parsing::KnownSystemName::OneHot || - subroutine.knownNameId == slang::parsing::KnownSystemName::OneHot0) && - (valTy.getDomain() == Domain::FourValued)) { - // In SystemVerilog, these system only returns 1b1 if the expression is - // fully known and the condition is met. So if any x or y bits, then - // these must return 1'b0. - - // Detect if input contain unknown bits. - Value isUnknownMoore = - getIsUnknown(builder, loc, value, valTy, getContext()); - Value isUnknown = - builder.createOrFold(loc, isUnknownMoore); - - Value coerced = builder.createOrFold(loc, value); - Value state2IntVal = - builder.createOrFold(loc, coerced); - if (!state2IntVal) - return {}; - - auto systemResult = this->convertAssertionSystemCallArity1( - subroutine, loc, state2IntVal, originalType, clockVal); - if (failed(systemResult) || !*systemResult) - return {}; - Value onehot2state = *systemResult; - - // Squash to 0 if unknown bits exist. - Value onehot2stateBuiltin = convertToI1(onehot2state); - Value zeroBuiltin = - hw::ConstantOp::create(builder, loc, builder.getI1Type(), 0); - Value resultBuiltin = comb::MuxOp::create( - builder, loc, isUnknown, zeroBuiltin, onehot2stateBuiltin); - - Value finalResult = - moore::FromBuiltinIntOp::create(builder, loc, resultBuiltin); - return moore::IntToLogicOp::create(builder, loc, finalResult); - } - // If the value is four-valued, we need to map it to two-valued before we // cast it to a builtin int if (valTy.getDomain() == Domain::FourValued) { @@ -517,8 +438,11 @@ Value Context::convertAssertionCallExpression( if (failed(result)) return {}; - if (*result) - return *result; + if (*result) { + auto expectedTy = convertType(*expr.type); + return materializeConversion(expectedTy, *result, expr.type->isSigned(), + loc); + } mlir::emitError(loc) << "unsupported system call `" << subroutine.name << "`"; return {}; diff --git a/lib/Conversion/ImportVerilog/Expressions.cpp b/lib/Conversion/ImportVerilog/Expressions.cpp index ec941d5b1f04..ac53dd86ca98 100644 --- a/lib/Conversion/ImportVerilog/Expressions.cpp +++ b/lib/Conversion/ImportVerilog/Expressions.cpp @@ -7,8 +7,10 @@ //===----------------------------------------------------------------------===// #include "ImportVerilogInternals.h" +#include "circt/Dialect/Comb/CombOps.h" #include "circt/Dialect/Moore/MooreOps.h" #include "circt/Dialect/Moore/MooreTypes.h" +#include "circt/Support/FVInt.h" #include "mlir/IR/Operation.h" #include "mlir/IR/Value.h" #include "slang/ast/EvalContext.h" @@ -36,6 +38,30 @@ static FVInt convertSVIntToFVInt(const slang::SVInt &svint) { return FVInt(APInt(svint.getBitWidth(), value)); } +/// Check if a Moore integer value contains any unknown (x/z) bits. +/// Returns a Moore i1 result: 1 if any bit is unknown, 0 otherwise. +static Value getIsUnknown(OpBuilder &builder, Location loc, Value value, + moore::IntType valTy, MLIRContext *ctx) { + Value bitVal = value; + if (valTy.getWidth() > 1) { + auto mooreI1Type = moore::IntType::get(ctx, 1, valTy.getDomain()); + bitVal = moore::ReduceXorOp::create(builder, loc, mooreI1Type, value); + } + auto xType = moore::IntType::get(ctx, 1, moore::Domain::FourValued); + auto xConst = + moore::ConstantOp::create(builder, loc, xType, FVInt::getAllX(1)); + return moore::CaseEqOp::create(builder, loc, bitVal, xConst).getResult(); +} + +/// Coerce a Moore integer value to a builtin integer, handling four-valued +/// inputs by first mapping x/z to 0 via LogicToIntOp. +static Value coerceToBuiltinInt(OpBuilder &builder, Location loc, Value value, + moore::IntType valTy) { + if (valTy.getDomain() == moore::Domain::FourValued) + value = builder.createOrFold(loc, value); + return builder.createOrFold(loc, value); +} + /// Map an index into an array, with bounds `range`, to a bit offset of the /// underlying bit storage. This is a dynamic version of /// `slang::ConstantRange::translateIndex`. @@ -2031,7 +2057,7 @@ struct RvalueExprVisitor : public ExprVisitor { const auto &subroutine = *info.subroutine; auto nameId = subroutine.knownNameId; - // $rose, $fell, $stable, $changed, and $past are only valid in + // $rose, $fell, $stable, $changed, $past, and $sampled are only valid in // the context of properties and assertions. Those are treated in the // LTLDialect; treat them there instead. switch (nameId) { @@ -2041,9 +2067,6 @@ struct RvalueExprVisitor : public ExprVisitor { case ksn::Changed: case ksn::Past: case ksn::Sampled: - case ksn::IsUnknown: - case ksn::OneHot: - case ksn::OneHot0: return context.convertAssertionCallExpression(expr, info, loc); default: break; @@ -2072,8 +2095,14 @@ struct RvalueExprVisitor : public ExprVisitor { return {}; auto ty = context.convertType(*expr.type); - return context.materializeConversion(ty, result, expr.type->isSigned(), - loc); + // Bit vector builtins ($countones, $isunknown, $onehot, $onehot0) return + // inherently unsigned results that must be zero-extended, even though + // Slang's declared return type may be signed int. + bool isSigned = expr.type->isSigned(); + if (nameId == ksn::CountOnes || nameId == ksn::IsUnknown || + nameId == ksn::OneHot || nameId == ksn::OneHot0) + isSigned = false; + return context.materializeConversion(ty, result, isSigned, loc); } /// Handle string literals. @@ -3262,6 +3291,112 @@ Value Context::convertSystemCall( return moore::Clog2BIOp::create(builder, loc, value); } + //===--------------------------------------------------------------------===// + // Bit Vector System Functions + //===--------------------------------------------------------------------===// + + if (nameId == ksn::IsUnknown) { + assert(numArgs == 1 && "`$isunknown` takes 1 argument"); + auto value = convertRvalueExpression(*args[0]); + if (!value) + return {}; + auto valTy = dyn_cast(value.getType()); + if (!valTy) { + mlir::emitError(loc) << "expected integer argument for `$isunknown`"; + return {}; + } + return getIsUnknown(builder, loc, value, valTy, getContext()); + } + + if (nameId == ksn::OneHot0 || nameId == ksn::OneHot) { + assert(numArgs == 1 && "`$onehot`/`$onehot0` takes 1 argument"); + auto value = convertRvalueExpression(*args[0]); + if (!value) + return {}; + auto valTy = dyn_cast(value.getType()); + if (!valTy) { + mlir::emitError(loc) << "expected integer argument for `" + << subroutine.name << "`"; + return {}; + } + + // In SystemVerilog, $onehot/$onehot0 return 1'b0 if the expression + // contains any unknown (x/z) bits. Detect and squash if four-valued. + Value isUnknown; + if (valTy.getDomain() == Domain::FourValued) { + Value isUnknownMoore = + getIsUnknown(builder, loc, value, valTy, getContext()); + isUnknown = + builder.createOrFold(loc, isUnknownMoore); + } + + // Coerce four-valued input to two-valued for the comb ops. + Value intVal = coerceToBuiltinInt(builder, loc, value, valTy); + + // Compute onehot0: (value & (value - 1)) == 0 + auto one = hw::ConstantOp::create(builder, loc, intVal.getType(), 1); + auto minusOne = comb::SubOp::create(builder, loc, intVal, one); + auto anded = comb::AndOp::create(builder, loc, intVal, minusOne); + auto zero = hw::ConstantOp::create(builder, loc, intVal.getType(), 0); + Value result = comb::ICmpOp::create(builder, loc, comb::ICmpPredicate::eq, + anded, zero, false); + + // For $onehot, additionally require value != 0. + if (nameId == ksn::OneHot) { + auto isNotZero = comb::ICmpOp::create( + builder, loc, comb::ICmpPredicate::ne, intVal, zero, false); + result = comb::AndOp::create(builder, loc, result, isNotZero); + } + + // If four-valued, squash to 0 when unknown bits exist. + if (isUnknown) { + Value zeroI1 = + hw::ConstantOp::create(builder, loc, builder.getI1Type(), 0); + result = comb::MuxOp::create(builder, loc, isUnknown, zeroI1, result); + Value resultMoore = moore::FromBuiltinIntOp::create(builder, loc, result); + return moore::IntToLogicOp::create(builder, loc, resultMoore).getResult(); + } + return moore::FromBuiltinIntOp::create(builder, loc, result); + } + + if (nameId == ksn::CountOnes) { + assert(numArgs == 1 && "`$countones` takes 1 argument"); + auto value = convertRvalueExpression(*args[0]); + if (!value) + return {}; + auto valTy = dyn_cast(value.getType()); + if (!valTy) { + mlir::emitError(loc) << "expected integer argument for `$countones`"; + return {}; + } + + // Coerce four-valued input to two-valued for the comb ops. + Value intVal = coerceToBuiltinInt(builder, loc, value, valTy); + + // Popcount: extract each bit, zero-extend to result width, and sum. + auto builtinIntTy = cast(intVal.getType()); + unsigned width = builtinIntTy.getWidth(); + unsigned resultWidth = llvm::Log2_32_Ceil(width + 1); + auto i1Ty = builder.getI1Type(); + unsigned padWidth = resultWidth - 1; + auto zeros = hw::ConstantOp::create(builder, loc, + builder.getIntegerType(padWidth), 0); + + // Zero-extend the first bit to seed the accumulator. + auto bit0 = comb::ExtractOp::create(builder, loc, i1Ty, intVal, 0); + Value sum = comb::ConcatOp::create(builder, loc, ValueRange{zeros, bit0}); + + for (unsigned i = 1; i < width; ++i) { + auto bit = comb::ExtractOp::create(builder, loc, i1Ty, intVal, i); + auto extended = + comb::ConcatOp::create(builder, loc, ValueRange{zeros, bit}); + sum = comb::AddOp::create(builder, loc, sum, extended); + } + + // Wrap back into Moore type (unsigned — CountOnes result is never signed). + return moore::FromBuiltinIntOp::create(builder, loc, sum); + } + // Real math functions (all take 1 real argument) if (nameId == ksn::Ln) return convertRealMathBI(*this, loc, name, args); diff --git a/test/Conversion/ImportVerilog/builtins.sv b/test/Conversion/ImportVerilog/builtins.sv index 4c36a55e3afe..56a6d4b46a39 100644 --- a/test/Conversion/ImportVerilog/builtins.sv +++ b/test/Conversion/ImportVerilog/builtins.sv @@ -602,16 +602,11 @@ module SampleValueBuiltins #() ( // CHECK: [[AND:%.+]] = comb.and [[DB]], [[SUB]] : i8 // CHECK: [[ZERO:%.+]] = hw.constant 0 : i8 // CHECK: [[EQ:%.+]] = comb.icmp eq [[AND]], [[ZERO]] : i8 - // CHECK: [[EQ_INT:%.+]] = moore.from_builtin_int [[EQ]] : i1 - // CHECK: [[EQ_LOGIC:%.+]] = moore.int_to_logic [[EQ_INT]] : i1 - // CHECK: [[EQ_L2I:%.+]] = moore.logic_to_int [[EQ_LOGIC]] : l1 - // CHECK: [[EQ_BUILTIN:%.+]] = moore.to_builtin_int [[EQ_L2I]] : i1 // CHECK: [[FALSE:%.+]] = hw.constant false - // CHECK: [[MUX:%.+]] = comb.mux [[ISUNKNOWN_I1]], [[FALSE]], [[EQ_BUILTIN]] : i1 + // CHECK: [[MUX:%.+]] = comb.mux [[ISUNKNOWN_I1]], [[FALSE]], [[EQ]] : i1 // CHECK: [[RES_INT:%.+]] = moore.from_builtin_int [[MUX]] : i1 // CHECK: [[RES_LOGIC:%.+]] = moore.int_to_logic [[RES_INT]] : i1 - // CHECK: [[RES_L2I:%.+]] = moore.logic_to_int [[RES_LOGIC]] : l1 - // CHECK: [[RES_BUILTIN:%.+]] = moore.to_builtin_int [[RES_L2I]] : i1 + // CHECK: [[RES_BUILTIN:%.+]] = moore.to_builtin_int [[RES_INT]] : i1 // CHECK: ltl.clock [[RES_BUILTIN]] onehot0_data: assert property (@(posedge clk_i) $onehot0(data_i)); @@ -630,16 +625,11 @@ module SampleValueBuiltins #() ( // CHECK: [[EQ:%.+]] = comb.icmp eq [[AND]], [[ZERO]] : i8 // CHECK: [[NE:%.+]] = comb.icmp ne [[DB]], [[ZERO]] : i8 // CHECK: [[AND2:%.+]] = comb.and [[EQ]], [[NE]] : i1 - // CHECK: [[RES_INT_2:%.+]] = moore.from_builtin_int [[AND2]] : i1 - // CHECK: [[RES_LOGIC_2:%.+]] = moore.int_to_logic [[RES_INT_2]] : i1 - // CHECK: [[RES_L2I_2:%.+]] = moore.logic_to_int [[RES_LOGIC_2]] : l1 - // CHECK: [[RES_BUILTIN_2:%.+]] = moore.to_builtin_int [[RES_L2I_2]] : i1 // CHECK: [[FALSE:%.+]] = hw.constant false - // CHECK: [[MUX:%.+]] = comb.mux [[ISUNKNOWN_I1]], [[FALSE]], [[RES_BUILTIN_2]] : i1 + // CHECK: [[MUX:%.+]] = comb.mux [[ISUNKNOWN_I1]], [[FALSE]], [[AND2]] : i1 // CHECK: [[RES_INT:%.+]] = moore.from_builtin_int [[MUX]] : i1 // CHECK: [[RES_LOGIC:%.+]] = moore.int_to_logic [[RES_INT]] : i1 - // CHECK: [[RES_L2I:%.+]] = moore.logic_to_int [[RES_LOGIC]] : l1 - // CHECK: [[RES_BUILTIN:%.+]] = moore.to_builtin_int [[RES_L2I]] : i1 + // CHECK: [[RES_BUILTIN:%.+]] = moore.to_builtin_int [[RES_INT]] : i1 // CHECK: ltl.clock [[RES_BUILTIN]] onehot_data: assert property (@(posedge clk_i) $onehot(data_i)); @@ -671,6 +661,37 @@ module SampleValueBuiltins #() ( // CHECK: ltl.clock [[RES_BUILTIN]] onehot_bit_data: assert property (@(posedge clk_i) $onehot(data_bit_i)); + // CHECK: moore.procedure always { + // CHECK: [[D:%.+]] = moore.read [[DATAWIRE]] : + // CHECK: [[D_L2I:%.+]] = moore.logic_to_int [[D]] : l8 + // CHECK: [[DB:%.+]] = moore.to_builtin_int [[D_L2I]] : i8 + // CHECK: [[Z3:%.+]] = hw.constant 0 : i3 + // CHECK: [[B0:%.+]] = comb.extract [[DB]] from 0 : (i8) -> i1 + // CHECK: [[EXT0:%.+]] = comb.concat [[Z3]], [[B0]] : i3, i1 + // CHECK: [[B1:%.+]] = comb.extract [[DB]] from 1 : (i8) -> i1 + // CHECK: [[EXT1:%.+]] = comb.concat [[Z3]], [[B1]] : i3, i1 + // CHECK: [[RES_INT:%.+]] = moore.from_builtin_int {{%.+}} : i4 + // CHECK: [[SEXT:%.+]] = moore.zext [[RES_INT]] : i4 -> i32 + // CHECK: [[ZERO:%.+]] = moore.constant 0 : i32 + // CHECK: [[EQ:%.+]] = moore.eq [[SEXT]], [[ZERO]] : i32 -> i1 + countones_data: + assert property (@(posedge clk_i) $countones(data_i) == 0); + + // CHECK: moore.procedure always { + // CHECK: [[D:%.+]] = moore.read [[DATABITWIRE]] : + // CHECK: [[DB:%.+]] = moore.to_builtin_int [[D]] : i8 + // CHECK: [[Z3:%.+]] = hw.constant 0 : i3 + // CHECK: [[B0:%.+]] = comb.extract [[DB]] from 0 : (i8) -> i1 + // CHECK: [[EXT0:%.+]] = comb.concat [[Z3]], [[B0]] : i3, i1 + // CHECK: [[B1:%.+]] = comb.extract [[DB]] from 1 : (i8) -> i1 + // CHECK: [[EXT1:%.+]] = comb.concat [[Z3]], [[B1]] : i3, i1 + // CHECK: comb.add + // CHECK: [[RES_INT:%.+]] = moore.from_builtin_int {{%.+}} : i4 + // CHECK: [[SEXT:%.+]] = moore.zext [[RES_INT]] : i4 -> i32 + // CHECK: [[ZERO:%.+]] = moore.constant 0 : i32 + // CHECK: [[EQ:%.+]] = moore.eq [[SEXT]], [[ZERO]] : i32 -> i1 + countones_bit_data: + assert property (@(posedge clk_i) $countones(data_bit_i) == 0); endmodule // CHECK-LABEL: func.func private @StringBuiltins(