[LTL] Add ClockedAtomOp description

docs/Dialects/LTL.md

@@ -160,6 +160,18 @@ 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`.
 
+#### Atomic clocking
+
+An `i1` can be introduced as a one-cycle sequence sampled on an explicit clock with `ltl.clocked_atom`:
+
+```mlir
+ltl.clocked_atom %input, posedge %clock : i1
+```
+
+This operation is the explicitly clocked form of a boolean atom. It does not create a clocking scope for a sequence or property tree; it only records the clocking event used to sample `%input` and returns an `!ltl.sequence`.
+
+For example, `ltl.clocked_atom %a, posedge %clk : i1` represents the atomic sequence `a` sampled on the rising edge of `%clk`.
+
 #### Delay clocking
 
 `ltl.delay` takes the delayed input first, followed by the delay window:

include/circt/Dialect/LTL/LTLOps.td

@@ -103,6 +103,30 @@ def ClockOp : LTLOp<"clock", [
   }];
 }
 
+def ClockedAtomOp : LTLOp<"clocked_atom", [Pure]> {
+  let arguments = (ins I1:$input, ClockEdgeAttr:$edge, I1:$clock);
+  let results = (outs LTLSequenceType:$result);
+  let assemblyFormat = [{
+    $input `,` $edge $clock attr-dict `:` type($input)
+  }];
+
+  let summary = "Convert a boolean into a sequence on an explicit clock.";
+  let description = [{
+    Converts the boolean `$input` into a one-cycle sequence which matches when
+    `$input` is true on the specified `$edge` of `$clock`.
+
+    This operation is an explicitly clocked atomic sequence. Unlike `ltl.clock`,
+    it does not establish a clocking scope for a property or sequence expression
+    tree. It only records the clocking event associated with a single boolean
+    atom and returns an `!ltl.sequence`.
+
+    For example:
+
+    - `ltl.clocked_atom %a, posedge %clk : i1` matches `%a` on the positive
+      edge of `%clk`.
+  }];
+}
+
 //===----------------------------------------------------------------------===//
 // Sequences
 //===----------------------------------------------------------------------===//

include/circt/Dialect/LTL/LTLVisitors.h

@@ -23,10 +23,11 @@ class Visitor {
     return TypeSwitch<Operation *, ResultType>(op)
         .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...);
-        })
+                       ClockedAtomOp, IntersectOp, NonConsecutiveRepeatOp,
+                       GoToRepeatOp, BooleanConstantOp>(
+            [&](auto op) -> ResultType {
+              return thisCast->visitLTL(op, args...);
+            })
         .Default([&](auto) -> ResultType {
           return thisCast->visitInvalidLTL(op, args...);
         });
@@ -60,6 +61,7 @@ class Visitor {
   HANDLE(UntilOp, Unhandled);
   HANDLE(EventuallyOp, Unhandled);
   HANDLE(ClockOp, Unhandled);
+  HANDLE(ClockedAtomOp, Unhandled);
   HANDLE(IntersectOp, Unhandled);
   HANDLE(NonConsecutiveRepeatOp, Unhandled);
   HANDLE(GoToRepeatOp, Unhandled);