[LTL] Update delay syntax to include clock and edge specifications

Author: Clo91eaf

docs/Dialects/LTL.md

@@ -160,6 +160,26 @@ Sequence and property expressions in SVAs can specify a clock with respect to wh
 - `@(negedge clk) seqOrProp`. **Trigger on high-to-low clock edge.** Equivalent to `ltl.clock %seqOrProp, negedge %clk`.
 - `@(edge clk) seqOrProp`. **Trigger on any clock edge.** Equivalent to `ltl.clock %seqOrProp, edge %clk`.
 
+#### Delay clocking
+
+`ltl.delay` takes the delayed input first, followed by the delay window. An optional clocking clause may be appended:
+
+```
+ltl.delay %input, <delay>[, <length>] [clock %clock, <edge>]
+```
+
+`%clock` is an optional `i1` value (e.g. a module clock); `<edge>` is `posedge`, `negedge`, or `edge`. When present, the `delay`/`length` are counted on the specified clock/edge. For example, `ltl.delay %s, 3 clock %clk, posedge` means `%s` must hold 3 cycles later on `%clk` rising edges. 
+
+When the clocking clause is omitted, the delay is unclocked and may be resolved by an enclosing `ltl.clock` or by the `InferLTLClocks` pass. `ltl.clock` globally associates a sequence/property with a clock/edge; using the same pair in `ltl.delay` keeps expressions in the same clocking domain.
+
+Examples:
+
+```mlir
+ltl.delay %s, 3
+ltl.delay %s, 3, 0
+ltl.delay %s, 3, 0 clock %clk, posedge
+```
+
 
 ### Disable Iff
 
@@ -273,13 +293,13 @@ where the `logic_to_int` conversion is only necessary if `%cond` is 4-valued.
 ```mlir
 %ds1 = ltl.delay %s1, 1
 %s1s2 = ltl.concat %ds1, %s2 : !ltl.sequence  
-```  
+```
 
 - **`s1 ##[*] s2`**:   
 ```mlir
 %ds1 = ltl.delay %s1, 0
 %s1s2 = ltl.concat %ds1, %s2 : !ltl.sequence  
-```  
+```
 
 - **`s1 and s2`**:   
 ```mlir
@@ -369,12 +389,12 @@ ltl.not %s1 : !ltl.sequence
 - **`nexttime p`**:   
 ```mlir
 ltl.delay %p, 1, 0 : !ltl.sequence   
-```  
+```
 
 - **`nexttime[n] p`**:  
 ```mlir
 ltl.delay %p, n, 0 : !ltl.sequence   
-```  
+```
 
 - **`s_nexttime p`**: not really distinguishable from the weak version in CIRCT.
 - **`s_nexttime[n] p`**: not really distinguishable from the weak version in CIRCT.

include/circt/Dialect/LTL/LTLOps.td

@@ -62,18 +62,61 @@ 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);
+      LTLAnySequenceType:$input,
+      I64Attr:$delay,
+      OptionalAttr<I64Attr>:$length,
+      Optional<I1>:$clock,
+      OptionalAttr<ClockEdgeAttr>:$edge);
   let results = (outs LTLSequenceType:$result);
   let assemblyFormat = [{
-    $input `,` $delay (`,` $length^)? attr-dict `:` type($input)
+    $input `,` $delay (`,` $length^)? (`clock` $clock^ `,` $edge)? attr-dict `:` type($input)
   }];
   let hasFolder = 1;
   let hasCanonicalizer = 1;
@@ -83,25 +126,32 @@ def DelayOp : LTLOp<"delay", [Pure]> {
     Delays the `$input` sequence by the number of cycles specified by `$delay`.
     The delay must be greater than or equal to zero. The optional `$length`
     specifies during how many cycles after the initial delay the sequence can
-    match. Omitting `$length` indicates an unbounded but finite delay. For
-    example:
-
-    - `ltl.delay %seq, 2, 0` delays `%seq` by exactly 2 cycles. The resulting
-      sequence matches if `%seq` matches exactly 2 cycles in the future.
-    - `ltl.delay %seq, 2, 2` delays `%seq` by 2, 3, or 4 cycles. The resulting
-      sequence matches if `%seq` matches 2, 3, or 4 cycles in the future.
-    - `ltl.delay %seq, 2` delays `%seq` by 2 or more cycles. The number of
-      cycles is unbounded but finite, which means that `%seq` *has* to match at
-      some point, instead of effectively never occuring by being delayed an
-      infinite number of cycles.
+    match. Omitting `$length` indicates an unbounded but finite delay.
+
+    The optional `$clock` and `$edge` specify an explicit clock for the delay.
+    When omitted, the delay is "unclocked" and must be resolved by an enclosing
+    `ltl.clock` operation or by the `InferLTLClocks` pass.
+
+    For example:
+
+    - `ltl.delay %seq, 2, 0` delays `%seq` by exactly 2 cycles (unclocked).
+    - `ltl.delay %seq, 2, 0 clock %clk, posedge` delays `%seq` by exactly 2
+      cycles on the positive edge of `%clk`.
+    - `ltl.delay %seq, 2, 2` delays `%seq` by 2, 3, or 4 cycles.
+    - `ltl.delay %seq, 2` delays `%seq` by 2 or more cycles (unbounded but
+      finite).
     - `ltl.delay %seq, 0, 0` is equivalent to just `%seq`.
 
     #### Clocking
 
-    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.
+    When the `$clock` and `$edge` are present, the delay explicitly refers to
+    that clock signal. When absent, the delay is unclocked and the
+    `InferLTLClocks` pass (`--ltl-infer-clocks`) will propagate clock
+    information from enclosing `ltl.clock` ops.
+
+    Backends (e.g., ExportVerilog) may auto-hoist a clock from explicitly
+    clocked delays to the outermost SVA level when no enclosing `ltl.clock`
+    is present.
   }];
 }
 
@@ -368,45 +418,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