Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 25 additions & 2 deletions docs/Dialects/LTL.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)`**:

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should I move these to Moore.md or add a new ImportVerilog.md doc? (and with this PR or a follow up?)

@fabianschuiki fabianschuiki Jun 4, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think Moore.md might make sense since it is pretty much tailored to be the Verilog ingestion dialect. Feel free to do this whenever works for you, this PR or a follow up -- I don't want to hold up nice contributions over small documentation tweaks 😁

We could do a cleanup PR later where we move all of these over into Expressions.cpp, and also move the documentation if that makes sense.

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`**:
Expand Down
104 changes: 14 additions & 90 deletions lib/Conversion/ImportVerilog/AssertionExpr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -318,6 +316,11 @@ FailureOr<Value> 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));
Expand All @@ -326,79 +329,42 @@ FailureOr<Value> 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));
}

// Translate $rose to x[0] ∧ ¬x[-1]
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));
}

// Translate $changed to x[0] ≠ x[-1]
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));
}

// Translate $stable to x[0] = x[-1]
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) {
Expand Down Expand Up @@ -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<moore::ToBuiltinIntOp>(loc, isUnknownMoore);

Value coerced = builder.createOrFold<moore::LogicToIntOp>(loc, value);
Value state2IntVal =
builder.createOrFold<moore::ToBuiltinIntOp>(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) {
Expand All @@ -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 {};
Expand Down
147 changes: 141 additions & 6 deletions lib/Conversion/ImportVerilog/Expressions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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<moore::LogicToIntOp>(loc, value);
return builder.createOrFold<moore::ToBuiltinIntOp>(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`.
Expand Down Expand Up @@ -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) {
Expand All @@ -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;
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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<moore::IntType>(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<moore::IntType>(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<moore::ToBuiltinIntOp>(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<moore::IntType>(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<IntegerType>(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<moore::LnBIOp>(*this, loc, name, args);
Expand Down
Loading
Loading