[HWToBTOR2] Generate register initial constant before state declarati…

…on (#7939)
llvm · Dec 3, 2024 · 3004ca1 · 3004ca1
1 parent be1add1
commit 3004ca1
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 12 deletions.
diff --git a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
@@ -885,9 +885,9 @@ struct ConvertHWToBTOR2Pass
     // btor2
     auto init = reg.getInitialValue();
 
-    // Generate state instruction (represents the register declaration)
-    genState(reg, w, regName);
-
+    // If there's an initial value, we need to generate a constant for the
+    // initial value, then declare the state, then generate the init statement
+    // (BTOR2 parsers are picky about it being in this order)
     if (init) {
       if (!init.getDefiningOp<seq::InitialOp>()) {
         reg->emitError(
@@ -906,8 +906,14 @@ struct ConvertHWToBTOR2Pass
       // Add it to the list of visited operations
       handledOps.insert(initialConstant);
 
+      // Now we can declare the state
+      genState(reg, w, regName);
+
       // Finally generate the init statement
       genInit(reg, initialConstant, w);
+    } else {
+      // Just generate state instruction (represents the register declaration)
+      genState(reg, w, regName);
     }
 
     // Record the operation for future `next` instruction generation

diff --git a/test/Conversion/HWToBTOR2/compreg.mlir b/test/Conversion/HWToBTOR2/compreg.mlir
@@ -8,8 +8,8 @@ module {
     %0 = seq.from_clock %clock
     // 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:    [[NID12:[0-9]+]] state [[NID6]] count
     //CHECK:    [[INIT:[0-9]+]] init [[NID6]] [[NID12]] [[INITCONST]]
     //CHECK:    [[REG2NID:[0-9]+]] state [[NID6]] count2
     //CHECK-NOT: [[INITCONST]] constd [[NID6]] 0

diff --git a/test/Conversion/HWToBTOR2/init.mlir b/test/Conversion/HWToBTOR2/init.mlir
@@ -4,10 +4,10 @@ module {
   //CHECK:    [[NID0:[0-9]+]] sort bitvec 1
   //CHECK:    [[NID1:[0-9]+]] input [[NID0]] reset
   hw.module @test(in %clock : !seq.clock, in %reset : i1) {
-    // Register states get pregenerated
-    //CHECK:    [[NID2:[0-9]+]] state [[NID0]] reg
     %0 = seq.from_clock %clock 
     //CHECK:    [[NID3:[0-9]+]] constd [[NID0]] 0
+    // Register states get pregenerated
+    //CHECK:    [[NID2:[0-9]+]] state [[NID0]] reg
     %false = hw.constant false
     //CHECK:    [[INIT:[0-9]+]] init [[NID0]] [[NID2]] [[NID3]]
     %init = seq.initial() {

diff --git a/test/firtool/btor2-assertproperty.fir b/test/firtool/btor2-assertproperty.fir
@@ -24,9 +24,9 @@ circuit Counter :
 ; CHECK:  2 input 1 reset
 ; CHECK:  3 sort bitvec 32
 ; CHECK:  4 state 3 count
-; CHECK:  5 state 1 hbr
-; CHECK:  6 constd 1 0
-; CHECK:  7 init 1 5 6
+; CHECK:  5 constd 1 0
+; CHECK:  6 state 1 hbr
+; CHECK:  7 init 1 6 5
 ; CHECK:  8 constd 3 1
 ; CHECK:  9 constd 3 10
 ; CHECK:  10 constd 3 22
@@ -36,12 +36,12 @@ circuit Counter :
 ; CHECK:  14 ite 3 12 11 13
 ; CHECK:  15 neq 1 4 9
 ; CHECK:  16 constd 1 -1
-; CHECK:  17 or 1 2 5
+; CHECK:  17 or 1 2 6
 ; CHECK:  18 xor 1 2 16
-; CHECK:  19 and 1 5 18
+; CHECK:  19 and 1 6 18
 ; CHECK:  20 implies 1 19 15
 ; CHECK:  21 not 1 20
 ; CHECK:  22 bad 21
 ; CHECK:  23 ite 3 2 11 14
 ; CHECK:  24 next 3 4 23
-; CHECK:  25 next 1 5 17
+; CHECK:  25 next 1 6 17