Skip to content

Commit d18a2d2

Browse files
Clo91eafClo91eaf
committed
[LTL][SVA] Add explict clocked operations and types
- Introduced new clocked operations: ClockedAndOp, ClockedOrOp, ClockedIntersectOp, CreateClockedSequenceOp, ClockedDelayOp, ClockedConcatOp, and ClockedImplicationOp. - Added LTLClockedSequenceType to represent clocked sequences. - Updated LTLTypes and LTLVisitors to support new clocked operations.
1 parent bbe2444 commit d18a2d2

File tree

4 files changed

+318
-50
lines changed

4 files changed

+318
-50
lines changed

‎include/circt/Dialect/LTL/LTLOps.td‎

Lines changed: 223 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -61,10 +61,183 @@ def IntersectOp : AssocLTLOp<"intersect"> {
6161
let hasCanonicalizeMethod = 1;
6262
}
6363

64+
//===----------------------------------------------------------------------===//
65+
// Clocking
66+
//===----------------------------------------------------------------------===//
67+
68+
// Edge behavior enum for always block. See SV Spec 9.4.2.
69+
70+
/// AtPosEdge triggers on a rise from 0 to 1/X/Z, or X/Z to 1.
71+
def AtPosEdge : I32EnumAttrCase<"Pos", 0, "posedge">;
72+
/// AtNegEdge triggers on a drop from 1 to 0/X/Z, or X/Z to 0.
73+
def AtNegEdge : I32EnumAttrCase<"Neg", 1, "negedge">;
74+
/// AtEdge is syntactic sugar for AtPosEdge or AtNegEdge.
75+
def AtEdge : I32EnumAttrCase<"Both", 2, "edge">;
76+
77+
def ClockEdgeAttr
78+
: I32EnumAttr<"ClockEdge", "clock edge", [AtPosEdge, AtNegEdge, AtEdge]> {
79+
let cppNamespace = "circt::ltl";
80+
}
81+
82+
def ClockOp : LTLOp<"clock", [Pure, InferTypeOpInterface,
83+
DeclareOpInterfaceMethods<InferTypeOpInterface>]> {
84+
let arguments = (ins
85+
LTLAnyPropertyType:$input,
86+
ClockEdgeAttr:$edge,
87+
I1:$clock);
88+
let results = (outs LTLSequenceOrPropertyType:$result);
89+
let assemblyFormat = [{
90+
$input `,` $edge $clock attr-dict `:` type($input)
91+
}];
92+
93+
let summary = "Specify the clock for a property or sequence.";
94+
let description = [{
95+
Specifies the `$edge` on a given `$clock` to be the clock for an `$input`
96+
property or sequence. All cycle delays in the `$input` implicitly refer to a
97+
clock that advances the state to the next cycle. The `ltl.clock` operation
98+
provides that clock. The clock applies to the entire property or sequence
99+
expression tree below `$input`, up to any other nested `ltl.clock`
100+
operations.
101+
102+
The operation returns a property if the `$input` is a property, and a
103+
sequence otherwise.
104+
}];
105+
}
106+
64107
//===----------------------------------------------------------------------===//
65108
// Sequences
66109
//===----------------------------------------------------------------------===//
67110

