Skip to content

[LTL] Add ClockedDelayOp description#10415

Merged
TaoBi22 merged 1 commit intollvm:mainfrom
Clo91eaf:explict-delay-1-1
May 9, 2026
Merged

[LTL] Add ClockedDelayOp description#10415
TaoBi22 merged 1 commit intollvm:mainfrom
Clo91eaf:explict-delay-1-1

Conversation

@Clo91eaf
Copy link
Copy Markdown
Contributor

@Clo91eaf Clo91eaf commented May 8, 2026

This PR is the small piece of first step of the #9859.

Create a new operation of ltl.clocked_delay

Example:

ltl.delay %s, 2, 0
ltl.clocked_delay %s, posedge %clk, 2, 0

Assisted-by: Claude Code : claude-opus-4.6

Close: #9869

@Clo91eaf
Copy link
Copy Markdown
Contributor Author

Clo91eaf commented May 8, 2026

@TaoBi22 Thanks for your recent work on the PastOp. I’m really glad to see CIRCT moving forward on explicit clock semantics. Could you please take a look at this smaller PR? I’m optimistic that we’ll be able to make good progress on this work soon!

Copy link
Copy Markdown
Contributor

@TaoBi22 TaoBi22 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for splitting this up @Clo91eaf!

Comment thread include/circt/Dialect/LTL/LTLOps.td Outdated
Comment on lines +163 to +164
let hasFolder = 1;
let hasCanonicalizer = 1;
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You'll need to drop these until the respective methods are added (I believe that's what's causing the CI failure)

Comment thread include/circt/Dialect/LTL/LTLOps.td Outdated
OptionalAttr<I64Attr>:$length);
let results = (outs LTLSequenceType:$result);
let assemblyFormat = [{
$clock `,` $edge `,` $input `,` $delay (`,` $length^)? attr-dict `:` type($input)
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: could we make the syntax something like:

Suggested change
$clock `,` $edge `,` $input `,` $delay (`,` $length^)? attr-dict `:` type($input)
$input `,` $edge $clock `,` $delay (`,` $length^)? attr-dict `:` type($input)

to keep this in line with ltl.clock and ltl.past (which doesn't actually have an edge specification yet, but that's on my todo list once #10392 lands)

Comment thread include/circt/Dialect/LTL/LTLOps.td Outdated
Comment on lines +147 to +148
This operation is intentionally unclocked. Use `ltl.clocked_delay` for
explicitly clocked delays.
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Super-nit: We've already explained the clocking situation above, so we can drop the first sentence and attach the second to the end of the paragraph above.

@Clo91eaf Clo91eaf force-pushed the explict-delay-1-1 branch from c74217c to 7486291 Compare May 8, 2026 17:35
@Clo91eaf
Copy link
Copy Markdown
Contributor Author

Clo91eaf commented May 8, 2026

@TaoBi22 fixed.

- Move ClockEdgeAttr and ClockOp definitions before the Sequences section so they can be referenced by sequence operations.
- Add new ClockedDelayOp for explicitly clocked delays with mandatory clock and edge parameters. Syntax: clocked_delay input, edge clock, delay[, length].
- Add ClockedDelayOp to LTL Visitor TypeSwitch for downstream consumers.
- Update DelayOp documentation to clarify unclocked semantics.
@TaoBi22
Copy link
Copy Markdown
Contributor

TaoBi22 commented May 8, 2026

Thanks @Clo91eaf! Are you happy for this to be merged?

@Clo91eaf
Copy link
Copy Markdown
Contributor Author

Clo91eaf commented May 9, 2026

@TaoBi22 Of course! Thank you!

@TaoBi22 TaoBi22 merged commit 157bd2d into llvm:main May 9, 2026
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants