From 181355aea05bc941822fad98ed49f3329ce713ee Mon Sep 17 00:00:00 2001
From: Bea Healy <beahealy22@gmail.com>
Date: Tue, 19 Nov 2024 17:04:17 +0000
Subject: [PATCH] [HWToBTOR2] Fix crashes on initial value corner cases

---
 lib/Conversion/HWToBTOR2/HWToBTOR2.cpp | 10 ++++++++--
 test/Conversion/HWToBTOR2/errors.mlir  | 25 +++++++++++++++++++++++++
 2 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 test/Conversion/HWToBTOR2/errors.mlir

diff --git a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
index dd0fce8fc143..8f887a14582f 100644
--- a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
+++ b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
@@ -594,8 +594,8 @@ struct ConvertHWToBTOR2Pass
   void visit(hw::PortInfo &port) {
     // Separate the inputs from outputs and generate the first btor2 lines for
     // input declaration We only consider ports with an explicit bit-width (so
-    // ignore clocks)
-    if (port.isInput() && !isa<seq::ClockType>(port.type)) {
+    // ignore clocks and immutables)
+    if (port.isInput() && !isa<seq::ClockType, seq::ImmutableType>(port.type)) {
       // Generate the associated btor declaration for the inputs
       StringRef iName = port.getName();
 
@@ -880,6 +880,12 @@ struct ConvertHWToBTOR2Pass
     genState(reg, w, regName);
 
     if (init) {
+      if (init && (isa<BlockArgument>(init) ||
+                   !isa<seq::InitialOp>(init.getDefiningOp()))) {
+        reg->emitError(
+            "Initial value must be emitted directly by a seq.initial op");
+        return;
+      }
       // Check that the initial value is a non-null constant
       auto initialConstant = circt::seq::unwrapImmutableValue(init)
                                  .getDefiningOp<hw::ConstantOp>();
diff --git a/test/Conversion/HWToBTOR2/errors.mlir b/test/Conversion/HWToBTOR2/errors.mlir
new file mode 100644
index 000000000000..6106e54d3c95
--- /dev/null
+++ b/test/Conversion/HWToBTOR2/errors.mlir
@@ -0,0 +1,25 @@
+// RUN: circt-opt %s --convert-hw-to-btor2 --verify-diagnostics --split-input-file -o tmp.mlir
+
+hw.module @init_emitter(out out: !seq.immutable<i32>) {
+  %init = seq.initial () {
+    %c0_i32 = hw.constant 0 : i32
+    seq.yield %c0_i32 : i32
+  } : () -> !seq.immutable<i32>
+  hw.output %init : !seq.immutable<i32>
+}
+
+hw.module @reg_with_instance_initial(in %clk: !seq.clock, in %in: i32, out out: i32) {
+  // expected-error @below {{'hw.instance' op not supported in BTOR2 conversion}}
+  %init = hw.instance "foo" @init_emitter () -> (out: !seq.immutable<i32>)
+  // expected-error @below {{Initial value must be emitted directly by a seq.initial op}}
+  %1 = seq.compreg %in, %clk initial %init : i32
+  hw.output %1 : i32
+}
+
+// -----
+
+hw.module @reg_with_argument_initial(in %clk: !seq.clock, in %in: i32, in %init: !seq.immutable<i32>, out out: i32) {
+  // expected-error @below {{Initial value must be emitted directly by a seq.initial op}}
+  %1 = seq.compreg %in, %clk initial %init : i32
+  hw.output %1 : i32
+}