[LTL] Explicit ltl.delay clocking
- Dominant language
- C++
- Stars
- 2.2k
- Forks
- 524
- Avg merge
- 3d 2h
- Merged PRs (30d)
- 46
Description
## 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)](https://github.com/llvm/circt/pull/9392)**
- 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, [, ] :
```
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, , %input, [, ] :
```
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
Contributor guide
No contributing guide indexed for this repository
Research direction
Start with the LTL dialect's existing delay operation and the proposed PR 1 foundation for ClockedDelayOp and fold infrastructure. Then review the InferLTLClocks, ExportVerilog, and ImportVerilog components to determine which of the three planned PRs is being undertaken. Done means implementing the selected stage while preserving the clock lifecycle and compatibility described here.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- cpp
- Domain
- compilers
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100