[HWToBTOR2] Avoid duplicating initial consts (#7854)

llvm · Nov 20, 2024 · 65e230c · 65e230c
1 parent 87948a2
commit 65e230c
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 1 deletion.
diff --git a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
@@ -621,6 +621,10 @@ struct ConvertHWToBTOR2Pass
   // simplicity, we will only emit `constd` in order to avoid bit-string
   // conversions
   void visitTypeOp(hw::ConstantOp op) {
+    // Make sure the constant hasn't already been created
+    if (handledOps.contains(op))
+      return;
+
     // Make sure that a sort has been created for our operation
     int64_t w = requireSort(op.getType());
 

diff --git a/test/Conversion/HWToBTOR2/compreg.mlir b/test/Conversion/HWToBTOR2/compreg.mlir
@@ -9,6 +9,11 @@ module {
     // Registers are all emitted before any other operation
     //CHECK:    [[NID6:[0-9]+]] sort bitvec 32
     //CHECK:    [[NID12:[0-9]+]] state [[NID6]] count
+    //CHECK:    [[INITCONST:[0-9]+]] constd [[NID6]] 0
+    //CHECK:    [[INIT:[0-9]+]] init [[NID6]] [[NID12]] [[INITCONST]]
+    //CHECK:    [[REG2NID:[0-9]+]] state [[NID6]] count2
+    //CHECK-NOT: [[INITCONST]] constd [[NID6]] 0
+    //CHECK:    [[INIT:[0-9]+]] init [[NID6]] [[REG2NID]] [[INITCONST]]
 
     //CHECK:    [[NID3:[0-9]+]] sort bitvec 28
     //CHECK:    [[NID4:[0-9]+]] constd [[NID3]] 0 
@@ -30,7 +35,13 @@ module {
     //CHECK:    [[NID11:[0-9]+]] constd [[NID6]] 0
     %c0_i32 = hw.constant 0 : i32
 
-    %count = seq.compreg %9, %clock reset %reset, %c0_i32 : i32
+    %init = seq.initial () {
+        %c0_i8 = hw.constant 0 : i32
+        seq.yield %c0_i8 : i32
+    } : () -> !seq.immutable<i32>
+
+    %count = seq.compreg %9, %clock reset %reset, %c0_i32 initial %init : i32
+    %count2 = seq.compreg %9, %clock reset %reset, %c0_i32 initial %init : i32
 
     //CHECK:    [[NID13:[0-9]+]] eq [[NID0]] [[NID12]] [[NID7]]
     %1 = comb.icmp bin eq %count, %c22_i32 : i32