-
Notifications
You must be signed in to change notification settings - Fork 437
Expand file tree
/
Copy pathbasic.mlir
More file actions
134 lines (111 loc) · 5.34 KB
/
basic.mlir
File metadata and controls
134 lines (111 loc) · 5.34 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
// RUN: circt-opt %s | circt-opt | FileCheck %s
%true = hw.constant true
%c0_i8 = hw.constant 0 : i8
%clk = hw.constant true
//===----------------------------------------------------------------------===//
// Types
//===----------------------------------------------------------------------===//
// CHECK: unrealized_conversion_cast to !ltl.sequence
// CHECK: unrealized_conversion_cast to !ltl.property
%s = unrealized_conversion_cast to !ltl.sequence
%p = unrealized_conversion_cast to !ltl.property
//===----------------------------------------------------------------------===//
// Generic
//===----------------------------------------------------------------------===//
// CHECK-NEXT: ltl.and {{%.+}}, {{%.+}} : i1, i1
// CHECK-NEXT: ltl.and {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.sequence
// CHECK-NEXT: ltl.and {{%.+}}, {{%.+}} : !ltl.property, !ltl.property
ltl.and %true, %true : i1, i1
ltl.and %s, %s : !ltl.sequence, !ltl.sequence
ltl.and %p, %p : !ltl.property, !ltl.property
// CHECK-NEXT: ltl.or {{%.+}}, {{%.+}} : i1, i1
// CHECK-NEXT: ltl.or {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.sequence
// CHECK-NEXT: ltl.or {{%.+}}, {{%.+}} : !ltl.property, !ltl.property
ltl.or %true, %true : i1, i1
ltl.or %s, %s : !ltl.sequence, !ltl.sequence
ltl.or %p, %p : !ltl.property, !ltl.property
// Type inference. `unrealized_conversion_cast` used to detect unexpected return
// types on `ltl.and`.
%s0 = ltl.and %true, %true : i1, i1
%s1 = ltl.and %true, %s : i1, !ltl.sequence
%s2 = ltl.and %s, %true : !ltl.sequence, i1
%p0 = ltl.and %true, %p : i1, !ltl.property
%p1 = ltl.and %p, %true : !ltl.property, i1
%p2 = ltl.and %s, %p : !ltl.sequence, !ltl.property
%p3 = ltl.and %p, %s : !ltl.property, !ltl.sequence
unrealized_conversion_cast %s0 : i1 to index
unrealized_conversion_cast %s1 : !ltl.sequence to index
unrealized_conversion_cast %s2 : !ltl.sequence to index
unrealized_conversion_cast %p0 : !ltl.property to index
unrealized_conversion_cast %p1 : !ltl.property to index
unrealized_conversion_cast %p2 : !ltl.property to index
unrealized_conversion_cast %p3 : !ltl.property to index
//===----------------------------------------------------------------------===//
// Sequences
//===----------------------------------------------------------------------===//
// CHECK: ltl.delay {{%.+}}, 0 : !ltl.sequence
// CHECK: ltl.delay {{%.+}}, 42, 1337 : !ltl.sequence
// CHECK: ltl.clocked_delay {{%.+}}, posedge, {{%.+}}, 0 : !ltl.sequence
// CHECK: ltl.clocked_delay {{%.+}}, posedge, {{%.+}}, 42, 1337 : !ltl.sequence
ltl.delay %s, 0 : !ltl.sequence
ltl.delay %s, 42, 1337 : !ltl.sequence
ltl.clocked_delay %clk, posedge, %s, 0 : !ltl.sequence
ltl.clocked_delay %clk, posedge, %s, 42, 1337 : !ltl.sequence
// CHECK: ltl.concat {{%.+}} : !ltl.sequence
// CHECK: ltl.concat {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.sequence
// CHECK: ltl.concat {{%.+}}, {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.sequence, !ltl.sequence
ltl.concat %s : !ltl.sequence
ltl.concat %s, %s : !ltl.sequence, !ltl.sequence
ltl.concat %s, %s, %s : !ltl.sequence, !ltl.sequence, !ltl.sequence
// CHECK: ltl.repeat {{%.+}}, 0 : !ltl.sequence
// CHECK: ltl.repeat {{%.+}}, 42 : !ltl.sequence
// CHECK: ltl.repeat {{%.+}}, 42, 1337 : !ltl.sequence
ltl.repeat %s, 0 : !ltl.sequence
ltl.repeat %s, 42 : !ltl.sequence
ltl.repeat %s, 42, 1337 : !ltl.sequence
//===----------------------------------------------------------------------===//
// Properties
//===----------------------------------------------------------------------===//
// CHECK: ltl.boolean_constant true
%bc = ltl.boolean_constant true
unrealized_conversion_cast %bc : !ltl.property to index
// CHECK: ltl.not {{%.+}} : i1
// CHECK: ltl.not {{%.+}} : !ltl.sequence
// CHECK: ltl.not {{%.+}} : !ltl.property
ltl.not %true : i1
ltl.not %s : !ltl.sequence
ltl.not %p : !ltl.property
// CHECK: ltl.implication {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.property
ltl.implication %s, %p : !ltl.sequence, !ltl.property
// CHECK: ltl.until {{%.+}}, {{%.+}} : !ltl.property, !ltl.property
ltl.until %p, %p : !ltl.property, !ltl.property
// CHECK: ltl.eventually {{%.+}} : i1
// CHECK: ltl.eventually {{%.+}} : !ltl.sequence
// CHECK: ltl.eventually {{%.+}} : !ltl.property
ltl.eventually %true : i1
ltl.eventually %s : !ltl.sequence
ltl.eventually %p : !ltl.property
// CHECK: ltl.past {{%.+}}, 1 : i1
// CHECK: ltl.past {{%.+}}, 5 : i8
ltl.past %true, 1 : i1
ltl.past %c0_i8, 5 : i8
// CHECK: ltl.past {{%.+}}, 5 clk {{%.+}} : i8
ltl.past %c0_i8, 5 clk %true : i8
//===----------------------------------------------------------------------===//
// Clocking
//===----------------------------------------------------------------------===//
// CHECK: ltl.clock {{%.+}}, posedge {{%.+}} : !ltl.sequence
// CHECK: ltl.clock {{%.+}}, negedge {{%.+}} : !ltl.sequence
// CHECK: ltl.clock {{%.+}}, edge {{%.+}} : i1
// CHECK: ltl.clock {{%.+}}, edge {{%.+}} : !ltl.sequence
// CHECK: ltl.clock {{%.+}}, edge {{%.+}} : !ltl.property
ltl.clock %s, posedge %true : !ltl.sequence
ltl.clock %s, negedge %true : !ltl.sequence
%clk0 = ltl.clock %true, edge %true : i1
%clk1 = ltl.clock %s, edge %true : !ltl.sequence
%clk2 = ltl.clock %p, edge %true : !ltl.property
// Type inference. `unrealized_conversion_cast` used to detect unexpected return
// types on `ltl.and`.
unrealized_conversion_cast %clk0 : !ltl.sequence to index
unrealized_conversion_cast %clk1 : !ltl.sequence to index
unrealized_conversion_cast %clk2 : !ltl.property to index