Skip to content

Commit 206be23

Browse files
Clo91eafClo91eaf
committed
[LTL] Update documentation and tests for ClockedDelayOp
- Document ClockedDelayOp syntax, semantics, and examples in LTL.md. - Update DelayOp docs to clarify purely unclocked semantics. - Add ClockedDelayOp roundtrip tests to basic.mlir. - Update canonicalization.mlir for ClockedDelayOp fold patterns.
1 parent 78b086f commit 206be23

File tree

3 files changed

+128
-6
lines changed

3 files changed

+128
-6
lines changed

‎docs/Dialects/LTL.md‎

Lines changed: 30 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -160,6 +160,32 @@ Sequence and property expressions in SVAs can specify a clock with respect to wh
160160
- `@(negedge clk) seqOrProp`. **Trigger on high-to-low clock edge.** Equivalent to `ltl.clock %seqOrProp, negedge %clk`.
161161
- `@(edge clk) seqOrProp`. **Trigger on any clock edge.** Equivalent to `ltl.clock %seqOrProp, edge %clk`.
162162

163+
#### Delay clocking
164+
165+
`ltl.delay` takes the delayed input first, followed by the delay window:
166+
167+
```
168+
ltl.delay %input, <delay>[, <length>]
169+
```
170+
171+
For explicitly clocked delays, use `ltl.clocked_delay`:
172+
173+
```
174+
ltl.clocked_delay %clock, <edge>, %input, <delay>[, <length>]
175+
```
176+
177+
`%clock` is an `i1` value (e.g. a module clock); `<edge>` is `posedge`, `negedge`, or `edge`. For example, `ltl.clocked_delay %clk, posedge, %s, 3` means `%s` must hold 3 cycles later on `%clk` rising edges.
178+
179+
`ltl.delay` is unclocked and may be resolved by an enclosing `ltl.clock` or by the `InferLTLClocks` pass. `ltl.clock` globally associates a sequence/property with a clock/edge; `ltl.clocked_delay` carries an explicit per-delay clock.
180+
181+
Examples:
182+
183+
```mlir
184+
ltl.delay %s, 3
185+
ltl.delay %s, 3, 0
186+
ltl.clocked_delay %clk, posedge, %s, 3, 0
187+
```
188+
163189

164190
### Disable Iff
165191

@@ -273,13 +299,13 @@ where the `logic_to_int` conversion is only necessary if `%cond` is 4-valued.
273299
```mlir
274300
%ds1 = ltl.delay %s1, 1
275301
%s1s2 = ltl.concat %ds1, %s2 : !ltl.sequence
276-
```
302+
```
277303

278304
- **`s1 ##[*] s2`**:
279305
```mlir
280306
%ds1 = ltl.delay %s1, 0
281307
%s1s2 = ltl.concat %ds1, %s2 : !ltl.sequence
282-
```
308+
```
283309

284310
- **`s1 and s2`**:
285311
```mlir
@@ -369,12 +395,12 @@ ltl.not %s1 : !ltl.sequence
369395
- **`nexttime p`**:
370396
```mlir
371397
ltl.delay %p, 1, 0 : !ltl.sequence
372-
```
398+
```
373399

374400
- **`nexttime[n] p`**:
375401
```mlir
376402
ltl.delay %p, n, 0 : !ltl.sequence
377-
```
403+
```
378404

379405
- **`s_nexttime p`**: not really distinguishable from the weak version in CIRCT.
380406
- **`s_nexttime[n] p`**: not really distinguishable from the weak version in CIRCT.

‎test/Dialect/LTL/basic.mlir‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22

33
%true = hw.constant true
44
%c0_i8 = hw.constant 0 : i8
5+
%clk = hw.constant true
56

67
//===----------------------------------------------------------------------===//
78
// Types
@@ -53,8 +54,12 @@ unrealized_conversion_cast %p3 : !ltl.property to index
5354

