diff --git a/docs/Dialects/LTL.md b/docs/Dialects/LTL.md
index cf5124ea4cc5..4940a735bba8 100644
--- a/docs/Dialects/LTL.md
+++ b/docs/Dialects/LTL.md
@@ -160,6 +160,32 @@ Sequence and property expressions in SVAs can specify a clock with respect to wh
 - `@(negedge clk) seqOrProp`. **Trigger on high-to-low clock edge.** Equivalent to `ltl.clock %seqOrProp, negedge %clk`.
 - `@(edge clk) seqOrProp`. **Trigger on any clock edge.** Equivalent to `ltl.clock %seqOrProp, edge %clk`.
 
+#### Delay clocking
+
+`ltl.delay` takes the delayed input first, followed by the delay window:
+
+```
+ltl.delay %input, <delay>[, <length>]
+```
+
+For explicitly clocked delays, use `ltl.clocked_delay`:
+
+```
+ltl.clocked_delay %clock, <edge>, %input, <delay>[, <length>]
+```
+
+`%clock` is an `i1` value (e.g. a module clock); `<edge>` is `posedge`, `negedge`, or `edge`. For example, `ltl.clocked_delay %clk, posedge, %s, 3` means `%s` must hold 3 cycles later on `%clk` rising edges.
+
+`ltl.delay` is unclocked and may be resolved by an enclosing `ltl.clock` or by the `InferLTLClocks` pass. `ltl.clock` globally associates a sequence/property with a clock/edge; `ltl.clocked_delay` carries an explicit per-delay clock.
+
+Examples:
+
+```mlir
+ltl.delay %s, 3
+ltl.delay %s, 3, 0
+ltl.clocked_delay %clk, posedge, %s, 3, 0
+```
+
 
 ### Disable Iff
 
@@ -273,13 +299,13 @@ where the `logic_to_int` conversion is only necessary if `%cond` is 4-valued.
 ```mlir
 %ds1 = ltl.delay %s1, 1
 %s1s2 = ltl.concat %ds1, %s2 : !ltl.sequence  
-```  
+```
 
 - **`s1 ##[*] s2`**:   
 ```mlir
 %ds1 = ltl.delay %s1, 0
 %s1s2 = ltl.concat %ds1, %s2 : !ltl.sequence  
-```  
+```
 
 - **`s1 and s2`**:   
 ```mlir
@@ -369,12 +395,12 @@ ltl.not %s1 : !ltl.sequence
 - **`nexttime p`**:   
 ```mlir
 ltl.delay %p, 1, 0 : !ltl.sequence   
-```  
+```
 
 - **`nexttime[n] p`**:  
 ```mlir
 ltl.delay %p, n, 0 : !ltl.sequence   
-```  
+```
 
 - **`s_nexttime p`**: not really distinguishable from the weak version in CIRCT.
 - **`s_nexttime[n] p`**: not really distinguishable from the weak version in CIRCT.
diff --git a/include/circt/Dialect/LTL/LTLFolds.td b/include/circt/Dialect/LTL/LTLFolds.td
index 6db7668f1923..8732f38d6a45 100644
--- a/include/circt/Dialect/LTL/LTLFolds.td
+++ b/include/circt/Dialect/LTL/LTLFolds.td
@@ -21,6 +21,10 @@ def valueTail : NativeCodeCall<"$0.drop_front()">;
 def concatValues : NativeCodeCall<
   "concatValues(ValueRange{$0}, ValueRange{$1})">;
 
+// Ensure that outer and inner clocked delays use the same clock and edge
+// before merging. Accepts (outerClock, innerClock, outerEdge, innerEdge).
+def SameClockAndEdge : Constraint<CPred<"$0 == $1 && $2 == $3">>;
+
 //===----------------------------------------------------------------------===//
 // DelayOp
 //===----------------------------------------------------------------------===//
@@ -40,12 +44,30 @@ def NestedDelays : Pat<
   (DelayOp $input, (mergedDelays $delay1, $delay2),
                    (mergedLengths $length1, $length2))>;
 
