[LTL] Explicit ltl.delay clocking

[Clo91eaf]

Background

Today, ltl.delay clock handling is inconsistent across layers:

• SVA allows clocked and unclocked ##N delays (clock from @(...) or default clocking context).
• FIRRTL circt_ltl_delay currently has no explicit clock operand and can rely on surrounding context (e.g., circt_ltl_clock).
• CIRCT lowering/emission currently requires special handling to recover/propagate clock context.

This mismatch leads to implicit clock inference spread across passes and conversions, making behavior hard to reason about and review.

Core Problem

We currently rely on implicit clock inference in multiple places.
The long-term direction is to make delay clock semantics explicit and uniform, while still preserving compatibility during migration.

Candidate Implementation Strategies

1. Aggressive full switch to explicit delay clocks (single large change)

   • Pros: direct end-state.
   • Cons: large review surface; placeholder-clock semantic issues.

2. Optional clock on ltl.delay (incremental transition)

   • Pros: good intermediate compatibility; smaller, reviewable changes.
   • Cons: temporary mixed mode (clocked + unclocked delay).

3. Two ops coexisting (delay + clocked_delay)

   • Pros: explicit separation.
   • Cons: duplicated infrastructure and migration overhead.

Here use Option 3 as the intermediate path, then converge to the explicit-clock end state.

Design

ltl.delay (unclocked)

%result = ltl.delay %input, <delay> [, <length>] : <type>

Pure sequence delay with no clock. Clock is provided externally by an enclosing ltl.clock operation or resolved by the InferLTLClocks pass.

ltl.clocked_delay (explicitly clocked)

%result = ltl.clocked_delay %clk, <edge>, %input, <delay> [, <length>] : <type>

Self-contained clocked delay. The clock and edge parameters are mandatory. Produced by:

• InferLTLClocks pass (from unclocked ltl.delay + enclosing ltl.clock context)
• ImportVerilog (when assertion clock context is present)
• Direct construction in frontends with explicit clock intent

Clock Lifecycle

ltl.clock and ltl.clocked_delay serve different roles at different pipeline stages:

• Before InferLTLClocks: ltl.clock broadcasts a clock to a subtree of delays; ltl.clocked_delay carries its own clock. Both may coexist.
• InferLTLClocks: Converts ltl.delay under ltl.clock to ltl.clocked_delay, then eliminates the ltl.clock op. Clones subtrees for multi-clock fan-out.
• After: Only ltl.clocked_delay (explicit clock) and unresolved ltl.delay (warning) remain. No ltl.clock.
• ExportVerilog: Extracts clock from clocked_delay, hoists to SVA @(edge clk), emits delays as ##N.

InferLTLClocks pass

1. Propagates clock/edge from ltl.clock to unclocked ltl.delay, producing ltl.clocked_delay.
2. Removes the ltl.clock op — clock now lives solely on clocked_delay.
3. Clones delay subtrees for multi-clock fan-out.
4. Warns on unresolved ltl.delay (no enclosing clock).

---

Implementation Plan (3 PRs)

PR 1: LTL IR foundation — ClockedDelayOp + fold infrastructure

• Pure LTL dialect changes. No conversions, no passes.

This is the foundational PR that all others depend on.

PR 2: InferLTLClocks pass

• New standalone pass + registration infrastructure.

PR 3: ExportVerilog + ImportVerilog adaptation

• Update both Verilog conversions to handle dual-op model.

This RFC was discussed by me and @Claude-opus-4.6, and reviewed by myself

[Clo91eaf]

@uenoku wdyt about this issue?
I will start split my previous pr into different pr in Stage 1 soon. Thanks for your suggestion!

[uenoku]

I think this looks good, though it's not clear to me PR 6 is possible as we need to infer clocks anyway. Also please disclose LLM use if this is generated from LLM (please take a look at LLVM AI policy https://llvm.org/docs/AIToolPolicy.html).

[Clo91eaf]

I'm not entirely confident about completely eliminating implicit clock deduction, but given the current situation, explicit clock declarations offer many advantages in IR design, so I'm trying to promote explicit clocking as much as possible.