[ImportVerilog] Add support for oneshot

jpienaar · jpienaar · commit 863896847565 · 2026-05-14T16:27:26.000Z
This followed a mix of isuknown and regular LTL lowering. This is to
ensure that the behavior is correct with unknown values.
diff --git a/docs/Dialects/LTL.md b/docs/Dialects/LTL.md
@@ -263,9 +263,59 @@ where the `logic_to_int` conversion is only necessary if `%cond` is 4-valued.
 %isunknown = moore.case_eq %reduced, %x : i1
 ```
 
+- **`$onehot0(a)`**:
+For 2-state input `%a` (where `%a` has type `iN`):
+
+```mlir
+%one = hw.constant 1 : iN
+%sub = comb.sub %a, %one : iN
+%and = comb.and %a, %sub : iN
+%zero = hw.constant 0 : iN
+%onehot0 = comb.icmp eq %and, %zero : iN
+```
+
+For 4-state input `%a` (where `%a` has type `!moore.lN`):
+First, `%a` is checked for unknown values (equivalent to `$isunknown(a)`). If
+any bits are unknown, the result is `1'b0`. Otherwise, it uses the 2-state
+lowering above on the coerced 2-state value:
+
+```mlir
+%isunknown = ... // see $isunknown lowering
+%coerced_a = moore.logic_to_int %a
+%int_a = moore.to_builtin_int %coerced_a
+%onehot0_2state = ... // 2-state lowering on %int_a
+%zero = hw.constant 0 : i1
+%onehot0 = comb.mux %isunknown, %zero, %onehot0_2state : i1
+```
+
+- **`$onehot(a)`**:
+For 2-state input `%a` (where `%a` has type `iN`):
+
+```mlir
+%one = hw.constant 1 : iN
+%sub = comb.sub %a, %one : iN
+%and = comb.and %a, %sub : iN
+%zero = hw.constant 0 : iN
+%onehot0 = comb.icmp eq %and, %zero : iN
+%notzero = comb.icmp ne %a, %zero : iN
+%onehot = comb.and %onehot0, %notzero : i1
+```
+
+For 4-state input `%a` (where `%a` has type `!moore.lN`):
+First, `%a` is checked for unknown values (equivalent to `$isunknown(a)`). If
+any bits are unknown, the result is `1'b0`. Otherwise, it uses the 2-state
+lowering above on the coerced 2-state value:
+
+```mlir
+%isunknown = ... // see $isunknown lowering
+%coerced_a = moore.logic_to_int %a
+%int_a = moore.to_builtin_int %coerced_a
+%onehot_2state = ... // 2-state lowering on %int_a
+%zero = hw.constant 0 : i1
+%onehot = comb.mux %isunknown, %zero, %onehot_2state : i1
+```
+
 > The following functions are not yet supported by CIRCT:  
-> - **`$onehot(a)`**  
-> - **`$onehot0(a)`**  
 > - **`$countones(a)`**     
   
   