+// clocked_delay(clk, edge, clocked_delay(clk, edge, s, I, N), J, M)
+//   -> clocked_delay(clk, edge, s, I+J, N+M)
+def NestedClockedDelays : Pat<
+  (ClockedDelayOp $clock0, $edge0,
+                  (ClockedDelayOp $clock1, $edge1, $input, $delay1, $length1),
+                  $delay2, $length2),
+  (ClockedDelayOp $clock0, $edge0, $input, (mergedDelays $delay1, $delay2),
+                  (mergedLengths $length1, $length2)),
+  [(SameClockAndEdge $clock0, $clock1, $edge0, $edge1)]>;
+
 // delay(concat(s, ...), N, M) -> concat(delay(s, N, M), ...)
 def MoveDelayIntoConcat : Pat<
   (DelayOp (ConcatOp $inputs), $delay, $length),
   (ConcatOp (concatValues (DelayOp (valueHead $inputs), $delay, $length),
                           (valueTail $inputs)))>;
 
+// clocked_delay(clk, edge, concat(s, ...), N, M)
+//   -> concat(clocked_delay(clk, edge, s, N, M), ...)
+def MoveClockedDelayIntoConcat : Pat<
+  (ClockedDelayOp $clock, $edge, (ConcatOp $inputs), $delay, $length),
+  (ConcatOp (concatValues (ClockedDelayOp $clock, $edge, (valueHead $inputs),
+                                         $delay, $length),
+                          (valueTail $inputs)))>;
+
 //===----------------------------------------------------------------------===//
 // ConcatOp
 //===----------------------------------------------------------------------===//
diff --git a/include/circt/Dialect/LTL/LTLOps.td b/include/circt/Dialect/LTL/LTLOps.td
index 4e46c5d3db25..a8aece520b65 100644
--- a/include/circt/Dialect/LTL/LTLOps.td
+++ b/include/circt/Dialect/LTL/LTLOps.td
@@ -62,6 +62,47 @@ def IntersectOp : AssocLTLOp<"intersect"> {
   let hasCanonicalizeMethod = 1;
 }
 
+//===----------------------------------------------------------------------===//
+// Clocking
+//===----------------------------------------------------------------------===//
+
+// Edge behavior enum for always block.  See SV Spec 9.4.2.
+
+/// AtPosEdge triggers on a rise from 0 to 1/X/Z, or X/Z to 1.
+def AtPosEdge: I32EnumAttrCase<"Pos", 0, "posedge">;
+/// AtNegEdge triggers on a drop from 1 to 0/X/Z, or X/Z to 0.
+def AtNegEdge: I32EnumAttrCase<"Neg", 1, "negedge">;
+/// AtEdge is syntactic sugar for AtPosEdge or AtNegEdge.
+def AtEdge   : I32EnumAttrCase<"Both", 2, "edge">;
+
+def ClockEdgeAttr : I32EnumAttr<"ClockEdge", "clock edge",
+                                [AtPosEdge, AtNegEdge, AtEdge]> {
+  let cppNamespace = "circt::ltl";
+}
+
+def ClockOp : LTLOp<"clock", [
+  Pure, InferTypeOpInterface, DeclareOpInterfaceMethods<InferTypeOpInterface>
+]> {
+  let arguments = (ins LTLAnyPropertyType:$input, ClockEdgeAttr:$edge, I1:$clock);
+  let results = (outs LTLSequenceOrPropertyType:$result);
+  let assemblyFormat = [{
+    $input `,` $edge $clock attr-dict `:` type($input)
+  }];
+
+  let summary = "Specify the clock for a property or sequence.";
+  let description = [{
+    Specifies the `$edge` on a given `$clock` to be the clock for an `$input`
+    property or sequence. All cycle delays in the `$input` implicitly refer to a
+    clock that advances the state to the next cycle. The `ltl.clock` operation
+    provides that clock. The clock applies to the entire property or sequence
+    expression tree below `$input`, up to any other nested `ltl.clock`
+    operations.
+
+    The operation returns a property if the `$input` is a property, and a
+    sequence otherwise.
+  }];
+}
+
 //===----------------------------------------------------------------------===//
 // Sequences
 //===----------------------------------------------------------------------===//
