[HWToBTOR2] Fix incorrect le/ge predicate name emission (#8028)

llvm · Jan 4, 2025 · a15654c · a15654c
1 parent f58c2d9
commit a15654c
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 0 deletions.
diff --git 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
@@ -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]+]]