From 4cee287397bb39bc16537c7da9add4beecdbfc35 Mon Sep 17 00:00:00 2001
From: Bea Healy <57840981+TaoBi22@users.noreply.github.com>
Date: Thu, 18 Apr 2024 22:38:49 +0100
Subject: [PATCH] [HWToBTOR2] Deduce resets from (Fir)RegOps (#6918)

* Fetch reset value from (Fir)RegOp instead of hardcoded signal name

* Add block arg check on reset

* Add test for multiple resets &non-block-arg resets

* Fix test module name

* Add EOF newline to test
---
 lib/Conversion/HWToBTOR2/HWToBTOR2.cpp        | 25 +++++++++----
 test/Conversion/HWToBTOR2/compreg-resets.mlir | 36 +++++++++++++++++++
 2 files changed, 54 insertions(+), 7 deletions(-)
 create mode 100644 test/Conversion/HWToBTOR2/compreg-resets.mlir

diff --git a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
index 9b79bc118623..87951d0f9bdd 100644
--- a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
+++ b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
@@ -53,7 +53,6 @@ struct ConvertHWToBTOR2Pass
 
   // Create a counter that attributes a unique id to each generated btor2 line
   size_t lid = 1;          // btor2 line identifiers usually start at 1
-  size_t resetLID = noLID; // keeps track of the reset's LID
   size_t nclocks = 0;
 
   // Create maps to keep track of lid associations
@@ -488,16 +487,18 @@ struct ConvertHWToBTOR2Pass
   // transition system conversion
   void finalizeRegVisit(Operation *op) {
     int64_t width;
-    Value next, resetVal;
+    Value next, reset, 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();
+      reset = reg.getReset();
       resetVal = reg.getResetValue();
     } else if (auto reg = dyn_cast<seq::FirRegOp>(op)) {
       width = hw::getBitWidth(reg.getType());
       next = reg.getNext();
+      reset = reg.getReset();
       resetVal = reg.getResetValue();
     } else {
       op->emitError("Invalid register operation !");
@@ -525,9 +526,23 @@ struct ConvertHWToBTOR2Pass
     }
 
     // Check if the register has a reset
-    if (resetLID != noLID) {
+    if (reset) {
       size_t resetValLID = noLID;
 
+      // Check if the reset signal is a port to avoid nullptrs (as done above
+      // with next)
+      size_t resetLID = noLID;
+      if (BlockArgument barg = dyn_cast<BlockArgument>(reset)) {
+        // Extract the block argument index and use that to get the line number
+        size_t argIdx = barg.getArgNumber();
+
+        // Check that the extracted argument is in range before using it
+        resetLID = inputLIDs[argIdx];
+
+      } else {
+        resetLID = getOpLID(reset);
+      }
+
       // Check for a reset value, if none exists assume it's zero
       if (resetVal)
         resetValLID = getOpLID(resetVal.getDefiningOp());
@@ -581,10 +596,6 @@ struct ConvertHWToBTOR2Pass
       // of ports)
       inputLIDs[port.argNum] = lid;
 
-      // We assume that the explicit name is always %reset for reset ports
-      if (iName == "reset")
-        resetLID = lid;
-
       // Increment the lid to keep it unique
       lid++;
 
diff --git a/test/Conversion/HWToBTOR2/compreg-resets.mlir b/test/Conversion/HWToBTOR2/compreg-resets.mlir
new file mode 100644
index 000000000000..5f475cfcdd2b
--- /dev/null
+++ b/test/Conversion/HWToBTOR2/compreg-resets.mlir
@@ -0,0 +1,36 @@
+// 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]] reset0
+  //CHECK:    [[NID2:[0-9]+]] input [[NID0]] reset1
+  //CHECK:    [[NID3:[0-9]+]] sort bitvec 32
+  //CHECK:    [[NID4:[0-9]+]] input [[NID3]] in
+  hw.module @MultipleResets(in %clock : !seq.clock, in %reset0 : i1, in %reset1 : i1, in %in : i32) {
+    // Registers are all emitted before any other operation
+    //CHECK:    [[NID5:[0-9]+]] state [[NID3]] reg0
+    //CHECK:    [[NID6:[0-9]+]] state [[NID3]] reg1
+    //CHECK:    [[NID7:[0-9]+]] state [[NID3]] reg2
+
+    //CHECK:    [[NID8:[0-9]+]] constd [[NID3]] 0
+    %c0_i32 = hw.constant 0 : i32
+
+    %reg0 = seq.compreg %in, %clock reset %reset0, %c0_i32 : i32
+    %reg1 = seq.compreg %in, %clock reset %reset1, %c0_i32 : i32
+
+    //CHECK:    [[NID9:[0-9]+]] and [[NID0]] [[NID1]] [[NID2]]
+    %reset_and = comb.and bin %reset0, %reset1 : i1
+
+    %reg2 = seq.compreg %in, %clock reset %reset_and, %c0_i32 : i32
+
+    // Register reset ITEs and next statements are emitted last
+    //CHECK:    [[NID10:[0-9]+]] ite [[NID3]] [[NID1]] [[NID8]] [[NID4]]
+    //CHECK:    [[NID11:[0-9]+]] next [[NID3]] [[NID5]] [[NID10]]
+    //CHECK:    [[NID12:[0-9]+]] ite [[NID3]] [[NID2]] [[NID8]] [[NID4]]
+    //CHECK:    [[NID13:[0-9]+]] next [[NID3]] [[NID6]] [[NID12]]
+    //CHECK:    [[NID14:[0-9]+]] ite [[NID3]] [[NID9]] [[NID8]] [[NID4]]
+    //CHECK:    [[NID15:[0-9]+]] next [[NID3]] [[NID7]] [[NID14]]
+
+    hw.output
+  }
+}