diff --git a/docs/Dialects/LTL.md b/docs/Dialects/LTL.md
index 37b20099cf59..00c48550403a 100644
--- a/docs/Dialects/LTL.md
+++ b/docs/Dialects/LTL.md
@@ -48,11 +48,11 @@ a ##1 b ##1 c      // 1 cycle delay between a, b, and c
 
 In the simplest form, a cycle delay can appear as a prefix of another sequence, e.g., `##1 a`. This is essentially a concatenation with only one sequence, `a`, and an initial cycle delay of the concatenation of `1`. The prefix delays map to the LTL dialect as follows:
 
-- `##N seq`. **Fixed delay.** Sequence `seq` has to match exactly `N` cycles in the future. Equivalent to `ltl.delay %seq, N, 0`.
-- `##[N:M] seq`. **Bounded range delay.** Sequence `seq` has to match anywhere between `N` and `M` cycles in the future, inclusive. Equivalent to `ltl.delay %seq, N, (M-N)`
-- `##[N:$] seq`. **Unbounded range delay.** Sequence `seq` has to match anywhere at or beyond `N` cycles in the future, after a finite amount of cycles. Equivalent to `ltl.delay %seq, N`.
-- `##[*] seq`. Shorthand for `##[0:$]`. Equivalent to `ltl.delay %seq, 0`.
-- `##[+] seq`. Shorthand for `##[1:$]`. Equivalent to `ltl.delay %seq, 1`.
+- `##N seq`. **Fixed delay.** Sequence `seq` has to match exactly `N` cycles in the future. Equivalent to `ltl.delay %clk, posedge, %seq, N, 0`.
+- `##[N:M] seq`. **Bounded range delay.** Sequence `seq` has to match anywhere between `N` and `M` cycles in the future, inclusive. Equivalent to `ltl.delay %clk, posedge, %seq, N, (M-N)`
+- `##[N:$] seq`. **Unbounded range delay.** Sequence `seq` has to match anywhere at or beyond `N` cycles in the future, after a finite amount of cycles. Equivalent to `ltl.delay %clk, posedge, %seq, N`.
+- `##[*] seq`. Shorthand for `##[0:$]`. Equivalent to `ltl.delay %clk, posedge, %seq, 0`.
+- `##[+] seq`. Shorthand for `##[1:$]`. Equivalent to `ltl.delay %clk, posedge, %seq, 1`.
 
 Concatenation of two sequences always involves a cycle delay specification in between them, e.g., `a ##1 b` where sequence `b` starts in the cycle after `a` ends. Zero-cycle delays can be specified, e.g., `a ##0 b` where `b` starts in the same cycle as `a` ends. If `a` and `b` are booleans, `a ##0 b` is equivalent to `a && b`.
 
@@ -60,42 +60,42 @@ The dialect separates concatenation and cycle delay into two orthogonal operatio
 
 - `seqA ##N seqB`. **Binary concatenation.** Sequence `seqB` follows `N` cycles after `seqA`. This can be represented as `seqA ##0 (##N seqB)`, which is equivalent to
   ```
-  %0 = ltl.delay %seqB, N, 0
+  %0 = ltl.delay %clk, posedge, %seqB, N, 0
   ltl.concat %seqA, %0
   ```
 
 - `seqA ##N seqB ##M seqC`. **Variadic concatenation.** Sequence `seqC` follows `M` cycles after `seqB`, which itself follows `N` cycles after `seqA`. This can be represented as `seqA ##0 (##N seqB) ##0 (##M seqC)`, which is equivalent to
   ```
-  %0 = ltl.delay %seqB, N, 0
-  %1 = ltl.delay %seqC, M, 0
+  %0 = ltl.delay %clk, posedge, %seqB, N, 0
+  %1 = ltl.delay %clk, posedge, %seqC, M, 0
   ltl.concat %seqA, %0, %1
   ```
   Since concatenation is associative, this is also equivalent to `seqA ##N (seqB ##M seqC)`:
   ```
-  %0 = ltl.delay %seqC, M, 0
+  %0 = ltl.delay %clk, posedge, %seqC, M, 0
   %1 = ltl.concat %seqB, %0
-  %2 = ltl.delay %1, N, 0
+  %2 = ltl.delay %clk, posedge, %1, N, 0
   ltl.concat %seqA, %2
   ```
   And also `(seqA ##N seqB) ##M seqC`:
   ```
-  %0 = ltl.delay %seqB, N, 0
+  %0 = ltl.delay %clk, posedge, %seqB, N, 0
   %1 = ltl.concat %seqA, %0
-  %2 = ltl.delay %seqC, M, 0
+  %2 = ltl.delay %clk, posedge, %seqC, M, 0
   ltl.concat %1, %2
   ```
 
 - `##N seqA ##M seqB`. **Initial delay.** Sequence `seqB` follows `M` cycles afer `seqA`, which itself starts `N` cycles in the future. This is equivalent to a delay on `seqA` within the concatenation:
   ```
-  %0 = ltl.delay %seqA, N, 0
-  %1 = ltl.delay %seqB, M, 0
+  %0 = ltl.delay %clk, posedge, %seqA, N, 0
+  %1 = ltl.delay %clk, posedge, %seqB, M, 0
   ltl.concat %0, %1
   ```
   Alternatively, the delay can also be placed on the entire concatenation:
   ```
-  %0 = ltl.delay %seqB, M, 0
+  %0 = ltl.delay %clk, posedge, %seqB, M, 0
   %1 = ltl.concat %seqA, %0
-  ltl.delay %1, N, 0
+  ltl.delay %clk, posedge, %1, N, 0
   ```
 
 - Only the fixed delay `##N` is shown here for simplicity, but the examples extend to the other delay flavors `##[N:M]`, `##[N:$]`, `##[*]`, and `##[+]`.
@@ -160,6 +160,25 @@ 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 (concise)
+
+`ltl.delay` takes a clock `Value` and a `ClockEdgeAttr` as its first two
+operands:
+
+```
+ltl.delay %clock, <edge>, %input, <delay>[, <length>]
+```
+
+`%clock` is an `i1` value (e.g. a module clock); `<edge>` is `posedge`,
+`negedge`, or `edge`. The `delay`/`length` are counted on the specified
+clock/edge (for example `ltl.delay %clk, posedge, %s, 3` means `%s` must hold
+3 cycles later on `%clk` rising edges). `ltl.clock` globally associates a
+sequence/property with a clock/edge; using the same pair in `ltl.delay`
+keeps expressions in the same clocking domain.
+
+Note: lowering may insert an explicit clock value (e.g. `hw.constant` or
+`seq.from_clock`) when a direct `Value` for the clock is not available.
+
 
 ### Disable Iff
 
@@ -220,13 +239,13 @@ Knowing how to map SVA constructs to CIRCT is important to allow these to expres
   
 - **`a ##n b`**:   
 ```mlir
-%a_n = ltl.delay %a, n, 0 : i1
+%a_n = ltl.delay %clk, posedge, %a, n, 0 : i1
 %anb = ltl.concat %a_n, %b : !ltl.sequence 
 ```
 
 - **`a ##[n:m] b`**:
 ```mlir
-%a_n = ltl.delay %a, n, (m-n) : i1
+%a_n = ltl.delay %clk, posedge, %a, n, (m-n) : i1
 %anb = ltl.concat %a_n, %b : !ltl.sequence   
 ```
 