@@ -83,25 +124,53 @@ def DelayOp : LTLOp<"delay", [Pure]> {
     Delays the `$input` sequence by the number of cycles specified by `$delay`.
     The delay must be greater than or equal to zero. The optional `$length`
     specifies during how many cycles after the initial delay the sequence can
-    match. Omitting `$length` indicates an unbounded but finite delay. For
-    example:
-
-    - `ltl.delay %seq, 2, 0` delays `%seq` by exactly 2 cycles. The resulting
-      sequence matches if `%seq` matches exactly 2 cycles in the future.
-    - `ltl.delay %seq, 2, 2` delays `%seq` by 2, 3, or 4 cycles. The resulting
-      sequence matches if `%seq` matches 2, 3, or 4 cycles in the future.
-    - `ltl.delay %seq, 2` delays `%seq` by 2 or more cycles. The number of
-      cycles is unbounded but finite, which means that `%seq` *has* to match at
-      some point, instead of effectively never occuring by being delayed an
-      infinite number of cycles.
+    match. Omitting `$length` indicates an unbounded but finite delay.
+
+    This operation is intentionally unclocked. Use `ltl.clocked_delay` for
+    explicitly clocked delays.
+
+    For example:
+
+    - `ltl.delay %seq, 2, 0` delays `%seq` by exactly 2 cycles (unclocked).
+    - `ltl.delay %seq, 2, 2` delays `%seq` by 2, 3, or 4 cycles.
+    - `ltl.delay %seq, 2` delays `%seq` by 2 or more cycles (unbounded but
+      finite).
     - `ltl.delay %seq, 0, 0` is equivalent to just `%seq`.
 
-    #### Clocking
+    Unclocked delays may be resolved by an enclosing `ltl.clock` operation or
+    by the `InferLTLClocks` pass (`--ltl-infer-clocks`).
+  }];
+}
 
-    The cycle delay specified on the operation refers to a clocking event. This
-    event is not directly specified by the delay operation itself. Instead, the
-    [`ltl.clock`](#ltlclock-circtltlclockop) operation can be used to associate
-    all delays within a sequence with a clock.
+def ClockedDelayOp : LTLOp<"clocked_delay", [Pure]> {
+  let arguments = (ins
+    I1:$clock,
+    ClockEdgeAttr:$edge,
+    LTLAnySequenceType:$input,
+    I64Attr:$delay,
+    OptionalAttr<I64Attr>:$length);
+  let results = (outs LTLSequenceType:$result);
+  let assemblyFormat = [{
+    $clock `,` $edge `,` $input `,` $delay (`,` $length^)? attr-dict `:` type($input)
+  }];
+  let hasFolder = 1;
+  let hasCanonicalizer = 1;
+
+  let summary = "Delay a sequence by a number of cycles on an explicit clock.";
+  let description = [{
+    Delays the `$input` sequence by the number of cycles specified by `$delay`
+    on the specified `$clock` and `$edge`.
+
+    The optional `$length` specifies during how many cycles after the initial
+    delay the sequence can match. Omitting `$length` indicates an unbounded but
+    finite delay.
+
+    For example:
+
+    - `ltl.clocked_delay %clk, posedge, %seq, 2, 0` delays `%seq` by
+      exactly 2 cycles on the positive edge of `%clk`.
+    - `ltl.clocked_delay %clk, negedge, %seq, 2, 2` delays `%seq` by 2,
+      3, or 4 cycles on the negative edge of `%clk`.
   }];
 }
 
@@ -368,45 +437,4 @@ def EventuallyOp : LTLOp<"eventually", [Pure]> {
   }];
 }
 
-//===----------------------------------------------------------------------===//
-// Clocking
-//===----------------------------------------------------------------------===//
-
-// Edge behavior enum for always block.  See SV Spec 9.4.2.
-
-/// AtPosEdge triggers on a rise from 0 to 1/X/Z, or X/Z to 1.
-def AtPosEdge: I32EnumAttrCase<"Pos", 0, "posedge">;
-/// AtNegEdge triggers on a drop from 1 to 0/X/Z, or X/Z to 0.
-def AtNegEdge: I32EnumAttrCase<"Neg", 1, "negedge">;
-/// AtEdge is syntactic sugar for AtPosEdge or AtNegEdge.
-def AtEdge   : I32EnumAttrCase<"Both", 2, "edge">;
-
-def ClockEdgeAttr : I32EnumAttr<"ClockEdge", "clock edge",
-                                [AtPosEdge, AtNegEdge, AtEdge]> {
-  let cppNamespace = "circt::ltl";
-}
-
-def ClockOp : LTLOp<"clock", [
-  Pure, InferTypeOpInterface, DeclareOpInterfaceMethods<InferTypeOpInterface>
-]> {
-  let arguments = (ins LTLAnyPropertyType:$input, ClockEdgeAttr:$edge, I1:$clock);
-  let results = (outs LTLSequenceOrPropertyType:$result);
-  let assemblyFormat = [{
-    $input `,` $edge $clock attr-dict `:` type($input)
-  }];
-
-  let summary = "Specify the clock for a property or sequence.";
-  let description = [{
-    Specifies the `$edge` on a given `$clock` to be the clock for an `$input`
-    property or sequence. All cycle delays in the `$input` implicitly refer to a
-    clock that advances the state to the next cycle. The `ltl.clock` operation
-    provides that clock. The clock applies to the entire property or sequence
-    expression tree below `$input`, up to any other nested `ltl.clock`
-    operations.
-
-    The operation returns a property if the `$input` is a property, and a
-    sequence otherwise.
-  }];
-}
-
 #endif // CIRCT_DIALECT_LTL_LTLOPS_TD
