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

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
57 changes: 47 additions & 10 deletions lib/Conversion/ImportVerilog/AssertionExpr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -318,6 +318,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,31 +331,31 @@ 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));
}

Expand All @@ -362,7 +367,7 @@ FailureOr<Value> Context::convertAssertionSystemCallArity1(
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(
return castToTwoValued(comb::ICmpOp::create(
builder, loc, comb::ICmpPredicate::eq, anded, zero, false));
}

Expand All @@ -376,7 +381,30 @@ FailureOr<Value> Context::convertAssertionSystemCallArity1(
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);
return castToTwoValued(result);
}

case ksn::CountOnes: {
// Popcount: extract each bit, zero-extend to result width, and sum.
auto intTy = cast<IntegerType>(value.getType());
unsigned width = intTy.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, value, 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, value, i);
auto extended =
comb::ConcatOp::create(builder, loc, ValueRange{zeros, bit});
sum = comb::AddOp::create(builder, loc, sum, extended);
}
return castToTwoValued(sum);
}

default:
Expand Down Expand Up @@ -458,7 +486,8 @@ Value Context::convertAssertionCallExpression(
// 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());
result = getIsUnknown(builder, loc, value, valTy, getContext());
break;
}

// OneHot/OneHot0 are handled both here and below.
Expand Down Expand Up @@ -496,7 +525,9 @@ Value Context::convertAssertionCallExpression(

Value finalResult =
moore::FromBuiltinIntOp::create(builder, loc, resultBuiltin);
return moore::IntToLogicOp::create(builder, loc, finalResult);
result =
moore::IntToLogicOp::create(builder, loc, finalResult).getResult();
break;
}

// If the value is four-valued, we need to map it to two-valued before we
Expand All @@ -517,8 +548,14 @@ Value Context::convertAssertionCallExpression(

if (failed(result))
return {};
if (*result)
return *result;
if (*result) {
auto expectedTy = convertType(*expr.type);
return materializeConversion(expectedTy, *result,
(subroutine.knownNameId !=
slang::parsing::KnownSystemName::CountOnes) &&
expr.type->isSigned(),
loc);
}

mlir::emitError(loc) << "unsupported system call `" << subroutine.name << "`";
return {};
Expand Down
1 change: 1 addition & 0 deletions lib/Conversion/ImportVerilog/Expressions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2044,6 +2044,7 @@ struct RvalueExprVisitor : public ExprVisitor {
case ksn::IsUnknown:
case ksn::OneHot:
case ksn::OneHot0:
case ksn::CountOnes:
return context.convertAssertionCallExpression(expr, info, loc);
default:
break;
Expand Down
45 changes: 35 additions & 10 deletions test/Conversion/ImportVerilog/builtins.sv
Original file line number Diff line number Diff line change
Expand Up @@ -603,15 +603,12 @@ module SampleValueBuiltins #() (
// 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: [[EQ_BUILTIN:%.+]] = moore.to_builtin_int [[EQ_INT]] : i1
// CHECK: [[FALSE:%.+]] = hw.constant false
// CHECK: [[MUX:%.+]] = comb.mux [[ISUNKNOWN_I1]], [[FALSE]], [[EQ_BUILTIN]] : 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));

Expand All @@ -631,15 +628,12 @@ module SampleValueBuiltins #() (
// 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: [[RES_BUILTIN_2:%.+]] = moore.to_builtin_int [[RES_INT_2]] : i1
// CHECK: [[FALSE:%.+]] = hw.constant false
// CHECK: [[MUX:%.+]] = comb.mux [[ISUNKNOWN_I1]], [[FALSE]], [[RES_BUILTIN_2]] : 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));

Expand Down Expand Up @@ -671,6 +665,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]] : <l8>
// 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]] : <i8>
// 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(
Expand Down
Loading