[LTL][SVA] Proposal for Explicit Clocking in the CIRCT LTL(SVA) Intermediate Representation

[sequencer]

Analysis of SystemVerilog Assertions (SVA) Clocking Semantics: A Foundation for Ambiguity

In SystemVerilog, concurrent assertions without an explicit clocking event infer the clock from the surrounding context. This "action at a distance" violates the principle of locality, a key tenet of effective compiler IR design, where an operation's semantics should be self-contained.

The inference hierarchy, in descending order of priority, is as follows:

• Explicit Clock in the Property/Sequence Instance: An explicit clocking event specified directly in the assertion statement or property instance takes highest precedence.
• Explicit Clock in the Property/Sequence Declaration: A leading clocking event within a named property or sequence declaration is used if the instance itself has no explicit clock.9
• Inferred Clock from a Procedural Block: If a concurrent assertion is embedded within a procedural block (e.g., always, always_ff), the clocking event of that block is inferred as the clock for the assertion. This is a common source of confusion, as the procedural activation mechanism becomes entangled - with the temporal sampling clock of the assertion. Inferred Clock from a default clocking Block: A module- or interface-level default clocking block can specify a default clock for all concurrent assertions within its scope that have not otherwise determined a clock.

Clock determination for SVA is complex, hindering automated analysis. A simple sequence like ##1 b requires checking for explicit clocks in assert statements or property definitions, then traversing the IR tree for procedural block sensitivity (e.g., always @(posedge clk)), and finally scanning for default clocking definitions. This non-local dependency complicates IR transformations. For example, hoisting a common sub-sequence from blocks with different clocks could silently alter program meaning, creating "murky semantics" and analytical "annoyance." IR should facilitate, not obstruct, transformations with hidden semantic dependencies.

Opaque Semantics of Clock Flow and Propagation

SVA's intricate rules for clock flow, especially concerning named sequences and parenthesized expressions, lead to non-compositional semantics problematic for IR.

The LRM defines two key concepts: clock flow and clock trapping:

• Clock Flow: A leading clocking event generally flows from left to right across sequence operators like ## and implication operators like |=>. For example, in @(posedge clk) a ##1 b, the posedge clk event serves as the clock for both a and the ##1 delay leading to b.
• Clock Trapping: Crucially, a clocking event specified inside a named sequence declaration or a parenthesized expression is "trapped." It does not flow out of that scope to influence subsequent elements of the larger expression.

This "trapping" rule has profound consequences for IR design. Consider the following example based on the rules in the SystemVerilog specification:

• Case 1: Inline Sequence