111+
def CreateClockedSequenceOp : LTLOp<"create_clocked_sequence", [Pure]> {
112+
let arguments = (ins
113+
LTLAnySequenceType:$input,
114+
ClockEdgeAttr:$edge,
115+
I1:$clock);
116+
let results = (outs LTLClockedSequenceType:$result);
117+
let assemblyFormat = [{
118+
$input `,` $edge $clock attr-dict `:` type($input)
119+
}];
120+
121+
let summary = "Create an explicitly clocked sequence from input "
122+
"sequences/booleans.";
123+
let description = [{
124+
Creates an explicitly clocked sequence by binding a single input sequence
125+
or boolean value to a specific clock edge. This operation is fundamental to
126+
the explicit clocking model, ensuring that all temporal operations have
127+
well-defined clock semantics.
128+
}];
129+
}
130+
131+
def ClockedAndOp : LTLOp<"clocked_and", [Pure, Commutative]> {
132+
let arguments = (ins
133+
Variadic<LTLAnyClockedSequenceType>:$inputs,
134+
ClockEdgeAttr:$edge,
135+
I1:$clock);
136+
let results = (outs LTLClockedSequenceType:$result);
137+
let assemblyFormat = [{
138+
$edge $clock `,` $inputs attr-dict `:` type($inputs)
139+
}];
140+
let hasCanonicalizeMethod = 1;
141+
142+
let summary = "A conjunction of explicitly clocked sequences with a "
143+
"specified clock domain.";
144+
let description = [{
145+
Computes the logical AND of explicitly clocked sequences, binding the
146+
result to a newly specified clock domain (`$edge`, `$clock`). All
147+
input sequences must share the same clock, but the result is explicitly
148+
re-clocked to the provided clock domain, regardless of the input clocks.
149+
150+
Boolean inputs are implicitly lifted to zero-length clocked sequences
151+
with the specified clock.
152+
153+
This operation is useful for clock domain crossing or for enforcing a
154+
new clock context on the conjunction result.
155+
}];
156+
}
157+
158+
def ClockedOrOp : LTLOp<"clocked_or", [Pure, Commutative]> {
159+
let arguments = (ins
160+
Variadic<LTLAnyClockedSequenceType>:$inputs,
161+
ClockEdgeAttr:$edge,
162+
I1:$clock);
163+
let results = (outs LTLClockedSequenceType:$result);
164+
let assemblyFormat = [{
165+
$edge $clock `,` $inputs attr-dict `:` type($inputs)
166+
}];
167+
let hasCanonicalizeMethod = 1;
168+
169+
let summary = "A disjunction of explicitly clocked sequences with a specified clock domain.";
170+
let description = [{
171+
Computes the logical OR of explicitly clocked sequences, binding the result
172+
to a newly specified clock domain (`$edge`, `$clock`). All input sequences
173+
must share the same clock, but the result is explicitly re-clocked to the
174+
provided clock domain, regardless of the input clocks.
175+
176+
Boolean inputs are implicitly lifted to zero-length clocked sequences with
177+
the specified clock.
178+
179+
This operation is useful for clock domain crossing or for enforcing a new
180+
clock context on the disjunction result.
181+
}];
182+
}
183+
184+
def ClockedIntersectOp : LTLOp<"clocked_intersect", [Pure, Commutative]> {
185+
let arguments = (ins
186+
Variadic<LTLAnyClockedSequenceType>:$inputs,
187+
ClockEdgeAttr:$edge,
188+
I1:$clock);
189+
let results = (outs LTLClockedSequenceType:$result);
190+
let assemblyFormat = [{
191+
$edge $clock `,` $inputs attr-dict `:` type($inputs)
192+
}];
193+
let hasCanonicalizeMethod = 1;
194+
195+
let summary = "Intersection of explicitly clocked sequences with a specified clock domain.";
196+
let description = [{
197+
Computes the intersection of explicitly clocked sequences, binding the result to a newly
198+
specified clock domain (`$edge`, `$clock`). All input sequences must share the same clock,
199+
but the result is explicitly re-clocked to the provided clock domain, regardless of the input clocks.
200+
201+
This operation checks that all input sequences hold and have the same start and end times
202+
in the new clock domain. It differs from `ltl.clocked_and` by considering the timing of each operand.
203+
}];
204+
}
205+
206+
def ClockedDelayOp : LTLOp<"clocked_delay", [Pure]> {
207+
let arguments = (ins
208+
ClockEdgeAttr:$edge,
209+
I1:$clock,
210+
I64Attr:$delay,
211+
OptionalAttr<I64Attr>:$length);
212+
let results = (outs LTLClockedSequenceType:$result);
213+
let assemblyFormat = [{
214+
$edge $clock `,` $delay (`,` $length^)? attr-dict
215+
}];
216+
217+
let summary = "Create an explicitly clocked delay sequence.";
218+
let description = [{
219+
Creates a standalone "pure delay" sequence that is explicitly bound to a
220+
specific clock. This sequence evaluates to true immediately and matches
221+
after the specified number of clock ticks.
222+
223+
The `$delay` specifies the number of clock cycles to delay, and the optional
224+
`$length` specifies the range of cycles during which the delay can match.
225+
Omitting `$length` indicates an unbounded but finite delay.
226+
227+
Examples:
228+
- `ltl.clocked_delay posedge %clk, 2, 0` creates a delay that matches
229+
exactly 2 cycles after the current time on the positive edge of %clk.
230+
- `ltl.clocked_delay posedge %clk, 2, 2` creates a delay that matches
231+
2, 3, or 4 cycles after the current time.
232+
- `ltl.clocked_delay posedge %clk, 2` creates an unbounded but finite
233+
delay of 2 or more cycles.
234+
235+
This operation enables clean lowering of SVA expressions like `a ##1 b`
236+
by representing the `##1` as a first-class clocked sequence object that
237+
can be composed with `ltl.concat`.
238+
}];
239+
}
240+
68241
def DelayOp : LTLOp<"delay", [Pure]> {
69242
let arguments = (ins
70243
LTLAnySequenceType:$input,
@@ -119,6 +292,27 @@ def PastOp : LTLOp<"past", [Pure]> {
119292
}];
120293
}
121294