@@ -257,15 +276,15 @@ Knowing how to map SVA constructs to CIRCT is important to allow these to expres
 
 - **`s1 ##[+] s2`**:   
 ```mlir
-%ds1 = ltl.delay %s1, 1
+%ds1 = ltl.delay %clk, posedge, %s1, 1
 %s1s2 = ltl.concat %ds1, %s2 : !ltl.sequence  
-```  
+```
 
 - **`s1 ##[*] s2`**:   
 ```mlir
-%ds1 = ltl.delay %s1, 0
+%ds1 = ltl.delay %clk, posedge, %s1, 0
 %s1s2 = ltl.concat %ds1, %s2 : !ltl.sequence  
-```  
+```
 
 - **`s1 and s2`**:   
 ```mlir
@@ -299,8 +318,8 @@ ltl.not %s1 : !ltl.sequence
 ```mlir
 %c1 = hw.constant 1 : i1
 %rep1 = ltl.repeat %c1, 0 : !ltl.sequence
-%drep1 = ltl.delay %rep1, 1, 0 : !ltl.sequence
-%ds1 = ltl.delay %s1, 1, 0 : !ltl.sequence
+%drep1 = ltl.delay %clk, posedge, %rep1, 1, 0 : !ltl.sequence
+%ds1 = ltl.delay %clk, posedge, %s1, 1, 0 : !ltl.sequence
 %evs1 = ltl.concat %drep1, %ds1, %c1 : !ltl.sequence
 %res = ltl.intersect %evs1, %s2 : !ltl.sequence  
 ```
@@ -313,7 +332,7 @@ ltl.not %s1 : !ltl.sequence
 - **`s |=> p`**:  
 ```mlir
 %c1 = hw.constant 1 : i1
-%ds = ltl.delay %s, 1, 0 : i1
+%ds = ltl.delay %clk, posedge, %s, 1, 0 : i1
 %antecedent = ltl.concat %ds, %c1 : !ltl.sequence
 %impl = ltl.implication %antecedent, %p : !ltl.property  
 ```
@@ -342,7 +361,7 @@ ltl.not %s1 : !ltl.sequence
 - **`s #=# p`**:  
 ```mlir
 %np = ltl.not %p : !ltl.property	
-%ds = ltl.delay %s, 1, 0 : !ltl.sequence
+%ds = ltl.delay %clk, posedge, %s, 1, 0 : !ltl.sequence
 %c1 = hw.constant 1 : i1
 %ant = ltl.concat %ds, c1 : !ltl.sequence 
 %impl = ltl.implication %ant, %np : !ltl.property
@@ -354,13 +373,13 @@ ltl.not %s1 : !ltl.sequence
 
 - **`nexttime p`**:   
 ```mlir
-ltl.delay %p, 1, 0 : !ltl.sequence   
-```  
+ltl.delay %clk, posedge, %p, 1, 0 : !ltl.sequence   
+```
 
 - **`nexttime[n] p`**:  
 ```mlir
-ltl.delay %p, n, 0 : !ltl.sequence   
-```  
+ltl.delay %clk, posedge, %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.
@@ -418,13 +437,13 @@ The `ltl.delay` sequence operation represents various shorthands for the *next*/
 
 | Operation            | LTL Formula                 |
 |----------------------|-----------------------------|
-| `ltl.delay %a, 0, 0` | a                           |
-| `ltl.delay %a, 1, 0` | **X**a                      |
-| `ltl.delay %a, 3, 0` | **XXX**a                    |
-| `ltl.delay %a, 0, 2` | a ∨ **X**a ∨ **XX**a        |
-| `ltl.delay %a, 1, 2` | **X**(a ∨ **X**a ∨ **XX**a) |
-| `ltl.delay %a, 0`    | **F**a                      |
-| `ltl.delay %a, 2`    | **XXF**a                    |
+| `ltl.delay %clk, posedge, %a, 0, 0` | a                           |
+| `ltl.delay %clk, posedge, %a, 1, 0` | **X**a                      |
+| `ltl.delay %clk, posedge, %a, 3, 0` | **XXX**a                    |
+| `ltl.delay %clk, posedge, %a, 0, 2` | a ∨ **X**a ∨ **XX**a        |
+| `ltl.delay %clk, posedge, %a, 1, 2` | **X**(a ∨ **X**a ∨ **XX**a) |
+| `ltl.delay %clk, posedge, %a, 0`    | **F**a                      |
+| `ltl.delay %clk, posedge, %a, 2`    | **XXF**a                    |
 
 
 ### Until and Eventually
