[HWToBTOR2] Fix crashes on initial value corner cases

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>();

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
+}