[LTL] Make ltl.delay support optional clocking

docs/Dialects/LTL.md

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

include/circt/Dialect/LTL/LTLFolds.td

@@ -21,6 +21,10 @@ def valueTail : NativeCodeCall<"$0.drop_front()">;
 def concatValues : NativeCodeCall<
   "concatValues(ValueRange{$0}, ValueRange{$1})">;
 
+// Ensure that outer and inner clocked delays use the same clock and edge
+// before merging. Accepts (outerClock, innerClock, outerEdge, innerEdge).
+def SameClockAndEdge : Constraint<CPred<"$0 == $1 && $2 == $3">>;
+
 //===----------------------------------------------------------------------===//
 // DelayOp
 //===----------------------------------------------------------------------===//
@@ -40,12 +44,30 @@ def NestedDelays : Pat<
   (DelayOp $input, (mergedDelays $delay1, $delay2),
                    (mergedLengths $length1, $length2))>;
 
+// clocked_delay(clk, edge, clocked_delay(clk, edge, s, I, N), J, M)
+//   -> clocked_delay(clk, edge, s, I+J, N+M)
+def NestedClockedDelays : Pat<
+  (ClockedDelayOp $clock0, $edge0,
+                  (ClockedDelayOp $clock1, $edge1, $input, $delay1, $length1),
+                  $delay2, $length2),
+  (ClockedDelayOp $clock0, $edge0, $input, (mergedDelays $delay1, $delay2),
+                  (mergedLengths $length1, $length2)),
+  [(SameClockAndEdge $clock0, $clock1, $edge0, $edge1)]>;
+
 // delay(concat(s, ...), N, M) -> concat(delay(s, N, M), ...)
 def MoveDelayIntoConcat : Pat<
   (DelayOp (ConcatOp $inputs), $delay, $length),
   (ConcatOp (concatValues (DelayOp (valueHead $inputs), $delay, $length),
                           (valueTail $inputs)))>;
 
+// clocked_delay(clk, edge, concat(s, ...), N, M)
+//   -> concat(clocked_delay(clk, edge, s, N, M), ...)
+def MoveClockedDelayIntoConcat : Pat<
+  (ClockedDelayOp $clock, $edge, (ConcatOp $inputs), $delay, $length),
+  (ConcatOp (concatValues (ClockedDelayOp $clock, $edge, (valueHead $inputs),
+                                         $delay, $length),
+                          (valueTail $inputs)))>;
+
 //===----------------------------------------------------------------------===//
 // ConcatOp
 //===----------------------------------------------------------------------===//

include/circt/Dialect/LTL/LTLOps.td

@@ -62,6 +62,47 @@ def IntersectOp : AssocLTLOp<"intersect"> {
   let hasCanonicalizeMethod = 1;
 }
 
+//===----------------------------------------------------------------------===//
+// Clocking
+//===----------------------------------------------------------------------===//
+
+// Edge behavior enum for always block.  See SV Spec 9.4.2.
+
+/// AtPosEdge triggers on a rise from 0 to 1/X/Z, or X/Z to 1.
+def AtPosEdge: I32EnumAttrCase<"Pos", 0, "posedge">;
+/// AtNegEdge triggers on a drop from 1 to 0/X/Z, or X/Z to 0.
+def AtNegEdge: I32EnumAttrCase<"Neg", 1, "negedge">;
+/// AtEdge is syntactic sugar for AtPosEdge or AtNegEdge.
+def AtEdge   : I32EnumAttrCase<"Both", 2, "edge">;
+
+def ClockEdgeAttr : I32EnumAttr<"ClockEdge", "clock edge",
+                                [AtPosEdge, AtNegEdge, AtEdge]> {
+  let cppNamespace = "circt::ltl";
+}
+
+def ClockOp : LTLOp<"clock", [
+  Pure, InferTypeOpInterface, DeclareOpInterfaceMethods<InferTypeOpInterface>
+]> {
+  let arguments = (ins LTLAnyPropertyType:$input, ClockEdgeAttr:$edge, I1:$clock);
+  let results = (outs LTLSequenceOrPropertyType:$result);
+  let assemblyFormat = [{
+    $input `,` $edge $clock attr-dict `:` type($input)
+  }];
+
+  let summary = "Specify the clock for a property or sequence.";
+  let description = [{
+    Specifies the `$edge` on a given `$clock` to be the clock for an `$input`
+    property or sequence. All cycle delays in the `$input` implicitly refer to a
+    clock that advances the state to the next cycle. The `ltl.clock` operation
+    provides that clock. The clock applies to the entire property or sequence
+    expression tree below `$input`, up to any other nested `ltl.clock`
+    operations.
+
+    The operation returns a property if the `$input` is a property, and a
+    sequence otherwise.
+  }];
+}
+
 //===----------------------------------------------------------------------===//
 // Sequences
 //===----------------------------------------------------------------------===//