5455
// CHECK: ltl.delay {{%.+}}, 0 : !ltl.sequence
5556
// CHECK: ltl.delay {{%.+}}, 42, 1337 : !ltl.sequence
57+
// CHECK: ltl.clocked_delay {{%.+}}, posedge, {{%.+}}, 0 : !ltl.sequence
58+
// CHECK: ltl.clocked_delay {{%.+}}, posedge, {{%.+}}, 42, 1337 : !ltl.sequence
5659
ltl.delay %s, 0 : !ltl.sequence
5760
ltl.delay %s, 42, 1337 : !ltl.sequence
61+
ltl.clocked_delay %clk, posedge, %s, 0 : !ltl.sequence
62+
ltl.clocked_delay %clk, posedge, %s, 42, 1337 : !ltl.sequence
5863

5964
// CHECK: ltl.concat {{%.+}} : !ltl.sequence
6065
// CHECK: ltl.concat {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.sequence

‎test/Dialect/LTL/canonicalization.mlir‎

Lines changed: 93 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,8 @@ func.func @DelayFolds(%arg0: !ltl.sequence, %arg1: i1) {
2525

2626
// delay(delay(s, 1, N), 2) -> delay(s, 3)
2727
// N is dropped
28-
// CHECK-NEXT: ltl.delay %arg0, 3 :
29-
// CHECK-NEXT: ltl.delay %arg0, 3 :
28+
// CHECK-NEXT: ltl.delay {{%.+}}, 3 :
29+
// CHECK-NEXT: ltl.delay {{%.+}}, 3 :
3030
// CHECK-NEXT: call
3131
// CHECK-NEXT: call
3232
%3 = ltl.delay %arg0, 1, 0 : !ltl.sequence
@@ -64,6 +64,97 @@ func.func @DelayFolds(%arg0: !ltl.sequence, %arg1: i1) {
6464
return
6565
}
6666

67+
// CHECK-LABEL: @ClockedDelayFolds
68+
// CHECK-SAME: (%[[S:.+]]: !ltl.sequence, %[[I:.+]]: i1, %[[CLK:.+]]: i1)
69+
func.func @ClockedDelayFolds(%arg0: !ltl.sequence, %arg1: i1, %clk: i1) {
70+
// clocked_delay(clk, posedge, s, 0, 0) -> s
71+
// clocked_delay(clk, posedge, i, 0, 0) -> clocked_delay(clk, posedge, i, 0, 0)
72+
// CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[I]], 0, 0 : i1
73+
// CHECK-NEXT: call @Seq(%[[S]])
74+
// CHECK-NEXT: call @Seq({{%.+}})
75+
%0 = ltl.clocked_delay %clk, posedge, %arg0, 0, 0 : !ltl.sequence
76+
%n0 = ltl.clocked_delay %clk, posedge, %arg1, 0, 0 : i1
77+
call @Seq(%0) : (!ltl.sequence) -> ()
78+
call @Seq(%n0) : (!ltl.sequence) -> ()
79+
80+
// Nested clocked delays with same clock/edge: merge delays
81+
// clocked_delay(clk, posedge, clocked_delay(clk, posedge, s, 1), 2)
82+
// -> clocked_delay(clk, posedge, s, 3)
83+
// CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 3 :
84+
// CHECK-NEXT: call
85+
%1 = ltl.clocked_delay %clk, posedge, %arg0, 1 : !ltl.sequence
86+
%2 = ltl.clocked_delay %clk, posedge, %1, 2 : !ltl.sequence
87+
call @Seq(%2) : (!ltl.sequence) -> ()
88+
89+
// Inner has length, outer does not: length dropped
90+
// clocked_delay(clk, posedge, clocked_delay(clk, posedge, s, 1, 42), 2)
91+
// -> clocked_delay(clk, posedge, s, 3)
92+
// CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 3 :
93+
// CHECK-NEXT: call
94+
%3 = ltl.clocked_delay %clk, posedge, %arg0, 1, 42 : !ltl.sequence
95+
%4 = ltl.clocked_delay %clk, posedge, %3, 2 : !ltl.sequence
96+
call @Seq(%4) : (!ltl.sequence) -> ()
97+
98+
// Outer has length, inner does not: length dropped
99+
// clocked_delay(clk, posedge, clocked_delay(clk, posedge, s, 1), 2, 5)
100+
// -> clocked_delay(clk, posedge, s, 3)
101+
// CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 3 :
102+
// CHECK-NEXT: call
103+
%5 = ltl.clocked_delay %clk, posedge, %arg0, 1 : !ltl.sequence
104+
%6 = ltl.clocked_delay %clk, posedge, %5, 2, 5 : !ltl.sequence
105+
call @Seq(%6) : (!ltl.sequence) -> ()
106+
107+
// Both have length: lengths merged
108+
// clocked_delay(clk, posedge, clocked_delay(clk, posedge, s, 1, 2), 3, 5)
109+
// -> clocked_delay(clk, posedge, s, 4, 7)
110+
// CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 4, 7 :
111+
// CHECK-NEXT: call
112+
%7 = ltl.clocked_delay %clk, posedge, %arg0, 1, 2 : !ltl.sequence
113+
%8 = ltl.clocked_delay %clk, posedge, %7, 3, 5 : !ltl.sequence
114+
call @Seq(%8) : (!ltl.sequence) -> ()
115+
116+
// Both have length, outer length is 0: no drop
117+
// clocked_delay(clk, posedge, clocked_delay(clk, posedge, s, 1, 2), 3, 0)
118+
// -> clocked_delay(clk, posedge, s, 4, 2)
119+
// CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 4, 2 :
120+
// CHECK-NEXT: call
121+
%9 = ltl.clocked_delay %clk, posedge, %arg0, 1, 2 : !ltl.sequence
122+
%10 = ltl.clocked_delay %clk, posedge, %9, 3, 0 : !ltl.sequence
123+
call @Seq(%10) : (!ltl.sequence) -> ()
124+
125+
// Different edge: should NOT merge
126+
// CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 1 :
127+
// CHECK-NEXT: ltl.clocked_delay %[[CLK]], negedge, {{%.+}}, 2 :
128+
// CHECK-NEXT: call
129+
%11 = ltl.clocked_delay %clk, posedge, %arg0, 1 : !ltl.sequence
130+
%12 = ltl.clocked_delay %clk, negedge, %11, 2 : !ltl.sequence
131+
call @Seq(%12) : (!ltl.sequence) -> ()
132+
133+
// Different clock: should NOT merge
134+
// CHECK-NEXT: ltl.clocked_delay %[[CLK]], posedge, %[[S]], 1 :
135+
// CHECK-NEXT: ltl.clocked_delay %[[I]], posedge, {{%.+}}, 2 :
136+
// CHECK-NEXT: call
137+
%13 = ltl.clocked_delay %clk, posedge, %arg0, 1 : !ltl.sequence
138+
%14 = ltl.clocked_delay %arg1, posedge, %13, 2 : !ltl.sequence
139+
call @Seq(%14) : (!ltl.sequence) -> ()
140+
141+
return
142+
}
143+
144+
// CHECK-LABEL: @ClockedDelayIntoConcatFolds
145+
// CHECK-SAME: (%[[S0:.+]]: !ltl.sequence, %[[S1:.+]]: !ltl.sequence, %[[CLK:.+]]: i1)
146+
func.func @ClockedDelayIntoConcatFolds(%arg0: !ltl.sequence, %arg1: !ltl.sequence, %clk: i1) {
147+
// clocked_delay(clk, posedge, concat(s0, s1), N, M)
148+
// -> concat(clocked_delay(clk, posedge, s0, N, M), s1)
149+
// CHECK-NEXT: [[TMP:%.+]] = ltl.clocked_delay %[[CLK]], posedge, %[[S0]], 2, 3 :
150+
// CHECK-NEXT: ltl.concat [[TMP]], %[[S1]] :
151+
// CHECK-NEXT: call
152+
%0 = ltl.concat %arg0, %arg1 : !ltl.sequence, !ltl.sequence
153+
%1 = ltl.clocked_delay %clk, posedge, %0, 2, 3 : !ltl.sequence
154+
call @Seq(%1) : (!ltl.sequence) -> ()
155+
return
156+
}
157+
67158
// CHECK-LABEL: @ConcatFolds
68159
func.func @ConcatFolds(%arg0: !ltl.sequence, %arg1: !ltl.sequence, %arg2: !ltl.sequence) {
69160
// concat(s) -> s

0 commit comments

Comments
 (0)