[LTL] Add explict clocked operations and types #9026
Conversation
Clo91eaf
force-pushed
the
sva_clock
branch
2 times, most recently
from
d18a2d2 to
6689f89
Compare
Clo91eaf
changed the title
Clo91eaf
force-pushed
the
sva_clock
branch
2 times, most recently
from
c31983e to
175dc96
Compare
- Introduced new clocked operations: ClockedAndOp, ClockedOrOp, ClockedIntersectOp, CreateClockedSequenceOp, ClockedDelayOp, ClockedConcatOp... - Added LTLClockedSequenceType to represent clocked sequences. - Updated LTLTypes and LTLVisitors to support new clocked operations.
|
@fabianschuiki Sorry! Some things caused this PR to be late. Now I have time to implement #8673, wdyt about this PR? |
| def ClockedAndOp : LTLOp<"clocked_and", [Pure, Commutative]> { | ||
| let arguments = (ins | ||
| Variadic<LTLClockedSequenceType>:$inputs, | ||
| ClockEdgeAttr:$edge, | ||
| I1:$clock); | ||
| let results = (outs LTLClockedSequenceType:$result); | ||
| let assemblyFormat = [{ | ||
| $edge $clock `,` $inputs attr-dict | ||
| }]; | ||
| let hasCanonicalizeMethod = 1; | ||
|
|
||
| let summary = "A conjunction of explicitly clocked sequences with a specified clock domain."; | ||
| let description = [{ | ||
| See `ltl.and` op. $edge and $clock specify the clock domain for the result. | ||
| }]; | ||
| } | ||
|
|
||
| def ClockedOrOp : LTLOp<"clocked_or", [Pure, Commutative]> { | ||
| let arguments = (ins | ||
| Variadic<LTLClockedSequenceType>:$inputs, | ||
| ClockEdgeAttr:$edge, | ||
| I1:$clock); | ||
| let results = (outs LTLClockedSequenceType:$result); | ||
| let assemblyFormat = [{ | ||
| $edge $clock `,` $inputs attr-dict | ||
| }]; | ||
| let hasCanonicalizeMethod = 1; | ||
|
|
||
| let summary = "A disjunction of explicitly clocked sequences with a specified clock domain."; | ||
| let description = [{ | ||
| See `ltl.or` op. $edge and $clock specify the clock domain for the result. | ||
| }]; | ||
| } |
There was a problem hiding this comment.
Do and/or operations require a clock? These oparations sound like they only take two sequences and performa a boolean and/or on them. But if those sequences contain any delays, those delays would already specify a clock. Wouldn't that suffice?
There was a problem hiding this comment.
Do and/or operations require a clock? These oparations sound like they only take two sequences and performa a boolean and/or on them. But if those sequences contain any delays, those delays would already specify a clock. Wouldn't that suffice?
The clock in the operand is mainly used to specify the clock of the result type, because when two operands are in different clock domains, the clock of the result becomes difficult to determine
| def ClockedDelayOp : LTLOp<"clocked_delay", [Pure]> { | ||
| let arguments = (ins | ||
| LTLAnySequenceType:$input, | ||
| ClockEdgeAttr:$edge, | ||
| I1:$clock, | ||
| I64Attr:$delay, | ||
| OptionalAttr<I64Attr>:$length); | ||
| let results = (outs LTLClockedSequenceType:$result); | ||
| let assemblyFormat = [{ | ||
| $edge $clock `,` $input `,` $delay (`,` $length^)? attr-dict `:` type($input) | ||
| }]; | ||
|
|
||
| let summary = "Create an explicitly clocked delay sequence from i1 or sequence."; | ||
| let description = [{ | ||
| Creates a standalone "pure delay" sequence that is explicitly bound to a | ||
| specific clock. This sequence evaluates to true immediately and matches | ||
| after the specified number of clock ticks. | ||
|
|
||
| The `$input` must be an explicitly clocked sequence. The `$delay` specifies | ||
| the number of clock cycles to delay, and the optional `$length` specifies | ||
| the range of cycles during which the delay can match. Omitting `$length` | ||
| indicates an unbounded but finite delay. | ||
|
|
||
| Examples: | ||
| - `ltl.clocked_delay posedge %clk, %seq, 2, 0` creates a delay that matches | ||
| exactly 2 cycles after the current time on the positive edge of %clk. | ||
| - `ltl.clocked_delay posedge %clk, %seq, 2, 2` creates a delay that matches | ||
| 2, 3, or 4 cycles after the current time. | ||
| - `ltl.clocked_delay posedge %clk, %seq, 2` creates an unbounded but finite | ||
| delay of 2 or more cycles. | ||
|
|
||
| This operation enables clean lowering of SVA expressions like `##1 b` | ||
| }]; | ||
| } |
There was a problem hiding this comment.
It's very cool that we get a properly clocked delay operation! Could we just name this ltl.delay and delete the old unclocked ltl.delay? I don't think we need both ops.
There was a problem hiding this comment.
It's very cool that we get a properly clocked delay operation! Could we just name this
ltl.delayand delete the old unclockedltl.delay? I don't think we need both ops.
Yes! This is a good suggestion, in fact I'm not sure if break changes should be made in this PR, if you think it's okay then it would be a good idea to replace the delay entirely
| def ClockedConcatOp : LTLOp<"clocked_concat", [Pure]> { | ||
| let arguments = (ins | ||
| Variadic<LTLClockedSequenceType>:$inputs, | ||
| ClockEdgeAttr:$edge, | ||
| I1:$clock); | ||
| let results = (outs LTLClockedSequenceType:$result); | ||
| let assemblyFormat = [{ | ||
| $edge $clock `,` $inputs attr-dict | ||
| }]; | ||
| let hasFolder = 1; | ||
| let hasCanonicalizer = 1; | ||
|
|
||
| let summary = "Concatenate explicitly clocked sequences with a specified clock domain."; | ||
| let description = [{ | ||
| See `ltl.concat` op. $edge and $clock specify the clock domain for the result. | ||
| }]; | ||
| } | ||
|
|
There was a problem hiding this comment.
Same as with the and/or operation: ltl.concat probably doesn't need to know what clock the input sequences are sensitive to. The concat corresponds to a ##0 b in Verilog, which means a and b happen at the exact same time, not a specific clocked delay apart. And since there's no delay, the op probably doesn't need a clock 🤔
| def LTLClockedSequenceType : LTLTypeDef<"ClockedSequence", "clocked_sequence"> { | ||
| let summary = "LTL clocked sequence type"; | ||
| let description = [{ | ||
| The `ltl.clocked_sequence` type is the fundamental type for representing | ||
| temporal sequences in linear temporal logic, for example, *"on the rising | ||
| edge of clk, A is true two cycles after B is true"*. | ||
|
|
||
| This type 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 operate on `ltl.clocked_sequence` operands, ensuring | ||
| all sequence operands share the same clock. This makes clock domains | ||
| explicit and type-checked, preventing errors and clarifying clock domains | ||
| for analysis passes. | ||
|
|
||
| Boolean inputs (`i1`) are implicitly lifted to a zero-length clocked | ||
| sequence. Operations that accept a clocked sequence as an operand will use | ||
| the `AnyClockedSequence` constraint, which also accepts `i1`. | ||
| }]; | ||
| } | ||
|
|
||
| def LTLPropertyType : LTLTypeDef<"Property", "property"> { | ||
| let summary = "LTL property type"; | ||
| let description = [{ | ||
| The `ltl.property` type represents a verifiable property built from linear | ||
| temporal logic sequences and quantifiers, for example, *"if you see sequence | ||
| A, eventually you will see sequence B"*. | ||
|
|
||
| Note that this type explicitly identifies a *property*. However, a boolean | ||
| value (`i1`) or a sequence (`ltl.sequence`) is also a valid property. | ||
| Operations that accept a property as an operand will use the `AnyProperty` | ||
| constraint, which also accepts `ltl.sequence` and `i1`. | ||
| The `ltl.property` type represents a clock-agnostic, verifiable property | ||
| built from explicitly clocked sequences and quantifiers, for example, *"if | ||
| you see sequence A, eventually you will see sequence B"*. | ||
|
|
||
| This type is fundamentally clock-independent - it represents a quantified | ||
| statement about explicitly clocked sequences rather than being 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`. | ||
|
|
||
| Properties can describe relationships between temporal patterns that may | ||
| exist in different clock domains, enabling cross-domain verification. | ||
| }]; | ||
| } |
There was a problem hiding this comment.
Do we need to distinguish between these two? If we have all clocked operations (basically just delay, repeat, and some of the goto stuff I'd guess) have an explicit clock, and all other operations are clock agnostic (because they don't need a clock to express their semantics), I think all of that would just be a plain old !ltl.property. I don't think we need an explicit distinction betweem clocked and unclocked here 🤔. When we emit things to Verilog, we can just scan the LTL operations to find all the clocks used, and insert @(posedge clock) around all the LTL ops that share the same clock 🤔
There was a problem hiding this comment.
Do we need to distinguish between these two? If we have all clocked operations (basically just delay, repeat, and some of the goto stuff I'd guess) have an explicit clock, and all other operations are clock agnostic (because they don't need a clock to express their semantics), I think all of that would just be a plain old
!ltl.property. I don't think we need an explicit distinction betweem clocked and unclocked here 🤔. When we emit things to Verilog, we can just scan the LTL operations to find all the clocks used, and insert@(posedge clock)around all the LTL ops that share the same clock 🤔
Yes, thank you for your suggestion. After thinking about it, I agree with your point. There are actually two core aspects here: the "clock of the operands" and "clocked delays". For operations like concat/and/or, if the operands are in different clock domains, the semantics become unclear, so these operations do not need to explicitly carry a clock—it's enough to ensure that all their input operands have the same clock.
Although the proposal in #8673 suggests enforcing clock consistency for operands at the type system level, the fundamental goal is to prevent combining operands from different clock domains. In other words, these logical/combination operations can be designed as clock-agnostic—as long as the type system guarantees that operands with different clocks cannot be mixed, the semantics remain clear.
Additionally, I will remove APIs such as clocked_and and clocked_or. Based on our discussion and the recommendations from #8673, as long as these logical operations ensure operand clocks are consistent, there's no need to explicitly distinguish "clocked" versions of and/or. This will make the API simpler and the type system clearer.
Thank you again for your insightful suggestions!
2 participants
This pr partially implement the issue #8673
LTL Dialect Explicit Clocking Model Refactoring
Problem and Motivation
The original LTL dialect uses implicit clock inference, violating IR locality principles. The
ltl.clockoperation creates non-local dependencies, hindering safe transformations.Type Hierarchy
Refactoring Principles
Input Unification: All
clocked_*operations acceptLTLClockedSequenceTypeas inputResult Clock Rules:
ClockEdgeAttrandclockparametersLTLPropertyTypeKey Changes:
ltl.delay→ltl.clocked_delay: From input-dependent to standalone delay objectltl.create_clocked_sequence: Create clocked sequence instead of adding a clock to sequenceCompatibility
sequenceoperations for Immediate Assertion supportltl.create_clocked_sequenceImplementation roadmap:
clocked_sequencewould be rename tosequence, andsequencewould be rename tounclocked_sequenceltl.clock✅input: LTLAnyPropertyTypeedge: ClockEdgeAttrclock: I1LTLSequenceOrPropertyTypeltl.create_clocked_sequenceinput: LTLAnySequenceTypeedge: ClockEdgeAttrclock: I1LTLClockedSequenceTypeltl.and✅inputs: Variadic<LTLAnyPropertyType>LTLAnyPropertyTypeltl.clocked_andinputs: Variadic<LTLClockedSequenceType>edge: ClockEdgeAttrclock: I1LTLClockedSequenceTypeltl.or✅inputs: Variadic<LTLAnyPropertyType>LTLAnyPropertyTypeltl.clocked_orinputs: Variadic<LTLClockedSequenceType>edge: ClockEdgeAttrclock: I1LTLClockedSequenceTypeltl.intersect✅inputs: Variadic<LTLAnyPropertyType>LTLPropertyTypeltl.clocked_intersectinputs: Variadic<LTLClockedSequenceType>edge: ClockEdgeAttrclock: I1LTLClockedSequenceTypeltl.concat✅inputs: Variadic<LTLAnySequenceType>LTLSequenceTypeltl.clocked_concatinputs: Variadic<LTLClockedSequenceType>edge: ClockEdgeAttrclock: I1LTLClockedSequenceTypeltl.delay❌input: LTLAnySequenceTypedelay: I64Attrlength: OptionalAttr<I64Attr>LTLSequenceTypeltl.clocked_delayinput: LTLClockedSequenceTypeedge: ClockEdgeAttrclock: I1delay: I64Attrlength: OptionalAttr<I64Attr>LTLClockedSequenceTypeltl.repeat✅input: LTLAnySequenceTypebase: I64Attrmore: OptionalAttr<I64Attr>LTLSequenceTypeltl.clocked_repeatinput: LTLClockedSequenceTypebase: I64Attrmore: OptionalAttr<I64Attr>LTLClockedSequenceTypeltl.goto_repeat✅input: LTLAnySequenceTypebase: I64Attrmore: I64AttrLTLSequenceTypeltl.clocked_goto_repeatinput: LTLClockedSequenceTypebase: I64Attrmore: I64AttrLTLClockedSequenceTypeltl.non_consecutive_repeat✅input: LTLAnySequenceTypebase: I64Attrmore: I64AttrLTLSequenceTypeltl.clocked_non_consecutive_repeatinput: LTLClockedSequenceTypebase: I64Attrmore: I64AttrLTLClockedSequenceType✅ indicates retention, ❌ indicates removal