@@ -83,25 +124,53 @@ def DelayOp : LTLOp<"delay", [Pure]> {
     Delays the `$input` sequence by the number of cycles specified by `$delay`.
     The delay must be greater than or equal to zero. The optional `$length`
     specifies during how many cycles after the initial delay the sequence can
-    match. Omitting `$length` indicates an unbounded but finite delay. For
-    example:
-
-    - `ltl.delay %seq, 2, 0` delays `%seq` by exactly 2 cycles. The resulting
-      sequence matches if `%seq` matches exactly 2 cycles in the future.
-    - `ltl.delay %seq, 2, 2` delays `%seq` by 2, 3, or 4 cycles. The resulting
-      sequence matches if `%seq` matches 2, 3, or 4 cycles in the future.
-    - `ltl.delay %seq, 2` delays `%seq` by 2 or more cycles. The number of
-      cycles is unbounded but finite, which means that `%seq` *has* to match at
-      some point, instead of effectively never occuring by being delayed an
-      infinite number of cycles.
+    match. Omitting `$length` indicates an unbounded but finite delay.
+
+    This operation is intentionally unclocked. Use `ltl.clocked_delay` for
+    explicitly clocked delays.
+
+    For example:
+
+    - `ltl.delay %seq, 2, 0` delays `%seq` by exactly 2 cycles (unclocked).
+    - `ltl.delay %seq, 2, 2` delays `%seq` by 2, 3, or 4 cycles.
+    - `ltl.delay %seq, 2` delays `%seq` by 2 or more cycles (unbounded but
+      finite).
     - `ltl.delay %seq, 0, 0` is equivalent to just `%seq`.
 
-    #### Clocking
+    Unclocked delays may be resolved by an enclosing `ltl.clock` operation or
+    by the `InferLTLClocks` pass (`--ltl-infer-clocks`).
+  }];
+}
 
-    The cycle delay specified on the operation refers to a clocking event. This
-    event is not directly specified by the delay operation itself. Instead, the
-    [`ltl.clock`](#ltlclock-circtltlclockop) operation can be used to associate
-    all delays within a sequence with a clock.
+def ClockedDelayOp : LTLOp<"clocked_delay", [Pure]> {
+  let arguments = (ins
+    I1:$clock,
+    ClockEdgeAttr:$edge,
+    LTLAnySequenceType:$input,
+    I64Attr:$delay,
+    OptionalAttr<I64Attr>:$length);
+  let results = (outs LTLSequenceType:$result);
+  let assemblyFormat = [{
+    $clock `,` $edge `,` $input `,` $delay (`,` $length^)? attr-dict `:` type($input)
+  }];
+  let hasFolder = 1;
+  let hasCanonicalizer = 1;
+
+  let summary = "Delay a sequence by a number of cycles on an explicit clock.";
+  let description = [{
+    Delays the `$input` sequence by the number of cycles specified by `$delay`
+    on the specified `$clock` and `$edge`.
+
+    The optional `$length` specifies during how many cycles after the initial
+    delay the sequence can match. Omitting `$length` indicates an unbounded but
+    finite delay.
+
+    For example:
+
+    - `ltl.clocked_delay %clk, posedge, %seq, 2, 0` delays `%seq` by
+      exactly 2 cycles on the positive edge of `%clk`.
+    - `ltl.clocked_delay %clk, negedge, %seq, 2, 2` delays `%seq` by 2,
+      3, or 4 cycles on the negative edge of `%clk`.
   }];
 }
 
@@ -368,45 +437,4 @@ def EventuallyOp : LTLOp<"eventually", [Pure]> {
   }];
 }
 
-//===----------------------------------------------------------------------===//
-// Clocking
-//===----------------------------------------------------------------------===//
-
-// Edge behavior enum for always block.  See SV Spec 9.4.2.
-
-/// AtPosEdge triggers on a rise from 0 to 1/X/Z, or X/Z to 1.
-def AtPosEdge: I32EnumAttrCase<"Pos", 0, "posedge">;
-/// AtNegEdge triggers on a drop from 1 to 0/X/Z, or X/Z to 0.
-def AtNegEdge: I32EnumAttrCase<"Neg", 1, "negedge">;
-/// AtEdge is syntactic sugar for AtPosEdge or AtNegEdge.
-def AtEdge   : I32EnumAttrCase<"Both", 2, "edge">;
-
-def ClockEdgeAttr : I32EnumAttr<"ClockEdge", "clock edge",
-                                [AtPosEdge, AtNegEdge, AtEdge]> {
-  let cppNamespace = "circt::ltl";
-}
-
-def ClockOp : LTLOp<"clock", [
-  Pure, InferTypeOpInterface, DeclareOpInterfaceMethods<InferTypeOpInterface>
-]> {
-  let arguments = (ins LTLAnyPropertyType:$input, ClockEdgeAttr:$edge, I1:$clock);
-  let results = (outs LTLSequenceOrPropertyType:$result);
-  let assemblyFormat = [{
-    $input `,` $edge $clock attr-dict `:` type($input)
-  }];
-
-  let summary = "Specify the clock for a property or sequence.";
-  let description = [{
-    Specifies the `$edge` on a given `$clock` to be the clock for an `$input`
-    property or sequence. All cycle delays in the `$input` implicitly refer to a
-    clock that advances the state to the next cycle. The `ltl.clock` operation
-    provides that clock. The clock applies to the entire property or sequence
-    expression tree below `$input`, up to any other nested `ltl.clock`
-    operations.
-
-    The operation returns a property if the `$input` is a property, and a
-    sequence otherwise.
-  }];
-}
-
 #endif // CIRCT_DIALECT_LTL_LTLOPS_TD

