[LTL] Make ltl.delay support optional clocking

[Clo91eaf]

This PR is the first step of the explicit-delay stack.

Create a new operation of ltl.clocked_delay

Example:

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

This pr is participated with @Claude-opus-4.6 and reviewed by myself

[Clo91eaf]

@uenoku cc

[uenoku]

Probably we should add an operation instead of adding optional operand because we could break existing delay op's semantics.

[Clo91eaf]

Probably we should add an operation instead of adding optional operand because we could break existing delay op's semantics.

Ok, this way seems better, i will change the RFC first and then redo this pr's commits.

[Clo91eaf]

@uenoku cc

[Clo91eaf]

@fabianschuiki cc pls 👀

[dobios]

I'm curious as to why this is totally necessary, won't this create semantic issues when paired with assert-property style things (so lowerings that yield clocked_assert) or other ltl.clock ops? Or are you going to add extra validation to enforce that only one clock is used across an expression like in the clocked assert validation?

[Clo91eaf]

I'm curious as to why this is totally necessary

The initial issue came from #8673, and its main purpose was to ensure that IR (In-Relational Analysis) had clear semantic relationships when analyzing clocks.

won't this create semantic issues when paired with assert-property style things (so lowerings that yield clocked_assert) or other ltl.clock ops?

Good question. The current VerifyClockedAssertLike pass already walks the property tree under clocked_assert and rejects any nested ltl.clock ops. This PR (PR1) only adds the ClockedDelayOp definition — at this stage, nothing produces ClockedDelayOp yet, so there's no interaction to worry about.

In the follow-up PR (PR2: InferLTLClocks), ltl.clock ops are lowered by pushing their clock info into ltl.delay → ltl.clocked_delay, and then the ltl.clock is eliminated. So after InferLTLClocks runs, the clock lives exclusively on clocked_delay ops rather than on ltl.clock.

Or are you going to add extra validation to enforce that only one clock is used across an expression like in the clocked assert validation?

That said, you're right that VerifyClockedAssertLike should be updated to also reject ClockedDelayOp with mismatched clocks under clocked_assert. I'll add that check in PR2 — the validation will verify that all ClockedDelayOp clocks in the property tree are consistent with the clocked_assert clock, similar to the existing ltl.clock rejection.

[Clo91eaf]

Hi @uenoku @dobios @fabianschuiki, just wanted to gently bump this. I've updated the PR based on the feedback from last week. I know everyone is busy, but could you let me know if these changes look correct or if there's anything else needed before we move forward with the next steps in this new direction? Thanks!