From a15654cd5d518e844d7187d10d748a184e0ce282 Mon Sep 17 00:00:00 2001
From: Bea Healy <57840981+TaoBi22@users.noreply.github.com>
Date: Sat, 4 Jan 2025 21:14:21 +0000
Subject: [PATCH] [HWToBTOR2] Fix incorrect le/ge predicate name emission
 (#8028)

---
 lib/Conversion/HWToBTOR2/HWToBTOR2.cpp |  8 ++++++++
 test/Conversion/HWToBTOR2/comb.mlir    | 12 ++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
index 2ecd16cfa8d9..d6a0f30cc8ff 100644
--- a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
+++ b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
@@ -711,6 +711,14 @@ struct ConvertHWToBTOR2Pass
     // Check for special cases where hw doesn't align with btor syntax
     if (pred == "ne")
       pred = "neq";
+    else if (pred == "ule")
+      pred = "ulte";
+    else if (pred == "sle")
+      pred = "slte";
+    else if (pred == "uge")
+      pred = "ugte";
+    else if (pred == "sge")
+      pred = "sgte";
 
     // Width of result is always 1 for comparison
     genSort("bitvec", 1);
diff --git a/test/Conversion/HWToBTOR2/comb.mlir b/test/Conversion/HWToBTOR2/comb.mlir
index 6e0cc506c2cc..7a5fcebbe5af 100644
--- a/test/Conversion/HWToBTOR2/comb.mlir
+++ b/test/Conversion/HWToBTOR2/comb.mlir
@@ -39,6 +39,18 @@ module {
     // CHECK:   [[NID12:[0-9]+]] ugt [[NID3]] [[NID10]] 2
     %5 = comb.icmp bin ugt %3, %a : i32
 
+    // CHECK:   [[NID13:[0-9]+]] ulte [[NID3]] [[NID10]] 2
+    %6 = comb.icmp bin ule %3, %a : i32
+
+    // CHECK:   [[NID14:[0-9]+]] slte [[NID3]] [[NID10]] 2
+    %7 = comb.icmp bin sle %3, %a : i32
+
+    // CHECK:   [[NID15:[0-9]+]] ugte [[NID3]] [[NID10]] 2
+    %8 = comb.icmp bin uge %3, %a : i32
+
+    // CHECK:   [[NID16:[0-9]+]] sgte [[NID3]] [[NID10]] 2
+    %9 = comb.icmp bin sge %3, %a : i32
+
     // CHECK:   [[NID13:[0-9]+]] implies [[NID3]] [[NID5]] [[NID12]]
     // CHECK:   [[NID14:[0-9]+]] not [[NID3]] [[NID13]]
     // CHECK:   [[NID15:[0-9]+]] bad [[NID14:[0-9]+]]