include/circt/Dialect/LTL/LTLVisitors.h

@@ -21,8 +21,8 @@ class Visitor {
   ResultType dispatchLTLVisitor(Operation *op, ExtraArgs... args) {
     auto *thisCast = static_cast<ConcreteType *>(this);
     return TypeSwitch<Operation *, ResultType>(op)
-        .template Case<AndOp, OrOp, DelayOp, ConcatOp, RepeatOp, NotOp,
-                       ImplicationOp, UntilOp, EventuallyOp, ClockOp,
+        .template Case<AndOp, OrOp, DelayOp, ClockedDelayOp, ConcatOp, RepeatOp,
+                       NotOp, ImplicationOp, UntilOp, EventuallyOp, ClockOp,
                        IntersectOp, NonConsecutiveRepeatOp, GoToRepeatOp,
                        BooleanConstantOp>([&](auto op) -> ResultType {
           return thisCast->visitLTL(op, args...);
@@ -52,6 +52,7 @@ class Visitor {
   HANDLE(AndOp, Unhandled);
   HANDLE(OrOp, Unhandled);
   HANDLE(DelayOp, Unhandled);
+  HANDLE(ClockedDelayOp, Unhandled);
   HANDLE(ConcatOp, Unhandled);
   HANDLE(RepeatOp, Unhandled);
   HANDLE(NotOp, Unhandled);

lib/Dialect/LTL/LTLFolds.cpp

@@ -79,21 +79,40 @@ LogicalResult IntersectOp::canonicalize(IntersectOp op,
 // DelayOp
 //===----------------------------------------------------------------------===//
 
-OpFoldResult DelayOp::fold(FoldAdaptor adaptor) {
+template <typename DelayLikeOp, typename FoldAdaptorT>
+static OpFoldResult foldDelayLike(DelayLikeOp op, FoldAdaptorT adaptor) {
   // delay(s, 0, 0) -> s
   if (adaptor.getDelay() == 0 && adaptor.getLength() == 0 &&
-      isa<SequenceType>(getInput().getType()))
-    return getInput();
+      isa<SequenceType>(op.getInput().getType()))
+    return op.getInput();
 
   return {};
 }
 
+OpFoldResult DelayOp::fold(FoldAdaptor adaptor) {
+  return foldDelayLike(*this, adaptor);
+}
+
 void DelayOp::getCanonicalizationPatterns(RewritePatternSet &results,
                                           MLIRContext *context) {
   results.add<patterns::NestedDelays>(results.getContext());
   results.add<patterns::MoveDelayIntoConcat>(results.getContext());
 }
 
+//===----------------------------------------------------------------------===//
+// ClockedDelayOp
+//===----------------------------------------------------------------------===//
+
+OpFoldResult ClockedDelayOp::fold(FoldAdaptor adaptor) {
+  return foldDelayLike(*this, adaptor);
+}
+
+void ClockedDelayOp::getCanonicalizationPatterns(RewritePatternSet &results,
+                                                 MLIRContext *context) {
+  results.add<patterns::NestedClockedDelays>(results.getContext());
+  results.add<patterns::MoveClockedDelayIntoConcat>(results.getContext());
+}
+
 //===----------------------------------------------------------------------===//
 // ConcatOp
 //===----------------------------------------------------------------------===//

test/Dialect/LTL/basic.mlir

@@ -2,6 +2,7 @@
 
 %true = hw.constant true
 %c0_i8 = hw.constant 0 : i8
+%clk = hw.constant true
 
 //===----------------------------------------------------------------------===//
 // Types
@@ -53,8 +54,12 @@ unrealized_conversion_cast %p3 : !ltl.property to index
 
 // CHECK: ltl.delay {{%.+}}, 0 : !ltl.sequence
 // CHECK: ltl.delay {{%.+}}, 42, 1337 : !ltl.sequence
+// CHECK: ltl.clocked_delay {{%.+}}, posedge, {{%.+}}, 0 : !ltl.sequence
+// CHECK: ltl.clocked_delay {{%.+}}, posedge, {{%.+}}, 42, 1337 : !ltl.sequence
 ltl.delay %s, 0 : !ltl.sequence
 ltl.delay %s, 42, 1337 : !ltl.sequence
+ltl.clocked_delay %clk, posedge, %s, 0 : !ltl.sequence
+ltl.clocked_delay %clk, posedge, %s, 42, 1337 : !ltl.sequence
 
 // CHECK: ltl.concat {{%.+}} : !ltl.sequence
 // CHECK: ltl.concat {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.sequence