diff --git a/docs/FormalVerification.md b/docs/FormalVerification.md
index 7d22897e5e83..5d7d1e875baa 100644
--- a/docs/FormalVerification.md
+++ b/docs/FormalVerification.md
@@ -232,7 +232,7 @@ hw.module @mod(in %clk: !seq.clock, in %arg0: i32, in %rst: i1,
   %3 = comb.icmp eq, %2, %c0_i32 : i32
   verif.assume %3 : i1
   %4 = comb.xor %rst, %true : i1
-  %5 = ltl.delay %4, 2 : i1
+  %5 = ltl.delay %clk, posedge, %4, 2 : i1
   %6 = ltl.concat %rst, %5 : i1, !ltl.sequence
   %7 = ltl.clock %6, posedge %clk : !ltl.sequence
   verif.assume %7 : !ltl.sequence
@@ -265,7 +265,7 @@ verif.bmc bound 10 {
   %3 = comb.icmp eq, %2, %c0_i32 : i32
   verif.assume %3 : i1
   %4 = comb.xor %rst, %true : i1
-  %5 = ltl.delay %4, 2 : i1
+  %5 = ltl.delay %clk, posedge, %4, 2 : i1
   %6 = ltl.concat %rst, %5 : i1, !ltl.sequence
   %7 = ltl.clock %6, posedge %clk : !ltl.sequence
   verif.assume %7 : !ltl.sequence
diff --git a/include/circt/Dialect/LTL/LTLFolds.td b/include/circt/Dialect/LTL/LTLFolds.td
index 6db7668f1923..61c666d160e5 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 delays use the same clock and edge before
+// merging. Accepts (outerClock, innerClock, outerEdge, innerEdge).
+def SameClockAndEdge : Constraint<CPred<"$0 == $1 && $2 == $3">>;
+
 //===----------------------------------------------------------------------===//
 // DelayOp
 //===----------------------------------------------------------------------===//
@@ -36,14 +40,15 @@ def mergedLengths : NativeCodeCall<[{
            : IntegerAttr{}
 }]>;
 def NestedDelays : Pat<
-  (DelayOp (DelayOp $input, $delay1, $length1), $delay2, $length2),
-  (DelayOp $input, (mergedDelays $delay1, $delay2),
-                   (mergedLengths $length1, $length2))>;
+  (DelayOp $clock0, $edge0, (DelayOp $clock1, $edge1, $input, $delay1, $length1), $delay2, $length2),
+  (DelayOp $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),
+  (DelayOp $clock, $edge, (ConcatOp $inputs), $delay, $length),
+  (ConcatOp (concatValues (DelayOp $clock, $edge, (valueHead $inputs), $delay, $length),
                           (valueTail $inputs)))>;
 
 //===----------------------------------------------------------------------===//
diff --git a/include/circt/Dialect/LTL/LTLOps.td b/include/circt/Dialect/LTL/LTLOps.td
index eda848b1dea3..c96969015cf7 100644
--- a/include/circt/Dialect/LTL/LTLOps.td
+++ b/include/circt/Dialect/LTL/LTLOps.td
@@ -61,46 +61,96 @@ 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
 //===----------------------------------------------------------------------===//
 
 def DelayOp : LTLOp<"delay", [Pure]> {
-  let arguments = (ins
-    LTLAnySequenceType:$input,
-    I64Attr:$delay,
-    OptionalAttr<I64Attr>:$length);
+  // Require an explicit clock SSA operand. The clock is now an operand
+  // (e.g. `%clk`) and must be provided when creating a delay. The edge is
+  // specified as a `ClockEdgeAttr` operand. The assembly places the clock
+  // first to make the clocking context explicit at the call site.
+  let arguments = (ins 
+      I1:$clock,
+      ClockEdgeAttr:$edge, 
+      LTLAnySequenceType:$input,
+      I64Attr:$delay,
+      OptionalAttr<I64Attr>:$length);
   let results = (outs LTLSequenceType:$result);
   let assemblyFormat = [{
-    $input `,` $delay (`,` $length^)? attr-dict `:` type($input)
+    $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.";
   let description = [{
-    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.
-    - `ltl.delay %seq, 0, 0` is equivalent to just `%seq`.
+    Delays the `$input` sequence by the number of cycles specified by `$delay` on
+    the given `$clock` operand and `$edge` operand. The clock must be passed
+    as an explicit SSA operand (for example `%clk`). 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 %clk, posedge, %seq, 2, 0` delays `%seq` by exactly 2 cycles on
+      the positive edge of `%clk`. The resulting sequence matches if `%seq`
+      matches exactly 2 cycles in the future.
+    - `ltl.delay %clk, posedge, %seq, 2, 2` delays `%seq` by 2, 3, or 4 cycles on
+      the positive edge of `%clk`. The resulting sequence matches if `%seq` 
+      matches 2, 3, or 4 cycles in the future.
+    - `ltl.delay %clk, posedge, %seq, 2` delays `%seq` by 2 or more cycles on the
+      positive edge of `%clk`. 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.
+    - `ltl.delay %clk, posedge, %seq, 0, 0` is equivalent to just `%seq`.
 
     #### Clocking
 
-    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.
+    The cycle delay now explicitly refers to the `$clock` SSA operand and the
+    `$edge` attribute. There is no implicit clock inference for delays; callers
+    must provide the desired clock. Backends should discover the clock for a
+    larger sequence by scanning its subtree for such explicit clocked delays.
   }];
 }
 
@@ -346,45 +396,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/lib/Conversion/FIRRTLToHW/LowerToHW.cpp b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp
index eacc1c814ae1..c8e71a45f9c5 100644
--- a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp
+++ b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp
@@ -4411,7 +4411,15 @@ LogicalResult FIRRTLLowering::visitExpr(LTLIntersectIntrinsicOp op) {
 }
 
 LogicalResult FIRRTLLowering::visitExpr(LTLDelayIntrinsicOp op) {
-  return setLoweringToLTL<ltl::DelayOp>(op, getLoweredValue(op.getInput()),
+  // The FIRRTL intrinsic doesn't carry an explicit clock; synthesize a
+  // default 1-bit clock value (true) and use the positive edge by default.
+  // Backends or later passes may replace this with a real clock wire when
+  // composing larger clocked sequences.
+  auto clock = getOrCreateIntConstant(1, 1);
+  auto edgeAttr =
+      ltl::ClockEdgeAttr::get(builder.getContext(), ltl::ClockEdge::Pos);
+  return setLoweringToLTL<ltl::DelayOp>(op, clock, edgeAttr,
+                                        getLoweredValue(op.getInput()),
                                         op.getDelayAttr(), op.getLengthAttr());
 }
 
diff --git a/lib/Conversion/ImportVerilog/AssertionExpr.cpp b/lib/Conversion/ImportVerilog/AssertionExpr.cpp
index 6fdf7748a2da..20e044c1bd21 100644
--- a/lib/Conversion/ImportVerilog/AssertionExpr.cpp
+++ b/lib/Conversion/ImportVerilog/AssertionExpr.cpp
@@ -121,8 +121,14 @@ struct AssertionExprVisitor {
 
       auto [delayMin, delayRange] =
           convertRangeToAttrs(concatElement.delay.min, concatElement.delay.max);
-      auto delayedSequence = ltl::DelayOp::create(builder, loc, sequenceValue,
-                                                  delayMin, delayRange);
+      auto delayedClock =
+          hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1)
+              .getResult();
+      auto delayedEdge =
+          ltl::ClockEdgeAttr::get(builder.getContext(), ltl::ClockEdge::Pos);
+      auto delayedSequence =
+          ltl::DelayOp::create(builder, loc, delayedClock, delayedEdge,
+                               sequenceValue, delayMin, delayRange);
       sequenceElements.push_back(delayedSequence);
     }
 
@@ -159,8 +165,12 @@ struct AssertionExprVisitor {
       if (expr.range.has_value()) {
         minRepetitions = builder.getI64IntegerAttr(expr.range.value().min);
       }
-      return ltl::DelayOp::create(builder, loc, value, minRepetitions,
-                                  builder.getI64IntegerAttr(0));
+      auto clock = hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1)
+                       .getResult();
+      auto edge =
+          ltl::ClockEdgeAttr::get(builder.getContext(), ltl::ClockEdge::Pos);
+      return ltl::DelayOp::create(builder, loc, clock, edge, value,
+                                  minRepetitions, builder.getI64IntegerAttr(0));
     }
     case UnaryAssertionOperator::Eventually:
     case UnaryAssertionOperator::SNextTime:
@@ -198,12 +208,22 @@ struct AssertionExprVisitor {
       auto oneRepeat = ltl::RepeatOp::create(builder, loc, constOne,
                                              builder.getI64IntegerAttr(0),
                                              mlir::IntegerAttr{});
-      auto repeatDelay = ltl::DelayOp::create(builder, loc, oneRepeat,
-                                              builder.getI64IntegerAttr(1),
-                                              builder.getI64IntegerAttr(0));
-      auto lhsDelay =
-          ltl::DelayOp::create(builder, loc, lhs, builder.getI64IntegerAttr(1),
-                               builder.getI64IntegerAttr(0));
+      auto repeatClock =
+          hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1)
+              .getResult();
+      auto repeatEdge =
+          ltl::ClockEdgeAttr::get(builder.getContext(), ltl::ClockEdge::Pos);
+      auto repeatDelay = ltl::DelayOp::create(
+          builder, loc, repeatClock, repeatEdge, oneRepeat,
+          builder.getI64IntegerAttr(1), builder.getI64IntegerAttr(0));
+      auto lhsClock =
+          hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1)
+              .getResult();
+      auto lhsEdge =
+          ltl::ClockEdgeAttr::get(builder.getContext(), ltl::ClockEdge::Pos);
+      auto lhsDelay = ltl::DelayOp::create(builder, loc, lhsClock, lhsEdge, lhs,
+                                           builder.getI64IntegerAttr(1),
+                                           builder.getI64IntegerAttr(0));
       auto combined = ltl::ConcatOp::create(
           builder, loc, SmallVector<Value, 3>{repeatDelay, lhsDelay, constOne});
       return ltl::IntersectOp::create(builder, loc,
@@ -235,9 +255,14 @@ struct AssertionExprVisitor {
     case BinaryAssertionOperator::NonOverlappedImplication: {
       auto constOne =
           hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1);
-      auto lhsDelay =
-          ltl::DelayOp::create(builder, loc, lhs, builder.getI64IntegerAttr(1),
-                               builder.getI64IntegerAttr(0));
+      auto lhsClock =
+          hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1)
+              .getResult();
+      auto lhsEdge =
+          ltl::ClockEdgeAttr::get(builder.getContext(), ltl::ClockEdge::Pos);
+      auto lhsDelay = ltl::DelayOp::create(builder, loc, lhsClock, lhsEdge, lhs,
+                                           builder.getI64IntegerAttr(1),
+                                           builder.getI64IntegerAttr(0));
       auto antecedent = ltl::ConcatOp::create(
           builder, loc, SmallVector<Value, 2>{lhsDelay, constOne});
       return ltl::ImplicationOp::create(builder, loc,
@@ -253,9 +278,14 @@ struct AssertionExprVisitor {
       auto constOne =
           hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1);
       auto notRhs = ltl::NotOp::create(builder, loc, rhs);
-      auto lhsDelay =
-          ltl::DelayOp::create(builder, loc, lhs, builder.getI64IntegerAttr(1),
-                               builder.getI64IntegerAttr(0));
+      auto lhsClock =
+          hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1)
+              .getResult();
+      auto lhsEdge =
+          ltl::ClockEdgeAttr::get(builder.getContext(), ltl::ClockEdge::Pos);
+      auto lhsDelay = ltl::DelayOp::create(builder, loc, lhsClock, lhsEdge, lhs,
+                                           builder.getI64IntegerAttr(1),
+                                           builder.getI64IntegerAttr(0));
       auto antecedent = ltl::ConcatOp::create(
           builder, loc, SmallVector<Value, 2>{lhsDelay, constOne});
       auto implication = ltl::ImplicationOp::create(
diff --git a/lib/Dialect/LTL/LTLFolds.cpp b/lib/Dialect/LTL/LTLFolds.cpp
index 33611f75c136..5f80178f36a2 100644
--- a/lib/Dialect/LTL/LTLFolds.cpp
+++ b/lib/Dialect/LTL/LTLFolds.cpp
@@ -80,7 +80,7 @@ LogicalResult IntersectOp::canonicalize(IntersectOp op,
 //===----------------------------------------------------------------------===//
 
 OpFoldResult DelayOp::fold(FoldAdaptor adaptor) {
-  // delay(s, 0, 0) -> s
+  // delay(posedge, clock, s, 0, 0) -> s
   if (adaptor.getDelay() == 0 && adaptor.getLength() == 0 &&
       isa<SequenceType>(getInput().getType()))
     return getInput();
diff --git a/test/Conversion/ExportVerilog/prepare-for-emission.mlir b/test/Conversion/ExportVerilog/prepare-for-emission.mlir
index 5b1fbfeabdeb..ee0640d55a5d 100644
--- a/test/Conversion/ExportVerilog/prepare-for-emission.mlir
+++ b/test/Conversion/ExportVerilog/prepare-for-emission.mlir
@@ -258,13 +258,13 @@ module attributes { circt.loweringOptions = "disallowPackedStructAssignments"} {
 // 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(in %a: i1, in %b: i1) {
+hw.module @Issue5613(in %a: i1, in %b: i1, in %clk: 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
+  %4 = ltl.delay %clk, posedge, %a, 42 : i1
   hw.output
 }
 
diff --git a/test/Conversion/ExportVerilog/verif.mlir b/test/Conversion/ExportVerilog/verif.mlir
index 1cffd4414f9b..baf05f914b13 100644
--- a/test/Conversion/ExportVerilog/verif.mlir
+++ b/test/Conversion/ExportVerilog/verif.mlir
@@ -67,22 +67,22 @@ hw.module @BasicEmissionTemporal(in %a: i1) {
 // CHECK-LABEL: module Sequences
 hw.module @Sequences(in %clk: i1, in %a: i1, in %b: i1) {
   // CHECK: assert property (##0 a);
-  %d0 = ltl.delay %a, 0, 0 : i1
+  %d0 = ltl.delay %clk, posedge, %a, 0, 0 : i1
   sv.assert_property %d0 : !ltl.sequence
   // CHECK: assert property (##4 a);
-  %d1 = ltl.delay %a, 4, 0 : i1
+  %d1 = ltl.delay %clk, posedge, %a, 4, 0 : i1
   sv.assert_property %d1 : !ltl.sequence
   // CHECK: assert property (##[5:6] a);
-  %d2 = ltl.delay %a, 5, 1 : i1
+  %d2 = ltl.delay %clk, posedge, %a, 5, 1 : i1
   sv.assert_property %d2 : !ltl.sequence
   // CHECK: assert property (##[7:$] a);
-  %d3 = ltl.delay %a, 7 : i1
+  %d3 = ltl.delay %clk, posedge, %a, 7 : i1
   sv.assert_property %d3 : !ltl.sequence
   // CHECK: assert property (##[*] a);
-  %d4 = ltl.delay %a, 0 : i1
+  %d4 = ltl.delay %clk, posedge, %a, 0 : i1
   sv.assert_property %d4 : !ltl.sequence
   // CHECK: assert property (##[+] a);
-  %d5 = ltl.delay %a, 1 : i1
+  %d5 = ltl.delay %clk, posedge, %a, 1 : i1
   sv.assert_property %d5 : !ltl.sequence
 
   // CHECK: assert property (a ##0 a);
@@ -180,11 +180,11 @@ hw.module @Properties(in %clk: i1, in %a: i1, in %b: i1) {
   // CHECK: assert property (a ##1 b |=> not a);
   %i0 = ltl.implication %a, %b : i1, i1
   sv.assert_property %i0 : !ltl.property
-  %i1 = ltl.delay %b, 1, 0 : i1
+  %i1 = ltl.delay %clk, posedge, %b, 1, 0 : i1
   %i2 = ltl.concat %a, %i1 : i1, !ltl.sequence
   %i3 = ltl.implication %i2, %n0 : !ltl.sequence, !ltl.property
   sv.assert_property %i3 : !ltl.property
-  %i4 = ltl.delay %true, 1, 0 : i1
+  %i4 = ltl.delay %clk, posedge, %true, 1, 0 : i1
   %i5 = ltl.concat %a, %i1, %i4 : i1, !ltl.sequence, !ltl.sequence
   %i6 = ltl.implication %i5, %n0 : !ltl.sequence, !ltl.property
   sv.assert_property %i6 : !ltl.property
@@ -211,14 +211,15 @@ hw.module @Properties(in %clk: i1, in %a: i1, in %b: i1) {
 
 // CHECK-LABEL: module Precedence
 hw.module @Precedence(in %a: i1, in %b: i1) {
+  %true = hw.constant true
   // CHECK: assert property ((a or ##0 b) and b);
-  %a0 = ltl.delay %b, 0, 0 : i1
+  %a0 = ltl.delay %true, posedge, %b, 0, 0 : i1
   %a1 = ltl.or %a, %a0 : i1, !ltl.sequence
   %a2 = ltl.and %a1, %b : !ltl.sequence, i1
   sv.assert_property %a2 : !ltl.sequence
 
   // CHECK: assert property (##1 (a or ##0 b));
-  %d0 = ltl.delay %a1, 1, 0 : !ltl.sequence
+  %d0 = ltl.delay %true, posedge, %a1, 1, 0 : !ltl.sequence
   sv.assert_property %d0 : !ltl.sequence
 
   // CHECK: assert property (not (a or ##0 b));
@@ -249,8 +250,8 @@ hw.module @SystemVerilogSpecExamples(in %clk: i1, in %a: i1, in %b: i1, in %c: i
   // Section 16.7 "Sequences"
 
   // CHECK: assert property (a ##1 b ##0 c ##1 d);
-  %a0 = ltl.delay %b, 1, 0 : i1
-  %a1 = ltl.delay %d, 1, 0 : i1
+  %a0 = ltl.delay %clk, posedge, %b, 1, 0 : i1
+  %a1 = ltl.delay %clk, posedge, %d, 1, 0 : i1
   %a2 = ltl.concat %a, %a0 : i1, !ltl.sequence
   %a3 = ltl.concat %c, %a1 : i1, !ltl.sequence
   %a4 = ltl.concat %a2, %a3 : !ltl.sequence, !ltl.sequence
@@ -259,7 +260,7 @@ hw.module @SystemVerilogSpecExamples(in %clk: i1, in %a: i1, in %b: i1, in %c: i
   // Section 16.12.20 "Property examples"
 
   // CHECK: assert property (@(posedge clk) a |-> b ##1 c ##1 d);
-  %b0 = ltl.delay %c, 1, 0 : i1
+  %b0 = ltl.delay %clk, posedge, %c, 1, 0 : i1
   %b1 = ltl.concat %b, %b0, %a1 : i1, !ltl.sequence, !ltl.sequence
   %b2 = ltl.implication %a, %b1 : i1, !ltl.sequence
   %b3 = ltl.clock %b2, posedge %clk : !ltl.property
@@ -272,7 +273,7 @@ hw.module @SystemVerilogSpecExamples(in %clk: i1, in %a: i1, in %b: i1, in %c: i
   sv.assert_property %c3 disable_iff %e : !ltl.property
 
   // CHECK: assert property (##1 a |-> b);
-  %d0 = ltl.delay %a, 1, 0 : i1
+  %d0 = ltl.delay %clk, posedge, %a, 1, 0 : i1
   %d1 = ltl.implication %d0, %b : !ltl.sequence, i1
   sv.assert_property %d1 : !ltl.property
 }
@@ -295,7 +296,7 @@ hw.module @LivenessExample(in %clock: i1, in %reset: i1, in %isLive: i1) {
 
   // CHECK: assert property (disable iff (reset) @(posedge clock) isLive ##1 _GEN |-> (s_eventually isLive));
   // CHECK-NEXT: assume property (disable iff (reset) @(posedge clock) isLive ##1 _GEN |-> (s_eventually isLive));
-  %4 = ltl.delay %not_isLive, 1, 0 : i1
+  %4 = ltl.delay %clock, posedge, %not_isLive, 1, 0 : i1
   %5 = ltl.concat %isLive, %4 : i1, !ltl.sequence
   %6 = ltl.implication %5, %1 : !ltl.sequence, !ltl.property
   %liveness_after_fall = ltl.clock %6, posedge %clock : !ltl.property
diff --git a/test/Conversion/FIRRTLToHW/intrinsics.mlir b/test/Conversion/FIRRTLToHW/intrinsics.mlir
index 93234e89918c..cb26549bc975 100644
--- a/test/Conversion/FIRRTLToHW/intrinsics.mlir
+++ b/test/Conversion/FIRRTLToHW/intrinsics.mlir
@@ -62,9 +62,10 @@ firrtl.circuit "Intrinsics" {
   // CHECK-LABEL: hw.module @LTLAndVerif
   firrtl.module @LTLAndVerif(in %clk: !firrtl.clock, in %a: !firrtl.uint<1>, in %b: !firrtl.uint<1>) {
     // CHECK-NEXT: [[CLK:%.+]] = seq.from_clock %clk
-    // CHECK-NEXT: [[D0:%.+]] = ltl.delay %a, 42 : i1
+    // CHECK-NEXT: {{%.*}} = hw.constant true
+    // CHECK-NEXT: [[D0:%.+]] = ltl.delay {{%.*}}, posedge, %a, 42 : i1
     %d0 = firrtl.int.ltl.delay %a, 42 : (!firrtl.uint<1>) -> !firrtl.uint<1>
-    // CHECK-NEXT: [[D1:%.+]] = ltl.delay %b, 42, 1337 : i1
+    // CHECK-NEXT: [[D1:%.+]] = ltl.delay {{%.*}}, posedge, %b, 42, 1337 : i1
     %d1 = firrtl.int.ltl.delay %b, 42, 1337 : (!firrtl.uint<1>) -> !firrtl.uint<1>
 
     // CHECK-NEXT: [[L0:%.+]] = ltl.and [[D0]], [[D1]] : !ltl.sequence, !ltl.sequence
@@ -149,6 +150,7 @@ firrtl.circuit "Intrinsics" {
     %f = firrtl.wire : !firrtl.uint<1>
     %g = firrtl.wire : !firrtl.uint<1>
 
+    // CHECK-NEXT: {{%.*}} = hw.constant true
     // CHECK-NEXT: verif.assert [[E:%.+]] : !ltl.sequence
     // CHECK-NEXT: verif.assert [[F:%.+]] : !ltl.property
     // CHECK-NEXT: verif.assert [[G:%.+]] : !ltl.property
@@ -177,7 +179,7 @@ firrtl.circuit "Intrinsics" {
     firrtl.matchingconnect %d, %1 : !firrtl.uint<1>
 
     // !ltl.sequence
-    // CHECK-NEXT: [[C]] = ltl.delay %a, 42 : i1
+    // CHECK-NEXT: [[C]] = ltl.delay {{%.*}}, posedge, %a, 42 : i1
     %0 = firrtl.int.ltl.delay %a, 42 : (!firrtl.uint<1>) -> !firrtl.uint<1>
     firrtl.matchingconnect %c, %0 : !firrtl.uint<1>
   }
diff --git a/test/Conversion/ImportVerilog/basic.sv b/test/Conversion/ImportVerilog/basic.sv
index 33bfaf218202..66295e7b15a2 100644
--- a/test/Conversion/ImportVerilog/basic.sv
+++ b/test/Conversion/ImportVerilog/basic.sv
@@ -2419,10 +2419,10 @@ module ConcurrentAssert(input clk);
   // CHECK: moore.procedure always
     // CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
     // CHECK: [[CONV_A:%.+]] = moore.to_builtin_bool [[READ_A]] : i1
-    // CHECK: [[DELAY_A:%.+]] = ltl.delay [[CONV_A]], 0, 0 : i1
+    // CHECK: [[DELAY_A:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 0, 0 : i1
     // CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
     // CHECK: [[CONV_B:%.+]] = moore.to_builtin_bool [[READ_B]] : l1
-    // CHECK: [[DELAY_B:%.+]] = ltl.delay [[CONV_B]], 0, 0 : i1
+    // CHECK: [[DELAY_B:%.+]] = ltl.delay [[PRE:.*]] [[CONV_B]], 0, 0 : i1
     // CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_A]], [[DELAY_B]] : !ltl.sequence, !ltl.sequence
     // CHECK: verif.assert [[CONCAT_OP]] : !ltl.sequence
     // CHECK: moore.return
@@ -2431,13 +2431,13 @@ module ConcurrentAssert(input clk);
   // CHECK: moore.procedure always
     // CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
     // CHECK: [[CONV_A:%.+]] = moore.to_builtin_bool [[READ_A]] : i1
-    // CHECK: [[DELAY_A:%.+]] = ltl.delay [[CONV_A]], 0, 0 : i1
+    // CHECK: [[DELAY_A:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 0, 0 : i1
     // CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
     // CHECK: [[CONV_B:%.+]] = moore.to_builtin_bool [[READ_B]] : l1
-    // CHECK: [[DELAY_B:%.+]] = ltl.delay [[CONV_B]], 1 : i1
+    // CHECK: [[DELAY_B:%.+]] = ltl.delay [[PRE:.*]] [[CONV_B]], 1 : i1
     // CHECK: [[READ_A2:%.+]] = moore.read [[A]] : <i1>
     // CHECK: [[CONV_A2:%.+]] = moore.to_builtin_bool [[READ_A2]] : i1
-    // CHECK: [[DELAY_A2:%.+]] = ltl.delay [[CONV_A2]], 3, 2 : i1
+    // CHECK: [[DELAY_A2:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A2]], 3, 2 : i1
     // CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_A]], [[DELAY_B]], [[DELAY_A2]] : !ltl.sequence, !ltl.sequence, !ltl.sequence
     // CHECK: verif.assert [[CONCAT_OP]] : !ltl.sequence
     // CHECK: moore.return
@@ -2480,7 +2480,7 @@ module ConcurrentAssert(input clk);
   // CHECK: moore.procedure always
     // CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
     // CHECK: [[CONV_A:%.+]] = moore.to_builtin_bool [[READ_A]] : i1
-    // CHECK: [[DELAY_OP:%.+]] = ltl.delay [[CONV_A]], 1, 0 : i1
+    // CHECK: [[DELAY_OP:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 1, 0 : i1
     // CHECK: verif.assert [[DELAY_OP]] : !ltl.sequence
     // CHECK: moore.return
   // CHECK: }
@@ -2488,7 +2488,7 @@ module ConcurrentAssert(input clk);
   // CHECK: moore.procedure always
     // CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
     // CHECK: [[CONV_A:%.+]] = moore.to_builtin_bool [[READ_A]] : i1
-    // CHECK: [[DELAY_OP:%.+]] = ltl.delay [[CONV_A]], 5, 0 : i1
+    // CHECK: [[DELAY_OP:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 5, 0 : i1
     // CHECK: verif.assert [[DELAY_OP]] : !ltl.sequence
     // CHECK: moore.return
   // CHECK: }
@@ -2543,8 +2543,8 @@ module ConcurrentAssert(input clk);
     // CHECK: [[CONV_B:%.+]] = moore.to_builtin_bool [[READ_B]] : l1
     // CHECK: [[CONST_T:%.+]] = hw.constant true
     // CHECK: [[REPEAT_T:%.+]] = ltl.repeat [[CONST_T]], 0 : i1
-    // CHECK: [[DELAY_RT:%.+]] = ltl.delay [[REPEAT_T]], 1, 0 : !ltl.sequence
-    // CHECK: [[DELAY_A:%.+]] = ltl.delay [[CONV_A]], 1, 0 : i1
+    // CHECK: [[DELAY_RT:%.+]] = ltl.delay [[PRE:.*]] [[REPEAT_T]], 1, 0 : !ltl.sequence
+    // CHECK: [[DELAY_A:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 1, 0 : i1
     // CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_RT]], [[DELAY_A]], [[CONST_T]] : !ltl.sequence, !ltl.sequence, i1
     // CHECK: [[INTER_OP:%.+]] = ltl.intersect [[CONCAT_OP]], [[CONV_B]] : !ltl.sequence, i1
     // CHECK: verif.assert [[INTER_OP]] : !ltl.sequence
@@ -2614,7 +2614,7 @@ module ConcurrentAssert(input clk);
     // CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
     // CHECK: [[CONV_B:%.+]] = moore.to_builtin_bool [[READ_B]] : l1
     // CHECK: [[CONST_T:%.+]] = hw.constant true
-    // CHECK: [[DELAY_OP:%.+]] = ltl.delay [[CONV_A]], 1, 0 : i1
+    // CHECK: [[DELAY_OP:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 1, 0 : i1
     // CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_OP]], [[CONST_T]] : !ltl.sequence, i1
     // CHECK: [[IMPLICATION_OP:%.+]] = ltl.implication [[CONCAT_OP]], [[CONV_B]] : !ltl.sequence, i1
     // CHECK: verif.assert [[IMPLICATION_OP]] : !ltl.property
@@ -2640,7 +2640,7 @@ module ConcurrentAssert(input clk);
     // CHECK: [[CONV_B:%.+]] = moore.to_builtin_bool [[READ_B]] : l1
     // CHECK: [[CONST_T:%.+]] = hw.constant true
     // CHECK: [[NOT_OP:%.+]] = ltl.not [[CONV_B]] : i1
-    // CHECK: [[DELAY_OP:%.+]] = ltl.delay [[CONV_A]], 1, 0 : i1
+    // CHECK: [[DELAY_OP:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 1, 0 : i1
     // CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_OP]], [[CONST_T]] : !ltl.sequence, i1
     // CHECK: [[IMPLICATION_OP:%.+]] = ltl.implication [[CONCAT_OP]], [[NOT_OP]] : !ltl.sequence, !ltl.property
     // CHECK: [[NOT_IMPLI_OP:%.+]] = ltl.not [[IMPLICATION_OP]] : !ltl.property
@@ -2665,10 +2665,10 @@ module ConcurrentAssert(input clk);
   // CHECK: moore.procedure always {
     // CHECK: [[TMP:%.+]] = moore.read %a : <i1>
     // CHECK: [[A:%.+]] = moore.to_builtin_bool [[TMP]] : i1
-    // CHECK: [[DA:%.+]] = ltl.delay [[A]], 0, 0 : i1
+    // CHECK: [[DA:%.+]] = ltl.delay [[PRE:.*]] [[A]], 0, 0 : i1
     // CHECK: [[TMP:%.+]] = moore.read %b : <l1>
     // CHECK: [[B:%.+]] = moore.to_builtin_bool [[TMP]] : l1
-    // CHECK: [[DB:%.+]] = ltl.delay [[B]], 1, 0 : i1
+    // CHECK: [[DB:%.+]] = ltl.delay [[PRE:.*]] [[B]], 1, 0 : i1
     // CHECK: [[RES:%.+]] = ltl.concat %6, %9 : !ltl.sequence, !ltl.sequence
     // CHECK: verif.assert [[RES]] : !ltl.sequence
     // CHECK: moore.return
@@ -2685,8 +2685,8 @@ module ConcurrentAssert(input clk);
     // CHECK: [[A:%.+]] = moore.to_builtin_bool [[TMP]] : i1
     // CHECK: [[TRUE:%.+]] = hw.constant true
     // CHECK: [[OP1:%.+]] = ltl.repeat [[TRUE]], 0 : i1
-    // CHECK: [[OP2:%.+]] = ltl.delay [[OP1]], 1, 0 : !ltl.sequence
-    // CHECK: [[OP3:%.+]] = ltl.delay [[B]], 1, 0 : i1
+    // CHECK: [[OP2:%.+]] = ltl.delay [[PRE:.*]] [[OP1]], 1, 0 : !ltl.sequence
+    // CHECK: [[OP3:%.+]] = ltl.delay [[PRE:.*]] [[B]], 1, 0 : i1
     // CHECK: [[OP4:%.+]] = ltl.concat [[OP2]], [[OP3]], [[TRUE]] : !ltl.sequence, !ltl.sequence, i1
     // CHECK: [[RES:%.+]] = ltl.intersect [[OP4]], [[A]] : !ltl.sequence, i1
     // CHECK: verif.assert [[RES]] : !ltl.sequence
@@ -2700,10 +2700,10 @@ module ConcurrentAssert(input clk);
   // CHECK: moore.procedure always {
     // CHECK: [[TMP:%.+]] = moore.read %a : <i1>
     // CHECK: [[A:%.+]] = moore.to_builtin_bool [[TMP]] : i1
-    // CHECK: [[DA:%.+]] = ltl.delay [[A]], 0, 0 : i1
+    // CHECK: [[DA:%.+]] = ltl.delay [[PRE:.*]] [[A]], 0, 0 : i1
     // CHECK: [[TMP:%.+]] = moore.read %b : <l1>
     // CHECK: [[B:%.+]] = moore.to_builtin_bool [[TMP]] : l1
-    // CHECK: [[DB:%.+]] = ltl.delay [[B]], 1, 0 : i1
+    // CHECK: [[DB:%.+]] = ltl.delay [[PRE:.*]] [[B]], 1, 0 : i1
     // CHECK: [[OP1:%.+]] = ltl.concat [[DA]], [[DB]] : !ltl.sequence, !ltl.sequence
     // CHECK: [[TMP:%.+]] = moore.read %b : <l1>
     // CHECK: [[B2:%.+]] = moore.to_builtin_bool [[TMP]] : l1
@@ -2725,14 +2725,14 @@ module ConcurrentAssert(input clk);
     // CHECK: [[B1:%.+]] = moore.to_builtin_bool [[TMP]] : l1
     // CHECK: [[TRUE:%.+]] = hw.constant true
     // CHECK: [[OP1:%.+]] = ltl.repeat [[TRUE]], 0 : i1
-    // CHECK: [[OP2:%.+]] = ltl.delay [[OP1]], 1, 0 : !ltl.sequence
-    // CHECK: [[OP3:%.+]] = ltl.delay [[A2]], 1, 0 : i1
+    // CHECK: [[OP2:%.+]] = ltl.delay [[PRE:.*]] [[OP1]], 1, 0 : !ltl.sequence
+    // CHECK: [[OP3:%.+]] = ltl.delay [[PRE:.*]] [[A2]], 1, 0 : i1
     // CHECK: [[OP4:%.+]] = ltl.concat [[OP2]], [[OP3]], [[TRUE]] : !ltl.sequence, !ltl.sequence, i1
     // CHECK: [[OP5:%.+]] = ltl.intersect [[OP4]], [[B1]] : !ltl.sequence, i1
     // CHECK: [[TRUE1:%.+]] = hw.constant true
     // CHECK: [[OP6:%.+]] = ltl.repeat [[TRUE1]], 0 : i1
-    // CHECK: [[OP7:%.+]] = ltl.delay [[OP6]], 1, 0 : !ltl.sequence
-    // CHECK: [[OP8:%.+]] = ltl.delay [[A1]], 1, 0 : i1
+    // CHECK: [[OP7:%.+]] = ltl.delay [[PRE:.*]] [[OP6]], 1, 0 : !ltl.sequence
+    // CHECK: [[OP8:%.+]] = ltl.delay [[PRE:.*]] [[A1]], 1, 0 : i1
     // CHECK: [[OP9:%.+]] = ltl.concat [[OP7]], [[OP8]], [[TRUE1]] : !ltl.sequence, !ltl.sequence, i1
     // CHECK: [[OP10:%.+]] = ltl.intersect [[OP9]], [[OP5]] : !ltl.sequence, !ltl.sequence
     // CHECK: [[TMP:%.+]] = moore.read %a : <i1>
diff --git a/test/Dialect/LTL/basic.mlir b/test/Dialect/LTL/basic.mlir
index ef6d0b1319a0..c1119a616fdf 100644
--- a/test/Dialect/LTL/basic.mlir
+++ b/test/Dialect/LTL/basic.mlir
@@ -1,6 +1,7 @@
 // RUN: circt-opt %s | circt-opt | FileCheck %s
 
 %true = hw.constant true
+%clk = hw.constant true
 
 //===----------------------------------------------------------------------===//
 // Types
@@ -50,10 +51,10 @@ unrealized_conversion_cast %p3 : !ltl.property to index
 // Sequences
 //===----------------------------------------------------------------------===//
 
-// CHECK: ltl.delay {{%.+}}, 0 : !ltl.sequence
-// CHECK: ltl.delay {{%.+}}, 42, 1337 : !ltl.sequence
-ltl.delay %s, 0 : !ltl.sequence
-ltl.delay %s, 42, 1337 : !ltl.sequence
+// CHECK: ltl.delay {{%.+}}, posedge, {{%.+}}, 0 : !ltl.sequence
+// CHECK: ltl.delay {{%.+}}, posedge, {{%.+}}, 42, 1337 : !ltl.sequence
+ltl.delay %clk, posedge, %s, 0 : !ltl.sequence
+ltl.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..ddcb51c88f62 100644
--- a/test/Dialect/LTL/canonicalization.mlir
+++ b/test/Dialect/LTL/canonicalization.mlir
@@ -8,57 +8,59 @@ func.func private @Prop(%arg0: !ltl.property)
 func.func @DelayFolds(%arg0: !ltl.sequence, %arg1: i1) {
   // delay(s, 0, 0) -> s
   // delay(i, 0, 0) -> delay(i, 0, 0)
-  // CHECK-NEXT: ltl.delay %arg1, 0, 0 : i1
+  // CHECK-NEXT: {{%.*}} = hw.constant true
+  // CHECK-NEXT: ltl.delay {{%.*}}, posedge, %arg1, 0, 0 : i1
   // CHECK-NEXT: call @Seq(%arg0)
   // CHECK-NEXT: call @Seq({{%.+}})
-  %0 = ltl.delay %arg0, 0, 0 : !ltl.sequence
-  %n0 = ltl.delay %arg1, 0, 0 : i1
+  %clk = hw.constant true
+  %0 = ltl.delay %clk, posedge, %arg0, 0, 0 : !ltl.sequence
+  %n0 = ltl.delay %clk, posedge, %arg1, 0, 0 : i1
   call @Seq(%0) : (!ltl.sequence) -> ()
   call @Seq(%n0) : (!ltl.sequence) -> ()
 
   // delay(delay(s, 1), 2) -> delay(s, 3)
-  // CHECK-NEXT: ltl.delay %arg0, 3 :
+  // CHECK-NEXT: ltl.delay {{%.*}}, posedge, %arg0, 3 :
   // CHECK-NEXT: call
-  %1 = ltl.delay %arg0, 1 : !ltl.sequence
-  %2 = ltl.delay %1, 2 : !ltl.sequence
+  %1 = ltl.delay %clk, posedge, %arg0, 1 : !ltl.sequence
+  %2 = ltl.delay %clk, posedge, %1, 2 : !ltl.sequence
   call @Seq(%2) : (!ltl.sequence) -> ()
 
   // 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 {{%.*}}, posedge, {{%.+}}, 3 :
+  // CHECK-NEXT: ltl.delay {{%.*}}, posedge, {{%.+}}, 3 :
   // CHECK-NEXT: call
   // CHECK-NEXT: call
-  %3 = ltl.delay %arg0, 1, 0 : !ltl.sequence
-  %4 = ltl.delay %arg0, 1, 42 : !ltl.sequence
-  %5 = ltl.delay %3, 2 : !ltl.sequence
-  %6 = ltl.delay %4, 2 : !ltl.sequence
+  %3 = ltl.delay %clk, posedge, %arg0, 1, 0 : !ltl.sequence
+  %4 = ltl.delay %clk, posedge, %arg0, 1, 42 : !ltl.sequence
+  %5 = ltl.delay %clk, posedge, %3, 2 : !ltl.sequence
+  %6 = ltl.delay %clk, posedge, %4, 2 : !ltl.sequence
   call @Seq(%5) : (!ltl.sequence) -> ()
   call @Seq(%6) : (!ltl.sequence) -> ()
 
   // delay(delay(s, 1), 2, N) -> delay(s, 3)
   // N is dropped
-  // CHECK-NEXT: ltl.delay %arg0, 3 :
-  // CHECK-NEXT: ltl.delay %arg0, 3 :
+  // CHECK-NEXT: ltl.delay {{%.*}}, posedge, %arg0, 3 :
+  // CHECK-NEXT: ltl.delay {{%.*}}, posedge, %arg0, 3 :
   // CHECK-NEXT: call
   // CHECK-NEXT: call
-  %7 = ltl.delay %arg0, 1 : !ltl.sequence
-  %8 = ltl.delay %arg0, 1 : !ltl.sequence
-  %9 = ltl.delay %7, 2, 0 : !ltl.sequence
-  %10 = ltl.delay %8, 2, 42 : !ltl.sequence
+  %7 = ltl.delay %clk, posedge, %arg0, 1 : !ltl.sequence
+  %8 = ltl.delay %clk, posedge, %arg0, 1 : !ltl.sequence
+  %9 = ltl.delay %clk, posedge, %7, 2, 0 : !ltl.sequence
+  %10 = ltl.delay %clk, posedge, %8, 2, 42 : !ltl.sequence
   call @Seq(%9) : (!ltl.sequence) -> ()
   call @Seq(%10) : (!ltl.sequence) -> ()
 
   // delay(delay(s, 1, 2), 3, 0) -> delay(s, 4, 2)
   // delay(delay(s, 1, 2), 3, 5) -> delay(s, 4, 7)
-  // CHECK-NEXT: ltl.delay %arg0, 4, 2 :
-  // CHECK-NEXT: ltl.delay %arg0, 4, 7 :
+  // CHECK-NEXT: ltl.delay {{%.*}}, posedge, %arg0, 4, 2 :
+  // CHECK-NEXT: ltl.delay {{%.*}}, posedge, %arg0, 4, 7 :
   // CHECK-NEXT: call
   // CHECK-NEXT: call
-  %11 = ltl.delay %arg0, 1, 2 : !ltl.sequence
-  %12 = ltl.delay %arg0, 1, 2 : !ltl.sequence
-  %13 = ltl.delay %11, 3, 0 : !ltl.sequence
-  %14 = ltl.delay %12, 3, 5 : !ltl.sequence
+  %11 = ltl.delay %clk, posedge, %arg0, 1, 2 : !ltl.sequence
+  %12 = ltl.delay %clk, posedge, %arg0, 1, 2 : !ltl.sequence
+  %13 = ltl.delay %clk, posedge, %11, 3, 0 : !ltl.sequence
+  %14 = ltl.delay %clk, posedge, %12, 3, 5 : !ltl.sequence
   call @Seq(%13) : (!ltl.sequence) -> ()
   call @Seq(%14) : (!ltl.sequence) -> ()
   return
@@ -67,7 +69,9 @@ func.func @DelayFolds(%arg0: !ltl.sequence, %arg1: i1) {
 // CHECK-LABEL: @ConcatFolds
 func.func @ConcatFolds(%arg0: !ltl.sequence, %arg1: !ltl.sequence, %arg2: !ltl.sequence) {
   // concat(s) -> s
+  // CHECK-NEXT: {{%.*}} = hw.constant true
   // CHECK-NEXT: call @Seq(%arg0)
+  %clk = hw.constant true
   %0 = ltl.concat %arg0 : !ltl.sequence
   call @Seq(%0) : (!ltl.sequence) -> ()
 
@@ -90,11 +94,11 @@ func.func @ConcatFolds(%arg0: !ltl.sequence, %arg1: !ltl.sequence, %arg2: !ltl.s
   call @Seq(%5) : (!ltl.sequence) -> ()
 
   // delay(concat(s0, s1), N, M) -> concat(delay(s0, N, M), s1)
-  // CHECK-NEXT: [[TMP:%.+]] = ltl.delay %arg0, 2, 3 :
+  // CHECK-NEXT: [[TMP:%.+]] = ltl.delay {{%.*}}, posedge, %arg0, 2, 3 :
   // CHECK-NEXT: ltl.concat [[TMP]], %arg1 :
   // CHECK-NEXT: call
   %6 = ltl.concat %arg0, %arg1 : !ltl.sequence, !ltl.sequence
-  %7 = ltl.delay %6, 2, 3 : !ltl.sequence
+  %7 = ltl.delay %clk, posedge, %6, 2, 3 : !ltl.sequence
   call @Seq(%7) : (!ltl.sequence) -> ()
   return
 }