From ee686ffd57024888df150eb0ac8c21df462b44df Mon Sep 17 00:00:00 2001
From: Clo91eaf <Clo91eaf@qq.com>
Date: Mon, 29 Dec 2025 18:54:50 +0800
Subject: [PATCH 1/8] [LTL] Update delay syntax to include clock and edge
 specifications

---
 docs/Dialects/LTL.md       | 93 +++++++++++++++++++++++---------------
 docs/FormalVerification.md |  4 +-
 2 files changed, 58 insertions(+), 39 deletions(-)

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

From c6880078f302f0fa70272fc3f16e7b3d0a85c3ba Mon Sep 17 00:00:00 2001
From: Clo91eaf <Clo91eaf@qq.com>
Date: Mon, 29 Dec 2025 18:55:05 +0800
Subject: [PATCH 2/8] [LTL] Make ltl.delay clocking explicit

---
 include/circt/Dialect/LTL/LTLFolds.td         |  15 +-
 include/circt/Dialect/LTL/LTLOps.td           | 139 ++++++++++--------
 lib/Conversion/FIRRTLToHW/LowerToHW.cpp       |  10 +-
 .../ImportVerilog/AssertionExpr.cpp           |  62 ++++++--
 lib/Dialect/LTL/LTLFolds.cpp                  |   2 +-
 5 files changed, 140 insertions(+), 88 deletions(-)

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 c2fcbbf7668f..8f4490720a87 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();

From 9b034b5236dcc6337b9e44d119296ad85864f0cb Mon Sep 17 00:00:00 2001
From: Clo91eaf <Clo91eaf@qq.com>
Date: Mon, 29 Dec 2025 18:55:13 +0800
Subject: [PATCH 3/8] [LTL] Update delay operations tests