295+
def ClockedConcatOp : LTLOp<"clocked_concat", [Pure]> {
296+
let arguments = (ins
297+
Variadic<LTLAnyClockedSequenceType>:$inputs,
298+
ClockEdgeAttr:$edge,
299+
I1:$clock);
300+
let results = (outs LTLClockedSequenceType:$result);
301+
let assemblyFormat = [{
302+
$edge $clock `,` $inputs attr-dict `:` type($inputs)
303+
}];
304+
let hasFolder = 1;
305+
let hasCanonicalizer = 1;
306+
307+
let summary = "Concatenate explicitly clocked sequences with a specified clock domain.";
308+
let description = [{
309+
Concatenate multiple explicitly clocked sequences into a longer sequence,
310+
binding the result to a newly specified clock domain (`$edge`, `$clock`).
311+
All input sequences must share the same clock, but the result is explicitly
312+
re-clocked to the provided clock domain, regardless of the input clocks.
313+
}];
314+
}
315+
122316
def ConcatOp : LTLOp<"concat", [Pure]> {
123317
let arguments = (ins Variadic<LTLAnySequenceType>:$inputs);
124318
let results = (outs LTLSequenceType:$result);
@@ -248,6 +442,35 @@ def NonConsecutiveRepeatOp : LTLOp<"non_consecutive_repeat", [Pure]> {
248442
}];
249443
}
250444

445+
def ClockedImplicationOp : LTLOp<"clocked_implication", [Pure]> {
446+
let arguments = (ins
447+
LTLAnyClockedSequenceType:$antecedent,
448+
LTLAnyClockedSequenceType:$consequent,
449+
ClockEdgeAttr:$edge,
450+
I1:$clock);
451+
let results = (outs LTLPropertyType:$result);
452+
let assemblyFormat = [{
453+
$antecedent `,` $consequent `,` $edge $clock attr-dict `:` type($antecedent) `,` type($consequent)
454+
}];
455+
456+
let summary = "Cross-domain property assertion with explicit clocking.";
457+
let description = [{
458+
Creates a clock-agnostic property that asserts a relationship between
459+
two explicitly clocked sequences. The `$antecedent` and `$consequent`
460+
sequences can have different clocks, enabling cross-domain verification.
461+
462+
The `$edge` and `$clock` specify the clock domain for the property assertion.
463+
464+
This operation is crucial for Clock Domain Crossing (CDC) verification.
465+
Unlike the traditional implication, the clocked version explicitly handles
466+
the case where temporal patterns in different clock domains need to be
467+
related. The resulting property is clock-agnostic and represents a
468+
quantified statement about the relationship between the two sequences.
469+
470+
Example: A request in one clock domain must be followed by an acknowledgment
471+
in another clock domain within a certain time window.
472+
}];
473+
}
251474

