diff --git a/lib/Conversion/ExportVerilog/PrepareForEmission.cpp b/lib/Conversion/ExportVerilog/PrepareForEmission.cpp index 40567b7740..24f560c1b3 100644 --- a/lib/Conversion/ExportVerilog/PrepareForEmission.cpp +++ b/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(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 seenOperations; for (auto &op : llvm::make_early_inc_range(block)) { + // Do not reorder LTL expressions, which are always emitted inline. + if (isa(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. diff --git a/test/Conversion/ExportVerilog/prepare-for-emission.mlir b/test/Conversion/ExportVerilog/prepare-for-emission.mlir index 65cce39376..9b91e29d15 100644 --- a/test/Conversion/ExportVerilog/prepare-for-emission.mlir +++ b/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 +}