diff --git a/include/circt/Dialect/LTL/LTLVisitors.h b/include/circt/Dialect/LTL/LTLVisitors.h
index 8713f0446a77..b2486ad6c603 100644
--- a/include/circt/Dialect/LTL/LTLVisitors.h
+++ b/include/circt/Dialect/LTL/LTLVisitors.h
@@ -21,8 +21,8 @@ class Visitor {
   ResultType dispatchLTLVisitor(Operation *op, ExtraArgs... args) {
     auto *thisCast = static_cast<ConcreteType *>(this);
     return TypeSwitch<Operation *, ResultType>(op)
-        .template Case<AndOp, OrOp, DelayOp, ConcatOp, RepeatOp, NotOp,
-                       ImplicationOp, UntilOp, EventuallyOp, ClockOp,
+        .template Case<AndOp, OrOp, DelayOp, ClockedDelayOp, ConcatOp, RepeatOp,
+                       NotOp, ImplicationOp, UntilOp, EventuallyOp, ClockOp,
                        IntersectOp, NonConsecutiveRepeatOp, GoToRepeatOp,
                        BooleanConstantOp>([&](auto op) -> ResultType {
           return thisCast->visitLTL(op, args...);
@@ -52,6 +52,7 @@ class Visitor {
   HANDLE(AndOp, Unhandled);
   HANDLE(OrOp, Unhandled);
   HANDLE(DelayOp, Unhandled);
+  HANDLE(ClockedDelayOp, Unhandled);
   HANDLE(ConcatOp, Unhandled);
   HANDLE(RepeatOp, Unhandled);
   HANDLE(NotOp, Unhandled);
diff --git a/lib/Dialect/LTL/LTLFolds.cpp b/lib/Dialect/LTL/LTLFolds.cpp
index 33611f75c136..f9eb793d490f 100644
--- a/lib/Dialect/LTL/LTLFolds.cpp
+++ b/lib/Dialect/LTL/LTLFolds.cpp
@@ -79,21 +79,40 @@ LogicalResult IntersectOp::canonicalize(IntersectOp op,
 // DelayOp
 //===----------------------------------------------------------------------===//
 
-OpFoldResult DelayOp::fold(FoldAdaptor adaptor) {
+template <typename DelayLikeOp, typename FoldAdaptorT>
+static OpFoldResult foldDelayLike(DelayLikeOp op, FoldAdaptorT adaptor) {
   // delay(s, 0, 0) -> s
   if (adaptor.getDelay() == 0 && adaptor.getLength() == 0 &&
-      isa<SequenceType>(getInput().getType()))
-    return getInput();
+      isa<SequenceType>(op.getInput().getType()))
+    return op.getInput();
 
   return {};
 }
 
+OpFoldResult DelayOp::fold(FoldAdaptor adaptor) {
+  return foldDelayLike(*this, adaptor);
+}
+
 void DelayOp::getCanonicalizationPatterns(RewritePatternSet &results,
                                           MLIRContext *context) {
   results.add<patterns::NestedDelays>(results.getContext());
   results.add<patterns::MoveDelayIntoConcat>(results.getContext());
 }
 
+//===----------------------------------------------------------------------===//
+// ClockedDelayOp
+//===----------------------------------------------------------------------===//
+
+OpFoldResult ClockedDelayOp::fold(FoldAdaptor adaptor) {
+  return foldDelayLike(*this, adaptor);
+}
+
+void ClockedDelayOp::getCanonicalizationPatterns(RewritePatternSet &results,
+                                                 MLIRContext *context) {
+  results.add<patterns::NestedClockedDelays>(results.getContext());
+  results.add<patterns::MoveClockedDelayIntoConcat>(results.getContext());
+}
+
 //===----------------------------------------------------------------------===//
 // ConcatOp
 //===----------------------------------------------------------------------===//
diff --git a/test/Dialect/LTL/basic.mlir b/test/Dialect/LTL/basic.mlir
index 2c4004cc1459..7a7af2983aa9 100644
--- a/test/Dialect/LTL/basic.mlir
+++ b/test/Dialect/LTL/basic.mlir
@@ -2,6 +2,7 @@
 
 %true = hw.constant true
 %c0_i8 = hw.constant 0 : i8
+%clk = hw.constant true
 
 //===----------------------------------------------------------------------===//
 // Types
@@ -53,8 +54,12 @@ unrealized_conversion_cast %p3 : !ltl.property to index
 
 // CHECK: ltl.delay {{%.+}}, 0 : !ltl.sequence
 // CHECK: ltl.delay {{%.+}}, 42, 1337 : !ltl.sequence
+// CHECK: ltl.clocked_delay {{%.+}}, posedge, {{%.+}}, 0 : !ltl.sequence
+// CHECK: ltl.clocked_delay {{%.+}}, posedge, {{%.+}}, 42, 1337 : !ltl.sequence
 ltl.delay %s, 0 : !ltl.sequence
 ltl.delay %s, 42, 1337 : !ltl.sequence
+ltl.clocked_delay %clk, posedge, %s, 0 : !ltl.sequence
+ltl.clocked_delay %clk, posedge, %s, 42, 1337 : !ltl.sequence
 
 // CHECK: ltl.concat {{%.+}} : !ltl.sequence
 // CHECK: ltl.concat {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.sequence
diff --git a/test/Dialect/LTL/canonicalization.mlir b/test/Dialect/LTL/canonicalization.mlir
index 424b0ecb74eb..4c9ca76015ca 100644
--- a/test/Dialect/LTL/canonicalization.mlir
+++ b/test/Dialect/LTL/canonicalization.mlir
@@ -25,8 +25,8 @@ func.func @DelayFolds(%arg0: !ltl.sequence, %arg1: i1) {
 
   // delay(delay(s, 1, N), 2) -> delay(s, 3)
   // N is dropped
-  // CHECK-NEXT: ltl.delay %arg0, 3 :
-  // CHECK-NEXT: ltl.delay %arg0, 3 :
+  // CHECK-NEXT: ltl.delay {{%.+}}, 3 :
+  // CHECK-NEXT: ltl.delay {{%.+}}, 3 :
   // CHECK-NEXT: call
   // CHECK-NEXT: call
   %3 = ltl.delay %arg0, 1, 0 : !ltl.sequence
@@ -64,6 +64,97 @@ func.func @DelayFolds(%arg0: !ltl.sequence, %arg1: i1) {
   return
 }
 
+// CHECK-LABEL: @ClockedDelayFolds
+// CHECK-SAME: (%[[S:.+]]: !ltl.sequence, %[[I:.+]]: i1, %[[CLK:.+]]: i1)
+func.func @ClockedDelayFolds(%arg0: !ltl.sequence, %arg1: i1, %clk: i1) {
+  // clocked_delay(clk, posedge, s, 0, 0) -> s
+  // clocked_delay(clk, posedge, i, 0, 0) -> clocked_delay(clk, posedge, i, 0, 0)
+  // CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[I]], 0, 0 : i1
+  // CHECK-NEXT: call @Seq(%[[S]])
+  // CHECK-NEXT: call @Seq({{%.+}})
+  %0 = ltl.clocked_delay %clk, posedge, %arg0, 0, 0 : !ltl.sequence
+  %n0 = ltl.clocked_delay %clk, posedge, %arg1, 0, 0 : i1
+  call @Seq(%0) : (!ltl.sequence) -> ()
+  call @Seq(%n0) : (!ltl.sequence) -> ()
+
+  // Nested clocked delays with same clock/edge: merge delays
+  // clocked_delay(clk, posedge, clocked_delay(clk, posedge, s, 1), 2)
+  //   -> clocked_delay(clk, posedge, s, 3)
+  // CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 3 :
+  // CHECK-NEXT: call
+  %1 = ltl.clocked_delay %clk, posedge, %arg0, 1 : !ltl.sequence
+  %2 = ltl.clocked_delay %clk, posedge, %1, 2 : !ltl.sequence
+  call @Seq(%2) : (!ltl.sequence) -> ()
+
+  // Inner has length, outer does not: length dropped
+  // clocked_delay(clk, posedge, clocked_delay(clk, posedge, s, 1, 42), 2)
+  //   -> clocked_delay(clk, posedge, s, 3)
+  // CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 3 :
+  // CHECK-NEXT: call
+  %3 = ltl.clocked_delay %clk, posedge, %arg0, 1, 42 : !ltl.sequence
+  %4 = ltl.clocked_delay %clk, posedge, %3, 2 : !ltl.sequence
+  call @Seq(%4) : (!ltl.sequence) -> ()
+
+  // Outer has length, inner does not: length dropped
+  // clocked_delay(clk, posedge, clocked_delay(clk, posedge, s, 1), 2, 5)
+  //   -> clocked_delay(clk, posedge, s, 3)
+  // CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 3 :
+  // CHECK-NEXT: call
+  %5 = ltl.clocked_delay %clk, posedge, %arg0, 1 : !ltl.sequence
+  %6 = ltl.clocked_delay %clk, posedge, %5, 2, 5 : !ltl.sequence
+  call @Seq(%6) : (!ltl.sequence) -> ()
+
+  // Both have length: lengths merged
+  // clocked_delay(clk, posedge, clocked_delay(clk, posedge, s, 1, 2), 3, 5)
+  //   -> clocked_delay(clk, posedge, s, 4, 7)
+  // CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 4, 7 :
+  // CHECK-NEXT: call
+  %7 = ltl.clocked_delay %clk, posedge, %arg0, 1, 2 : !ltl.sequence
+  %8 = ltl.clocked_delay %clk, posedge, %7, 3, 5 : !ltl.sequence
+  call @Seq(%8) : (!ltl.sequence) -> ()
+
+  // Both have length, outer length is 0: no drop
+  // clocked_delay(clk, posedge, clocked_delay(clk, posedge, s, 1, 2), 3, 0)
+  //   -> clocked_delay(clk, posedge, s, 4, 2)
+  // CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 4, 2 :
+  // CHECK-NEXT: call
+  %9 = ltl.clocked_delay %clk, posedge, %arg0, 1, 2 : !ltl.sequence
+  %10 = ltl.clocked_delay %clk, posedge, %9, 3, 0 : !ltl.sequence
+  call @Seq(%10) : (!ltl.sequence) -> ()
+
+  // Different edge: should NOT merge
+  // CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 1 :
+  // CHECK-NEXT: ltl.clocked_delay %[[CLK]], negedge, {{%.+}}, 2 :
+  // CHECK-NEXT: call
+  %11 = ltl.clocked_delay %clk, posedge, %arg0, 1 : !ltl.sequence
+  %12 = ltl.clocked_delay %clk, negedge, %11, 2 : !ltl.sequence
+  call @Seq(%12) : (!ltl.sequence) -> ()
+
+  // Different clock: should NOT merge
+  // CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 1 :
+  // CHECK-NEXT: ltl.clocked_delay %[[I]], posedge, {{%.+}}, 2 :
+  // CHECK-NEXT: call
+  %13 = ltl.clocked_delay %clk, posedge, %arg0, 1 : !ltl.sequence
+  %14 = ltl.clocked_delay %arg1, posedge, %13, 2 : !ltl.sequence
+  call @Seq(%14) : (!ltl.sequence) -> ()
+
+  return
+}
+
+// CHECK-LABEL: @ClockedDelayIntoConcatFolds
+// CHECK-SAME: (%[[S0:.+]]: !ltl.sequence, %[[S1:.+]]: !ltl.sequence, %[[CLK:.+]]: i1)
+func.func @ClockedDelayIntoConcatFolds(%arg0: !ltl.sequence, %arg1: !ltl.sequence, %clk: i1) {
+  // clocked_delay(clk, posedge, concat(s0, s1), N, M)
+  //   -> concat(clocked_delay(clk, posedge, s0, N, M), s1)
+  // CHECK-NEXT: [[TMP:%.+]] = ltl.clocked_delay %[[CLK]], posedge, %[[S0]], 2, 3 :
+  // CHECK-NEXT: ltl.concat [[TMP]], %[[S1]] :
+  // CHECK-NEXT: call
+  %0 = ltl.concat %arg0, %arg1 : !ltl.sequence, !ltl.sequence
+  %1 = ltl.clocked_delay %clk, posedge, %0, 2, 3 : !ltl.sequence
+  call @Seq(%1) : (!ltl.sequence) -> ()
+  return
+}
+
 // CHECK-LABEL: @ConcatFolds
 func.func @ConcatFolds(%arg0: !ltl.sequence, %arg1: !ltl.sequence, %arg2: !ltl.sequence) {
   // concat(s) -> s