Skip to content

Commit 10be181

Browse files
Clo91eafClo91eaf
committed
[LTL] Update delay operations tests
1 parent 16fcb8c commit 10be181

File tree

6 files changed

+80
-71
lines changed

6 files changed

+80
-71
lines changed

‎test/Conversion/ExportVerilog/prepare-for-emission.mlir‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -258,13 +258,13 @@ module attributes { circt.loweringOptions = "disallowPackedStructAssignments"} {
258258
// wires, where they crash the PrepareForEmission pass. They are always emitted
259259
// inline, so no need to restructure the IR.
260260
// CHECK-LABEL: hw.module @Issue5613
261-
hw.module @Issue5613(in %a: i1, in %b: i1) {
261+
hw.module @Issue5613(in %a: i1, in %b: i1, in %clk: i1) {
262262
verif.assert %2 : !ltl.sequence
263263
%0 = ltl.implication %2, %1 : !ltl.sequence, !ltl.property
264264
%1 = ltl.or %b, %3 : i1, !ltl.property
265265
%2 = ltl.and %b, %4 : i1, !ltl.sequence
266266
%3 = ltl.not %b : i1
267-
%4 = ltl.delay %a, 42 : i1
267+
%4 = ltl.delay %clk, posedge, %a, 42 : i1
268268
hw.output
269269
}
270270

‎test/Conversion/ExportVerilog/verif.mlir‎

Lines changed: 16 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -67,22 +67,22 @@ hw.module @BasicEmissionTemporal(in %a: i1) {
6767
// CHECK-LABEL: module Sequences
6868
hw.module @Sequences(in %clk: i1, in %a: i1, in %b: i1) {
6969
// CHECK: assert property (##0 a);
70-
%d0 = ltl.delay %a, 0, 0 : i1
70+
%d0 = ltl.delay %clk, posedge, %a, 0, 0 : i1
7171
sv.assert_property %d0 : !ltl.sequence
7272
// CHECK: assert property (##4 a);
73-
%d1 = ltl.delay %a, 4, 0 : i1
73+
%d1 = ltl.delay %clk, posedge, %a, 4, 0 : i1
7474
sv.assert_property %d1 : !ltl.sequence
7575
// CHECK: assert property (##[5:6] a);
76-
%d2 = ltl.delay %a, 5, 1 : i1
76+
%d2 = ltl.delay %clk, posedge, %a, 5, 1 : i1
7777
sv.assert_property %d2 : !ltl.sequence
7878
// CHECK: assert property (##[7:$] a);
79-
%d3 = ltl.delay %a, 7 : i1
79+
%d3 = ltl.delay %clk, posedge, %a, 7 : i1
8080
sv.assert_property %d3 : !ltl.sequence
8181
// CHECK: assert property (##[*] a);
82-
%d4 = ltl.delay %a, 0 : i1
82+
%d4 = ltl.delay %clk, posedge, %a, 0 : i1
8383
sv.assert_property %d4 : !ltl.sequence
8484
// CHECK: assert property (##[+] a);
85-
%d5 = ltl.delay %a, 1 : i1
85+
%d5 = ltl.delay %clk, posedge, %a, 1 : i1
8686
sv.assert_property %d5 : !ltl.sequence
8787

8888
// CHECK: assert property (a ##0 a);
@@ -180,11 +180,11 @@ hw.module @Properties(in %clk: i1, in %a: i1, in %b: i1) {
180180
// CHECK: assert property (a ##1 b |=> not a);
181181
%i0 = ltl.implication %a, %b : i1, i1
182182
sv.assert_property %i0 : !ltl.property
183-
%i1 = ltl.delay %b, 1, 0 : i1
183+
%i1 = ltl.delay %clk, posedge, %b, 1, 0 : i1
184184
%i2 = ltl.concat %a, %i1 : i1, !ltl.sequence
185185
%i3 = ltl.implication %i2, %n0 : !ltl.sequence, !ltl.property
186186
sv.assert_property %i3 : !ltl.property
187-
%i4 = ltl.delay %true, 1, 0 : i1
187+
%i4 = ltl.delay %clk, posedge, %true, 1, 0 : i1
188188
%i5 = ltl.concat %a, %i1, %i4 : i1, !ltl.sequence, !ltl.sequence
189189
%i6 = ltl.implication %i5, %n0 : !ltl.sequence, !ltl.property
190190
sv.assert_property %i6 : !ltl.property
@@ -211,14 +211,15 @@ hw.module @Properties(in %clk: i1, in %a: i1, in %b: i1) {
211211

212212
// CHECK-LABEL: module Precedence
213213
hw.module @Precedence(in %a: i1, in %b: i1) {
214+
%true = hw.constant true
214215
// CHECK: assert property ((a or ##0 b) and b);
215-
%a0 = ltl.delay %b, 0, 0 : i1
216+
%a0 = ltl.delay %true, posedge, %b, 0, 0 : i1
216217
%a1 = ltl.or %a, %a0 : i1, !ltl.sequence
217218
%a2 = ltl.and %a1, %b : !ltl.sequence, i1
218219
sv.assert_property %a2 : !ltl.sequence
219220

220221
// CHECK: assert property (##1 (a or ##0 b));
221-
%d0 = ltl.delay %a1, 1, 0 : !ltl.sequence
222+
%d0 = ltl.delay %true, posedge, %a1, 1, 0 : !ltl.sequence
222223
sv.assert_property %d0 : !ltl.sequence
223224

224225
// CHECK: assert property (not (a or ##0 b));
@@ -249,8 +250,8 @@ hw.module @SystemVerilogSpecExamples(in %clk: i1, in %a: i1, in %b: i1, in %c: i
249250
// Section 16.7 "Sequences"
250251

251252
// CHECK: assert property (a ##1 b ##0 c ##1 d);
252-
%a0 = ltl.delay %b, 1, 0 : i1
253-
%a1 = ltl.delay %d, 1, 0 : i1
253+
%a0 = ltl.delay %clk, posedge, %b, 1, 0 : i1
254+
%a1 = ltl.delay %clk, posedge, %d, 1, 0 : i1
254255
%a2 = ltl.concat %a, %a0 : i1, !ltl.sequence
255256
%a3 = ltl.concat %c, %a1 : i1, !ltl.sequence
256257
%a4 = ltl.concat %a2, %a3 : !ltl.sequence, !ltl.sequence
@@ -259,7 +260,7 @@ hw.module @SystemVerilogSpecExamples(in %clk: i1, in %a: i1, in %b: i1, in %c: i
259260
// Section 16.12.20 "Property examples"
260261

261262
// CHECK: assert property (@(posedge clk) a |-> b ##1 c ##1 d);
262-
%b0 = ltl.delay %c, 1, 0 : i1
263+
%b0 = ltl.delay %clk, posedge, %c, 1, 0 : i1
263264
%b1 = ltl.concat %b, %b0, %a1 : i1, !ltl.sequence, !ltl.sequence
264265
%b2 = ltl.implication %a, %b1 : i1, !ltl.sequence
265266
%b3 = ltl.clock %b2, posedge %clk : !ltl.property
@@ -272,7 +273,7 @@ hw.module @SystemVerilogSpecExamples(in %clk: i1, in %a: i1, in %b: i1, in %c: i
272273
sv.assert_property %c3 disable_iff %e : !ltl.property
273274

274275
// CHECK: assert property (##1 a |-> b);
275-
%d0 = ltl.delay %a, 1, 0 : i1
276+
%d0 = ltl.delay %clk, posedge, %a, 1, 0 : i1
276277
%d1 = ltl.implication %d0, %b : !ltl.sequence, i1
277278
sv.assert_property %d1 : !ltl.property
278279
}
@@ -295,7 +296,7 @@ hw.module @LivenessExample(in %clock: i1, in %reset: i1, in %isLive: i1) {
295296

296297
// CHECK: assert property (disable iff (reset) @(posedge clock) isLive ##1 _GEN |-> (s_eventually isLive));
297298
// CHECK-NEXT: assume property (disable iff (reset) @(posedge clock) isLive ##1 _GEN |-> (s_eventually isLive));
298-
%4 = ltl.delay %not_isLive, 1, 0 : i1
299+
%4 = ltl.delay %clock, posedge, %not_isLive, 1, 0 : i1
299300
%5 = ltl.concat %isLive, %4 : i1, !ltl.sequence
300301
%6 = ltl.implication %5, %1 : !ltl.sequence, !ltl.property
301302
%liveness_after_fall = ltl.clock %6, posedge %clock : !ltl.property

‎test/Conversion/FIRRTLToHW/intrinsics.mlir‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -62,9 +62,11 @@ firrtl.circuit "Intrinsics" {
6262
// CHECK-LABEL: hw.module @LTLAndVerif
6363
firrtl.module @LTLAndVerif(in %clk: !firrtl.clock, in %a: !firrtl.uint<1>, in %b: !firrtl.uint<1>) {
6464
// CHECK-NEXT: [[CLK:%.+]] = seq.from_clock %clk
65-
// CHECK-NEXT: [[D0:%.+]] = ltl.delay %a, 42 : i1
65+
// CHECK-NEXT: {{%.*}} = hw.constant true
66+
// CHECK-NEXT: [[D0:%.+]] = ltl.delay {{%.*}}, posedge, %a, 42 : i1
6667
%d0 = firrtl.int.ltl.delay %a, 42 : (!firrtl.uint<1>) -> !firrtl.uint<1>
67-
// CHECK-NEXT: [[D1:%.+]] = ltl.delay %b, 42, 1337 : i1
68+
// CHECK-NEXT: {{%.*}} = hw.constant true
69+
// CHECK-NEXT: [[D1:%.+]] = ltl.delay {{%.*}}, posedge, %b, 42, 1337 : i1
6870
%d1 = firrtl.int.ltl.delay %b, 42, 1337 : (!firrtl.uint<1>) -> !firrtl.uint<1>
6971

7072
// CHECK-NEXT: [[L0:%.+]] = ltl.and [[D0]], [[D1]] : !ltl.sequence, !ltl.sequence
@@ -177,7 +179,8 @@ firrtl.circuit "Intrinsics" {
177179
firrtl.matchingconnect %d, %1 : !firrtl.uint<1>
178180

179181
// !ltl.sequence
180-
// CHECK-NEXT: [[C]] = ltl.delay %a, 42 : i1
182+
// CHECK-NEXT: {{%.*}} = hw.constant true
183+
// CHECK-NEXT: [[C]] = ltl.delay {{%.*}}, posedge, %a, 42 : i1
181184
%0 = firrtl.int.ltl.delay %a, 42 : (!firrtl.uint<1>) -> !firrtl.uint<1>
182185
firrtl.matchingconnect %c, %0 : !firrtl.uint<1>
183186
}

‎test/Conversion/ImportVerilog/basic.sv‎

Lines changed: 21 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -2419,10 +2419,10 @@ module ConcurrentAssert(input clk);
24192419
// CHECK: moore.procedure always
24202420
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
24212421
// CHECK: [[CONV_A:%.+]] = moore.to_builtin_bool [[READ_A]] : i1
2422-
// CHECK: [[DELAY_A:%.+]] = ltl.delay [[CONV_A]], 0, 0 : i1
2422+
// CHECK: [[DELAY_A:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 0, 0 : i1
24232423
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
24242424
// CHECK: [[CONV_B:%.+]] = moore.to_builtin_bool [[READ_B]] : l1
2425-
// CHECK: [[DELAY_B:%.+]] = ltl.delay [[CONV_B]], 0, 0 : i1
2425+
// CHECK: [[DELAY_B:%.+]] = ltl.delay [[PRE:.*]] [[CONV_B]], 0, 0 : i1
24262426
// CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_A]], [[DELAY_B]] : !ltl.sequence, !ltl.sequence
24272427
// CHECK: verif.assert [[CONCAT_OP]] : !ltl.sequence
24282428
// CHECK: moore.return
@@ -2431,13 +2431,13 @@ module ConcurrentAssert(input clk);
24312431
// CHECK: moore.procedure always
24322432
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
24332433
// CHECK: [[CONV_A:%.+]] = moore.to_builtin_bool [[READ_A]] : i1
2434-
// CHECK: [[DELAY_A:%.+]] = ltl.delay [[CONV_A]], 0, 0 : i1
2434+
// CHECK: [[DELAY_A:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 0, 0 : i1
24352435
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
24362436
// CHECK: [[CONV_B:%.+]] = moore.to_builtin_bool [[READ_B]] : l1
2437-
// CHECK: [[DELAY_B:%.+]] = ltl.delay [[CONV_B]], 1 : i1
2437+
// CHECK: [[DELAY_B:%.+]] = ltl.delay [[PRE:.*]] [[CONV_B]], 1 : i1
24382438
// CHECK: [[READ_A2:%.+]] = moore.read [[A]] : <i1>
24392439
// CHECK: [[CONV_A2:%.+]] = moore.to_builtin_bool [[READ_A2]] : i1
2440-
// CHECK: [[DELAY_A2:%.+]] = ltl.delay [[CONV_A2]], 3, 2 : i1
2440+
// CHECK: [[DELAY_A2:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A2]], 3, 2 : i1
24412441
// CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_A]], [[DELAY_B]], [[DELAY_A2]] : !ltl.sequence, !ltl.sequence, !ltl.sequence
24422442
// CHECK: verif.assert [[CONCAT_OP]] : !ltl.sequence
24432443
// CHECK: moore.return
@@ -2480,15 +2480,15 @@ module ConcurrentAssert(input clk);
24802480
// CHECK: moore.procedure always
24812481
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
24822482
// CHECK: [[CONV_A:%.+]] = moore.to_builtin_bool [[READ_A]] : i1
2483-
// CHECK: [[DELAY_OP:%.+]] = ltl.delay [[CONV_A]], 1, 0 : i1
2483+
// CHECK: [[DELAY_OP:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 1, 0 : i1
24842484
// CHECK: verif.assert [[DELAY_OP]] : !ltl.sequence
24852485
// CHECK: moore.return
24862486
// CHECK: }
24872487
assert property (nexttime a);
24882488
// CHECK: moore.procedure always
24892489
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
24902490
// CHECK: [[CONV_A:%.+]] = moore.to_builtin_bool [[READ_A]] : i1
2491-
// CHECK: [[DELAY_OP:%.+]] = ltl.delay [[CONV_A]], 5, 0 : i1
2491+
// CHECK: [[DELAY_OP:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 5, 0 : i1
24922492
// CHECK: verif.assert [[DELAY_OP]] : !ltl.sequence
24932493
// CHECK: moore.return
24942494
// CHECK: }
@@ -2543,8 +2543,8 @@ module ConcurrentAssert(input clk);
25432543
// CHECK: [[CONV_B:%.+]] = moore.to_builtin_bool [[READ_B]] : l1
25442544
// CHECK: [[CONST_T:%.+]] = hw.constant true
25452545
// CHECK: [[REPEAT_T:%.+]] = ltl.repeat [[CONST_T]], 0 : i1
2546-
// CHECK: [[DELAY_RT:%.+]] = ltl.delay [[REPEAT_T]], 1, 0 : !ltl.sequence
2547-
// CHECK: [[DELAY_A:%.+]] = ltl.delay [[CONV_A]], 1, 0 : i1
2546+
// CHECK: [[DELAY_RT:%.+]] = ltl.delay [[PRE:.*]] [[REPEAT_T]], 1, 0 : !ltl.sequence
2547+
// CHECK: [[DELAY_A:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 1, 0 : i1
25482548
// CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_RT]], [[DELAY_A]], [[CONST_T]] : !ltl.sequence, !ltl.sequence, i1
25492549
// CHECK: [[INTER_OP:%.+]] = ltl.intersect [[CONCAT_OP]], [[CONV_B]] : !ltl.sequence, i1
25502550
// CHECK: verif.assert [[INTER_OP]] : !ltl.sequence
@@ -2614,7 +2614,7 @@ module ConcurrentAssert(input clk);
26142614
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
26152615
// CHECK: [[CONV_B:%.+]] = moore.to_builtin_bool [[READ_B]] : l1
26162616
// CHECK: [[CONST_T:%.+]] = hw.constant true
2617-
// CHECK: [[DELAY_OP:%.+]] = ltl.delay [[CONV_A]], 1, 0 : i1
2617+
// CHECK: [[DELAY_OP:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 1, 0 : i1
26182618
// CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_OP]], [[CONST_T]] : !ltl.sequence, i1
26192619
// CHECK: [[IMPLICATION_OP:%.+]] = ltl.implication [[CONCAT_OP]], [[CONV_B]] : !ltl.sequence, i1
26202620
// CHECK: verif.assert [[IMPLICATION_OP]] : !ltl.property
@@ -2640,7 +2640,7 @@ module ConcurrentAssert(input clk);
26402640
// CHECK: [[CONV_B:%.+]] = moore.to_builtin_bool [[READ_B]] : l1
26412641
// CHECK: [[CONST_T:%.+]] = hw.constant true
26422642
// CHECK: [[NOT_OP:%.+]] = ltl.not [[CONV_B]] : i1
2643-
// CHECK: [[DELAY_OP:%.+]] = ltl.delay [[CONV_A]], 1, 0 : i1
2643+
// CHECK: [[DELAY_OP:%.+]] = ltl.delay [[PRE:.*]] [[CONV_A]], 1, 0 : i1
26442644
// CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_OP]], [[CONST_T]] : !ltl.sequence, i1
26452645
// CHECK: [[IMPLICATION_OP:%.+]] = ltl.implication [[CONCAT_OP]], [[NOT_OP]] : !ltl.sequence, !ltl.property
26462646
// CHECK: [[NOT_IMPLI_OP:%.+]] = ltl.not [[IMPLICATION_OP]] : !ltl.property
@@ -2665,10 +2665,10 @@ module ConcurrentAssert(input clk);
26652665
// CHECK: moore.procedure always {
26662666
// CHECK: [[TMP:%.+]] = moore.read %a : <i1>
26672667
// CHECK: [[A:%.+]] = moore.to_builtin_bool [[TMP]] : i1
2668-
// CHECK: [[DA:%.+]] = ltl.delay [[A]], 0, 0 : i1
2668+
// CHECK: [[DA:%.+]] = ltl.delay [[PRE:.*]] [[A]], 0, 0 : i1
26692669
// CHECK: [[TMP:%.+]] = moore.read %b : <l1>
26702670
// CHECK: [[B:%.+]] = moore.to_builtin_bool [[TMP]] : l1
2671-
// CHECK: [[DB:%.+]] = ltl.delay [[B]], 1, 0 : i1
2671+
// CHECK: [[DB:%.+]] = ltl.delay [[PRE:.*]] [[B]], 1, 0 : i1
26722672
// CHECK: [[RES:%.+]] = ltl.concat %6, %9 : !ltl.sequence, !ltl.sequence
26732673
// CHECK: verif.assert [[RES]] : !ltl.sequence
26742674
// CHECK: moore.return
@@ -2685,8 +2685,8 @@ module ConcurrentAssert(input clk);
26852685
// CHECK: [[A:%.+]] = moore.to_builtin_bool [[TMP]] : i1
26862686
// CHECK: [[TRUE:%.+]] = hw.constant true
26872687
// CHECK: [[OP1:%.+]] = ltl.repeat [[TRUE]], 0 : i1
2688-
// CHECK: [[OP2:%.+]] = ltl.delay [[OP1]], 1, 0 : !ltl.sequence
2689-
// CHECK: [[OP3:%.+]] = ltl.delay [[B]], 1, 0 : i1
2688+
// CHECK: [[OP2:%.+]] = ltl.delay [[PRE:.*]] [[OP1]], 1, 0 : !ltl.sequence
2689+
// CHECK: [[OP3:%.+]] = ltl.delay [[PRE:.*]] [[B]], 1, 0 : i1
26902690
// CHECK: [[OP4:%.+]] = ltl.concat [[OP2]], [[OP3]], [[TRUE]] : !ltl.sequence, !ltl.sequence, i1
26912691
// CHECK: [[RES:%.+]] = ltl.intersect [[OP4]], [[A]] : !ltl.sequence, i1
26922692
// CHECK: verif.assert [[RES]] : !ltl.sequence
@@ -2700,10 +2700,10 @@ module ConcurrentAssert(input clk);
27002700
// CHECK: moore.procedure always {
27012701
// CHECK: [[TMP:%.+]] = moore.read %a : <i1>
27022702
// CHECK: [[A:%.+]] = moore.to_builtin_bool [[TMP]] : i1
2703-
// CHECK: [[DA:%.+]] = ltl.delay [[A]], 0, 0 : i1
2703+
// CHECK: [[DA:%.+]] = ltl.delay [[PRE:.*]] [[A]], 0, 0 : i1
27042704
// CHECK: [[TMP:%.+]] = moore.read %b : <l1>
27052705
// CHECK: [[B:%.+]] = moore.to_builtin_bool [[TMP]] : l1
2706-
// CHECK: [[DB:%.+]] = ltl.delay [[B]], 1, 0 : i1
2706+
// CHECK: [[DB:%.+]] = ltl.delay [[PRE:.*]] [[B]], 1, 0 : i1
27072707
// CHECK: [[OP1:%.+]] = ltl.concat [[DA]], [[DB]] : !ltl.sequence, !ltl.sequence
27082708
// CHECK: [[TMP:%.+]] = moore.read %b : <l1>
27092709
// CHECK: [[B2:%.+]] = moore.to_builtin_bool [[TMP]] : l1
@@ -2725,14 +2725,14 @@ module ConcurrentAssert(input clk);
27252725
// CHECK: [[B1:%.+]] = moore.to_builtin_bool [[TMP]] : l1
27262726
// CHECK: [[TRUE:%.+]] = hw.constant true
27272727
// CHECK: [[OP1:%.+]] = ltl.repeat [[TRUE]], 0 : i1
2728-
// CHECK: [[OP2:%.+]] = ltl.delay [[OP1]], 1, 0 : !ltl.sequence
2729-
// CHECK: [[OP3:%.+]] = ltl.delay [[A2]], 1, 0 : i1
2728+
// CHECK: [[OP2:%.+]] = ltl.delay [[PRE:.*]] [[OP1]], 1, 0 : !ltl.sequence
2729+
// CHECK: [[OP3:%.+]] = ltl.delay [[PRE:.*]] [[A2]], 1, 0 : i1
27302730
// CHECK: [[OP4:%.+]] = ltl.concat [[OP2]], [[OP3]], [[TRUE]] : !ltl.sequence, !ltl.sequence, i1
27312731
// CHECK: [[OP5:%.+]] = ltl.intersect [[OP4]], [[B1]] : !ltl.sequence, i1
27322732
// CHECK: [[TRUE1:%.+]] = hw.constant true
27332733
// CHECK: [[OP6:%.+]] = ltl.repeat [[TRUE1]], 0 : i1
2734-
// CHECK: [[OP7:%.+]] = ltl.delay [[OP6]], 1, 0 : !ltl.sequence
2735-
// CHECK: [[OP8:%.+]] = ltl.delay [[A1]], 1, 0 : i1
2734+
// CHECK: [[OP7:%.+]] = ltl.delay [[PRE:.*]] [[OP6]], 1, 0 : !ltl.sequence
2735+
// CHECK: [[OP8:%.+]] = ltl.delay [[PRE:.*]] [[A1]], 1, 0 : i1
27362736
// CHECK: [[OP9:%.+]] = ltl.concat [[OP7]], [[OP8]], [[TRUE1]] : !ltl.sequence, !ltl.sequence, i1
27372737
// CHECK: [[OP10:%.+]] = ltl.intersect [[OP9]], [[OP5]] : !ltl.sequence, !ltl.sequence
27382738
// CHECK: [[TMP:%.+]] = moore.read %a : <i1>

‎test/Dialect/LTL/basic.mlir‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
// RUN: circt-opt %s | circt-opt | FileCheck %s
22

33
%true = hw.constant true
4+
%clk = hw.constant true
45

56
//===----------------------------------------------------------------------===//
67
// Types
@@ -50,10 +51,10 @@ unrealized_conversion_cast %p3 : !ltl.property to index
5051
// Sequences
5152
//===----------------------------------------------------------------------===//
5253

53-
// CHECK: ltl.delay {{%.+}}, 0 : !ltl.sequence
54-
// CHECK: ltl.delay {{%.+}}, 42, 1337 : !ltl.sequence
55-
ltl.delay %s, 0 : !ltl.sequence
56-
ltl.delay %s, 42, 1337 : !ltl.sequence
54+
// CHECK: ltl.delay {{%.+}}, posedge, {{%.+}}, 0 : !ltl.sequence
55+
// CHECK: ltl.delay {{%.+}}, posedge, {{%.+}}, 42, 1337 : !ltl.sequence
56+
ltl.delay %clk, posedge, %s, 0 : !ltl.sequence
57+
ltl.delay %clk, posedge, %s, 42, 1337 : !ltl.sequence
5758

5859
// CHECK: ltl.concat {{%.+}} : !ltl.sequence
5960
// CHECK: ltl.concat {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.sequence

0 commit comments

Comments
 (0)