@@ -61,46 +61,96 @@ 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 : I32EnumAttr<"ClockEdge", "clock edge",
78+ [AtPosEdge, AtNegEdge, AtEdge]> {
79+ let cppNamespace = "circt::ltl";
80+ }
81+
82+ def ClockOp : LTLOp<"clock", [
83+ Pure, InferTypeOpInterface, DeclareOpInterfaceMethods<InferTypeOpInterface>
84+ ]> {
85+ let arguments = (ins LTLAnyPropertyType:$input, ClockEdgeAttr:$edge, I1:$clock);
86+ let results = (outs LTLSequenceOrPropertyType:$result);
87+ let assemblyFormat = [{
88+ $input `,` $edge $clock attr-dict `:` type($input)
89+ }];
90+
91+ let summary = "Specify the clock for a property or sequence.";
92+ let description = [{
93+ Specifies the `$edge` on a given `$clock` to be the clock for an `$input`
94+ property or sequence. All cycle delays in the `$input` implicitly refer to a
95+ clock that advances the state to the next cycle. The `ltl.clock` operation
96+ provides that clock. The clock applies to the entire property or sequence
97+ expression tree below `$input`, up to any other nested `ltl.clock`
98+ operations.
99+
100+ The operation returns a property if the `$input` is a property, and a
101+ sequence otherwise.
102+ }];
103+ }
104+
64105//===----------------------------------------------------------------------===//
65106// Sequences
66107//===----------------------------------------------------------------------===//
67108
68109def DelayOp : LTLOp<"delay", [Pure]> {
69- let arguments = (ins
70- LTLAnySequenceType:$input,
71- I64Attr:$delay,
72- OptionalAttr<I64Attr>:$length);
110+ // Require an explicit clock SSA operand. The clock is now an operand
111+ // (e.g. `%clk`) and must be provided when creating a delay. The edge is
112+ // specified as a `ClockEdgeAttr` operand. The assembly places the clock
113+ // first to make the clocking context explicit at the call site.
114+ let arguments = (ins
115+ I1:$clock,
116+ ClockEdgeAttr:$edge,
117+ LTLAnySequenceType:$input,
118+ I64Attr:$delay,
119+ OptionalAttr<I64Attr>:$length);
73120 let results = (outs LTLSequenceType:$result);
74121 let assemblyFormat = [{
75- $input `,` $delay (`,` $length^)? attr-dict `:` type($input)
122+ $clock `,` $edge `,` $ input `,` $delay (`,` $length^)? attr-dict `:` type($input)
76123 }];
77124 let hasFolder = 1;
78125 let hasCanonicalizer = 1;
79126
80127 let summary = "Delay a sequence by a number of cycles.";
81128 let description = [{
82- Delays the `$input` sequence by the number of cycles specified by `$delay`.
83- The delay must be greater than or equal to zero. The optional `$length`
84- specifies during how many cycles after the initial delay the sequence can
85- match. Omitting `$length` indicates an unbounded but finite delay. For
86- example:
87-
88- - `ltl.delay %seq, 2, 0` delays `%seq` by exactly 2 cycles. The resulting
89- sequence matches if `%seq` matches exactly 2 cycles in the future.
90- - `ltl.delay %seq, 2, 2` delays `%seq` by 2, 3, or 4 cycles. The resulting
91- sequence matches if `%seq` matches 2, 3, or 4 cycles in the future.
92- - `ltl.delay %seq, 2` delays `%seq` by 2 or more cycles. The number of
93- cycles is unbounded but finite, which means that `%seq` *has* to match at
94- some point, instead of effectively never occuring by being delayed an
95- infinite number of cycles.
96- - `ltl.delay %seq, 0, 0` is equivalent to just `%seq`.
129+ Delays the `$input` sequence by the number of cycles specified by `$delay` on
130+ the given `$clock` operand and `$edge` operand. The clock must be passed
131+ as an explicit SSA operand (for example `%clk`). The delay must be greater
132+ than or equal to zero. The optional `$length` specifies during how many
133+ cycles after the initial delay the sequence can match. Omitting `$length`
134+ indicates an unbounded but finite delay. For example:
135+
136+ - `ltl.delay %clk, posedge, %seq, 2, 0` delays `%seq` by exactly 2 cycles on
137+ the positive edge of `%clk`. The resulting sequence matches if `%seq`
138+ matches exactly 2 cycles in the future.
139+ - `ltl.delay %clk, posedge, %seq, 2, 2` delays `%seq` by 2, 3, or 4 cycles on
140+ the positive edge of `%clk`. The resulting sequence matches if `%seq`
141+ matches 2, 3, or 4 cycles in the future.
142+ - `ltl.delay %clk, posedge, %seq, 2` delays `%seq` by 2 or more cycles on the
143+ positive edge of `%clk`. The number of cycles is unbounded but finite, which
144+ means that `%seq` *has* to match at some point, instead of effectively never
145+ occuring by being delayed an infinite number of cycles.
146+ - `ltl.delay %clk, posedge, %seq, 0, 0` is equivalent to just `%seq`.
97147
98148 #### Clocking
99149
100- The cycle delay specified on the operation refers to a clocking event. This
101- event is not directly specified by the delay operation itself. Instead, the
102- [`ltl. clock`](#ltlclock-circtltlclockop) operation can be used to associate
103- all delays within a sequence with a clock .
150+ The cycle delay now explicitly refers to the `$clock` SSA operand and the
151+ `$edge` attribute. There is no implicit clock inference for delays; callers
152+ must provide the desired clock. Backends should discover the clock for a
153+ larger sequence by scanning its subtree for such explicit clocked delays .
104154 }];
105155}
106156
@@ -346,45 +396,4 @@ def EventuallyOp : LTLOp<"eventually", [Pure]> {
346396 }];
347397}
348398
349- //===----------------------------------------------------------------------===//
350- // Clocking
351- //===----------------------------------------------------------------------===//
352-
353- // Edge behavior enum for always block. See SV Spec 9.4.2.
354-
355- /// AtPosEdge triggers on a rise from 0 to 1/X/Z, or X/Z to 1.
356- def AtPosEdge: I32EnumAttrCase<"Pos", 0, "posedge">;
357- /// AtNegEdge triggers on a drop from 1 to 0/X/Z, or X/Z to 0.
358- def AtNegEdge: I32EnumAttrCase<"Neg", 1, "negedge">;
359- /// AtEdge is syntactic sugar for AtPosEdge or AtNegEdge.
360- def AtEdge : I32EnumAttrCase<"Both", 2, "edge">;
361-
362- def ClockEdgeAttr : I32EnumAttr<"ClockEdge", "clock edge",
363- [AtPosEdge, AtNegEdge, AtEdge]> {
364- let cppNamespace = "circt::ltl";
365- }
366-
367- def ClockOp : LTLOp<"clock", [
368- Pure, InferTypeOpInterface, DeclareOpInterfaceMethods<InferTypeOpInterface>
369- ]> {
370- let arguments = (ins LTLAnyPropertyType:$input, ClockEdgeAttr:$edge, I1:$clock);
371- let results = (outs LTLSequenceOrPropertyType:$result);
372- let assemblyFormat = [{
373- $input `,` $edge $clock attr-dict `:` type($input)
374- }];
375-
376- let summary = "Specify the clock for a property or sequence.";
377- let description = [{
378- Specifies the `$edge` on a given `$clock` to be the clock for an `$input`
379- property or sequence. All cycle delays in the `$input` implicitly refer to a
380- clock that advances the state to the next cycle. The `ltl.clock` operation
381- provides that clock. The clock applies to the entire property or sequence
382- expression tree below `$input`, up to any other nested `ltl.clock`
383- operations.
384-
385- The operation returns a property if the `$input` is a property, and a
386- sequence otherwise.
387- }];
388- }
389-
390399#endif // CIRCT_DIALECT_LTL_LTLOPS_TD
0 commit comments