[HW to BTOR2] Add support for nested Wires and Compreg

lib/Conversion/HWToBTOR2/HWToBTOR2.cpp

@@ -156,15 +156,20 @@ struct ConvertHWToBTOR2Pass
   // If so, the original operation is returned
   // Otherwise the argument is returned as it is the original op
   Operation *getOpAlias(Operation *op) {
+
+    // Remove the alias until none are left (for wires of wires of wires ...)
     if (auto it = opAliasMap.find(op); it != opAliasMap.end())
       return it->second;
+
     // If the op isn't an alias then simply return it
     return op;
   }
 
   // Updates or creates an entry for the given operation
   // associating it with the current lid
-  void setOpAlias(Operation *alias, Operation *op) { opAliasMap[alias] = op; }
+  void setOpAlias(Operation *alias, Operation *op) {
+    opAliasMap[alias] = getOpAlias(op);
+  }
 
   // Checks if a sort was declared with the given width
   // If so, its lid will be returned
@@ -461,24 +466,31 @@ struct ConvertHWToBTOR2Pass
   // Generates the transitions required to finalize the register to state
   // transition system conversion
   void finalizeRegVisit(Operation *op) {
-    // Check the register type (done to support non-firrtl registers as well)
-    auto reg = cast<seq::FirRegOp>(op);
+    int64_t width;
+    Value next, resetVal;
+
+    // Extract the operands depending on the register type
+    if (auto reg = dyn_cast<seq::CompRegOp>(op)) {
+      width = hw::getBitWidth(reg.getType());
+      next = reg.getInput();
+      resetVal = reg.getResetValue();
+    } else if (auto reg = dyn_cast<seq::FirRegOp>(op)) {
+      width = hw::getBitWidth(reg.getType());
+      next = reg.getNext();
+      resetVal = reg.getResetValue();
+    } else {
+      op->emitError("Invalid register operation !");
+      return;
+    }
 
-    // Generate the reset condition (for sync & async resets)
-    // We assume for now that the reset value is always 0
-    size_t width = hw::getBitWidth(reg.getType());
     genSort("bitvec", width);
 
-    // Extract the `next` operation for each register (used to define the
-    // transition). We need to check if next is a port to avoid nullptrs
-    Value next = reg.getNext();
-
     // Next should already be associated to an LID at this point
     // As we are going to override it, we need to keep track of the original
     // instruction
     size_t nextLID = noLID;
 
-    // Check for special case where next is actually a port
+    // We need to check if the next value is a port to avoid nullptrs
     // To do so, we start by checking if our operation is a block argument
     if (BlockArgument barg = dyn_cast<BlockArgument>(next)) {
       // Extract the block argument index and use that to get the line number
@@ -503,8 +515,8 @@ struct ConvertHWToBTOR2Pass
       size_t resetValLID = noLID;
 
       // Check for a reset value, if none exists assume it's zero
-      if (auto resval = reg.getResetValue())
-        resetValLID = getOpLID(resval.getDefiningOp());
+      if (resetVal)
+        resetValLID = getOpLID(resetVal.getDefiningOp());
       else
         resetValLID = genZero(width);
 
@@ -514,7 +526,7 @@ struct ConvertHWToBTOR2Pass
     }
 
     // Finally generate the next statement
-    genNext(next, reg, width);
+    genNext(next, op, width);
   }
 
 public:
@@ -690,10 +702,8 @@ struct ConvertHWToBTOR2Pass
 
   void visitComb(Operation *op) { visitInvalidComb(op); }
 
-  void visitInvalidComb(Operation *op) {
-    // try sv ops
-    dispatchSVVisitor(op);
-  }
+  // Try sv ops when comb is done
+  void visitInvalidComb(Operation *op) { dispatchSVVisitor(op); }
 
   // Assertions are negated then converted to a btor2 bad instruction
   void visitSV(sv::AssertOp op) {
@@ -762,6 +772,21 @@ struct ConvertHWToBTOR2Pass
     regOps.push_back(reg);
   }
 
+  // Compregs behave in a similar way as firregs for btor2 emission
+  void visit(seq::CompRegOp reg) {
+    // Start by retrieving the register's name and width
+    StringRef regName = reg.getName().value();
+    int64_t w = requireSort(reg.getType());
+
+    // Generate state instruction (represents the register declaration)
+    genState(reg, w, regName);
+
+    // Record the operation for future `next` instruction generation
+    // This is required to model transitions between states (i.e. how a
+    // register's value evolves over time)
+    regOps.push_back(reg);
+  }
+
   // Ignore all other explicitly mentionned operations
   // ** Purposefully left empty **
   void ignore(Operation *op) {}