ap_ok: assert property(@(posedge clk) e ##[1:5] f ##1 a);

Here, the clock @(posedge clk) is the leading clock for the entire anonymous sequence. It flows across e ##[1:5] f and also across the ##1 to clock the evaluation of a. The meaning of ##1 a is "one clk cycle after f".

• Case 2: Named Sequence

sequence q_ef; @(posedge clk) e ##[1:5] f; endsequence;
ap_q_ef_a: assert property (q_ef ##1 a);

In this case, the @(posedge clk) is part of the q_ef declaration. According to the LRM, this clock is trapped within q_ef. It does not flow out of the q_ef instance. Therefore, the subsequent ##1 a has no clocking event. This expression is syntactically valid, but the evaluation of a is now unclocked, which is almost certainly not the user's intent and semantically distinct from Case 1. This reveals a core lack of compositionality: the meaning of ##1 a drastically shifts based on how its left operand (q_ef) was defined. An IR designed for local rewrites cannot accommodate this. Concatenation should have consistent semantics regardless of operand generation. SVA's rules force an IR to carry extra, non-local "containment" information, complicating a simple composition. This language feature, manageable for humans, poses significant problems for a compiler IR.

Implicit Dependencies in Temporal System Functions

The issue of implicit clocking extends to fundamental SVA building blocks, including the temporal system functions $stable, $rose, $fell, and $past. While their syntax suggests they are pure functions of their expression arguments (e.g., $stable(req)), their semantics are critically dependent on the hidden, implicitly inferred clocking event. These functions inherently describe a relationship between a signal's value at the current clock tick and its value at a previous clock tick. $stable(x) is true if the sampled value of x at the current tick is the same as its value at the previous tick. $rose(x) is true if the LSB of x was 0 at the previous tick and is 1 at the current tick. $fell(x) is true if the LSB of x was 1 at the previous tick and is 0 at the current tick. $past(x, N) returns the value of x from N ticks ago. The critical question is: "relative to which clock's ticks?" In all these cases, the clock is inferred from the context using the same problematic hierarchy as described above. The function call itself provides no local indication of its clock dependency. The $past system function is particularly illustrative because the LRM provides an optional syntax to specify the clocking event directly within the function call: $past(expression1, number_of_ticks, expression2, clocking_event). The optional clocking_event syntax in $past functions, unique among system functions, highlights the clock's fundamental role. Its absence in other functions like $stable, $rose, and $fell prioritizes brevity over clarity.

A Critique of the Current CIRCT LTL Dialect's Clocking Model

The CIRCT LTL dialect, designed for temporal logic and SVA constructs, inherits SVA's flawed implicit clocking model. This non-local and complex design hinders IR robustness and transformation.

The ltl.clock Operation as an Inherited Implicit Context

The primary mechanism for specifying a clock in the current LTL dialect is the ltl.clock operation. This operation takes a property or sequence as an input and produces a new property or sequence with an associated clocking event. This clock then applies to all cycle-delay-based operations (e.g., ltl.delay, ltl.repeat) within the logical expression tree of the input sequence.

An example in the dialect would be:

// %unclocked_seq is some sequence, e.g., ltl.delay(ltl.concat(%a, %b), 1)
%clocked_seq = ltl.clock %unclocked_seq, posedge %clk :!ltl.sequence,!hw.clock ->!ltl.sequence

The ltl.delay operation lacks an explicit clock, requiring an analysis pass to trace its use-def chain back to an ltl.clock operation to determine its clock. While better than SVA, this non-local semantic definition is a design flaw. It complicates IR analysis and transformations like common sub-expression elimination, as hoisting identical sequences with different ltl.clock operations would be invalid due to altered delay meanings. This implicit clock context should be eliminated, making ltl.delay explicit about its clock dependency via a direct SSA operand, ensuring self-contained semantics and safe transformations.

Semantic Gaps in Operator Mapping: The Case of ##

The implicit clocking model in the LTL dialect creates a semantic misalignment with SVA's compositional structure, particularly for the ## cycle delay operator. In SVA, a ##1 b naturally ties the delay's clock to sequence a. However, the current LTL dialect models delay as a prefix operation (ltl.delay %b, 1), leading to a mismatch where the delay's clock is derived from an outer ltl.clock block, not a.

This misalignment complicates lowering from frontend languages, especially in multi-clock scenarios. The proposed solution, refactoring delay into an explicitly clocked sequence object, would allow a ##1 b to be represented as a concatenation of three distinct, explicitly clocked sequences (a, delay1, b), providing a more robust and transparent mapping for frontends and backend tools.

Proposal for an Explicitly Clocked LTL Intermediate Representation

Addressing SVA and current CIRCT LTL dialect semantic flaws, this section proposes a new LTL IR based on explicitness and locality to remove ambiguity, improve analyzability, and support advanced verification. The guiding philosophy of this proposal is simple yet powerful: Any IR operation whose semantics are dependent on a clocking event must accept that clocking event as an explicit SSA operand.

This directly addresses previous issues by making clock dependencies explicit and local, achieving:

• Semantic Clarity: Operations are self-contained; no external search or inference is needed.
• Compositionality: Operations retain meaning regardless of context.
• Analyzability: IR analysis and transformations are simplified and more robust, acting locally without breaking non-local semantics.

This principle will redefine the LTL dialect's core types and operations.

The Clocked Sequence (!ltl.clocked_sequence)

The proposal introduces a new fundamental type, !ltl.clocked_sequence, to replace the current !ltl.sequence which has implicit clocking. !ltl.clocked_sequence intrinsically carries its clocking context, explicitly binding a temporal sequence of events to a specific clock. Operations like ltl.concat, ltl.and, and ltl.or will be modified to operate on !ltl.clocked_sequence operands, ensuring all sequence operands share the same clock. Boolean inputs will be implicitly lifted to a zero-length clocked sequence. This change makes clock domains explicit and type-checked, preventing errors and clarifying clock domains for analysis passes.

The Standalone ltl.delay Operation

We can refactor ltl.delay to be a standalone leaf operation producing !ltl.clocked_sequence, resolving ## operator misalignment and enhancing explicitness. The new signature, %delay_seq = ltl.delay(%clock :!sv.clock, range : RangeAttr) ->!ltl.clocked_sequence, defines a "pure delay" sequence that evaluates immediately and matches after a specified number of %clock ticks. This first-class object can be composed with ltl.concat, allowing clean lowering of SVA expressions like a ##1 b on clock clk.

The Clock-Agnostic Property (!ltl.property)

The proposal redefines !ltl.property as a clock-agnostic, verifiable entity. It's a quantified statement about explicitly clocked sequences, rather than a clocked entity itself. The "lifting" from clocked sequences to clock-agnostic properties occurs via property operators like ltl.implication, ltl.always, and ltl.eventually.

The ltl.implication operator is crucial for CDC. Its signature, %prop = ltl.implication(%lhs :!ltl.clocked_sequence, %rhs :!ltl.clocked_sequence) ->!ltl.property, allows %lhs and %rhs to be explicitly clocked sequence that don't need to share the same clock. This creates a property asserting a relationship between potentially asynchronous temporal patterns.

cc @fabianschuiki @dobios @seldridge

[fabianschuiki]

This is a fantastic write-up @sequencer! 🥳🏅

I totally agree with your concerns regarding SV's strange clock inference model, which makes sequence expressions depend on their surrounding context. That may make sense from a syntactic point of view to some degree, but it's pretty poor design and maps poorly to the IR. I also agree that the LTL dialect's AST-like model is not a good fit for an IR, since the exact same IR can have different interpretations depending on its users (e.g., which ltl.clock it flows into).

Your proposal to have the clocks hooked up to the IR ops that actually interact with them is really nice. That makes every clock-sensitive IR node have an explicit clock. We can in theory emit every delay as @(posedge clock) ## a, even when part of a larger sequence like @(posedge clock) (@(posedge clock) ##1 a) ##1 (@(posedge clock) ##1 b), but we can have the emitter track the parent expression's clock and only print the @(posedge clock2) for a subsequence if it differs from the parent. This would compose well with a clocked verif.assert, which would allow us to provide a single global clock across properties. We could also "guess" a global clock for a property if all its subsequences have the same clock, or are unclocked.

I would suggest calling the type !ltl.sequence, and making it clocked. We could also have an !ltl.unclocked_sequence if we ever need that to capture booleans 🤔

Another later addition we could consider is an ltl.sequence op that can contain a regex-like description of the sequence as a CFG:

%0 = ltl.sequence %clock {
  ltl.and {
    ltl.delay 1
    ltl.match %a
    ltl.delay 2..18
    ltl.match %b
  } {
    ltl.delay 19
    ltl.match %c
  }
}

WDYT?

I love this proposal! ❤️ Thanks for taking the time to write this all up so cleanly!

[Clo91eaf]

I will take this issue and aim to submit a PR in the near future. @@sequencer @fabianschuiki