From 3ecef0fbc0ff1722c3ba3f3e2c139b71028ad7ee Mon Sep 17 00:00:00 2001
From: Clo91eaf <Clo91eaf@qq.com>
Date: Sun, 24 May 2026 22:23:29 +0800
Subject: [PATCH] [LTL] Add ClockedAtomOp description

---
 docs/Dialects/LTL.md                    | 12 ++++++++++++
 include/circt/Dialect/LTL/LTLOps.td     | 24 ++++++++++++++++++++++++
 include/circt/Dialect/LTL/LTLVisitors.h | 10 ++++++----
 3 files changed, 42 insertions(+), 4 deletions(-)

diff --git a/docs/Dialects/LTL.md b/docs/Dialects/LTL.md
index 13aa900bcbf0..195236a0ec2c 100644
--- a/docs/Dialects/LTL.md
+++ b/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:
diff --git a/include/circt/Dialect/LTL/LTLOps.td b/include/circt/Dialect/LTL/LTLOps.td
index 1a8c3389a68b..3d7df10ed0ec 100644
--- a/include/circt/Dialect/LTL/LTLOps.td
+++ b/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
 //===----------------------------------------------------------------------===//
diff --git a/include/circt/Dialect/LTL/LTLVisitors.h b/include/circt/Dialect/LTL/LTLVisitors.h
index b2486ad6c603..b945e02bd097 100644
--- a/include/circt/Dialect/LTL/LTLVisitors.h
+++ b/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);