---
 .../ExportVerilog/prepare-for-emission.mlir   |  4 +-
 test/Conversion/ExportVerilog/verif.mlir      | 31 +++++-----
 test/Conversion/FIRRTLToHW/intrinsics.mlir    |  8 ++-
 test/Conversion/ImportVerilog/basic.sv        | 44 +++++++--------
 test/Dialect/LTL/basic.mlir                   |  9 +--
 test/Dialect/LTL/canonicalization.mlir        | 56 ++++++++++---------
 6 files changed, 80 insertions(+), 72 deletions(-)

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 33d5bcdd5a15..c4639aca3b9a 100644
--- a/test/Conversion/ImportVerilog/basic.sv
+++ b/test/Conversion/ImportVerilog/basic.sv
@@ -2446,23 +2446,23 @@ module ConcurrentAssert(input clk);
   // CHECK-NOT: 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 {{%.+}}, {{.*}}, [[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 {{%.+}}, {{.*}}, [[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
   assert property (a ##0 b);
   // CHECK-NOT: 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 {{%.+}}, {{.*}}, [[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 {{%.+}}, {{.*}}, [[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 {{%.+}}, {{.*}}, [[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
   assert property (a ##[+] b ##[3:5] a);
@@ -2495,13 +2495,13 @@ module ConcurrentAssert(input clk);
   // CHECK-NOT: 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 {{%.+}}, {{.*}}, [[CONV_A]], 1, 0 : i1
   // CHECK: verif.assert [[DELAY_OP]] : !ltl.sequence
   assert property (nexttime a);
   // CHECK-NOT: 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 {{%.+}}, {{.*}}, [[CONV_A]], 5, 0 : i1
   // CHECK: verif.assert [[DELAY_OP]] : !ltl.sequence
   assert property (nexttime [5] a);
 
@@ -2546,8 +2546,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 {{%.+}}, {{.*}}, [[REPEAT_T]], 1, 0 : !ltl.sequence
+  // CHECK: [[DELAY_A:%.+]] = ltl.delay {{%.+}}, {{.*}}, [[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
@@ -2605,7 +2605,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 {{%.+}}, {{.*}}, [[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
@@ -2627,7 +2627,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 {{%.+}}, {{.*}}, [[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
@@ -2648,10 +2648,10 @@ module ConcurrentAssert(input clk);
   // CHECK-NOT: 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 {{%.+}}, {{.*}}, [[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 {{%.+}}, {{.*}}, [[B]], 1, 0 : i1
   // CHECK: [[RES:%.+]] = ltl.concat [[DA]], [[DB]] : !ltl.sequence, !ltl.sequence
   // CHECK: verif.assert [[RES]] : !ltl.sequence
   sequence s1;
@@ -2666,8 +2666,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 {{%.+}}, {{.*}}, [[OP1]], 1, 0 : !ltl.sequence
+  // CHECK: [[OP3:%.+]] = ltl.delay {{%.+}}, {{.*}}, [[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
@@ -2679,10 +2679,10 @@ module ConcurrentAssert(input clk);
   // CHECK-NOT: 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 {{%.+}}, {{.*}}, [[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 {{%.+}}, {{.*}}, [[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
@@ -2702,8 +2702,8 @@ 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 {{%.+}}, {{.*}}, [[OP1]], 1, 0 : !ltl.sequence
+  // CHECK: [[OP3:%.+]] = ltl.delay {{%.+}}, {{.*}}, [[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
@@ -2714,16 +2714,16 @@ module ConcurrentAssert(input clk);
   // CHECK: [[OP10:%.+]] = ltl.intersect [[OP9]], [[OP5]] : !ltl.sequence, !ltl.sequence
   // CHECK: [[TMP:%.+]] = moore.read %a : <i1>
   // CHECK: [[A3:%.+]] = moore.to_builtin_bool [[TMP]] : i1
-  // CHECK: [[DA3:%.+]] = ltl.delay [[A3]], 0, 0 : i1
+  // CHECK: [[DA3:%.+]] = ltl.delay {{%.+}}, {{.*}}, [[A3]], 0, 0 : i1
   // CHECK: [[TMP:%.+]] = moore.read %b : <l1>
   // CHECK: [[B2:%.+]] = moore.to_builtin_bool [[TMP]] : l1
-  // CHECK: [[DB2:%.+]] = ltl.delay [[B2]], 1, 0 : i1
+  // CHECK: [[DB2:%.+]] = ltl.delay {{%.+}}, {{.*}}, [[B2]], 1, 0 : i1
   // CHECK: [[OP11:%.+]] = ltl.concat [[DA3]], [[DB2]] : !ltl.sequence, !ltl.sequence
   // CHECK: [[TMP:%.+]] = moore.read %b : <l1>
   // CHECK: [[B3:%.+]] = moore.to_builtin_bool [[TMP]] : l1
   // CHECK: [[OP12:%.+]] = ltl.implication [[OP11]], [[B3]] : !ltl.sequence, i1
   // CHECK: [[TRUE2:%.+]] = hw.constant true
-  // CHECK: [[OP13:%.+]] = ltl.delay [[OP10]], 1, 0 : !ltl.sequence
+  // CHECK: [[OP13:%.+]] = ltl.delay {{%.+}}, {{.*}}, [[OP10]], 1, 0 : !ltl.sequence
   // CHECK: [[OP14:%.+]] = ltl.concat [[OP13]], [[TRUE2]] : !ltl.sequence, i1
   // CHECK: [[RES:%.+]] = ltl.implication [[OP14]], [[OP12]] : !ltl.sequence, !ltl.property
   // CHECK: verif.assert [[RES]] : !ltl.property
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
 }

From 6b22cb3c9472a06d0a1193675387aaa1d6c870d4 Mon Sep 17 00:00:00 2001
From: Clo91eaf <Clo91eaf@qq.com>
Date: Wed, 21 Jan 2026 14:37:08 +0800
Subject: [PATCH 4/8] [ImportVerilog] Propagate clock context to ltl.delay in
 assertions

Previously, ltl.delay operations inside ClockingAssertionExpr (e.g.,
`@(posedge clk) a ##1 b`) used a dummy constant clock instead of the
actual clock from the timing control. This produced semantically
incorrect IR where delays would never trigger.

This patch adds clock context propagation to AssertionExprVisitor:
- Add `clockContext` field to store clock value and edge
- Add `getClockForDelay()` helper to retrieve clock for delay ops
- Extract clock from SignalEventControl before converting inner expr
- Pass clock context to inner visitor for recursive conversion

Now `@(posedge clk) a ##1 b` correctly generates:
  %d = ltl.delay %clk, posedge, %a, 1, 0 : i1
instead of:
  %d = ltl.delay %true, posedge, %a, 1, 0 : i1
---
 .../ImportVerilog/AssertionExpr.cpp           | 88 ++++++++++---------
 .../ImportVerilog/ImportVerilogInternals.h    |  3 +
 .../ImportVerilog/TimingControls.cpp          |  2 +-
 3 files changed, 52 insertions(+), 41 deletions(-)

diff --git a/lib/Conversion/ImportVerilog/AssertionExpr.cpp b/lib/Conversion/ImportVerilog/AssertionExpr.cpp
index 20e044c1bd21..8c0896e41bc8 100644
--- a/lib/Conversion/ImportVerilog/AssertionExpr.cpp
+++ b/lib/Conversion/ImportVerilog/AssertionExpr.cpp
@@ -28,8 +28,28 @@ struct AssertionExprVisitor {
   Location loc;
   OpBuilder &builder;
 
-  AssertionExprVisitor(Context &context, Location loc)
-      : context(context), loc(loc), builder(context.builder) {}
+  std::optional<std::pair<Value, ltl::ClockEdge>> clockContext;
+
+  AssertionExprVisitor(
+      Context &context, Location loc,
+      std::optional<std::pair<Value, ltl::ClockEdge>> clock = std::nullopt)
+      : context(context), loc(loc), builder(context.builder),
+        clockContext(clock) {}
+
+  std::pair<Value, ltl::ClockEdgeAttr> getClockForDelay() {
+    if (clockContext) {
+      auto edgeAttr =
+          ltl::ClockEdgeAttr::get(builder.getContext(), clockContext->second);
+      return {clockContext->first, edgeAttr};
+    }
+    // Fallback to dummy constant when no clock context available.
+    auto dummyClock =
+        hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1)
+            .getResult();
+    auto dummyEdge =
+        ltl::ClockEdgeAttr::get(builder.getContext(), ltl::ClockEdge::Pos);
+    return {dummyClock, dummyEdge};
+  }
 
   /// Helper to convert a range (min, optional max) to MLIR integer attributes
   std::pair<mlir::IntegerAttr, mlir::IntegerAttr>
@@ -121,13 +141,9 @@ struct AssertionExprVisitor {
 
       auto [delayMin, delayRange] =
           convertRangeToAttrs(concatElement.delay.min, concatElement.delay.max);
-      auto delayedClock =
-          hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1)
-              .getResult();
-      auto delayedEdge =
-          ltl::ClockEdgeAttr::get(builder.getContext(), ltl::ClockEdge::Pos);
+      auto [delayClock, delayEdge] = getClockForDelay();
       auto delayedSequence =
-          ltl::DelayOp::create(builder, loc, delayedClock, delayedEdge,
+          ltl::DelayOp::create(builder, loc, delayClock, delayEdge,
                                sequenceValue, delayMin, delayRange);
       sequenceElements.push_back(delayedSequence);
     }
@@ -165,10 +181,7 @@ struct AssertionExprVisitor {
       if (expr.range.has_value()) {
         minRepetitions = builder.getI64IntegerAttr(expr.range.value().min);
       }
-      auto clock = hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1)
-                       .getResult();
-      auto edge =
-          ltl::ClockEdgeAttr::get(builder.getContext(), ltl::ClockEdge::Pos);
+      auto [clock, edge] = getClockForDelay();
       return ltl::DelayOp::create(builder, loc, clock, edge, value,
                                   minRepetitions, builder.getI64IntegerAttr(0));
     }
@@ -208,21 +221,12 @@ struct AssertionExprVisitor {
       auto oneRepeat = ltl::RepeatOp::create(builder, loc, constOne,
                                              builder.getI64IntegerAttr(0),
                                              mlir::IntegerAttr{});
-      auto repeatClock =
-          hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1)
-              .getResult();
-      auto repeatEdge =
-          ltl::ClockEdgeAttr::get(builder.getContext(), ltl::ClockEdge::Pos);
+      auto [delayClock, delayEdge] = getClockForDelay();
       auto repeatDelay = ltl::DelayOp::create(
-          builder, loc, repeatClock, repeatEdge, oneRepeat,
+          builder, loc, delayClock, delayEdge, 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),
+      auto lhsDelay = ltl::DelayOp::create(builder, loc, delayClock, delayEdge,
+                                           lhs, builder.getI64IntegerAttr(1),
                                            builder.getI64IntegerAttr(0));
       auto combined = ltl::ConcatOp::create(
           builder, loc, SmallVector<Value, 3>{repeatDelay, lhsDelay, constOne});
@@ -255,13 +259,9 @@ struct AssertionExprVisitor {
     case BinaryAssertionOperator::NonOverlappedImplication: {
       auto constOne =
           hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1);
-      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),
+      auto [delayClock, delayEdge] = getClockForDelay();
+      auto lhsDelay = ltl::DelayOp::create(builder, loc, delayClock, delayEdge,
+                                           lhs, builder.getI64IntegerAttr(1),
                                            builder.getI64IntegerAttr(0));
       auto antecedent = ltl::ConcatOp::create(
           builder, loc, SmallVector<Value, 2>{lhsDelay, constOne});
@@ -278,13 +278,9 @@ struct AssertionExprVisitor {
       auto constOne =
           hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1);
       auto notRhs = ltl::NotOp::create(builder, loc, rhs);
-      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),
+      auto [delayClock, delayEdge] = getClockForDelay();
+      auto lhsDelay = ltl::DelayOp::create(builder, loc, delayClock, delayEdge,
+                                           lhs, builder.getI64IntegerAttr(1),
                                            builder.getI64IntegerAttr(0));
       auto antecedent = ltl::ConcatOp::create(
           builder, loc, SmallVector<Value, 2>{lhsDelay, constOne});
@@ -302,7 +298,19 @@ struct AssertionExprVisitor {
   }
 
   Value visit(const slang::ast::ClockingAssertionExpr &expr) {
-    auto assertionExpr = context.convertAssertionExpression(expr.expr, loc);
+    std::optional<std::pair<Value, ltl::ClockEdge>> extractedClock;
+    if (auto *sec = expr.clocking.as<slang::ast::SignalEventControl>()) {
+      auto clockExpr = context.convertRvalueExpression(sec->expr);
+      if (!clockExpr)
+        return {};
+      clockExpr = context.convertToI1(clockExpr);
+      if (!clockExpr)
+        return {};
+      extractedClock = {clockExpr, convertEdgeKindLTL(sec->edge)};
+    }
+
+    AssertionExprVisitor innerVisitor{context, loc, extractedClock};
+    auto assertionExpr = expr.expr.visit(innerVisitor);
     if (!assertionExpr)
       return {};
     return context.convertLTLTimingControl(expr.clocking, assertionExpr);
diff --git a/lib/Conversion/ImportVerilog/ImportVerilogInternals.h b/lib/Conversion/ImportVerilog/ImportVerilogInternals.h
index c692a3075c51..1c3b56736aef 100644
--- a/lib/Conversion/ImportVerilog/ImportVerilogInternals.h
+++ b/lib/Conversion/ImportVerilog/ImportVerilogInternals.h
@@ -31,6 +31,9 @@ namespace ImportVerilog {
 
 using moore::Domain;
 
+/// Convert Slang edge kind to LTL dialect clock edge.
+ltl::ClockEdge convertEdgeKindLTL(slang::ast::EdgeKind edge);
+
 /// Port lowering information.
 struct PortLowering {
   const slang::ast::PortSymbol &ast;
diff --git a/lib/Conversion/ImportVerilog/TimingControls.cpp b/lib/Conversion/ImportVerilog/TimingControls.cpp
index 2458cbfa8a8a..04bc75aa0891 100644
--- a/lib/Conversion/ImportVerilog/TimingControls.cpp
+++ b/lib/Conversion/ImportVerilog/TimingControls.cpp
@@ -13,7 +13,7 @@
 using namespace circt;
 using namespace ImportVerilog;
 
-static ltl::ClockEdge convertEdgeKindLTL(const slang::ast::EdgeKind edge) {
+ltl::ClockEdge convertEdgeKindLTL(const slang::ast::EdgeKind edge) {
   using slang::ast::EdgeKind;
   switch (edge) {
   case EdgeKind::NegEdge:

From b90c341a54d7044788bf62b372ef5e30db1bf9cc Mon Sep 17 00:00:00 2001
From: Clo91eaf <Clo91eaf@qq.com>
Date: Wed, 21 Jan 2026 14:49:17 +0800
Subject: [PATCH 5/8] [ImportVerilog] Add clock propagation to ltl.delay in
 ConcurrentAssert module test

---
 test/Conversion/ImportVerilog/basic.sv | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/test/Conversion/ImportVerilog/basic.sv b/test/Conversion/ImportVerilog/basic.sv
index c4639aca3b9a..c22699d9c3ff 100644
--- a/test/Conversion/ImportVerilog/basic.sv
+++ b/test/Conversion/ImportVerilog/basic.sv
@@ -2644,6 +2644,23 @@ module ConcurrentAssert(input clk);
   // CHECK: verif.assert [[CLK_OP]] : !ltl.sequence
   assert property (@(posedge clk) a);
 
+  // Clocking with delay - clock should propagate to ltl.delay
+  // CHECK: moore.procedure always
+    // CHECK: [[READ_CLK2:%.+]] = moore.read [[CLK]] : <l1>
+    // CHECK: [[CONV_CLK2:%.+]] = moore.to_builtin_bool [[READ_CLK2]] : l1
+    // CHECK: [[READ_A2:%.+]] = moore.read [[A]] : <i1>
+    // CHECK: [[CONV_A2:%.+]] = moore.to_builtin_bool [[READ_A2]] : i1
+    // CHECK: [[DELAY_A2:%.+]] = ltl.delay [[CONV_CLK2]], posedge, [[CONV_A2]], 0, 0 : i1
+    // CHECK: [[READ_B2:%.+]] = moore.read [[B]] : <l1>
+    // CHECK: [[CONV_B2:%.+]] = moore.to_builtin_bool [[READ_B2]] : l1
+    // CHECK: [[DELAY_B2:%.+]] = ltl.delay [[CONV_CLK2]], posedge, [[CONV_B2]], 1 : i1
+    // CHECK: [[CONCAT2:%.+]] = ltl.concat [[DELAY_A2]], [[DELAY_B2]] : !ltl.sequence, !ltl.sequence
+    // CHECK: [[CLK_OP2:%.+]] = ltl.clock [[CONCAT2]], posedge [[CONV_CLK2]] : !ltl.sequence
+    // CHECK: verif.assert [[CLK_OP2]] : !ltl.sequence
+    // CHECK: moore.return
+  // CHECK: }
+  assert property (@(posedge clk) a ##1 b);
+
   // Sequence declaration
   // CHECK-NOT: moore.procedure always {
   // CHECK: [[TMP:%.+]] = moore.read %a : <i1>

From 8647983acecc2cca61fb73785d64ab2b8ca12da0 Mon Sep 17 00:00:00 2001
From: Clo91eaf <Clo91eaf@qq.com>
Date: Wed, 21 Jan 2026 15:01:35 +0800
Subject: [PATCH 6/8] [ExportVerilog] Fix Precedence module to include clock
 input for ltl.delay operations

---
 test/Conversion/ExportVerilog/verif.mlir | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/test/Conversion/ExportVerilog/verif.mlir b/test/Conversion/ExportVerilog/verif.mlir
index baf05f914b13..17b1b498fadd 100644
--- a/test/Conversion/ExportVerilog/verif.mlir
+++ b/test/Conversion/ExportVerilog/verif.mlir
@@ -210,16 +210,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
+hw.module @Precedence(in %clk: i1, in %a: i1, in %b: i1) {
   // CHECK: assert property ((a or ##0 b) and b);
-  %a0 = ltl.delay %true, posedge, %b, 0, 0 : i1
+  %a0 = ltl.delay %clk, 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 %true, posedge, %a1, 1, 0 : !ltl.sequence
+  %d0 = ltl.delay %clk, posedge, %a1, 1, 0 : !ltl.sequence
   sv.assert_property %d0 : !ltl.sequence
 
   // CHECK: assert property (not (a or ##0 b));

From e2632c2234d7b12d6d567c6637a6565eb9f2e909 Mon Sep 17 00:00:00 2001
From: Clo91eaf <Clo91eaf@qq.com>
Date: Thu, 22 Jan 2026 16:14:37 +0800
Subject: [PATCH 7/8] [LTL] Add InferLTLClocks pass to propagate clock from
 ltl.clock to ltl.delay

After FIRRTLToHW lowering, ltl.delay operations have placeholder clocks
because FIRRTL's delay intrinsic doesn't carry clock information.

Three approaches were considered:
A) Delayed lowering at ClockIntrinsicOp - complex, breaks lowering pattern
B) Two-pass scanning - extra overhead, complex use-def tracking
C) Post-processing pass - minimal changes, independent, testable

Chose C for minimal disruption and incremental implementation.

The new pass walks ltl.clock ops, finds ltl.delay ops with placeholder
clocks in their input chains, and replaces them with properly clocked
versions.
---
 include/circt/Dialect/LTL/CMakeLists.txt      |   5 +
 include/circt/Dialect/LTL/LTLPasses.h         |  32 +++
 include/circt/Dialect/LTL/LTLPasses.td        |  47 ++++
 include/circt/InitAllPasses.h                 |   2 +
 lib/Dialect/LTL/CMakeLists.txt                |   2 +
 lib/Dialect/LTL/Transforms/CMakeLists.txt     |  13 +
 lib/Dialect/LTL/Transforms/InferLTLClocks.cpp | 243 ++++++++++++++++++
 test/Dialect/LTL/infer-clocks.mlir            | 122 +++++++++
 8 files changed, 466 insertions(+)
 create mode 100644 include/circt/Dialect/LTL/LTLPasses.h
 create mode 100644 include/circt/Dialect/LTL/LTLPasses.td
 create mode 100644 lib/Dialect/LTL/Transforms/CMakeLists.txt
 create mode 100644 lib/Dialect/LTL/Transforms/InferLTLClocks.cpp
 create mode 100644 test/Dialect/LTL/infer-clocks.mlir

diff --git a/include/circt/Dialect/LTL/CMakeLists.txt b/include/circt/Dialect/LTL/CMakeLists.txt
index 682fb0474604..c661ba01ab0b 100644
--- a/include/circt/Dialect/LTL/CMakeLists.txt
+++ b/include/circt/Dialect/LTL/CMakeLists.txt
@@ -11,3 +11,8 @@ add_dependencies(circt-headers CIRCTLTLEnumsIncGen)
 mlir_tablegen(LTLFolds.cpp.inc -gen-rewriters)
 add_public_tablegen_target(CIRCTLTLFoldsIncGen)
 add_dependencies(circt-headers CIRCTLTLFoldsIncGen)
+
+set(LLVM_TARGET_DEFINITIONS LTLPasses.td)
+mlir_tablegen(LTLPasses.h.inc -gen-pass-decls)
+add_public_tablegen_target(CIRCTLTLTransformsIncGen)
+add_dependencies(circt-headers CIRCTLTLTransformsIncGen)
diff --git a/include/circt/Dialect/LTL/LTLPasses.h b/include/circt/Dialect/LTL/LTLPasses.h
new file mode 100644
index 000000000000..1b79e3148a23
--- /dev/null
+++ b/include/circt/Dialect/LTL/LTLPasses.h
@@ -0,0 +1,32 @@
+//===- LTLPasses.h - LTL pass entry points ----------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This header file defines prototypes that expose pass constructors.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_LTL_LTLPASSES_H
+#define CIRCT_DIALECT_LTL_LTLPASSES_H
+
+#include "mlir/Pass/Pass.h"
+#include "mlir/Pass/PassRegistry.h"
+
+namespace circt {
+namespace ltl {
+
+#define GEN_PASS_DECL
+#include "circt/Dialect/LTL/LTLPasses.h.inc"
+
+/// Generate the code for registering passes.
+#define GEN_PASS_REGISTRATION
+#include "circt/Dialect/LTL/LTLPasses.h.inc"
+
+} // namespace ltl
+} // namespace circt
+
+#endif // CIRCT_DIALECT_LTL_LTLPASSES_H
diff --git a/include/circt/Dialect/LTL/LTLPasses.td b/include/circt/Dialect/LTL/LTLPasses.td
new file mode 100644
index 000000000000..28b1d01d8d4a
--- /dev/null
+++ b/include/circt/Dialect/LTL/LTLPasses.td
@@ -0,0 +1,47 @@
+//===-- Passes.td - LTL pass definition file ---------------*- tablegen -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines the passes that work on the LTL dialect.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_LTL_PASSES_TD
+#define CIRCT_DIALECT_LTL_PASSES_TD
+
+include "mlir/Pass/PassBase.td"
+
+def InferLTLClocks : Pass<"ltl-infer-clocks", "hw::HWModuleOp"> {
+  let summary =
+      "Infer clock for ltl.delay operations from surrounding ltl.clock ops";
+  let description = [{
+    This pass propagates clock information from `ltl.clock` operations down
+    to `ltl.delay` operations in their input chains. After FIRRTLToHW lowering,
+    `ltl.delay` operations may have placeholder clocks (constant true) because
+    the FIRRTL delay intrinsic doesn't carry explicit clock information.
+    
+    This pass walks through each `ltl.clock` operation, finds all `ltl.delay`
+    operations in its input chain that have placeholder clocks, and replaces
+    them with correctly clocked versions using the clock from the enclosing
+    `ltl.clock` operation.
+    
+    Example transformation:
+    ```mlir
+    // Before:
+    %true = hw.constant true
+    %d = ltl.delay %true, posedge, %a, 1, 0 : i1
+    %p = ltl.clock %d, posedge %clk : !ltl.sequence
+    
+    // After:
+    %d = ltl.delay %clk, posedge, %a, 1, 0 : i1
+    %p = ltl.clock %d, posedge %clk : !ltl.sequence
+    ```
+  }];
+  let dependentDialects = ["hw::HWDialect", "ltl::LTLDialect"];
+}
+
+#endif // CIRCT_DIALECT_LTL_PASSES_TD
diff --git a/include/circt/InitAllPasses.h b/include/circt/InitAllPasses.h
index eba575f01118..c347033d7bec 100644
--- a/include/circt/InitAllPasses.h
+++ b/include/circt/InitAllPasses.h
@@ -29,6 +29,7 @@
 #include "circt/Dialect/Handshake/HandshakePasses.h"
 #include "circt/Dialect/Kanagawa/KanagawaPasses.h"
 #include "circt/Dialect/LLHD/Transforms/LLHDPasses.h"
+#include "circt/Dialect/LTL/LTLPasses.h"
 #include "circt/Dialect/MSFT/MSFTPasses.h"
 #include "circt/Dialect/Moore/MoorePasses.h"
 #include "circt/Dialect/OM/OMPasses.h"
@@ -76,6 +77,7 @@ inline void registerAllPasses() {
   hw::registerPasses();
   kanagawa::registerPasses();
   llhd::registerPasses();
+  ltl::registerPasses();
   moore::registerPasses();
   msft::registerPasses();
   om::registerPasses();
diff --git a/lib/Dialect/LTL/CMakeLists.txt b/lib/Dialect/LTL/CMakeLists.txt
index 466fe64433b8..a4c5bd53a731 100644
--- a/lib/Dialect/LTL/CMakeLists.txt
+++ b/lib/Dialect/LTL/CMakeLists.txt
@@ -19,3 +19,5 @@ add_circt_dialect_library(CIRCTLTL
   MLIRIR
   MLIRInferTypeOpInterface
 )
+
+add_subdirectory(Transforms)
diff --git a/lib/Dialect/LTL/Transforms/CMakeLists.txt b/lib/Dialect/LTL/Transforms/CMakeLists.txt
new file mode 100644
index 000000000000..d6a3aae51dd3
--- /dev/null
+++ b/lib/Dialect/LTL/Transforms/CMakeLists.txt
@@ -0,0 +1,13 @@
+add_circt_dialect_library(CIRCTLTLTransforms
+  InferLTLClocks.cpp
+
+  DEPENDS
+  CIRCTLTLTransformsIncGen
+
+  LINK_LIBS PUBLIC
+  CIRCTLTL
+  CIRCTHW
+  MLIRIR
+  MLIRPass
+  MLIRTransformUtils
+)
diff --git a/lib/Dialect/LTL/Transforms/InferLTLClocks.cpp b/lib/Dialect/LTL/Transforms/InferLTLClocks.cpp
new file mode 100644
index 000000000000..ba81cc66d5af
--- /dev/null
+++ b/lib/Dialect/LTL/Transforms/InferLTLClocks.cpp
@@ -0,0 +1,243 @@
+//===- InferLTLClocks.cpp - Infer clocks for ltl.delay ops ------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This pass propagates clock information from ltl.clock operations down to
+// ltl.delay operations that have placeholder clocks.
+//
+// When a single delay is used by multiple clock ops with different clocks,
+// this pass creates separate copies of the delay (and its upstream chain)
+// for each clock, ensuring each clock op gets a correctly clocked version.
+//
+//===----------------------------------------------------------------------===//
+
+#include "circt/Dialect/HW/HWOps.h"
+#include "circt/Dialect/LTL/LTLOps.h"
+#include "circt/Dialect/LTL/LTLPasses.h"
+#include "mlir/IR/IRMapping.h"
+#include "mlir/Pass/Pass.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseSet.h"
+#include "llvm/ADT/SmallVector.h"
+
+namespace circt {
+namespace ltl {
+#define GEN_PASS_DEF_INFERLTLCLOCKS
+#include "circt/Dialect/LTL/LTLPasses.h.inc"
+} // namespace ltl
+} // namespace circt
+
+using namespace circt;
+using namespace ltl;
+using namespace hw;
+
+namespace {
+
+/// Check if a value is a placeholder clock (hw.constant true).
+///
+/// We use `hw.constant true` as a placeholder because it is semantically
+/// invalid as a real clock: a constant-high signal has no edges (no 0→1 or
+/// 1→0 transitions), so there are no sampling points and "clock cycles"
+/// cannot be defined. No legitimate hardware design would use a constant
+/// as a clock signal for sequential timing.
+static bool isPlaceholderClock(Value clock) {
+  if (auto constOp = clock.getDefiningOp<hw::ConstantOp>()) {
+    // Check if it's a 1-bit constant with value 1 (true)
+    auto value = constOp.getValue();
+    return value.getBitWidth() == 1 && value.isOne();
+  }
+  return false;
+}
+
+/// Check if a subtree (rooted at value) contains any placeholder delays.
+static bool hasPlaceholderDelays(Value value, DenseSet<Operation *> &visited) {
+  Operation *defOp = value.getDefiningOp();
+  if (!defOp || visited.contains(defOp))
+    return false;
+  visited.insert(defOp);
+
+  if (auto delayOp = dyn_cast<DelayOp>(defOp)) {
+    if (isPlaceholderClock(delayOp.getClock()))
+      return true;
+    return hasPlaceholderDelays(delayOp.getInput(), visited);
+  }
+
+  // For clock ops, don't traverse into the clock signal itself
+  if (auto clockOp = dyn_cast<ClockOp>(defOp)) {
+    return hasPlaceholderDelays(clockOp.getInput(), visited);
+  }
+
+  for (Value operand : defOp->getOperands()) {
+    if (hasPlaceholderDelays(operand, visited))
+      return true;
+  }
+  return false;
+}
+
+/// Recursively clone/update a value's subtree, replacing placeholder delays
+/// with properly clocked versions. Returns the new value (may be the same
+/// if no changes needed).
+static Value cloneWithClock(Value value, Value clock, ClockEdge edge,
+                            OpBuilder &builder, IRMapping &mapping,
+                            DenseSet<Operation *> &visited) {
+  // If already mapped, return the mapped value
+  if (Value mapped = mapping.lookupOrNull(value))
+    return mapped;
+
+  // If it's a block argument or has no defining op, return as-is
+  Operation *defOp = value.getDefiningOp();
+  if (!defOp) {
+    mapping.map(value, value);
+    return value;
+  }
+
+  // If already visited (cycle detection), return mapped or original
+  if (visited.contains(defOp)) {
+    if (Value mapped = mapping.lookupOrNull(value))
+      return mapped;
+    return value;
+  }
+  visited.insert(defOp);
+
+  // Handle DelayOp specially
+  if (auto delayOp = dyn_cast<DelayOp>(defOp)) {
+    // First, recursively process the input
+    Value newInput = cloneWithClock(delayOp.getInput(), clock, edge, builder,
+                                    mapping, visited);
+
+    if (isPlaceholderClock(delayOp.getClock())) {
+      // Create a new delay with the correct clock
+      builder.setInsertionPointAfter(defOp);
+      auto newDelay = DelayOp::create(
+          builder, delayOp.getLoc(), clock,
+          ClockEdgeAttr::get(builder.getContext(), edge), newInput,
+          delayOp.getDelayAttr(), delayOp.getLengthAttr());
+      mapping.map(value, newDelay.getResult());
+      return newDelay.getResult();
+    } else if (newInput != delayOp.getInput()) {
+      // Input changed but clock is not placeholder - clone with new input
+      builder.setInsertionPointAfter(defOp);
+      auto newDelay = DelayOp::create(
+          builder, delayOp.getLoc(), delayOp.getClock(), delayOp.getEdgeAttr(),
+          newInput, delayOp.getDelayAttr(), delayOp.getLengthAttr());
+      mapping.map(value, newDelay.getResult());
+      return newDelay.getResult();
+    } else {
+      // No changes needed
+      mapping.map(value, value);
+      return value;
+    }
+  }
+
+  // Handle ClockOp - don't traverse into clock signal, only input
+  if (auto clockOp = dyn_cast<ClockOp>(defOp)) {
+    Value newInput = cloneWithClock(clockOp.getInput(), clock, edge, builder,
+                                    mapping, visited);
+    if (newInput != clockOp.getInput()) {
+      builder.setInsertionPointAfter(defOp);
+      auto newClockOp = ClockOp::create(builder, clockOp.getLoc(), newInput,
+                                        clockOp.getEdge(), clockOp.getClock());
+      mapping.map(value, newClockOp.getResult());
+      return newClockOp.getResult();
+    }
+    mapping.map(value, value);
+    return value;
+  }
+
+  // For other ops, check if any operand needs updating
+  SmallVector<Value> newOperands;
+  bool anyChanged = false;
+  for (Value operand : defOp->getOperands()) {
+    Value newOperand =
+        cloneWithClock(operand, clock, edge, builder, mapping, visited);
+    newOperands.push_back(newOperand);
+    if (newOperand != operand)
+      anyChanged = true;
+  }
+
+  if (!anyChanged) {
+    mapping.map(value, value);
+    return value;
+  }
+
+  // Clone the operation with new operands
+  builder.setInsertionPointAfter(defOp);
+  Operation *newOp = builder.clone(*defOp, mapping);
+  // Update operands (clone uses mapping, but let's be explicit)
+  for (auto [idx, newOperand] : llvm::enumerate(newOperands)) {
+    newOp->setOperand(idx, newOperand);
+  }
+
+  Value newResult = newOp->getResult(0);
+  mapping.map(value, newResult);
+  return newResult;
+}
+
+struct InferLTLClocksPass
+    : public circt::ltl::impl::InferLTLClocksBase<InferLTLClocksPass> {
+  void runOnOperation() override;
+};
+
+} // namespace
+
+void InferLTLClocksPass::runOnOperation() {
+  auto module = getOperation();
+  OpBuilder builder(module.getContext());
+  bool changed = false;
+
+  // Collect all clock ops first to avoid iterator invalidation
+  SmallVector<ClockOp> clockOps;
+  module.walk([&](ClockOp clockOp) { clockOps.push_back(clockOp); });
+
+  for (ClockOp clockOp : clockOps) {
+    // Check if this clock op's input subtree has any placeholder delays
+    DenseSet<Operation *> checkVisited;
+    if (!hasPlaceholderDelays(clockOp.getInput(), checkVisited))
+      continue;
+
+    Value clock = clockOp.getClock();
+    ClockEdge edge = clockOp.getEdge();
+
+    // Clone/update the input subtree with the correct clock
+    IRMapping mapping;
+    DenseSet<Operation *> visited;
+    Value newInput = cloneWithClock(clockOp.getInput(), clock, edge, builder,
+                                    mapping, visited);
+
+    if (newInput != clockOp.getInput()) {
+      clockOp.getInputMutable().assign(newInput);
+      changed = true;
+    }
+  }
+
+  // Clean up dead operations (original delays that are no longer used)
+  // We need to iterate until fixpoint because deleting an op may make its
+  // operands dead.
+  if (changed) {
+    bool erased = true;
+    while (erased) {
+      erased = false;
+      SmallVector<Operation *> toErase;
+      module.walk([&](Operation *op) {
+        // Only clean up LTL ops that have no uses
+        if (isa<DelayOp, ConcatOp, AndOp, OrOp, IntersectOp, RepeatOp,
+                GoToRepeatOp, NonConsecutiveRepeatOp, NotOp, ImplicationOp,
+                UntilOp, EventuallyOp>(op)) {
+          if (op->use_empty())
+            toErase.push_back(op);
+        }
+      });
+      for (Operation *op : llvm::reverse(toErase)) {
+        op->erase();
+        erased = true;
+      }
+    }
+  }
+
+  if (!changed)
+    markAllAnalysesPreserved();
+}
diff --git a/test/Dialect/LTL/infer-clocks.mlir b/test/Dialect/LTL/infer-clocks.mlir
new file mode 100644
index 000000000000..a84df32bb12a
--- /dev/null
+++ b/test/Dialect/LTL/infer-clocks.mlir
@@ -0,0 +1,122 @@
+// RUN: circt-opt %s --ltl-infer-clocks | FileCheck %s
+
+// CHECK-LABEL: hw.module @InferClockFromClockOp
+hw.module @InferClockFromClockOp(in %clk: i1, in %a: i1, in %b: i1) {
+  %true = hw.constant true
+  
+  // Before: delay uses placeholder clock (%true)
+  // After: delay should use %clk from the enclosing ltl.clock
+  
+  // CHECK: [[DELAY:%.+]] = ltl.delay %clk, posedge, %a, 1, 0 : i1
+  // CHECK-NOT: ltl.delay %true
+  %d = ltl.delay %true, posedge, %a, 1, 0 : i1
+  
+  // CHECK: ltl.clock [[DELAY]], posedge %clk
+  %p = ltl.clock %d, posedge %clk : !ltl.sequence
+  
+  sv.assert_property %p : !ltl.sequence
+}
+
+// CHECK-LABEL: hw.module @InferClockNested
+hw.module @InferClockNested(in %clk: i1, in %a: i1, in %b: i1) {
+  %true = hw.constant true
+  
+  // Multiple delays in a chain should all get the clock
+  // CHECK: [[D1:%.+]] = ltl.delay %clk, posedge, %a, 1, 0 : i1
+  %d1 = ltl.delay %true, posedge, %a, 1, 0 : i1
+  
+  // CHECK: [[D2:%.+]] = ltl.delay %clk, posedge, %b, 2, 0 : i1
+  %d2 = ltl.delay %true, posedge, %b, 2, 0 : i1
+  
+  // CHECK: [[CONCAT:%.+]] = ltl.concat [[D1]], [[D2]]
+  %c = ltl.concat %d1, %d2 : !ltl.sequence, !ltl.sequence
+  
+  // CHECK: ltl.clock [[CONCAT]], posedge %clk
+  %p = ltl.clock %c, posedge %clk : !ltl.sequence
+  
+  sv.assert_property %p : !ltl.sequence
+}
+
+// CHECK-LABEL: hw.module @PreserveRealClock
+hw.module @PreserveRealClock(in %clk: i1, in %clk2: i1, in %a: i1) {
+  // Delay already has a real clock - should NOT be modified
+  // CHECK: [[DELAY:%.+]] = ltl.delay %clk2, posedge, %a, 1, 0 : i1
+  %d = ltl.delay %clk2, posedge, %a, 1, 0 : i1
+  
+  // The clock op has a different clock, but we don't change the delay
+  // because it already has a non-placeholder clock
+  // CHECK: ltl.clock [[DELAY]], posedge %clk
+  %p = ltl.clock %d, posedge %clk : !ltl.sequence
+  
+  sv.assert_property %p : !ltl.sequence
+}
+
+// CHECK-LABEL: hw.module @InferEdge
+hw.module @InferEdge(in %clk: i1, in %a: i1) {
+  %true = hw.constant true
+  
+  // The delay should get the edge from the clock op (negedge)
+  // CHECK: [[DELAY:%.+]] = ltl.delay %clk, negedge, %a, 1, 0 : i1
+  %d = ltl.delay %true, posedge, %a, 1, 0 : i1
+  
+  // CHECK: ltl.clock [[DELAY]], negedge %clk
+  %p = ltl.clock %d, negedge %clk : !ltl.sequence
+  
+  sv.assert_property %p : !ltl.sequence
+}
+
+// CHECK-LABEL: hw.module @NoClockOp
+hw.module @NoClockOp(in %a: i1) {
+  %true = hw.constant true
+  
+  // No clock op wrapping - delay keeps placeholder clock
+  // CHECK: ltl.delay %true, posedge, %a, 1, 0 : i1
+  %d = ltl.delay %true, posedge, %a, 1, 0 : i1
+  
+  sv.assert_property %d : !ltl.sequence
+}
+
+// CHECK-LABEL: hw.module @MultiClockSharedDelay
+// Test P2: A single delay used by multiple clock ops with different clocks
+// Each clock op should get its own copy of the delay with the correct clock
+hw.module @MultiClockSharedDelay(in %clk1: i1, in %clk2: i1, in %a: i1) {
+  %true = hw.constant true
+  
+  // Original delay with placeholder clock - used by two different clock ops
+  %d = ltl.delay %true, posedge, %a, 1, 0 : i1
+  
+  // CHECK-DAG: [[D1:%.+]] = ltl.delay %clk1, posedge, %a, 1, 0 : i1
+  // CHECK-DAG: [[D2:%.+]] = ltl.delay %clk2, negedge, %a, 1, 0 : i1
+  
+  // CHECK-DAG: [[P1:%.+]] = ltl.clock [[D1]], posedge %clk1
+  %p1 = ltl.clock %d, posedge %clk1 : !ltl.sequence
+  
+  // CHECK-DAG: [[P2:%.+]] = ltl.clock [[D2]], negedge %clk2
+  %p2 = ltl.clock %d, negedge %clk2 : !ltl.sequence
+  
+  sv.assert_property %p1 : !ltl.sequence
+  sv.assert_property %p2 : !ltl.sequence
+}
+
+// CHECK-LABEL: hw.module @MultiClockSharedChain
+// Test P2: A chain of ops used by multiple clock ops
+hw.module @MultiClockSharedChain(in %clk1: i1, in %clk2: i1, in %a: i1, in %b: i1) {
+  %true = hw.constant true
+  
+  // Shared chain: delay -> concat
+  %d1 = ltl.delay %true, posedge, %a, 1, 0 : i1
+  %d2 = ltl.delay %true, posedge, %b, 2, 0 : i1
+  %c = ltl.concat %d1, %d2 : !ltl.sequence, !ltl.sequence
+  
+  // Both clock ops use the same concat
+  // CHECK-DAG: ltl.delay %clk1, posedge, %a, 1, 0 : i1
+  // CHECK-DAG: ltl.delay %clk1, posedge, %b, 2, 0 : i1
+  // CHECK-DAG: ltl.delay %clk2, posedge, %a, 1, 0 : i1
+  // CHECK-DAG: ltl.delay %clk2, posedge, %b, 2, 0 : i1
+  
+  %p1 = ltl.clock %c, posedge %clk1 : !ltl.sequence
+  %p2 = ltl.clock %c, posedge %clk2 : !ltl.sequence
+  
+  sv.assert_property %p1 : !ltl.sequence
+  sv.assert_property %p2 : !ltl.sequence
+}

From 56b5c86b658decdb7ba7603dc8992c70c9ceba65 Mon Sep 17 00:00:00 2001
From: Clo91eaf <Clo91eaf@qq.com>
Date: Thu, 22 Jan 2026 16:28:28 +0800
Subject: [PATCH 8/8] [ExportVerilog] Enforce ltl.delay clock/edge match
 enclosing ltl.clock

Add validation so ltl.delay's clock and edge must match the enclosing ltl.clock,
as SVA only supports a single clock context for delays. Emit errors for mismatches. Placeholder clocks (hw.constant true) are allowed and inherit the outer clock.
---
 .../ExportVerilog/ExportVerilog.cpp           | 40 ++++++++++++++++++-
 1 file changed, 38 insertions(+), 2 deletions(-)

diff --git a/lib/Conversion/ExportVerilog/ExportVerilog.cpp b/lib/Conversion/ExportVerilog/ExportVerilog.cpp
index 8a5a50815557..d93ad5035681 100644
--- a/lib/Conversion/ExportVerilog/ExportVerilog.cpp
+++ b/lib/Conversion/ExportVerilog/ExportVerilog.cpp
@@ -2304,8 +2304,7 @@ class ExprEmitter : public EmitterBase,
 
   /// Emit braced list of values surrounded by `{` and `}`.
   void emitBracedList(ValueRange ops) {
-    return emitBracedList(
-        ops, [&]() { ps << "{"; }, [&]() { ps << "}"; });
+    return emitBracedList(ops, [&]() { ps << "{"; }, [&]() { ps << "}"; });
   }
 
   /// Print an APInt constant.
@@ -3603,6 +3602,12 @@ class PropertyEmitter : public EmitterBase,
   /// location information tracking.
   SmallPtrSetImpl<Operation *> &emittedOps;
 
+  /// Current clock context from enclosing ltl.clock op. Used to verify that
+  /// ltl.delay ops have consistent clocks, since SVA does not support
+  /// per-delay clocks.
+  Value currentClock;
+  std::optional<ltl::ClockEdge> currentEdge;
+
   /// Tokens buffered for inserting casts/parens after emitting children.
   SmallVector<Token> localTokens;
 
@@ -3752,6 +3757,26 @@ EmittedProperty PropertyEmitter::visitLTL(ltl::IntersectOp op) {
 }
 
 EmittedProperty PropertyEmitter::visitLTL(ltl::DelayOp op) {
+  // Verify that the delay's clock matches the enclosing clock context.
+  // SVA does not support per-delay clocks; all delays inherit from the
+  // enclosing @(edge clock) specification.
+  Value delayClock = op.getClock();
+  if (currentClock) {
+    // Check if delay has a real clock (not a placeholder constant)
+    bool isPlaceholder = false;
+    if (auto constOp = delayClock.getDefiningOp<hw::ConstantOp>()) {
+      auto value = constOp.getValue();
+      isPlaceholder = value.getBitWidth() == 1 && value.isOne();
+    }
+
+    if (!isPlaceholder && delayClock != currentClock) {
+      emitOpError(op, "delay clock does not match enclosing clock; "
+                      "SVA does not support per-delay clocks");
+    } else if (!isPlaceholder && currentEdge && op.getEdge() != *currentEdge) {
+      emitOpError(op, "delay clock edge does not match enclosing clock edge");
+    }
+  }
+
   ps << "##";
   if (auto length = op.getLength()) {
     if (*length == 0) {
@@ -3907,7 +3932,18 @@ EmittedProperty PropertyEmitter::visitLTL(ltl::ClockOp op) {
     ps << ")";
   });
   ps << PP::space;
+
+  // Set the clock context for nested property emission.
+  // Save and restore to handle nested clock ops correctly.
+  Value savedClock = currentClock;
+  auto savedEdge = currentEdge;
+  currentClock = op.getClock();
+  currentEdge = op.getEdge();
+
   emitNestedProperty(op.getInput(), PropertyPrecedence::Clocking);
+
+  currentClock = savedClock;
+  currentEdge = savedEdge;
   return {PropertyPrecedence::Clocking};
 }