From 385b394ccd64bcf2e3365626b18f8826379a1707 Mon Sep 17 00:00:00 2001
From: Bea Healy <beahealy22@gmail.com>
Date: Fri, 31 Oct 2025 14:41:45 +0000
Subject: [PATCH 1/2] [HWToBTOR2] Support unary case of variadics

---
 lib/Conversion/HWToBTOR2/HWToBTOR2.cpp | 11 ++++++++---
 test/Conversion/HWToBTOR2/comb.mlir    | 12 ++++++++----
 2 files changed, 16 insertions(+), 7 deletions(-)

diff --git a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
index 9faa5db1858f..c6b37543eb89 100644
--- a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
+++ b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
@@ -301,9 +301,14 @@ struct ConvertHWToBTOR2Pass
     auto operands = op->getOperands();
     size_t sid = sortToLIDMap.at(width);
 
-    if (operands.size() < 2) {
-      op->emitError("variadic operations with less than 2 operands are not "
-                    "currently supported");
+    // If there's only one operand, then we don't generate a BTOR2 instruction,
+    // we just reuse the operand's existing LID
+    if (operands.size() == 1) {
+      auto existingLID = getOpLID(operands[0]);
+      // Check that we haven't somehow got a value that doesn't have a
+      // corresponding LID
+      assert(existingLID != noLID);
+      opLIDMap[op] = existingLID;
       return;
     }
 
diff --git a/test/Conversion/HWToBTOR2/comb.mlir b/test/Conversion/HWToBTOR2/comb.mlir
index 5904b197f333..1f028c63f6f1 100644
--- a/test/Conversion/HWToBTOR2/comb.mlir
+++ b/test/Conversion/HWToBTOR2/comb.mlir
@@ -55,10 +55,14 @@ module {
     // CHECK:   [[NID18:[0-9]+]] and [[NID0]] [[NID17]] [[NID10]]
     %10 = comb.and %a, %3, %3 : i32
 
-
-    // CHECK:   [[NID19:[0-9]+]] implies [[NID3]] [[NID5]] [[NID12]]
-    // CHECK:   [[NID20:[0-9]+]] not [[NID3]] [[NID19]]
-    // CHECK:   [[NID21:[0-9]+]] bad [[NID20:[0-9]+]]
+    // Variadic ops with one operand should be forwarded to the operand's LID
+    // CHECK: [[NID19:[0-9]+]] and [[NID0]] 2 [[NID18]]
+    %11 = comb.and %10 : i32
+    %12 = comb.and %a, %11 : i32
+
+    // CHECK:   [[ASSERTNID1:[0-9]+]] implies [[NID3]] [[NID5]] [[NID12]]
+    // CHECK:   [[ASSERTNID2:[0-9]+]] not [[NID3]] [[ASSERTNID1]]
+    // CHECK:   [[ASSERTNID3:[0-9]+]] bad [[ASSERTNID2:[0-9]+]]
     sv.always posedge %0 {
       sv.if %true {
         sv.assert %5, immediate message "a + 1 should be greater than a"

From 16324e8c32d8750cd017842ef4d1ad1ee06774b3 Mon Sep 17 00:00:00 2001
From: Bea Healy <57840981+TaoBi22@users.noreply.github.com>
Date: Fri, 31 Oct 2025 15:29:39 +0000
Subject: [PATCH 2/2] Add 0-operand case comment

---
 lib/Conversion/HWToBTOR2/HWToBTOR2.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
index c6b37543eb89..8f9ba9dde945 100644
--- a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
+++ b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
@@ -301,6 +301,7 @@ struct ConvertHWToBTOR2Pass
     auto operands = op->getOperands();
     size_t sid = sortToLIDMap.at(width);
 
+    // No need to consider 0-operand case as it'll be rejected by the verifier
     // If there's only one operand, then we don't generate a BTOR2 instruction,
     // we just reuse the operand's existing LID
     if (operands.size() == 1) {