diff --git a/lib/Conversion/ImportVerilog/AssertionExpr.cpp b/lib/Conversion/ImportVerilog/AssertionExpr.cpp
@@ -357,11 +357,48 @@ FailureOr<Value> Context::convertAssertionSystemCallArity1(
   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 = builder.create<comb::SubOp>(loc, value, one);
+    auto anded = builder.create<comb::AndOp>(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 = builder.create<comb::SubOp>(loc, value, one);
+    auto anded = builder.create<comb::AndOp>(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) {
@@ -421,19 +458,46 @@ 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) {
-      Value bitVal = value;
-      if (valTy.getWidth() > 1) {
-        auto mooreI1Type =
-            moore::IntType::get(getContext(), 1, valTy.getDomain());
-        bitVal = moore::ReduceXorOp::create(builder, loc, mooreI1Type, value);
-      }
-
-      auto xType =
-          moore::IntType::get(getContext(), 1, moore::Domain::FourValued);
-      auto xValue = FVInt::getAllX(1);
-      auto xConst = moore::ConstantOp::create(builder, loc, xType, xValue);
+      return getIsUnknown(builder, loc, value, valTy, getContext());
+    }
 
-      return moore::CaseEqOp::create(builder, loc, bitVal, xConst).getResult();
+    // OneHot/OneHot0 are handled both here and below.
+    if (subroutine.knownNameId == slang::parsing::KnownSystemName::OneHot ||
+        subroutine.knownNameId == slang::parsing::KnownSystemName::OneHot0) {
+      if (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 = builder.create<comb::MuxOp>(
+            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
diff --git a/lib/Conversion/ImportVerilog/Expressions.cpp b/lib/Conversion/ImportVerilog/Expressions.cpp
@@ -2030,6 +2030,8 @@ struct RvalueExprVisitor : public ExprVisitor {
     case ksn::Past:
     case ksn::Sampled:
     case ksn::IsUnknown:
+    case ksn::OneHot:
+    case ksn::OneHot0:
       return context.convertAssertionCallExpression(expr, info, loc);
     default:
       break;
diff --git a/test/Conversion/ImportVerilog/builtins.sv b/test/Conversion/ImportVerilog/builtins.sv
@@ -409,10 +409,12 @@ endfunction
 // CHECK-SAME: in [[CLK:%.+]] : !moore.l1
 module SampleValueBuiltins #() (
     input clk_i,
-    input [7:0] data_i
+    input [7:0] data_i,
+    input bit [7:0] data_bit_i
 );
   // CHECK: [[CLKWIRE:%.+]] = moore.net name "clk_i" wire : <l1>
   // CHECK: [[DATAWIRE:%.+]] = moore.net name "data_i" wire : <l8>
+  // CHECK: [[DATABITWIRE:%.+]] = moore.variable name "data_bit_i" : <i8>
   // CHECK: moore.procedure always {
   // CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
   // CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
@@ -587,6 +589,88 @@ module SampleValueBuiltins #() (
   // CHECK: ltl.clock [[CEQ_I1]]
   isunknown_data: assert property (@(posedge clk_i) $isunknown(data_i));
 
+  // CHECK: moore.procedure always {
+  // CHECK: [[D:%.+]] = moore.read [[DATAWIRE]] : <l8>
+  // CHECK: [[RED:%.+]] = moore.reduce_xor [[D]] : l8 -> l1
+  // CHECK: [[X:%.+]] = moore.constant bX : l1
+  // CHECK: [[ISUNKNOWN:%.+]] = moore.case_eq [[RED]], [[X]] : l1
+  // CHECK: [[ISUNKNOWN_I1:%.+]] = moore.to_builtin_int [[ISUNKNOWN]] : i1
+  // CHECK: [[D_L2I:%.+]] = moore.logic_to_int [[D]] : l8
+  // CHECK: [[DB:%.+]] = moore.to_builtin_int [[D_L2I]] : i8
+  // CHECK: [[ONE:%.+]] = hw.constant 1 : i8
+  // CHECK: [[SUB:%.+]] = comb.sub [[DB]], [[ONE]] : i8
+  // 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: [[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: ltl.clock [[RES_BUILTIN]]
+  onehot0_data: assert property (@(posedge clk_i) $onehot0(data_i));
+
+  // CHECK: moore.procedure always {
+  // CHECK: [[D:%.+]] = moore.read [[DATAWIRE]] : <l8>
+  // CHECK: [[RED:%.+]] = moore.reduce_xor [[D]] : l8 -> l1
+  // CHECK: [[X:%.+]] = moore.constant bX : l1
+  // CHECK: [[ISUNKNOWN:%.+]] = moore.case_eq [[RED]], [[X]] : l1
+  // CHECK: [[ISUNKNOWN_I1:%.+]] = moore.to_builtin_int [[ISUNKNOWN]] : i1
+  // CHECK: [[D_L2I:%.+]] = moore.logic_to_int [[D]] : l8
+  // CHECK: [[DB:%.+]] = moore.to_builtin_int [[D_L2I]] : i8
+  // CHECK: [[ONE:%.+]] = hw.constant 1 : i8
+  // CHECK: [[SUB:%.+]] = comb.sub [[DB]], [[ONE]] : i8
+  // CHECK: [[AND:%.+]] = comb.and [[DB]], [[SUB]] : i8
+  // CHECK: [[ZERO:%.+]] = hw.constant 0 : i8
+  // 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: [[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: ltl.clock [[RES_BUILTIN]]
+  onehot_data: assert property (@(posedge clk_i) $onehot(data_i));
+
+  // CHECK: moore.procedure always {
+  // CHECK: [[D:%.+]] = moore.read [[DATABITWIRE]] : <i8>
+  // CHECK: [[DB:%.+]] = moore.to_builtin_int [[D]] : i8
+  // CHECK: [[ONE:%.+]] = hw.constant 1 : i8
+  // CHECK: [[SUB:%.+]] = comb.sub [[DB]], [[ONE]] : i8
+  // 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_BUILTIN:%.+]] = moore.to_builtin_int [[EQ_INT]] : i1
+  // CHECK: ltl.clock [[EQ_BUILTIN]]
+  onehot0_bit_data: assert property (@(posedge clk_i) $onehot0(data_bit_i));
+
+  // CHECK: moore.procedure always {
+  // CHECK: [[D:%.+]] = moore.read [[DATABITWIRE]] : <i8>
+  // CHECK: [[DB:%.+]] = moore.to_builtin_int [[D]] : i8
+  // CHECK: [[ONE:%.+]] = hw.constant 1 : i8
+  // CHECK: [[SUB:%.+]] = comb.sub [[DB]], [[ONE]] : i8
+  // CHECK: [[AND:%.+]] = comb.and [[DB]], [[SUB]] : i8
+  // CHECK: [[ZERO:%.+]] = hw.constant 0 : i8
+  // 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:%.+]] = moore.from_builtin_int [[AND2]] : i1
+  // CHECK: [[RES_BUILTIN:%.+]] = moore.to_builtin_int [[RES_INT]] : i1
+  // CHECK: ltl.clock [[RES_BUILTIN]]
+  onehot_bit_data: assert property (@(posedge clk_i) $onehot(data_bit_i));
+
 endmodule
 
 // CHECK-LABEL: func.func private @StringBuiltins(