252475
//===----------------------------------------------------------------------===//
253476
// Properties
@@ -322,45 +545,4 @@ def EventuallyOp : LTLOp<"eventually", [Pure]> {
322545
}];
323546
}
324547

325-
//===----------------------------------------------------------------------===//
326-
// Clocking
327-
//===----------------------------------------------------------------------===//
328-
329-
// Edge behavior enum for always block. See SV Spec 9.4.2.
330-
331-
/// AtPosEdge triggers on a rise from 0 to 1/X/Z, or X/Z to 1.
332-
def AtPosEdge: I32EnumAttrCase<"Pos", 0, "posedge">;
333-
/// AtNegEdge triggers on a drop from 1 to 0/X/Z, or X/Z to 0.
334-
def AtNegEdge: I32EnumAttrCase<"Neg", 1, "negedge">;
335-
/// AtEdge is syntactic sugar for AtPosEdge or AtNegEdge.
336-
def AtEdge : I32EnumAttrCase<"Both", 2, "edge">;
337-
338-
def ClockEdgeAttr : I32EnumAttr<"ClockEdge", "clock edge",
339-
[AtPosEdge, AtNegEdge, AtEdge]> {
340-
let cppNamespace = "circt::ltl";
341-
}
342-
343-
def ClockOp : LTLOp<"clock", [
344-
Pure, InferTypeOpInterface, DeclareOpInterfaceMethods<InferTypeOpInterface>
345-
]> {
346-
let arguments = (ins LTLAnyPropertyType:$input, ClockEdgeAttr:$edge, I1:$clock);
347-
let results = (outs LTLSequenceOrPropertyType:$result);
348-
let assemblyFormat = [{
349-
$input `,` $edge $clock attr-dict `:` type($input)
350-
}];
351-
352-
let summary = "Specify the clock for a property or sequence.";
353-
let description = [{
354-
Specifies the `$edge` on a given `$clock` to be the clock for an `$input`
355-
property or sequence. All cycle delays in the `$input` implicitly refer to a
356-
clock that advances the state to the next cycle. The `ltl.clock` operation
357-
provides that clock. The clock applies to the entire property or sequence
358-
expression tree below `$input`, up to any other nested `ltl.clock`
359-
operations.
360-
361-
The operation returns a property if the `$input` is a property, and a
362-
sequence otherwise.
363-
}];
364-
}
365-
366548
#endif // CIRCT_DIALECT_LTL_LTLOPS_TD

‎include/circt/Dialect/LTL/LTLTypes.td‎

Lines changed: 36 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -28,22 +28,50 @@ def LTLSequenceType : LTLTypeDef<"Sequence", "sequence"> {
2828
}];
2929
}
3030

