Skip to content
Merged
Show file tree
Hide file tree
Changes from 4 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?)

Copy link
Copy Markdown
Contributor

@fabianschuiki fabianschuiki Jun 4, 2026

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
Loading
Loading