[ExportVerilog] Fix crash when spilling LTL expr to wire (#5625)

Do not try to resolve use-before-def on LTL expressions by spilling them
to a wire. LTL expressions are always emitted inline, so just leave them
be in the IR and have ExportVerilog emit them as they are.

Fixes #5613.

lib/Conversion/ExportVerilog/PrepareForEmission.cpp

@@ -827,6 +827,10 @@ static LogicalResult legalizeHWModule(Block &block,
       return failure();
     }
 
+    // Do not reorder LTL expressions, which are always emitted inline.
+    if (isa<ltl::LTLDialect>(op.getDialect()))
+      continue;
+
     // Name legalization should have happened in a different pass for these sv
     // elements and we don't want to change their name through re-legalization
     // (e.g. letting a temporary take the name of an unvisited wire). Adding
@@ -1083,6 +1087,10 @@ static LogicalResult legalizeHWModule(Block &block,
   SmallPtrSet<Operation *, 32> seenOperations;
 
   for (auto &op : llvm::make_early_inc_range(block)) {
+    // Do not reorder LTL expressions, which are always emitted inline.
+    if (isa<ltl::LTLDialect>(op.getDialect()))
+      continue;
+
     // Check the users of any expressions to see if they are
     // lexically below the operation itself.  If so, it is being used out
     // of order.

test/Conversion/ExportVerilog/prepare-for-emission.mlir

@@ -228,3 +228,18 @@ module attributes { circt.loweringOptions = "disallowPackedStructAssignments"} {
       hw.output %0, %0 : !T, !T
   }
 }
+
+// -----
+// LTL expressions that are used before being defined should not be spilled to
+// wires, where they crash the PrepareForEmission pass. They are always emitted
+// inline, so no need to restructure the IR.
+// CHECK-LABEL: hw.module @Issue5613
+hw.module @Issue5613(%a: i1, %b: i1) {
+  verif.assert %2 : !ltl.sequence
+  %0 = ltl.implication %2, %1 : !ltl.sequence, !ltl.property
+  %1 = ltl.or %b, %3 : i1, !ltl.property
+  %2 = ltl.and %b, %4 : i1, !ltl.sequence
+  %3 = ltl.not %b : i1
+  %4 = ltl.delay %a, 42 : i1
+  hw.output
+}