@@ -809,10 +834,12 @@ void ConvertHWToBTOR2Pass::runOnOperation() {
 
     // Previsit all registers in the module in order to avoid dependency cylcles
     module.walk([&](Operation *op) {
-      if (auto reg = dyn_cast<seq::FirRegOp>(op)) {
-        visit(reg);
-        handledOps.insert(op);
-      }
+      TypeSwitch<Operation *, void>(op)
+          .Case<seq::FirRegOp, seq::CompRegOp>([&](auto reg) {
+            visit(reg);
+            handledOps.insert(op);
+          })
+          .Default([&](auto expr) {});
     });
 
     // Visit all of the operations in our module

test/Conversion/HWToBTOR2/alias.mlir

@@ -0,0 +1,48 @@
+// RUN: circt-opt %s --convert-hw-to-btor2 -o tmp.mlir | FileCheck %s  
+
+module {
+  //CHECK:  [[NID0:[0-9]+]] sort bitvec 1
+  //CHECK:  [[NID1:[0-9]+]] input [[NID0]] reset
+  //CHECK:  [[NID2:[0-9]+]] input [[NID0]] in
+  hw.module @Alias(in %clock : !seq.clock, in %reset : i1, in %in : i1, out out : i32) {
+  //CHECK:  [[NID3:[0-9]+]] sort bitvec 32
+  //CHECK:  [[NID4:[0-9]+]] state [[NID3]] count
+
+    //CHECK:  [[NID5:[0-9]+]] constd [[NID0]] 0
+    %false = hw.constant false
+    //CHECK:  [[NID6:[0-9]+]] constd [[NID3]] 0
+    %c0_i32 = hw.constant 0 : i32
+    //CHECK:  [[NID7:[0-9]+]] constd [[NID0]] -1
+    %true = hw.constant true
+    //CHECK:  [[NID8:[0-9]+]] sort bitvec 2
+    //CHECK:  [[NID9:[0-9]+]] constd [[NID8]] -2
+    %c-2_i2 = hw.constant -2 : i2
+    %count = seq.compreg %6, %clock reset %reset, %c0_i32 : i32
+    %b = hw.wire %2  : i32
+    %d = hw.wire %b  : i32
+    %c = hw.wire %5  : i32
+    //CHECK:  [[NID10:[0-9]+]] sort bitvec 33
+    //CHECK:  [[NID11:[0-9]+]] concat [[NID10]] [[NID5]] [[NID4]]
+    %0 = comb.concat %false, %count : i1, i32
+    //CHECK:  [[NID12:[0-9]+]] constd [[NID10]] 1
+    %c1_i33 = hw.constant 1 : i33
+    //CHECK:  [[NID13:[0-9]+]] sub [[NID10]] [[NID11]] [[NID12]]
+    %1 = comb.sub bin %0, %c1_i33 : i33
+    //CHECK:  [[NID14:[0-9]+]] slice [[NID3]] [[NID13]] 31 0
+    %2 = comb.extract %1 from 0 : (i33) -> i32
+    //CHECK:  [[NID15:[0-9]+]] concat [[NID10]] [[NID5]] [[NID14]]
+    %3 = comb.concat %false, %d : i1, i32
+    //CHECK:  [[NID16:[0-9]+]] constd [[NID10]] 2
+    %c2_i33 = hw.constant 2 : i33
+    //CHECK:  [[NID17:[0-9]+]] add [[NID10]] [[NID15]] [[NID16]]
+    %4 = comb.add bin %3, %c2_i33 : i33
+    //CHECK:  [[NID18:[0-9]+]] slice [[NID3]] [[NID17]] 31 0
+    %5 = comb.extract %4 from 0 : (i33) -> i32
+    //CHECK:  [[NID19:[0-9]+]] ite [[NID3]] [[NID2]] [[NID14]] [[NID18]]
+    //CHECK:  [[NID20:[0-9]+]] ite [[NID3]] [[NID1]] [[NID6]] [[NID19]]
+    %6 = comb.mux bin %in, %b, %c : i32
+    //CHECK:  [[NID21:[0-9]+]] next [[NID3]] [[NID4]] [[NID20]]
+    hw.output %count : i32
+  }
+
+}

test/Conversion/HWToBTOR2/compreg.mlir

@@ -0,0 +1,85 @@
+// RUN: circt-opt %s --convert-hw-to-btor2 -o tmp.mlir | FileCheck %s  
+
+module {
+    //CHECK:    [[NID0:[0-9]+]] sort bitvec 1
+    //CHECK:    [[NID1:[0-9]+]] input [[NID0]] reset
+    //CHECK:    [[NID2:[0-9]+]] input [[NID0]] en
+    hw.module @Counter(in %clock : !seq.clock, in %reset : i1, in %en : i1) {
+    %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:    [[NID3:[0-9]+]] sort bitvec 28
+    //CHECK:    [[NID4:[0-9]+]] constd [[NID3]] 0 
+    %c0_i28 = hw.constant 0 : i28
+
+    //CHECK:    [[NID5:[0-9]+]] constd [[NID0]] 0
+    %false = hw.constant false
+
+    //CHECK:    [[NID7:[0-9]+]] constd [[NID6]] 22
+    %c22_i32 = hw.constant 22 : i32
+
+    //CHECK:    [[NID8:[0-9]+]] constd [[NID0]] -1
+    %true = hw.constant true
+
+    //CHECK:    [[NID9:[0-9]+]] sort bitvec 4
+    //CHECK:    [[NID10:[0-9]+]] constd [[NID9]] -6
+    %c-6_i4 = hw.constant -6 : i4
+
+    //CHECK:    [[NID11:[0-9]+]] constd [[NID6]] 0
+    %c0_i32 = hw.constant 0 : i32
+
+    %count = seq.compreg %9, %clock reset %reset, %c0_i32 : i32
+
+    //CHECK:    [[NID13:[0-9]+]] eq [[NID0]] [[NID12]] [[NID7]]
+    %1 = comb.icmp bin eq %count, %c22_i32 : i32
+
+    //CHECK:    [[NID14:[0-9]+]] and [[NID0]] [[NID13]] [[NID2]]
+    %2 = comb.and bin %1, %en : i1
+
+    //CHECK:    [[NID15:[0-9]+]] ite [[NID6]] [[NID14]] [[NID11]] [[NID12]]
+    %3 = comb.mux bin %2, %c0_i32, %count : i32
+
+    //CHECK:    [[NID16:[0-9]+]] neq [[NID0]] [[NID12]] [[NID7]]
+    %4 = comb.icmp bin ne %count, %c22_i32 : i32
+
+    //CHECK:    [[NID17:[0-9]+]] and [[NID0]] [[NID16]] [[NID2]]
+    %5 = comb.and bin %4, %en : i1
+
+    //CHECK:    [[NID18:[0-9]+]] sort bitvec 33
+    //CHECK:    [[NID19:[0-9]+]] concat [[NID18]] [[NID5]] [[NID12]]
+    %6 = comb.concat %false, %count : i1, i32
+
+    //CHECK:    [[NID20:[0-9]+]] constd [[NID18]] 1
+    %c1_i33 = hw.constant 1 : i33
+
+    //CHECK:    [[NID21:[0-9]+]] add [[NID18]] [[NID19]] [[NID20]]
+    %7 = comb.add bin %6, %c1_i33 : i33
+
+    //CHECK:    [[NID22:[0-9]+]] slice [[NID6]] [[NID21]] 31 0
+    %8 = comb.extract %7 from 0 : (i33) -> i32
+
+    //CHECK:    [[NID23:[0-9]+]] ite [[NID6]] [[NID17]] [[NID22]] [[NID15]]
+    %9 = comb.mux bin %5, %8, %3 : i32
+
+    //CHECK:    [[NID24:[0-9]+]] constd [[NID6]] 10
+    %c10_i32 = hw.constant 10 : i32
+
+    //CHECK:    [[NID25:[0-9]+]] neq [[NID0]] [[NID12]] [[NID24]]
+    %10 = comb.icmp bin ne %count, %c10_i32 : i32
+    sv.always posedge %0 {
+      sv.if %en {
+
+        //CHECK:    [[NID26:[0-9]+]] implies [[NID0]] [[NID2]] [[NID25]]
+        //CHECK:    [[NID27:[0-9]+]] not [[NID0]] [[NID26]]
+        //CHECK:    [[NID28:[0-9]+]] bad [[NID27]]
+        sv.assert %10, immediate message "Counter reached 10!"
+      }
+    }
+    hw.output
+
+    //CHECK:    [[NID30:[0-9]+]] ite [[NID6]] [[NID1]] [[NID11]] [[NID23]]
+    //CHECK:    [[NID31:[0-9]+]] next [[NID6]] [[NID12]] [[NID30]]
+  }
+}