31+
def LTLClockedSequenceType : LTLTypeDef<"ClockedSequence", "clocked_sequence"> {
32+
let summary = "LTL clocked sequence type";
33+
let description = [{
34+
The `ltl.clocked_sequence` type is the fundamental type for representing
35+
temporal sequences in linear temporal logic, for example, *"on the rising
36+
edge of clk, A is true two cycles after B is true"*.
37+
38+
This type intrinsically carries its clocking context, explicitly binding a
39+
temporal sequence of events to a specific clock. Operations like ltl.concat,
40+
ltl.and, and ltl.or operate on `ltl.clocked_sequence` operands, ensuring
41+
all sequence operands share the same clock. This makes clock domains
42+
explicit and type-checked, preventing errors and clarifying clock domains
43+
for analysis passes.
44+
45+
Boolean inputs (`i1`) are implicitly lifted to a zero-length clocked
46+
sequence. Operations that accept a clocked sequence as an operand will use
47+
the `AnyClockedSequence` constraint, which also accepts `i1`.
48+
}];
49+
}
50+
3151
def LTLPropertyType : LTLTypeDef<"Property", "property"> {
3252
let summary = "LTL property type";
3353
let description = [{
34-
The `ltl.property` type represents a verifiable property built from linear
35-
temporal logic sequences and quantifiers, for example, *"if you see sequence
36-
A, eventually you will see sequence B"*.
37-
38-
Note that this type explicitly identifies a *property*. However, a boolean
39-
value (`i1`) or a sequence (`ltl.sequence`) is also a valid property.
40-
Operations that accept a property as an operand will use the `AnyProperty`
41-
constraint, which also accepts `ltl.sequence` and `i1`.
54+
The `ltl.property` type represents a clock-agnostic, verifiable property
55+
built from explicitly clocked sequences and quantifiers, for example, *"if
56+
you see sequence A, eventually you will see sequence B"*.
57+
58+
This type is fundamentally clock-independent - it represents a quantified
59+
statement about explicitly clocked sequences rather than being a clocked
60+
entity itself. The "lifting" from clocked sequences to clock-agnostic
61+
properties occurs via property operators like `ltl.implication`,
62+
`ltl.always`, and `ltl.eventually`.
63+
64+
Properties can describe relationships between temporal patterns that may
65+
exist in different clock domains, enabling cross-domain verification.
4266
}];
4367
}
4468

4569
def LTLAnySequenceType : AnyTypeOf<[I1, LTLSequenceType]>;
4670
def LTLAnyPropertyType : AnyTypeOf<[I1, LTLSequenceType, LTLPropertyType]>;
4771
def LTLSequenceOrPropertyType : AnyTypeOf<[LTLSequenceType, LTLPropertyType]>;
4872

73+
def LTLAnyClockedSequenceType : AnyTypeOf<[I1, LTLClockedSequenceType]>;
74+
def LTLAnyClockedPropertyType : AnyTypeOf<[I1, LTLClockedSequenceType, LTLPropertyType]>;
75+
def LTLClockedSequenceOrPropertyType : AnyTypeOf<[LTLClockedSequenceType, LTLPropertyType]>;
76+
4977
#endif // CIRCT_DIALECT_LTL_LTLTYPES_TD

‎include/circt/Dialect/LTL/LTLVisitors.h‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,10 @@ class Visitor {
2323
return TypeSwitch<Operation *, ResultType>(op)
2424
.template Case<AndOp, OrOp, DelayOp, ConcatOp, RepeatOp, NotOp,
2525
ImplicationOp, UntilOp, EventuallyOp, ClockOp,
26-
IntersectOp, NonConsecutiveRepeatOp, GoToRepeatOp>(
26+
ClockedAndOp, ClockedOrOp, ClockedIntersectOp,
27+
CreateClockedSequenceOp, ClockedDelayOp, ClockedConcatOp,
28+
ClockedImplicationOp, IntersectOp,
29+
NonConsecutiveRepeatOp, GoToRepeatOp>(
2730
[&](auto op) -> ResultType {
2831
return thisCast->visitLTL(op, args...);
2932
})
@@ -62,6 +65,13 @@ class Visitor {
6265
HANDLE(IntersectOp, Unhandled);
6366
HANDLE(NonConsecutiveRepeatOp, Unhandled);
6467
HANDLE(GoToRepeatOp, Unhandled);
68+
HANDLE(ClockedAndOp, Unhandled);
69+
HANDLE(ClockedOrOp, Unhandled);
70+
HANDLE(ClockedIntersectOp, Unhandled);
71+
HANDLE(CreateClockedSequenceOp, Unhandled);
72+
HANDLE(ClockedDelayOp, Unhandled);
73+
HANDLE(ClockedConcatOp, Unhandled);
74+
HANDLE(ClockedImplicationOp, Unhandled);
6575
#undef HANDLE
6676
};
6777

0 commit comments

Comments
 (0)