libpatron 0.17.3

Hardware bug-finding toolkit.
Documentation 
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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271

; BTOR description generated by Yosys 0.20+42 (git sha1 1c36f4cc2, clang 10.0.0-4ubuntu1 -fPIC -Os) for module sdram_controller.
1 sort bitvec 1
2 input 1 clk ; sdram_controller.no_tri_state.v:118.28-118.31
3 sort bitvec 16
4 input 3 data_in ; sdram_controller.no_tri_state.v:129.28-129.35
5 sort bitvec 24
6 input 5 rd_addr ; sdram_controller.no_tri_state.v:111.28-111.35
7 input 1 rd_enable ; sdram_controller.no_tri_state.v:113.28-113.37
8 input 1 rst_n ; sdram_controller.no_tri_state.v:117.28-117.33
9 input 5 wr_addr ; sdram_controller.no_tri_state.v:107.28-107.35
10 input 3 wr_data ; sdram_controller.no_tri_state.v:108.28-108.35
11 input 1 wr_enable ; sdram_controller.no_tri_state.v:109.28-109.37
12 sort bitvec 10
13 const 12 0000000000
14 sort bitvec 8
15 state 14 command
16 sort bitvec 2
17 const 16 00
18 slice 1 15 0 0
19 sort bitvec 11
20 concat 19 18 13
21 sort bitvec 13
22 concat 21 17 20
23 const 21 0000000000000
24 const 21 0001000110000
25 sort bitvec 5
26 state 25 state
27 const 25 01110
28 eq 1 26 27 $eq$sdram_controller.no_tri_state.v:276$22 ; sdram_controller.no_tri_state.v:276.13-276.31
29 ite 21 28 24 23 $procmux$120 ; sdram_controller.no_tri_state.v:276.13-276.31|sdram_controller.no_tri_state.v:276.9-284.9
30 state 5 haddr_r
31 sort bitvec 4
32 const 31 0010
33 sort bitvec 9
34 slice 33 30 8 0
35 concat 21 32 34
36 const 25 10010
37 eq 1 26 36 $eq$sdram_controller.no_tri_state.v:253$19 ; sdram_controller.no_tri_state.v:253.13-253.30
38 const 25 11010
39 eq 1 26 38 $eq$sdram_controller.no_tri_state.v:253$20 ; sdram_controller.no_tri_state.v:253.33-253.50
40 or 1 37 39 $or$sdram_controller.no_tri_state.v:253$21 ; sdram_controller.no_tri_state.v:253.13-253.50
41 ite 21 40 35 29 $procmux$129 ; sdram_controller.no_tri_state.v:253.13-253.50|sdram_controller.no_tri_state.v:253.9-284.9
42 slice 21 30 21 9
43 const 25 10000
44 eq 1 26 43 $eq$sdram_controller.no_tri_state.v:248$16 ; sdram_controller.no_tri_state.v:248.8-248.25
45 const 25 11000
46 eq 1 26 45 $eq$sdram_controller.no_tri_state.v:248$17 ; sdram_controller.no_tri_state.v:248.28-248.45
47 or 1 44 46 $or$sdram_controller.no_tri_state.v:248$18 ; sdram_controller.no_tri_state.v:248.8-248.45
48 ite 21 47 42 41 $procmux$141 ; sdram_controller.no_tri_state.v:248.8-248.45|sdram_controller.no_tri_state.v:248.4-284.9
49 slice 1 26 4 4
50 or 1 49 28 $or$sdram_controller.no_tri_state.v:173$3 ; sdram_controller.no_tri_state.v:173.26-173.55
51 ite 21 50 48 22 $ternary$sdram_controller.no_tri_state.v:173$4 ; sdram_controller.no_tri_state.v:173.25-173.115
52 output 51 addr ; sdram_controller.no_tri_state.v:123.28-123.32
53 slice 16 15 2 1
54 slice 16 30 23 22
55 ite 16 40 54 17 $procmux$135 ; sdram_controller.no_tri_state.v:253.13-253.50|sdram_controller.no_tri_state.v:253.9-284.9
56 ite 16 47 54 55 $procmux$144 ; sdram_controller.no_tri_state.v:248.8-248.45|sdram_controller.no_tri_state.v:248.4-284.9
57 ite 16 49 56 53 $ternary$sdram_controller.no_tri_state.v:172$1 ; sdram_controller.no_tri_state.v:172.25-172.64
58 output 57 bank_addr ; sdram_controller.no_tri_state.v:124.28-124.37
59 state 1
60 output 59 busy ; sdram_controller.no_tri_state.v:116.28-116.32
61 slice 1 15 4 4
62 output 61 cas_n ; sdram_controller.no_tri_state.v:133.28-133.33
63 slice 1 15 7 7
64 output 63 clock_enable ; sdram_controller.no_tri_state.v:130.28-130.40
65 slice 1 15 6 6
66 output 65 cs_n ; sdram_controller.no_tri_state.v:131.28-131.32
67 const 16 11
68 ite 16 49 17 67 $procmux$147 ; sdram_controller.no_tri_state.v:240.9-240.17|sdram_controller.no_tri_state.v:240.5-243.51
69 slice 1 68 0 0
70 output 69 data_mask_high ; sdram_controller.no_tri_state.v:136.28-136.42
71 slice 1 68 1 1
72 output 71 data_mask_low ; sdram_controller.no_tri_state.v:135.28-135.41
73 output 39 data_oe ; sdram_controller.no_tri_state.v:127.28-127.35
74 state 3 wr_data_r
75 output 74 data_out ; sdram_controller.no_tri_state.v:128.28-128.36
76 slice 1 15 5 5
77 output 76 ras_n ; sdram_controller.no_tri_state.v:132.28-132.33
78 state 3 rd_data_r
79 output 78 rd_data ; sdram_controller.no_tri_state.v:112.28-112.35
80 state 1 rd_ready_r
81 output 80 rd_ready ; sdram_controller.no_tri_state.v:114.28-114.36
82 slice 1 15 3 3
83 output 82 we_n ; sdram_controller.no_tri_state.v:134.28-134.32
84 uext 21 48 0 addr_r ; sdram_controller.no_tri_state.v:146.26-146.32
85 uext 16 56 0 bank_addr_r ; sdram_controller.no_tri_state.v:147.26-147.37
86 input 14
87 sort bitvec 17
88 sort array 25 87
89 state 88
90 const 87 10111000000000000
91 const 25 00000
92 write 88 89 91 90
93 const 87 10111000000100000
94 const 25 00001
95 write 88 92 94 93
96 const 87 10001000000110000
97 const 25 00010
98 write 88 95 97 96
99 const 87 10111000001000111
100 const 25 00011
101 write 88 98 100 99
102 const 25 00100
103 write 88 101 102 90
104 const 87 10001000010100000
105 const 25 00101
106 write 88 103 105 104
107 const 25 00110
108 write 88 106 107 90
109 const 25 00111
110 write 88 108 109 90
111 const 87 10010001010010000
112 const 25 01000
113 write 88 110 112 111
114 const 87 10111000001010000
115 const 25 01001
116 write 88 113 115 114
117 const 87 10111000010110111
118 const 25 01010
119 write 88 116 118 117
120 const 87 10001000011000000
121 const 25 01011
122 write 88 119 121 120
123 const 87 10111000011010111
124 const 25 01100
125 write 88 122 124 123
126 state 87
127 const 87 00000001000000000
128 and 87 126 127
129 const 87 10000000011100000
130 or 87 128 129
131 const 25 01101
132 write 88 125 131 130
133 const 87 10111000011110001
134 write 88 132 27 133
135 const 25 01111
136 write 88 134 135 90
137 const 87 10111000100010001
138 write 88 136 43 137
139 state 87
140 const 87 00000110000000000
141 and 87 139 140
142 const 87 10101001100100000
143 or 87 141 142
144 const 25 10001
145 write 88 138 144 143
146 const 87 10111000100110001
147 write 88 145 36 146
148 const 87 10111000101000000
149 const 25 10011
150 write 88 147 149 148
151 const 25 10100
152 write 88 150 151 90
153 const 25 10101
154 write 88 152 153 90
155 const 25 10110
156 write 88 154 155 90
157 const 25 10111
158 write 88 156 157 90
159 const 87 10111000110010001
160 write 88 158 45 159
161 state 87
162 and 87 161 140
163 const 87 10100001110100000
164 or 87 162 163
165 const 25 11001
166 write 88 160 165 164
167 const 87 10111000110110001
168 write 88 166 38 167
169 const 25 11011
170 write 88 168 169 90
171 const 25 11100
172 write 88 170 171 90
173 const 25 11101
174 write 88 172 173 90
175 const 25 11110
176 write 88 174 175 90
177 const 25 11111
178 write 88 176 177 90
179 state 88
180 init 88 179 178
181 read 87 179 26
182 slice 14 181 16 9
183 state 31 state_cnt
184 redor 1 183
185 not 1 184 $logic_not$sdram_controller.no_tri_state.v:315$26 ; sdram_controller.no_tri_state.v:315.11-315.21
186 ite 14 185 182 86 $procmux$51 ; sdram_controller.no_tri_state.v:315.11-315.21|sdram_controller.no_tri_state.v:315.7-426.12
187 const 14 10111000
188 input 14
189 const 14 00000111
190 and 14 188 189
191 const 14 10011000
192 or 14 190 191
193 ite 14 11 192 187 $procmux$58 ; sdram_controller.no_tri_state.v:304.18-304.27|sdram_controller.no_tri_state.v:304.14-313.14
194 input 14
195 and 14 194 189
196 or 14 195 191
197 ite 14 7 196 193 $procmux$82 ; sdram_controller.no_tri_state.v:299.18-299.27|sdram_controller.no_tri_state.v:299.14-313.14
198 const 14 10010001
199 state 12 refresh_cnt
200 sort bitvec 32
201 uext 200 199 22
202 const 200 00000000000000000000001000000111
203 ugte 1 201 202 $ge$sdram_controller.no_tri_state.v:294$25 ; sdram_controller.no_tri_state.v:294.13-294.50
204 ite 14 203 198 197 $procmux$100 ; sdram_controller.no_tri_state.v:294.13-294.50|sdram_controller.no_tri_state.v:294.9-313.14
205 redor 1 26
206 not 1 205 $eq$sdram_controller.no_tri_state.v:292$24 ; sdram_controller.no_tri_state.v:292.8-292.21
207 ite 14 206 204 186 $procmux$114 ; sdram_controller.no_tri_state.v:292.8-292.21|sdram_controller.no_tri_state.v:292.4-426.12
208 uext 14 207 0 command_nxt ; sdram_controller.no_tri_state.v:166.11-166.22
209 uext 1 69 0 data_mask_high_r ; sdram_controller.no_tri_state.v:145.26-145.42
210 uext 1 71 0 data_mask_low_r ; sdram_controller.no_tri_state.v:144.26-144.41
211 input 25
212 slice 25 181 8 4
213 ite 25 185 212 211 $procmux$39 ; sdram_controller.no_tri_state.v:315.11-315.21|sdram_controller.no_tri_state.v:315.7-426.12
214 ite 25 11 45 91 $procmux$70 ; sdram_controller.no_tri_state.v:304.18-304.27|sdram_controller.no_tri_state.v:304.14-313.14
215 ite 25 7 43 214 $procmux$91 ; sdram_controller.no_tri_state.v:299.18-299.27|sdram_controller.no_tri_state.v:299.14-313.14
216 ite 25 203 94 215 $procmux$106 ; sdram_controller.no_tri_state.v:294.13-294.50|sdram_controller.no_tri_state.v:294.9-313.14
217 ite 25 206 216 213 $procmux$111 ; sdram_controller.no_tri_state.v:292.8-292.21|sdram_controller.no_tri_state.v:292.4-426.12
218 uext 25 217 0 next ; sdram_controller.no_tri_state.v:168.11-168.15
219 slice 31 181 3 0
220 const 31 0000
221 ite 31 206 220 219 $procmux$117 ; sdram_controller.no_tri_state.v:292.8-292.21|sdram_controller.no_tri_state.v:292.4-426.12
222 uext 31 221 0 state_cnt_nxt ; sdram_controller.no_tri_state.v:167.11-167.24
223 concat 16 206 185
224 redor 1 223 $auto$opt_dff.cc:195:make_patterns_logic$224
225 ite 14 224 207 15 $auto$ff.cc:504:unmap_ce$252
226 ite 14 8 225 187 $auto$ff.cc:526:unmap_srst$254
227 next 14 15 226 $auto$ff.cc:266:slice$225 ; sdram_controller.no_tri_state.v:183.1-224.8
228 ite 25 224 217 26 $auto$ff.cc:504:unmap_ce$248
229 ite 25 8 228 112 $auto$ff.cc:526:unmap_srst$250
230 next 25 26 229 $auto$ff.cc:266:slice$222 ; sdram_controller.no_tri_state.v:183.1-224.8
231 const 5 000000000000000000000000
232 input 5
233 ite 5 11 9 232 $procmux$187 ; sdram_controller.no_tri_state.v:221.14-221.23|sdram_controller.no_tri_state.v:221.10-222.26
234 ite 5 7 6 233 $procmux$190 ; sdram_controller.no_tri_state.v:219.9-219.18|sdram_controller.no_tri_state.v:219.5-222.26
235 concat 16 7 11
236 redor 1 235 $auto$opt_dff.cc:195:make_patterns_logic$217
237 ite 5 236 234 30 $auto$ff.cc:504:unmap_ce$236
238 ite 5 8 237 231 $auto$ff.cc:526:unmap_srst$238
239 next 5 30 238 $auto$ff.cc:266:slice$215 ; sdram_controller.no_tri_state.v:183.1-224.8
240 const 1 0
241 ite 1 8 49 240 $auto$ff.cc:526:unmap_srst$234
242 next 1 59 241 $auto$ff.cc:266:slice$213 ; sdram_controller.no_tri_state.v:183.1-224.8
243 const 3 0000000000000000
244 ite 3 11 10 74 $auto$ff.cc:504:unmap_ce$240
245 ite 3 8 244 243 $auto$ff.cc:526:unmap_srst$242
246 next 3 74 245 $auto$ff.cc:266:slice$219 ; sdram_controller.no_tri_state.v:183.1-224.8
247 eq 1 26 151 $eq$sdram_controller.no_tri_state.v:209$10 ; sdram_controller.no_tri_state.v:209.9-209.27
248 ite 3 247 4 78 $auto$ff.cc:504:unmap_ce$244
249 ite 3 8 248 243 $auto$ff.cc:526:unmap_srst$246
250 next 3 78 249 $auto$ff.cc:266:slice$221 ; sdram_controller.no_tri_state.v:183.1-224.8
251 const 1 1
252 ite 1 247 251 240 $procmux$171 ; sdram_controller.no_tri_state.v:209.9-209.27|sdram_controller.no_tri_state.v:209.5-215.26
253 ite 1 8 252 80 $auto$ff.cc:504:unmap_ce$228
254 next 1 80 253 $auto$ff.cc:266:slice$204 ; sdram_controller.no_tri_state.v:183.1-224.8
255 const 31 1111
256 uext 31 251 3
257 sub 31 183 256 $sub$sdram_controller.no_tri_state.v:204$9 ; sdram_controller.no_tri_state.v:204.20-204.36
258 ite 31 185 221 257 $procmux$159 ; sdram_controller.no_tri_state.v:201.9-201.19|sdram_controller.no_tri_state.v:201.5-204.37
259 ite 31 8 258 255 $auto$ff.cc:526:unmap_srst$230
260 next 31 183 259 $auto$ff.cc:266:slice$205 ; sdram_controller.no_tri_state.v:183.1-224.8
261 uext 12 251 9
262 add 12 199 261 $add$sdram_controller.no_tri_state.v:234$14 ; sdram_controller.no_tri_state.v:234.21-234.39
263 eq 1 26 102 $eq$sdram_controller.no_tri_state.v:231$13 ; sdram_controller.no_tri_state.v:231.8-231.25
264 not 1 8 $auto$opt_dff.cc:250:combine_resets$209
265 concat 16 264 263
266 redor 1 265 $auto$opt_dff.cc:254:combine_resets$212
267 ite 12 266 13 262 $auto$ff.cc:524:unmap_srst$232
268 next 12 199 267 $auto$ff.cc:266:slice$208 ; sdram_controller.no_tri_state.v:227.1-234.40
269 next 88 179 179 $auto$proc_rom.cc:150:do_switch$28 ; sdram_controller.no_tri_state.v:316.9-420.18
; end of yosys output