llvm / llvm/circt

[LTL] Explicit ltl.delay clocking

Open
#9,859 3 comments 0 reactions 0 assignees View on GitHub
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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.