; BTOR description generated by Yosys 0.20+42 (git sha1 1c36f4cc2, clang 10.0.0-4ubuntu1 -fPIC -Os) for module keccak.
1 sort bitvec 2
2 input 1 byte_num ; keccak.v:30.24-30.32
3 sort bitvec 1
4 input 3 clk ; keccak.v:27.24-27.27
5 sort bitvec 32
6 input 5 in ; keccak.v:28.24-28.26
7 input 3 in_ready ; keccak.v:29.24-29.32
8 input 3 is_last ; keccak.v:29.34-29.41
9 input 3 reset ; keccak.v:27.29-27.34
10 sort bitvec 18
11 state 10 padder_.i
12 slice 3 11 17 17
13 output 12 buffer_full ; keccak.v:31.24-31.35
14 sort bitvec 1600
15 state 14 f_permutation_.out
16 sort bitvec 8
17 slice 16 15 1151 1144
18 slice 16 15 1143 1136
19 sort bitvec 16
20 concat 19 18 17
21 slice 16 15 1135 1128
22 sort bitvec 24
23 concat 22 21 20
24 slice 16 15 1127 1120
25 concat 5 24 23
26 slice 16 15 1119 1112
27 sort bitvec 40
28 concat 27 26 25
29 slice 16 15 1111 1104
30 sort bitvec 48
31 concat 30 29 28
32 slice 16 15 1103 1096
33 sort bitvec 56
34 concat 33 32 31
35 slice 16 15 1095 1088
36 sort bitvec 64
37 concat 36 35 34
38 slice 16 15 1215 1208
39 sort bitvec 72
40 concat 39 38 37
41 slice 16 15 1207 1200
42 sort bitvec 80
43 concat 42 41 40
44 slice 16 15 1199 1192
45 sort bitvec 88
46 concat 45 44 43
47 slice 16 15 1191 1184
48 sort bitvec 96
49 concat 48 47 46
50 slice 16 15 1183 1176
51 sort bitvec 104
52 concat 51 50 49
53 slice 16 15 1175 1168
54 sort bitvec 112
55 concat 54 53 52
56 slice 16 15 1167 1160
57 sort bitvec 120
58 concat 57 56 55
59 slice 16 15 1159 1152
60 sort bitvec 128
61 concat 60 59 58
62 slice 16 15 1279 1272
63 sort bitvec 136
64 concat 63 62 61
65 slice 16 15 1271 1264
66 sort bitvec 144
67 concat 66 65 64
68 slice 16 15 1263 1256
69 sort bitvec 152
70 concat 69 68 67
71 slice 16 15 1255 1248
72 sort bitvec 160
73 concat 72 71 70
74 slice 16 15 1247 1240
75 sort bitvec 168
76 concat 75 74 73
77 slice 16 15 1239 1232
78 sort bitvec 176
79 concat 78 77 76
80 slice 16 15 1231 1224
81 sort bitvec 184
82 concat 81 80 79
83 slice 16 15 1223 1216
84 sort bitvec 192
85 concat 84 83 82
86 slice 16 15 1343 1336
87 sort bitvec 200
88 concat 87 86 85
89 slice 16 15 1335 1328
90 sort bitvec 208
91 concat 90 89 88
92 slice 16 15 1327 1320
93 sort bitvec 216
94 concat 93 92 91
95 slice 16 15 1319 1312
96 sort bitvec 224
97 concat 96 95 94
98 slice 16 15 1311 1304
99 sort bitvec 232
100 concat 99 98 97
101 slice 16 15 1303 1296
102 sort bitvec 240
103 concat 102 101 100
104 slice 16 15 1295 1288
105 sort bitvec 248
106 concat 105 104 103
107 slice 16 15 1287 1280
108 sort bitvec 256
109 concat 108 107 106
110 slice 16 15 1407 1400
111 sort bitvec 264
112 concat 111 110 109
113 slice 16 15 1399 1392
114 sort bitvec 272
115 concat 114 113 112
116 slice 16 15 1391 1384
117 sort bitvec 280
118 concat 117 116 115
119 slice 16 15 1383 1376
120 sort bitvec 288
121 concat 120 119 118
122 slice 16 15 1375 1368
123 sort bitvec 296
124 concat 123 122 121
125 slice 16 15 1367 1360
126 sort bitvec 304
127 concat 126 125 124
128 slice 16 15 1359 1352
129 sort bitvec 312
130 concat 129 128 127
131 slice 16 15 1351 1344
132 sort bitvec 320
133 concat 132 131 130
134 slice 16 15 1471 1464
135 sort bitvec 328
136 concat 135 134 133
137 slice 16 15 1463 1456
138 sort bitvec 336
139 concat 138 137 136
140 slice 16 15 1455 1448
141 sort bitvec 344
142 concat 141 140 139
143 slice 16 15 1447 1440
144 sort bitvec 352
145 concat 144 143 142
146 slice 16 15 1439 1432
147 sort bitvec 360
148 concat 147 146 145
149 slice 16 15 1431 1424
150 sort bitvec 368
151 concat 150 149 148
152 slice 16 15 1423 1416
153 sort bitvec 376
154 concat 153 152 151
155 slice 16 15 1415 1408
156 sort bitvec 384
157 concat 156 155 154
158 slice 16 15 1535 1528
159 sort bitvec 392
160 concat 159 158 157
161 slice 16 15 1527 1520
162 sort bitvec 400
163 concat 162 161 160
164 slice 16 15 1519 1512
165 sort bitvec 408
166 concat 165 164 163
167 slice 16 15 1511 1504
168 sort bitvec 416
169 concat 168 167 166
170 slice 16 15 1503 1496
171 sort bitvec 424
172 concat 171 170 169
173 slice 16 15 1495 1488
174 sort bitvec 432
175 concat 174 173 172
176 slice 16 15 1487 1480
177 sort bitvec 440
178 concat 177 176 175
179 slice 16 15 1479 1472
180 sort bitvec 448
181 concat 180 179 178
182 slice 16 15 1599 1592
183 sort bitvec 456
184 concat 183 182 181
185 slice 16 15 1591 1584
186 sort bitvec 464
187 concat 186 185 184
188 slice 16 15 1583 1576
189 sort bitvec 472
190 concat 189 188 187
191 slice 16 15 1575 1568
192 sort bitvec 480
193 concat 192 191 190
194 slice 16 15 1567 1560
195 sort bitvec 488
196 concat 195 194 193
197 slice 16 15 1559 1552
198 sort bitvec 496
199 concat 198 197 196
200 slice 16 15 1551 1544
201 sort bitvec 504
202 concat 201 200 199
203 slice 16 15 1543 1536
204 sort bitvec 512
205 concat 204 203 202
206 output 205 out ; keccak.v:32.24-32.27
207 state 3
208 output 207 out_ready ; keccak.v:33.24-33.33
209 state 3 f_permutation_.calc
210 not 3 209 $flatten\f_permutation_.$not$f_permutation.v:34$26 ; keccak.v:94.7-94.91|f_permutation.v:34.33-34.39
211 and 3 12 210 $flatten\f_permutation_.$and$f_permutation.v:34$27 ; keccak.v:94.7-94.91|f_permutation.v:34.21-34.40
212 or 3 209 211 $flatten\f_permutation_.$or$f_permutation.v:44$33 ; keccak.v:94.7-94.91|f_permutation.v:44.21-44.34
213 uext 3 212 0 f_permutation_.update ; keccak.v:94.7-94.91|f_permutation.v:30.25-30.31
214 sort bitvec 576
215 state 214 padder_.out
216 slice 16 215 63 56
217 slice 16 215 55 48
218 concat 19 217 216
219 slice 16 215 47 40
220 concat 22 219 218
221 slice 16 215 39 32
222 concat 5 221 220
223 slice 16 215 31 24
224 concat 27 223 222
225 slice 16 215 23 16
226 concat 30 225 224
227 slice 16 215 15 8
228 concat 33 227 226
229 slice 16 215 7 0
230 concat 36 229 228
231 slice 16 215 127 120
232 concat 39 231 230
233 slice 16 215 119 112
234 concat 42 233 232
235 slice 16 215 111 104
236 concat 45 235 234
237 slice 16 215 103 96
238 concat 48 237 236
239 slice 16 215 95 88
240 concat 51 239 238
241 slice 16 215 87 80
242 concat 54 241 240
243 slice 16 215 79 72
244 concat 57 243 242
245 slice 16 215 71 64
246 concat 60 245 244
247 slice 16 215 191 184
248 concat 63 247 246
249 slice 16 215 183 176
250 concat 66 249 248
251 slice 16 215 175 168
252 concat 69 251 250
253 slice 16 215 167 160
254 concat 72 253 252
255 slice 16 215 159 152
256 concat 75 255 254
257 slice 16 215 151 144
258 concat 78 257 256
259 slice 16 215 143 136
260 concat 81 259 258
261 slice 16 215 135 128
262 concat 84 261 260
263 slice 16 215 255 248
264 concat 87 263 262
265 slice 16 215 247 240
266 concat 90 265 264
267 slice 16 215 239 232
268 concat 93 267 266
269 slice 16 215 231 224
270 concat 96 269 268
271 slice 16 215 223 216
272 concat 99 271 270
273 slice 16 215 215 208
274 concat 102 273 272
275 slice 16 215 207 200
276 concat 105 275 274
277 slice 16 215 199 192
278 concat 108 277 276
279 slice 16 215 319 312
280 concat 111 279 278
281 slice 16 215 311 304
282 concat 114 281 280
283 slice 16 215 303 296
284 concat 117 283 282
285 slice 16 215 295 288
286 concat 120 285 284
287 slice 16 215 287 280
288 concat 123 287 286
289 slice 16 215 279 272
290 concat 126 289 288
291 slice 16 215 271 264
292 concat 129 291 290
293 slice 16 215 263 256
294 concat 132 293 292
295 slice 16 215 383 376
296 concat 135 295 294
297 slice 16 215 375 368
298 concat 138 297 296
299 slice 16 215 367 360
300 concat 141 299 298
301 slice 16 215 359 352
302 concat 144 301 300
303 slice 16 215 351 344
304 concat 147 303 302
305 slice 16 215 343 336
306 concat 150 305 304
307 slice 16 215 335 328
308 concat 153 307 306
309 slice 16 215 327 320
310 concat 156 309 308
311 slice 16 215 447 440
312 concat 159 311 310
313 slice 16 215 439 432
314 concat 162 313 312
315 slice 16 215 431 424
316 concat 165 315 314
317 slice 16 215 423 416
318 concat 168 317 316
319 slice 16 215 415 408
320 concat 171 319 318
321 slice 16 215 407 400
322 concat 174 321 320
323 slice 16 215 399 392
324 concat 177 323 322
325 slice 16 215 391 384
326 concat 180 325 324
327 slice 16 215 511 504
328 concat 183 327 326
329 slice 16 215 503 496
330 concat 186 329 328
331 slice 16 215 495 488
332 concat 189 331 330
333 slice 16 215 487 480
334 concat 192 333 332
335 slice 16 215 479 472
336 concat 195 335 334
337 slice 16 215 471 464
338 concat 198 337 336
339 slice 16 215 463 456
340 concat 201 339 338
341 slice 16 215 455 448
342 concat 204 341 340
343 slice 16 215 575 568
344 sort bitvec 520
345 concat 344 343 342
346 slice 16 215 567 560
347 sort bitvec 528
348 concat 347 346 345
349 slice 16 215 559 552
350 sort bitvec 536
351 concat 350 349 348
352 slice 16 215 551 544
353 sort bitvec 544
354 concat 353 352 351
355 slice 16 215 543 536
356 sort bitvec 552
357 concat 356 355 354
358 slice 16 215 535 528
359 sort bitvec 560
360 concat 359 358 357
361 slice 16 215 527 520
362 sort bitvec 568
363 concat 362 361 360
364 slice 16 215 519 512
365 concat 214 364 363
366 slice 214 15 1599 1024
367 xor 214 365 366 $flatten\f_permutation_.$xor$f_permutation.v:56$35 ; keccak.v:94.7-94.91|f_permutation.v:56.33-56.56
368 sort bitvec 1024
369 slice 368 15 1023 0
370 concat 14 367 369
371 ite 14 211 370 15 $flatten\f_permutation_.$ternary$f_permutation.v:56$36 ; keccak.v:94.7-94.91|f_permutation.v:56.23-56.80
372 slice 36 371 255 192
373 slice 36 371 1599 1536
374 slice 36 371 1279 1216
375 xor 36 373 374 $flatten\f_permutation_.\round_.$xor$round.v:51$120 ; keccak.v:94.7-94.91|round.v:51.25-51.42|f_permutation.v:62.7-62.39
376 slice 36 371 959 896
377 xor 36 375 376 $flatten\f_permutation_.\round_.$xor$round.v:51$121 ; keccak.v:94.7-94.91|round.v:51.25-51.52|f_permutation.v:62.7-62.39
378 slice 36 371 639 576
379 xor 36 377 378 $flatten\f_permutation_.\round_.$xor$round.v:51$122 ; keccak.v:94.7-94.91|round.v:51.25-51.62|f_permutation.v:62.7-62.39
380 slice 36 371 319 256
381 xor 36 379 380 $flatten\f_permutation_.\round_.$xor$round.v:51$123 ; keccak.v:94.7-94.91|round.v:51.25-51.72|f_permutation.v:62.7-62.39
382 xor 36 372 381 $flatten\f_permutation_.\round_.$xor$round.v:61$182 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
383 slice 36 371 1471 1408
384 slice 36 371 1151 1088
385 xor 36 383 384 $flatten\f_permutation_.\round_.$xor$round.v:51$128 ; keccak.v:94.7-94.91|round.v:51.25-51.42|f_permutation.v:62.7-62.39
386 slice 36 371 831 768
387 xor 36 385 386 $flatten\f_permutation_.\round_.$xor$round.v:51$129 ; keccak.v:94.7-94.91|round.v:51.25-51.52|f_permutation.v:62.7-62.39
388 slice 36 371 511 448
389 xor 36 387 388 $flatten\f_permutation_.\round_.$xor$round.v:51$130 ; keccak.v:94.7-94.91|round.v:51.25-51.62|f_permutation.v:62.7-62.39
390 slice 36 371 191 128
391 xor 36 389 390 $flatten\f_permutation_.\round_.$xor$round.v:51$131 ; keccak.v:94.7-94.91|round.v:51.25-51.72|f_permutation.v:62.7-62.39
392 slice 3 391 63 63
393 sort bitvec 63
394 slice 393 391 62 0
395 concat 36 394 392
396 xor 36 382 395 $flatten\f_permutation_.\round_.$xor$round.v:61$183 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
397 slice 1 396 63 62
398 sort bitvec 62
399 slice 398 396 61 0
400 concat 36 399 397
401 slice 36 371 1535 1472
402 slice 36 371 1215 1152
403 xor 36 401 402 $flatten\f_permutation_.\round_.$xor$round.v:51$124 ; keccak.v:94.7-94.91|round.v:51.25-51.42|f_permutation.v:62.7-62.39
404 slice 36 371 895 832
405 xor 36 403 404 $flatten\f_permutation_.\round_.$xor$round.v:51$125 ; keccak.v:94.7-94.91|round.v:51.25-51.52|f_permutation.v:62.7-62.39
406 slice 36 371 575 512
407 xor 36 405 406 $flatten\f_permutation_.\round_.$xor$round.v:51$126 ; keccak.v:94.7-94.91|round.v:51.25-51.62|f_permutation.v:62.7-62.39
408 xor 36 407 372 $flatten\f_permutation_.\round_.$xor$round.v:51$127 ; keccak.v:94.7-94.91|round.v:51.25-51.72|f_permutation.v:62.7-62.39
409 xor 36 383 408 $flatten\f_permutation_.\round_.$xor$round.v:61$144 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
410 slice 36 371 1407 1344
411 slice 36 371 1087 1024
412 xor 36 410 411 $flatten\f_permutation_.\round_.$xor$round.v:51$132 ; keccak.v:94.7-94.91|round.v:51.25-51.42|f_permutation.v:62.7-62.39
413 slice 36 371 767 704
414 xor 36 412 413 $flatten\f_permutation_.\round_.$xor$round.v:51$133 ; keccak.v:94.7-94.91|round.v:51.25-51.52|f_permutation.v:62.7-62.39
415 slice 36 371 447 384
416 xor 36 414 415 $flatten\f_permutation_.\round_.$xor$round.v:51$134 ; keccak.v:94.7-94.91|round.v:51.25-51.62|f_permutation.v:62.7-62.39
417 slice 36 371 127 64
418 xor 36 416 417 $flatten\f_permutation_.\round_.$xor$round.v:51$135 ; keccak.v:94.7-94.91|round.v:51.25-51.72|f_permutation.v:62.7-62.39
419 slice 3 418 63 63
420 slice 393 418 62 0
421 concat 36 420 419
422 xor 36 409 421 $flatten\f_permutation_.\round_.$xor$round.v:61$145 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
423 slice 398 422 63 2
424 slice 1 422 1 0
425 concat 36 424 423
426 not 36 425 $flatten\f_permutation_.\round_.$not$round.v:126$262 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
427 xor 36 411 391 $flatten\f_permutation_.\round_.$xor$round.v:61$156 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
428 slice 36 371 1343 1280
429 slice 36 371 1023 960
430 xor 36 428 429 $flatten\f_permutation_.\round_.$xor$round.v:51$136 ; keccak.v:94.7-94.91|round.v:51.25-51.42|f_permutation.v:62.7-62.39
431 slice 36 371 703 640
432 xor 36 430 431 $flatten\f_permutation_.\round_.$xor$round.v:51$137 ; keccak.v:94.7-94.91|round.v:51.25-51.52|f_permutation.v:62.7-62.39
433 slice 36 371 383 320
434 xor 36 432 433 $flatten\f_permutation_.\round_.$xor$round.v:51$138 ; keccak.v:94.7-94.91|round.v:51.25-51.62|f_permutation.v:62.7-62.39
435 slice 36 371 63 0
436 xor 36 434 435 $flatten\f_permutation_.\round_.$xor$round.v:51$139 ; keccak.v:94.7-94.91|round.v:51.25-51.72|f_permutation.v:62.7-62.39
437 slice 3 436 63 63
438 slice 393 436 62 0
439 concat 36 438 437
440 xor 36 427 439 $flatten\f_permutation_.\round_.$xor$round.v:61$157 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
441 sort bitvec 55
442 slice 441 440 63 9
443 sort bitvec 9
444 slice 443 440 8 0
445 concat 36 444 442
446 and 36 426 445 $flatten\f_permutation_.\round_.$and$round.v:126$263 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
447 xor 36 400 446 $flatten\f_permutation_.\round_.$xor$round.v:126$264 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
448 xor 36 378 436 $flatten\f_permutation_.\round_.$xor$round.v:61$170 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
449 slice 3 408 63 63
450 slice 393 408 62 0
451 concat 36 450 449
452 xor 36 448 451 $flatten\f_permutation_.\round_.$xor$round.v:61$171 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
453 sort bitvec 41
454 slice 453 452 63 23
455 sort bitvec 23
456 slice 455 452 22 0
457 concat 36 456 454
458 not 36 400 $flatten\f_permutation_.\round_.$not$round.v:126$259 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
459 and 36 458 425 $flatten\f_permutation_.\round_.$and$round.v:126$260 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
460 xor 36 457 459 $flatten\f_permutation_.\round_.$xor$round.v:126$261 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
461 xor 36 431 418 $flatten\f_permutation_.\round_.$xor$round.v:61$168 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
462 slice 3 381 63 63
463 slice 393 381 62 0
464 concat 36 463 462
465 xor 36 461 464 $flatten\f_permutation_.\round_.$xor$round.v:61$169 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
466 sort bitvec 39
467 slice 466 465 63 25
468 sort bitvec 25
469 slice 468 465 24 0
470 concat 36 469 467
471 not 36 457 $flatten\f_permutation_.\round_.$not$round.v:126$256 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
472 and 36 471 400 $flatten\f_permutation_.\round_.$and$round.v:126$257 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
473 xor 36 470 472 $flatten\f_permutation_.\round_.$xor$round.v:126$258 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
474 not 36 470 $flatten\f_permutation_.\round_.$not$round.v:126$253 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
475 and 36 474 457 $flatten\f_permutation_.\round_.$and$round.v:126$254 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
476 xor 36 445 475 $flatten\f_permutation_.\round_.$xor$round.v:126$255 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
477 not 36 445 $flatten\f_permutation_.\round_.$not$round.v:126$250 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
478 and 36 477 470 $flatten\f_permutation_.\round_.$and$round.v:126$251 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
479 xor 36 425 478 $flatten\f_permutation_.\round_.$xor$round.v:126$252 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
480 xor 36 417 391 $flatten\f_permutation_.\round_.$xor$round.v:61$186 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
481 xor 36 480 439 $flatten\f_permutation_.\round_.$xor$round.v:61$187 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
482 slice 33 481 63 8
483 slice 16 481 7 0
484 concat 36 483 482
485 xor 36 428 418 $flatten\f_permutation_.\round_.$xor$round.v:61$148 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
486 xor 36 485 464 $flatten\f_permutation_.\round_.$xor$round.v:61$149 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
487 sort bitvec 27
488 slice 487 486 63 37
489 sort bitvec 37
490 slice 489 486 36 0
491 concat 36 490 488
492 not 36 491 $flatten\f_permutation_.\round_.$not$round.v:126$247 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
493 xor 36 374 436 $flatten\f_permutation_.\round_.$xor$round.v:61$150 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
494 xor 36 493 451 $flatten\f_permutation_.\round_.$xor$round.v:61$151 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
495 sort bitvec 36
496 slice 495 494 63 28
497 sort bitvec 28
498 slice 497 494 27 0
499 concat 36 498 496
500 and 36 492 499 $flatten\f_permutation_.\round_.$and$round.v:126$248 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
501 xor 36 484 500 $flatten\f_permutation_.\round_.$xor$round.v:126$249 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
502 xor 36 388 408 $flatten\f_permutation_.\round_.$xor$round.v:61$174 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
503 xor 36 502 421 $flatten\f_permutation_.\round_.$xor$round.v:61$175 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
504 sort bitvec 15
505 slice 504 503 63 49
506 sort bitvec 49
507 slice 506 503 48 0
508 concat 36 507 505
509 not 36 484 $flatten\f_permutation_.\round_.$not$round.v:126$244 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
510 and 36 509 491 $flatten\f_permutation_.\round_.$and$round.v:126$245 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
511 xor 36 508 510 $flatten\f_permutation_.\round_.$xor$round.v:126$246 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
512 xor 36 404 381 $flatten\f_permutation_.\round_.$xor$round.v:61$162 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
513 xor 36 512 395 $flatten\f_permutation_.\round_.$xor$round.v:61$163 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
514 sort bitvec 10
515 slice 514 513 63 54
516 sort bitvec 54
517 slice 516 513 53 0
518 concat 36 517 515
519 not 36 508 $flatten\f_permutation_.\round_.$not$round.v:126$241 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
520 and 36 519 484 $flatten\f_permutation_.\round_.$and$round.v:126$242 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
521 xor 36 518 520 $flatten\f_permutation_.\round_.$xor$round.v:126$243 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
522 not 36 518 $flatten\f_permutation_.\round_.$not$round.v:126$238 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
523 and 36 522 508 $flatten\f_permutation_.\round_.$and$round.v:126$239 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
524 xor 36 499 523 $flatten\f_permutation_.\round_.$xor$round.v:126$240 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
525 not 36 499 $flatten\f_permutation_.\round_.$not$round.v:126$235 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
526 and 36 525 518 $flatten\f_permutation_.\round_.$and$round.v:126$236 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
527 xor 36 491 526 $flatten\f_permutation_.\round_.$xor$round.v:126$237 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
528 xor 36 380 436 $flatten\f_permutation_.\round_.$xor$round.v:61$180 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
529 xor 36 528 451 $flatten\f_permutation_.\round_.$xor$round.v:61$181 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
530 slice 10 529 63 46
531 sort bitvec 46
532 slice 531 529 45 0
533 concat 36 532 530
534 xor 36 401 381 $flatten\f_permutation_.\round_.$xor$round.v:61$142 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
535 xor 36 534 395 $flatten\f_permutation_.\round_.$xor$round.v:61$143 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
536 slice 3 535 63 63
537 slice 393 535 62 0
538 concat 36 537 536
539 not 36 538 $flatten\f_permutation_.\round_.$not$round.v:126$232 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
540 xor 36 384 408 $flatten\f_permutation_.\round_.$xor$round.v:61$154 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
541 xor 36 540 421 $flatten\f_permutation_.\round_.$xor$round.v:61$155 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
542 sort bitvec 6
543 slice 542 541 63 58
544 sort bitvec 58
545 slice 544 541 57 0
546 concat 36 545 543
547 and 36 539 546 $flatten\f_permutation_.\round_.$and$round.v:126$233 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
548 xor 36 533 547 $flatten\f_permutation_.\round_.$xor$round.v:126$234 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
549 xor 36 433 418 $flatten\f_permutation_.\round_.$xor$round.v:61$178 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
550 xor 36 549 464 $flatten\f_permutation_.\round_.$xor$round.v:61$179 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
551 slice 16 550 63 56
552 slice 33 550 55 0
553 concat 36 552 551
554 not 36 533 $flatten\f_permutation_.\round_.$not$round.v:126$229 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
555 and 36 554 538 $flatten\f_permutation_.\round_.$and$round.v:126$230 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
556 xor 36 553 555 $flatten\f_permutation_.\round_.$xor$round.v:126$231 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
557 xor 36 413 391 $flatten\f_permutation_.\round_.$xor$round.v:61$166 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
558 xor 36 557 439 $flatten\f_permutation_.\round_.$xor$round.v:61$167 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
559 slice 468 558 63 39
560 slice 466 558 38 0
561 concat 36 560 559
562 not 36 553 $flatten\f_permutation_.\round_.$not$round.v:126$226 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
563 and 36 562 533 $flatten\f_permutation_.\round_.$and$round.v:126$227 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
564 xor 36 561 563 $flatten\f_permutation_.\round_.$xor$round.v:126$228 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
565 not 36 561 $flatten\f_permutation_.\round_.$not$round.v:126$223 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
566 and 36 565 553 $flatten\f_permutation_.\round_.$and$round.v:126$224 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
567 xor 36 546 566 $flatten\f_permutation_.\round_.$xor$round.v:126$225 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
568 not 36 546 $flatten\f_permutation_.\round_.$not$round.v:126$220 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
569 and 36 568 561 $flatten\f_permutation_.\round_.$and$round.v:126$221 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
570 xor 36 538 569 $flatten\f_permutation_.\round_.$xor$round.v:126$222 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
571 xor 36 390 408 $flatten\f_permutation_.\round_.$xor$round.v:61$184 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
572 xor 36 571 421 $flatten\f_permutation_.\round_.$xor$round.v:61$185 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
573 sort bitvec 61
574 slice 573 572 63 3
575 sort bitvec 3
576 slice 575 572 2 0
577 concat 36 576 574
578 xor 36 410 391 $flatten\f_permutation_.\round_.$xor$round.v:61$146 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
579 xor 36 578 439 $flatten\f_permutation_.\round_.$xor$round.v:61$147 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
580 slice 497 579 63 36
581 slice 495 579 35 0
582 concat 36 581 580
583 not 36 582 $flatten\f_permutation_.\round_.$not$round.v:126$217 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
584 xor 36 429 418 $flatten\f_permutation_.\round_.$xor$round.v:61$158 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
585 xor 36 584 464 $flatten\f_permutation_.\round_.$xor$round.v:61$159 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
586 sort bitvec 20
587 slice 586 585 63 44
588 sort bitvec 44
589 slice 588 585 43 0
590 concat 36 589 587
591 and 36 583 590 $flatten\f_permutation_.\round_.$and$round.v:126$218 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
592 xor 36 577 591 $flatten\f_permutation_.\round_.$xor$round.v:126$219 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
593 xor 36 406 381 $flatten\f_permutation_.\round_.$xor$round.v:61$172 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
594 xor 36 593 395 $flatten\f_permutation_.\round_.$xor$round.v:61$173 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
595 sort bitvec 45
596 slice 595 594 63 19
597 sort bitvec 19
598 slice 597 594 18 0
599 concat 36 598 596
600 not 36 577 $flatten\f_permutation_.\round_.$not$round.v:126$214 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
601 and 36 600 582 $flatten\f_permutation_.\round_.$and$round.v:126$215 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
602 xor 36 599 601 $flatten\f_permutation_.\round_.$xor$round.v:126$216 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
603 xor 36 376 436 $flatten\f_permutation_.\round_.$xor$round.v:61$160 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
604 xor 36 603 451 $flatten\f_permutation_.\round_.$xor$round.v:61$161 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
605 slice 575 604 63 61
606 slice 573 604 60 0
607 concat 36 606 605
608 not 36 599 $flatten\f_permutation_.\round_.$not$round.v:126$211 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
609 and 36 608 577 $flatten\f_permutation_.\round_.$and$round.v:126$212 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
610 xor 36 607 609 $flatten\f_permutation_.\round_.$xor$round.v:126$213 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
611 not 36 607 $flatten\f_permutation_.\round_.$not$round.v:126$208 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
612 and 36 611 599 $flatten\f_permutation_.\round_.$and$round.v:126$209 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
613 xor 36 590 612 $flatten\f_permutation_.\round_.$xor$round.v:126$210 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
614 not 36 590 $flatten\f_permutation_.\round_.$not$round.v:126$205 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
615 and 36 614 607 $flatten\f_permutation_.\round_.$and$round.v:126$206 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
616 xor 36 582 615 $flatten\f_permutation_.\round_.$xor$round.v:126$207 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
617 xor 36 435 418 $flatten\f_permutation_.\round_.$xor$round.v:61$188 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
618 xor 36 617 464 $flatten\f_permutation_.\round_.$xor$round.v:61$189 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
619 sort bitvec 14
620 slice 619 618 63 50
621 sort bitvec 50
622 slice 621 618 49 0
623 concat 36 622 620
624 xor 36 373 436 $flatten\f_permutation_.\round_.$xor$round.v:61$140 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
625 xor 36 624 451 $flatten\f_permutation_.\round_.$xor$round.v:61$141 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
626 not 36 625 $flatten\f_permutation_.\round_.$not$round.v:126$202 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
627 xor 36 402 381 $flatten\f_permutation_.\round_.$xor$round.v:61$152 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
628 xor 36 627 395 $flatten\f_permutation_.\round_.$xor$round.v:61$153 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
629 slice 588 628 63 20
630 slice 586 628 19 0
631 concat 36 630 629
632 and 36 626 631 $flatten\f_permutation_.\round_.$and$round.v:126$203 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
633 xor 36 623 632 $flatten\f_permutation_.\round_.$xor$round.v:126$204 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
634 xor 36 415 391 $flatten\f_permutation_.\round_.$xor$round.v:61$176 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
635 xor 36 634 439 $flatten\f_permutation_.\round_.$xor$round.v:61$177 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
636 sort bitvec 21
637 slice 636 635 63 43
638 sort bitvec 43
639 slice 638 635 42 0
640 concat 36 639 637
641 not 36 623 $flatten\f_permutation_.\round_.$not$round.v:126$199 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
642 and 36 641 625 $flatten\f_permutation_.\round_.$and$round.v:126$200 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
643 xor 36 640 642 $flatten\f_permutation_.\round_.$xor$round.v:126$201 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
644 xor 36 386 408 $flatten\f_permutation_.\round_.$xor$round.v:61$164 ; keccak.v:94.7-94.91|round.v:61.32-61.65|f_permutation.v:62.7-62.39
645 xor 36 644 421 $flatten\f_permutation_.\round_.$xor$round.v:61$165 ; keccak.v:94.7-94.91|round.v:61.32-61.129|f_permutation.v:62.7-62.39
646 slice 638 645 63 21
647 slice 636 645 20 0
648 concat 36 647 646
649 not 36 640 $flatten\f_permutation_.\round_.$not$round.v:126$196 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
650 and 36 649 623 $flatten\f_permutation_.\round_.$and$round.v:126$197 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
651 xor 36 648 650 $flatten\f_permutation_.\round_.$xor$round.v:126$198 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
652 not 36 648 $flatten\f_permutation_.\round_.$not$round.v:126$193 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
653 and 36 652 640 $flatten\f_permutation_.\round_.$and$round.v:126$194 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
654 xor 36 631 653 $flatten\f_permutation_.\round_.$xor$round.v:126$195 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
655 not 36 631 $flatten\f_permutation_.\round_.$not$round.v:126$190 ; keccak.v:94.7-94.91|round.v:126.44-126.73|f_permutation.v:62.7-62.39
656 and 36 655 648 $flatten\f_permutation_.\round_.$and$round.v:126$191 ; keccak.v:94.7-94.91|round.v:126.43-126.116|f_permutation.v:62.7-62.39
657 xor 36 625 656 $flatten\f_permutation_.\round_.$xor$round.v:126$192 ; keccak.v:94.7-94.91|round.v:126.32-126.117|f_permutation.v:62.7-62.39
658 slice 3 657 0 0
659 state 455 f_permutation_.i
660 slice 3 659 3 3
661 or 3 211 660 $flatten\f_permutation_.\rconst_.$or$rconst.v:25$40 ; keccak.v:94.7-94.91|rconst.v:25.17-25.28|f_permutation.v:59.7-59.32
662 slice 3 659 4 4
663 or 3 661 662 $flatten\f_permutation_.\rconst_.$or$rconst.v:25$41 ; keccak.v:94.7-94.91|rconst.v:25.17-25.35|f_permutation.v:59.7-59.32
664 slice 3 659 5 5
665 or 3 663 664 $flatten\f_permutation_.\rconst_.$or$rconst.v:25$42 ; keccak.v:94.7-94.91|rconst.v:25.17-25.42|f_permutation.v:59.7-59.32
666 slice 3 659 6 6
667 or 3 665 666 $flatten\f_permutation_.\rconst_.$or$rconst.v:25$43 ; keccak.v:94.7-94.91|rconst.v:25.17-25.49|f_permutation.v:59.7-59.32
668 slice 3 659 9 9
669 or 3 667 668 $flatten\f_permutation_.\rconst_.$or$rconst.v:25$44 ; keccak.v:94.7-94.91|rconst.v:25.17-25.57|f_permutation.v:59.7-59.32
670 slice 3 659 11 11
671 or 3 669 670 $flatten\f_permutation_.\rconst_.$or$rconst.v:25$45 ; keccak.v:94.7-94.91|rconst.v:25.17-25.65|f_permutation.v:59.7-59.32
672 slice 3 659 12 12
673 or 3 671 672 $flatten\f_permutation_.\rconst_.$or$rconst.v:25$46 ; keccak.v:94.7-94.91|rconst.v:25.17-25.73|f_permutation.v:59.7-59.32
674 slice 3 659 13 13
675 or 3 673 674 $flatten\f_permutation_.\rconst_.$or$rconst.v:25$47 ; keccak.v:94.7-94.91|rconst.v:25.17-25.81|f_permutation.v:59.7-59.32
676 slice 3 659 14 14
677 or 3 675 676 $flatten\f_permutation_.\rconst_.$or$rconst.v:25$48 ; keccak.v:94.7-94.91|rconst.v:25.17-25.89|f_permutation.v:59.7-59.32
678 slice 3 659 19 19
679 or 3 677 678 $flatten\f_permutation_.\rconst_.$or$rconst.v:25$49 ; keccak.v:94.7-94.91|rconst.v:25.17-25.97|f_permutation.v:59.7-59.32
680 slice 3 659 21 21
681 or 3 679 680 $flatten\f_permutation_.\rconst_.$or$rconst.v:25$50 ; keccak.v:94.7-94.91|rconst.v:25.17-25.105|f_permutation.v:59.7-59.32
682 xor 3 658 681 $flatten\f_permutation_.\round_.$xor$round.v:136$265 ; keccak.v:94.7-94.91|round.v:136.33-136.60|f_permutation.v:62.7-62.39
683 slice 3 657 1 1
684 slice 3 659 0 0
685 slice 3 659 1 1
686 or 3 684 685 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$84 ; keccak.v:94.7-94.91|rconst.v:29.18-29.29|f_permutation.v:59.7-59.32
687 or 3 686 660 $flatten\f_permutation_.\rconst_.$or$rconst.v:28$74 ; keccak.v:94.7-94.91|rconst.v:28.17-28.35|f_permutation.v:59.7-59.32
688 slice 3 659 7 7
689 or 3 687 688 $flatten\f_permutation_.\rconst_.$or$rconst.v:26$53 ; keccak.v:94.7-94.91|rconst.v:26.17-26.42|f_permutation.v:59.7-59.32
690 slice 3 659 10 10
691 or 3 689 690 $flatten\f_permutation_.\rconst_.$or$rconst.v:26$54 ; keccak.v:94.7-94.91|rconst.v:26.17-26.50|f_permutation.v:59.7-59.32
692 or 3 691 670 $flatten\f_permutation_.\rconst_.$or$rconst.v:26$55 ; keccak.v:94.7-94.91|rconst.v:26.17-26.58|f_permutation.v:59.7-59.32
693 or 3 692 672 $flatten\f_permutation_.\rconst_.$or$rconst.v:26$56 ; keccak.v:94.7-94.91|rconst.v:26.17-26.66|f_permutation.v:59.7-59.32
694 or 3 693 676 $flatten\f_permutation_.\rconst_.$or$rconst.v:26$57 ; keccak.v:94.7-94.91|rconst.v:26.17-26.74|f_permutation.v:59.7-59.32
695 slice 3 659 15 15
696 or 3 694 695 $flatten\f_permutation_.\rconst_.$or$rconst.v:26$58 ; keccak.v:94.7-94.91|rconst.v:26.17-26.82|f_permutation.v:59.7-59.32
697 slice 3 659 17 17
698 or 3 696 697 $flatten\f_permutation_.\rconst_.$or$rconst.v:26$59 ; keccak.v:94.7-94.91|rconst.v:26.17-26.90|f_permutation.v:59.7-59.32
699 slice 3 659 18 18
700 or 3 698 699 $flatten\f_permutation_.\rconst_.$or$rconst.v:26$60 ; keccak.v:94.7-94.91|rconst.v:26.17-26.98|f_permutation.v:59.7-59.32
701 xor 3 683 700 $flatten\f_permutation_.\round_.$xor$round.v:136$266 ; keccak.v:94.7-94.91|round.v:136.33-136.60|f_permutation.v:62.7-62.39
702 slice 3 657 3 3
703 or 3 685 660 $flatten\f_permutation_.\rconst_.$or$rconst.v:27$61 ; keccak.v:94.7-94.91|rconst.v:27.17-27.28|f_permutation.v:59.7-59.32
704 or 3 703 666 $flatten\f_permutation_.\rconst_.$or$rconst.v:27$62 ; keccak.v:94.7-94.91|rconst.v:27.17-27.35|f_permutation.v:59.7-59.32
705 or 3 704 688 $flatten\f_permutation_.\rconst_.$or$rconst.v:27$63 ; keccak.v:94.7-94.91|rconst.v:27.17-27.42|f_permutation.v:59.7-59.32
706 slice 3 659 8 8
707 or 3 705 706 $flatten\f_permutation_.\rconst_.$or$rconst.v:27$64 ; keccak.v:94.7-94.91|rconst.v:27.17-27.49|f_permutation.v:59.7-59.32
708 or 3 707 668 $flatten\f_permutation_.\rconst_.$or$rconst.v:27$65 ; keccak.v:94.7-94.91|rconst.v:27.17-27.57|f_permutation.v:59.7-59.32
709 or 3 708 690 $flatten\f_permutation_.\rconst_.$or$rconst.v:27$66 ; keccak.v:94.7-94.91|rconst.v:27.17-27.65|f_permutation.v:59.7-59.32
710 or 3 709 670 $flatten\f_permutation_.\rconst_.$or$rconst.v:27$67 ; keccak.v:94.7-94.91|rconst.v:27.17-27.73|f_permutation.v:59.7-59.32
711 or 3 710 672 $flatten\f_permutation_.\rconst_.$or$rconst.v:27$68 ; keccak.v:94.7-94.91|rconst.v:27.17-27.81|f_permutation.v:59.7-59.32
712 or 3 711 674 $flatten\f_permutation_.\rconst_.$or$rconst.v:27$69 ; keccak.v:94.7-94.91|rconst.v:27.17-27.89|f_permutation.v:59.7-59.32
713 or 3 712 697 $flatten\f_permutation_.\rconst_.$or$rconst.v:27$70 ; keccak.v:94.7-94.91|rconst.v:27.17-27.97|f_permutation.v:59.7-59.32
714 or 3 713 699 $flatten\f_permutation_.\rconst_.$or$rconst.v:27$71 ; keccak.v:94.7-94.91|rconst.v:27.17-27.105|f_permutation.v:59.7-59.32
715 slice 3 659 22 22
716 or 3 714 715 $flatten\f_permutation_.\rconst_.$or$rconst.v:27$72 ; keccak.v:94.7-94.91|rconst.v:27.17-27.113|f_permutation.v:59.7-59.32
717 xor 3 702 716 $flatten\f_permutation_.\round_.$xor$round.v:136$267 ; keccak.v:94.7-94.91|round.v:136.33-136.60|f_permutation.v:62.7-62.39
718 slice 3 657 7 7
719 or 3 687 664 $flatten\f_permutation_.\rconst_.$or$rconst.v:28$75 ; keccak.v:94.7-94.91|rconst.v:28.17-28.42|f_permutation.v:59.7-59.32
720 or 3 719 688 $flatten\f_permutation_.\rconst_.$or$rconst.v:28$76 ; keccak.v:94.7-94.91|rconst.v:28.17-28.49|f_permutation.v:59.7-59.32
721 or 3 720 706 $flatten\f_permutation_.\rconst_.$or$rconst.v:28$77 ; keccak.v:94.7-94.91|rconst.v:28.17-28.56|f_permutation.v:59.7-59.32
722 or 3 721 670 $flatten\f_permutation_.\rconst_.$or$rconst.v:28$78 ; keccak.v:94.7-94.91|rconst.v:28.17-28.64|f_permutation.v:59.7-59.32
723 or 3 722 672 $flatten\f_permutation_.\rconst_.$or$rconst.v:28$79 ; keccak.v:94.7-94.91|rconst.v:28.17-28.72|f_permutation.v:59.7-59.32
724 or 3 723 674 $flatten\f_permutation_.\rconst_.$or$rconst.v:28$80 ; keccak.v:94.7-94.91|rconst.v:28.17-28.80|f_permutation.v:59.7-59.32
725 slice 3 659 16 16
726 or 3 724 725 $flatten\f_permutation_.\rconst_.$or$rconst.v:28$81 ; keccak.v:94.7-94.91|rconst.v:28.17-28.88|f_permutation.v:59.7-59.32
727 or 3 726 678 $flatten\f_permutation_.\rconst_.$or$rconst.v:28$82 ; keccak.v:94.7-94.91|rconst.v:28.17-28.96|f_permutation.v:59.7-59.32
728 slice 3 659 20 20
729 or 3 727 728 $flatten\f_permutation_.\rconst_.$or$rconst.v:28$83 ; keccak.v:94.7-94.91|rconst.v:28.17-28.104|f_permutation.v:59.7-59.32
730 xor 3 718 729 $flatten\f_permutation_.\round_.$xor$round.v:136$268 ; keccak.v:94.7-94.91|round.v:136.33-136.60|f_permutation.v:62.7-62.39
731 slice 3 657 15 15
732 slice 3 659 2 2
733 or 3 686 732 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$85 ; keccak.v:94.7-94.91|rconst.v:29.18-29.36|f_permutation.v:59.7-59.32
734 or 3 733 660 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$86 ; keccak.v:94.7-94.91|rconst.v:29.18-29.43|f_permutation.v:59.7-59.32
735 or 3 734 664 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$87 ; keccak.v:94.7-94.91|rconst.v:29.18-29.50|f_permutation.v:59.7-59.32
736 or 3 735 666 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$88 ; keccak.v:94.7-94.91|rconst.v:29.18-29.57|f_permutation.v:59.7-59.32
737 or 3 736 668 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$89 ; keccak.v:94.7-94.91|rconst.v:29.18-29.65|f_permutation.v:59.7-59.32
738 or 3 737 670 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$90 ; keccak.v:94.7-94.91|rconst.v:29.18-29.73|f_permutation.v:59.7-59.32
739 or 3 738 674 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$91 ; keccak.v:94.7-94.91|rconst.v:29.18-29.81|f_permutation.v:59.7-59.32
740 or 3 739 676 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$92 ; keccak.v:94.7-94.91|rconst.v:29.18-29.89|f_permutation.v:59.7-59.32
741 or 3 740 695 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$93 ; keccak.v:94.7-94.91|rconst.v:29.18-29.97|f_permutation.v:59.7-59.32
742 or 3 741 697 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$94 ; keccak.v:94.7-94.91|rconst.v:29.18-29.105|f_permutation.v:59.7-59.32
743 or 3 742 678 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$95 ; keccak.v:94.7-94.91|rconst.v:29.18-29.113|f_permutation.v:59.7-59.32
744 or 3 743 728 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$96 ; keccak.v:94.7-94.91|rconst.v:29.18-29.121|f_permutation.v:59.7-59.32
745 or 3 744 715 $flatten\f_permutation_.\rconst_.$or$rconst.v:29$97 ; keccak.v:94.7-94.91|rconst.v:29.18-29.129|f_permutation.v:59.7-59.32
746 xor 3 731 745 $flatten\f_permutation_.\round_.$xor$round.v:136$269 ; keccak.v:94.7-94.91|round.v:136.33-136.60|f_permutation.v:62.7-62.39
747 slice 3 657 31 31
748 or 3 732 662 $flatten\f_permutation_.\rconst_.$or$rconst.v:30$98 ; keccak.v:94.7-94.91|rconst.v:30.18-30.29|f_permutation.v:59.7-59.32
749 or 3 748 664 $flatten\f_permutation_.\rconst_.$or$rconst.v:30$99 ; keccak.v:94.7-94.91|rconst.v:30.18-30.36|f_permutation.v:59.7-59.32
750 or 3 749 668 $flatten\f_permutation_.\rconst_.$or$rconst.v:30$100 ; keccak.v:94.7-94.91|rconst.v:30.18-30.44|f_permutation.v:59.7-59.32
751 or 3 750 690 $flatten\f_permutation_.\rconst_.$or$rconst.v:30$101 ; keccak.v:94.7-94.91|rconst.v:30.18-30.52|f_permutation.v:59.7-59.32
752 or 3 751 670 $flatten\f_permutation_.\rconst_.$or$rconst.v:30$102 ; keccak.v:94.7-94.91|rconst.v:30.18-30.60|f_permutation.v:59.7-59.32
753 or 3 752 699 $flatten\f_permutation_.\rconst_.$or$rconst.v:30$103 ; keccak.v:94.7-94.91|rconst.v:30.18-30.68|f_permutation.v:59.7-59.32
754 or 3 753 678 $flatten\f_permutation_.\rconst_.$or$rconst.v:30$104 ; keccak.v:94.7-94.91|rconst.v:30.18-30.76|f_permutation.v:59.7-59.32
755 or 3 754 680 $flatten\f_permutation_.\rconst_.$or$rconst.v:30$105 ; keccak.v:94.7-94.91|rconst.v:30.18-30.84|f_permutation.v:59.7-59.32
756 or 3 755 715 $flatten\f_permutation_.\rconst_.$or$rconst.v:30$106 ; keccak.v:94.7-94.91|rconst.v:30.18-30.92|f_permutation.v:59.7-59.32
757 xor 3 747 756 $flatten\f_permutation_.\round_.$xor$round.v:136$270 ; keccak.v:94.7-94.91|round.v:136.33-136.60|f_permutation.v:62.7-62.39
758 slice 3 657 63 63
759 or 3 685 732 $flatten\f_permutation_.\rconst_.$or$rconst.v:31$107 ; keccak.v:94.7-94.91|rconst.v:31.18-31.29|f_permutation.v:59.7-59.32
760 or 3 759 664 $flatten\f_permutation_.\rconst_.$or$rconst.v:31$108 ; keccak.v:94.7-94.91|rconst.v:31.18-31.36|f_permutation.v:59.7-59.32
761 or 3 760 666 $flatten\f_permutation_.\rconst_.$or$rconst.v:31$109 ; keccak.v:94.7-94.91|rconst.v:31.18-31.43|f_permutation.v:59.7-59.32
762 or 3 761 672 $flatten\f_permutation_.\rconst_.$or$rconst.v:31$110 ; keccak.v:94.7-94.91|rconst.v:31.18-31.51|f_permutation.v:59.7-59.32
763 or 3 762 674 $flatten\f_permutation_.\rconst_.$or$rconst.v:31$111 ; keccak.v:94.7-94.91|rconst.v:31.18-31.59|f_permutation.v:59.7-59.32
764 or 3 763 676 $flatten\f_permutation_.\rconst_.$or$rconst.v:31$112 ; keccak.v:94.7-94.91|rconst.v:31.18-31.67|f_permutation.v:59.7-59.32
765 or 3 764 695 $flatten\f_permutation_.\rconst_.$or$rconst.v:31$113 ; keccak.v:94.7-94.91|rconst.v:31.18-31.75|f_permutation.v:59.7-59.32
766 or 3 765 725 $flatten\f_permutation_.\rconst_.$or$rconst.v:31$114 ; keccak.v:94.7-94.91|rconst.v:31.18-31.83|f_permutation.v:59.7-59.32
767 or 3 766 699 $flatten\f_permutation_.\rconst_.$or$rconst.v:31$115 ; keccak.v:94.7-94.91|rconst.v:31.18-31.91|f_permutation.v:59.7-59.32
768 or 3 767 678 $flatten\f_permutation_.\rconst_.$or$rconst.v:31$116 ; keccak.v:94.7-94.91|rconst.v:31.18-31.99|f_permutation.v:59.7-59.32
769 or 3 768 728 $flatten\f_permutation_.\rconst_.$or$rconst.v:31$117 ; keccak.v:94.7-94.91|rconst.v:31.18-31.107|f_permutation.v:59.7-59.32
770 or 3 769 715 $flatten\f_permutation_.\rconst_.$or$rconst.v:31$118 ; keccak.v:94.7-94.91|rconst.v:31.18-31.115|f_permutation.v:59.7-59.32
771 xor 3 758 770 $flatten\f_permutation_.\round_.$xor$round.v:136$271 ; keccak.v:94.7-94.91|round.v:136.33-136.60|f_permutation.v:62.7-62.39
772 concat 60 460 447
773 concat 84 473 772
774 concat 108 476 773
775 concat 132 479 774
776 concat 156 501 775
777 concat 180 511 776
778 concat 204 521 777
779 concat 214 524 778
780 sort bitvec 640
781 concat 780 527 779
782 sort bitvec 704
783 concat 782 548 781
784 sort bitvec 768
785 concat 784 556 783
786 sort bitvec 832
787 concat 786 564 785
788 sort bitvec 896
789 concat 788 567 787
790 sort bitvec 960
791 concat 790 570 789
792 concat 368 592 791
793 sort bitvec 1088
794 concat 793 602 792
795 sort bitvec 1152
796 concat 795 610 794
797 sort bitvec 1216
798 concat 797 613 796
799 sort bitvec 1280
800 concat 799 616 798
801 sort bitvec 1344
802 concat 801 633 800
803 sort bitvec 1408
804 concat 803 643 802
805 sort bitvec 1472
806 concat 805 651 804
807 sort bitvec 1536
808 concat 807 654 806
809 sort bitvec 1537
810 concat 809 682 808
811 sort bitvec 1538
812 concat 811 701 810
813 slice 3 657 2 2
814 sort bitvec 1539
815 concat 814 813 812
816 sort bitvec 1540
817 concat 816 717 815
818 slice 575 657 6 4
819 sort bitvec 1543
820 concat 819 818 817
821 sort bitvec 1544
822 concat 821 730 820
823 sort bitvec 7
824 slice 823 657 14 8
825 sort bitvec 1551
826 concat 825 824 822
827 sort bitvec 1552
828 concat 827 746 826
829 slice 504 657 30 16
830 sort bitvec 1567
831 concat 830 829 828
832 sort bitvec 1568
833 concat 832 757 831
834 sort bitvec 31
835 slice 834 657 62 32
836 sort bitvec 1599
837 concat 836 835 833
838 concat 14 771 837
839 uext 14 838 0 f_permutation_.round_out ; keccak.v:94.7-94.91|f_permutation.v:28.35-28.44
840 uext 14 371 0 f_permutation_.round_in ; keccak.v:94.7-94.91|f_permutation.v:28.25-28.33
841 uext 3 9 0 f_permutation_.reset ; keccak.v:94.7-94.91|f_permutation.v:20.30-20.35
842 const 3 0
843 const 575 000
844 const 823 0000000
845 const 504 000000000000000
846 const 834 0000000000000000000000000000000
847 concat 1 700 681
848 concat 575 842 847
849 sort bitvec 4
850 concat 849 716 848
851 concat 823 843 850
852 concat 16 729 851
853 concat 504 844 852
854 concat 19 745 853
855 concat 834 845 854
856 concat 5 756 855
857 concat 393 846 856
858 concat 36 770 857
859 uext 36 858 0 f_permutation_.rc ; keccak.v:94.7-94.91|f_permutation.v:29.25-29.27
860 state 3 f_permutation_.out_ready
861 uext 3 12 0 f_permutation_.in_ready ; keccak.v:94.7-94.91|f_permutation.v:22.25-22.33
862 uext 214 365 0 f_permutation_.in ; keccak.v:94.7-94.91|f_permutation.v:21.25-21.27
863 uext 3 4 0 f_permutation_.clk ; keccak.v:94.7-94.91|f_permutation.v:20.25-20.28
864 uext 3 211 0 f_permutation_.ack ; keccak.v:94.7-94.91|f_permutation.v:23.25-23.28
865 uext 3 211 0 f_permutation_.accept ; keccak.v:94.7-94.91|f_permutation.v:31.25-31.31
866 uext 36 373 0 f_permutation_.round_.a[0] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
867 uext 36 383 0 f_permutation_.round_.a[10] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
868 uext 36 384 0 f_permutation_.round_.a[11] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
869 uext 36 386 0 f_permutation_.round_.a[12] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
870 uext 36 388 0 f_permutation_.round_.a[13] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
871 uext 36 390 0 f_permutation_.round_.a[14] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
872 uext 36 410 0 f_permutation_.round_.a[15] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
873 uext 36 411 0 f_permutation_.round_.a[16] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
874 uext 36 413 0 f_permutation_.round_.a[17] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
875 uext 36 415 0 f_permutation_.round_.a[18] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
876 uext 36 417 0 f_permutation_.round_.a[19] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
877 uext 36 374 0 f_permutation_.round_.a[1] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
878 uext 36 428 0 f_permutation_.round_.a[20] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
879 uext 36 429 0 f_permutation_.round_.a[21] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
880 uext 36 431 0 f_permutation_.round_.a[22] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
881 uext 36 433 0 f_permutation_.round_.a[23] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
882 uext 36 435 0 f_permutation_.round_.a[24] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
883 uext 36 376 0 f_permutation_.round_.a[2] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
884 uext 36 378 0 f_permutation_.round_.a[3] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
885 uext 36 380 0 f_permutation_.round_.a[4] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
886 uext 36 401 0 f_permutation_.round_.a[5] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
887 uext 36 402 0 f_permutation_.round_.a[6] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
888 uext 36 404 0 f_permutation_.round_.a[7] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
889 uext 36 406 0 f_permutation_.round_.a[8] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
890 uext 36 372 0 f_permutation_.round_.a[9] ; keccak.v:94.7-94.91|round.v:30.21-30.22|f_permutation.v:62.7-62.39
891 uext 36 381 0 f_permutation_.round_.b[0] ; keccak.v:94.7-94.91|round.v:31.21-31.22|f_permutation.v:62.7-62.39
892 uext 36 408 0 f_permutation_.round_.b[1] ; keccak.v:94.7-94.91|round.v:31.21-31.22|f_permutation.v:62.7-62.39
893 uext 36 391 0 f_permutation_.round_.b[2] ; keccak.v:94.7-94.91|round.v:31.21-31.22|f_permutation.v:62.7-62.39
894 uext 36 418 0 f_permutation_.round_.b[3] ; keccak.v:94.7-94.91|round.v:31.21-31.22|f_permutation.v:62.7-62.39
895 uext 36 436 0 f_permutation_.round_.b[4] ; keccak.v:94.7-94.91|round.v:31.21-31.22|f_permutation.v:62.7-62.39
896 uext 36 625 0 f_permutation_.round_.c[0] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
897 uext 36 422 0 f_permutation_.round_.c[10] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
898 uext 36 541 0 f_permutation_.round_.c[11] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
899 uext 36 645 0 f_permutation_.round_.c[12] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
900 uext 36 503 0 f_permutation_.round_.c[13] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
901 uext 36 572 0 f_permutation_.round_.c[14] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
902 uext 36 579 0 f_permutation_.round_.c[15] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
903 uext 36 440 0 f_permutation_.round_.c[16] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
904 uext 36 558 0 f_permutation_.round_.c[17] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
905 uext 36 635 0 f_permutation_.round_.c[18] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
906 uext 36 481 0 f_permutation_.round_.c[19] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
907 uext 36 494 0 f_permutation_.round_.c[1] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
908 uext 36 486 0 f_permutation_.round_.c[20] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
909 uext 36 585 0 f_permutation_.round_.c[21] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
910 uext 36 465 0 f_permutation_.round_.c[22] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
911 uext 36 550 0 f_permutation_.round_.c[23] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
912 uext 36 618 0 f_permutation_.round_.c[24] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
913 uext 36 604 0 f_permutation_.round_.c[2] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
914 uext 36 452 0 f_permutation_.round_.c[3] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
915 uext 36 529 0 f_permutation_.round_.c[4] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
916 uext 36 535 0 f_permutation_.round_.c[5] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
917 uext 36 628 0 f_permutation_.round_.c[6] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
918 uext 36 513 0 f_permutation_.round_.c[7] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
919 uext 36 594 0 f_permutation_.round_.c[8] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
920 uext 36 396 0 f_permutation_.round_.c[9] ; keccak.v:94.7-94.91|round.v:32.21-32.22|f_permutation.v:62.7-62.39
921 uext 36 625 0 f_permutation_.round_.d[0] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
922 uext 36 425 0 f_permutation_.round_.d[10] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
923 uext 36 546 0 f_permutation_.round_.d[11] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
924 uext 36 648 0 f_permutation_.round_.d[12] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
925 uext 36 508 0 f_permutation_.round_.d[13] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
926 uext 36 577 0 f_permutation_.round_.d[14] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
927 uext 36 582 0 f_permutation_.round_.d[15] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
928 uext 36 445 0 f_permutation_.round_.d[16] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
929 uext 36 561 0 f_permutation_.round_.d[17] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
930 uext 36 640 0 f_permutation_.round_.d[18] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
931 uext 36 484 0 f_permutation_.round_.d[19] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
932 uext 36 499 0 f_permutation_.round_.d[1] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
933 uext 36 491 0 f_permutation_.round_.d[20] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
934 uext 36 590 0 f_permutation_.round_.d[21] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
935 uext 36 470 0 f_permutation_.round_.d[22] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
936 uext 36 553 0 f_permutation_.round_.d[23] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
937 uext 36 623 0 f_permutation_.round_.d[24] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
938 uext 36 607 0 f_permutation_.round_.d[2] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
939 uext 36 457 0 f_permutation_.round_.d[3] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
940 uext 36 533 0 f_permutation_.round_.d[4] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
941 uext 36 538 0 f_permutation_.round_.d[5] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
942 uext 36 631 0 f_permutation_.round_.d[6] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
943 uext 36 518 0 f_permutation_.round_.d[7] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
944 uext 36 599 0 f_permutation_.round_.d[8] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
945 uext 36 400 0 f_permutation_.round_.d[9] ; keccak.v:94.7-94.91|round.v:32.34-32.35|f_permutation.v:62.7-62.39
946 uext 36 625 0 f_permutation_.round_.e[0] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
947 uext 36 648 0 f_permutation_.round_.e[10] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
948 uext 36 607 0 f_permutation_.round_.e[11] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
949 uext 36 561 0 f_permutation_.round_.e[12] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
950 uext 36 518 0 f_permutation_.round_.e[13] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
951 uext 36 470 0 f_permutation_.round_.e[14] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
952 uext 36 640 0 f_permutation_.round_.e[15] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
953 uext 36 599 0 f_permutation_.round_.e[16] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
954 uext 36 553 0 f_permutation_.round_.e[17] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
955 uext 36 508 0 f_permutation_.round_.e[18] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
956 uext 36 457 0 f_permutation_.round_.e[19] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
957 uext 36 582 0 f_permutation_.round_.e[1] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
958 uext 36 623 0 f_permutation_.round_.e[20] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
959 uext 36 577 0 f_permutation_.round_.e[21] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
960 uext 36 533 0 f_permutation_.round_.e[22] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
961 uext 36 484 0 f_permutation_.round_.e[23] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
962 uext 36 400 0 f_permutation_.round_.e[24] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
963 uext 36 538 0 f_permutation_.round_.e[2] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
964 uext 36 491 0 f_permutation_.round_.e[3] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
965 uext 36 425 0 f_permutation_.round_.e[4] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
966 uext 36 631 0 f_permutation_.round_.e[5] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
967 uext 36 590 0 f_permutation_.round_.e[6] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
968 uext 36 546 0 f_permutation_.round_.e[7] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
969 uext 36 499 0 f_permutation_.round_.e[8] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
970 uext 36 445 0 f_permutation_.round_.e[9] ; keccak.v:94.7-94.91|round.v:32.47-32.48|f_permutation.v:62.7-62.39
971 uext 36 657 0 f_permutation_.round_.f[0] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
972 uext 36 651 0 f_permutation_.round_.f[10] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
973 uext 36 610 0 f_permutation_.round_.f[11] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
974 uext 36 564 0 f_permutation_.round_.f[12] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
975 uext 36 521 0 f_permutation_.round_.f[13] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
976 uext 36 473 0 f_permutation_.round_.f[14] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
977 uext 36 643 0 f_permutation_.round_.f[15] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
978 uext 36 602 0 f_permutation_.round_.f[16] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
979 uext 36 556 0 f_permutation_.round_.f[17] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
980 uext 36 511 0 f_permutation_.round_.f[18] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
981 uext 36 460 0 f_permutation_.round_.f[19] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
982 uext 36 616 0 f_permutation_.round_.f[1] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
983 uext 36 633 0 f_permutation_.round_.f[20] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
984 uext 36 592 0 f_permutation_.round_.f[21] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
985 uext 36 548 0 f_permutation_.round_.f[22] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
986 uext 36 501 0 f_permutation_.round_.f[23] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
987 uext 36 447 0 f_permutation_.round_.f[24] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
988 uext 36 570 0 f_permutation_.round_.f[2] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
989 uext 36 527 0 f_permutation_.round_.f[3] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
990 uext 36 479 0 f_permutation_.round_.f[4] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
991 uext 36 654 0 f_permutation_.round_.f[5] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
992 uext 36 613 0 f_permutation_.round_.f[6] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
993 uext 36 567 0 f_permutation_.round_.f[7] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
994 uext 36 524 0 f_permutation_.round_.f[8] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
995 uext 36 476 0 f_permutation_.round_.f[9] ; keccak.v:94.7-94.91|round.v:32.60-32.61|f_permutation.v:62.7-62.39
996 concat 1 701 682
997 slice 3 657 2 2
998 concat 575 997 996
999 concat 849 717 998
1000 slice 575 657 6 4
1001 concat 823 1000 999
1002 concat 16 730 1001
1003 slice 823 657 14 8
1004 concat 504 1003 1002
1005 concat 19 746 1004
1006 slice 504 657 30 16
1007 concat 834 1006 1005
1008 concat 5 757 1007
1009 slice 834 657 62 32
1010 concat 393 1009 1008
1011 concat 36 771 1010
1012 uext 36 1011 0 f_permutation_.round_.g[0] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1013 uext 36 651 0 f_permutation_.round_.g[10] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1014 uext 36 610 0 f_permutation_.round_.g[11] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1015 uext 36 564 0 f_permutation_.round_.g[12] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1016 uext 36 521 0 f_permutation_.round_.g[13] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1017 uext 36 473 0 f_permutation_.round_.g[14] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1018 uext 36 643 0 f_permutation_.round_.g[15] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1019 uext 36 602 0 f_permutation_.round_.g[16] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1020 uext 36 556 0 f_permutation_.round_.g[17] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1021 uext 36 511 0 f_permutation_.round_.g[18] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1022 uext 36 460 0 f_permutation_.round_.g[19] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1023 uext 36 616 0 f_permutation_.round_.g[1] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1024 uext 36 633 0 f_permutation_.round_.g[20] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1025 uext 36 592 0 f_permutation_.round_.g[21] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1026 uext 36 548 0 f_permutation_.round_.g[22] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1027 uext 36 501 0 f_permutation_.round_.g[23] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1028 uext 36 447 0 f_permutation_.round_.g[24] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1029 uext 36 570 0 f_permutation_.round_.g[2] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1030 uext 36 527 0 f_permutation_.round_.g[3] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1031 uext 36 479 0 f_permutation_.round_.g[4] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1032 uext 36 654 0 f_permutation_.round_.g[5] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1033 uext 36 613 0 f_permutation_.round_.g[6] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1034 uext 36 567 0 f_permutation_.round_.g[7] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1035 uext 36 524 0 f_permutation_.round_.g[8] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1036 uext 36 476 0 f_permutation_.round_.g[9] ; keccak.v:94.7-94.91|round.v:32.73-32.74|f_permutation.v:62.7-62.39
1037 uext 14 371 0 f_permutation_.round_.in ; keccak.v:94.7-94.91|round.v:26.21-26.23|f_permutation.v:62.7-62.39
1038 uext 14 838 0 f_permutation_.round_.out ; keccak.v:94.7-94.91|round.v:28.21-28.24|f_permutation.v:62.7-62.39
1039 uext 36 858 0 f_permutation_.round_.round_const ; keccak.v:94.7-94.91|round.v:27.21-27.32|f_permutation.v:62.7-62.39
1040 concat 22 659 211
1041 uext 22 1040 0 f_permutation_.rconst_.i ; keccak.v:94.7-94.91|rconst.v:19.23-19.24|f_permutation.v:59.7-59.32
1042 uext 36 858 0 f_permutation_.rconst_.rc ; keccak.v:94.7-94.91|rconst.v:20.23-20.25|f_permutation.v:59.7-59.32
1043 slice 823 6 6 0
1044 input 5
1045 const 16 00000001
1046 slice 22 6 31 8
1047 concat 5 1046 1045
1048 const 1 11
1049 eq 3 2 1048 $flatten\padder_.\p0.$procmux$273_CMP0 ; keccak.v:91.7-91.112|padder1.v:0.0-0.0|padder1.v:31.7-36.14|padder.v:71.13-71.34
1050 ite 5 1049 1047 1044
1051 const 19 0000000100000000
1052 slice 19 6 31 16
1053 concat 5 1052 1051
1054 const 1 10
1055 eq 3 2 1054 $flatten\padder_.\p0.$procmux$274_CMP0 ; keccak.v:91.7-91.112|padder1.v:0.0-0.0|padder1.v:31.7-36.14|padder.v:71.13-71.34
1056 ite 5 1055 1053 1050
1057 const 22 000000010000000000000000
1058 slice 16 6 31 24
1059 concat 5 1058 1057
1060 const 1 01
1061 eq 3 2 1060 $flatten\padder_.\p0.$procmux$275_CMP0 ; keccak.v:91.7-91.112|padder1.v:0.0-0.0|padder1.v:31.7-36.14|padder.v:71.13-71.34
1062 ite 5 1061 1059 1056
1063 const 5 00000001000000000000000000000000
1064 redor 3 2
1065 not 3 1064 $flatten\padder_.\p0.$procmux$276_CMP0 ; keccak.v:91.7-91.112|padder1.v:0.0-0.0|padder1.v:31.7-36.14|padder.v:71.13-71.34
1066 ite 5 1065 1063 1062 $flatten\padder_.\p0.$procmux$272 ; keccak.v:91.7-91.112|padder1.v:0.0-0.0|padder1.v:31.7-36.14|padder.v:71.13-71.34
1067 slice 823 1066 6 0
1068 ite 823 8 1067 1043 $flatten\padder_.$procmux$322 ; keccak.v:91.7-91.112|padder.v:80.14-86.14|padder.v:80.18-80.30
1069 state 3 padder_.state
1070 ite 823 1069 844 1068 $flatten\padder_.$procmux$331 ; keccak.v:91.7-91.112|padder.v:75.9-86.14|padder.v:75.13-75.18
1071 slice 3 6 7 7
1072 slice 3 1066 7 7
1073 slice 3 11 16 16
1074 or 3 1072 1073 $flatten\padder_.$or$padder.v:85$21 ; keccak.v:91.7-91.112|padder.v:85.21-85.34
1075 ite 3 8 1074 1071 $flatten\padder_.$procmux$316 ; keccak.v:91.7-91.112|padder.v:80.14-86.14|padder.v:80.18-80.30
1076 ite 3 1069 1073 1075 $flatten\padder_.$procmux$334 ; keccak.v:91.7-91.112|padder.v:75.9-86.14|padder.v:75.13-75.18
1077 slice 22 6 31 8
1078 slice 22 1066 31 8
1079 ite 22 8 1078 1077 $flatten\padder_.$procmux$310 ; keccak.v:91.7-91.112|padder.v:80.14-86.14|padder.v:80.18-80.30
1080 const 22 000000000000000000000000
1081 ite 22 1069 1080 1079 $flatten\padder_.$procmux$328 ; keccak.v:91.7-91.112|padder.v:75.9-86.14|padder.v:75.13-75.18
1082 concat 16 1076 1070
1083 concat 5 1081 1082
1084 uext 5 1083 0 padder_.v1 ; keccak.v:91.7-91.112|padder.v:36.24-36.26
1085 uext 5 1066 0 padder_.v0 ; keccak.v:91.7-91.112|padder.v:35.24-35.26
1086 not 3 1069 $flatten\padder_.$not$padder.v:42$1 ; keccak.v:91.7-91.112|padder.v:42.22-42.29
1087 and 3 1086 7 $flatten\padder_.$and$padder.v:42$2 ; keccak.v:91.7-91.112|padder.v:42.21-42.41
1088 not 3 12 $flatten\padder_.$not$padder.v:43$5 ; keccak.v:91.7-91.112|padder.v:43.41-43.54
1089 and 3 1087 1088 $flatten\padder_.$and$padder.v:42$4 ; keccak.v:91.7-91.112|padder.v:42.21-42.59
1090 and 3 1069 1088 $flatten\padder_.$and$padder.v:43$6 ; keccak.v:91.7-91.112|padder.v:43.32-43.55
1091 or 3 1089 1090 $flatten\padder_.$or$padder.v:43$7 ; keccak.v:91.7-91.112|padder.v:43.22-43.56
1092 state 3 padder_.done
1093 not 3 1092 $flatten\padder_.$not$padder.v:43$8 ; keccak.v:91.7-91.112|padder.v:43.61-43.67
1094 and 3 1091 1093 $flatten\padder_.$and$padder.v:43$9 ; keccak.v:91.7-91.112|padder.v:43.21-43.68
1095 uext 3 1094 0 padder_.update ; keccak.v:91.7-91.112|padder.v:38.24-38.30
1096 uext 3 9 0 padder_.reset ; keccak.v:91.7-91.112|padder.v:22.29-22.34
1097 uext 3 12 0 padder_.out_ready ; keccak.v:91.7-91.112|padder.v:28.24-28.33
1098 uext 3 8 0 padder_.is_last ; keccak.v:91.7-91.112|padder.v:24.34-24.41
1099 uext 3 7 0 padder_.in_ready ; keccak.v:91.7-91.112|padder.v:24.24-24.32
1100 uext 5 6 0 padder_.in ; keccak.v:91.7-91.112|padder.v:23.24-23.26
1101 uext 3 211 0 padder_.f_ack ; keccak.v:91.7-91.112|padder.v:29.24-29.29
1102 uext 3 4 0 padder_.clk ; keccak.v:91.7-91.112|padder.v:22.24-22.27
1103 uext 1 2 0 padder_.byte_num ; keccak.v:91.7-91.112|padder.v:25.24-25.32
1104 uext 3 12 0 padder_.buffer_full ; keccak.v:91.7-91.112|padder.v:26.24-26.35
1105 uext 3 1089 0 padder_.accept ; keccak.v:91.7-91.112|padder.v:37.24-37.30
1106 uext 1 2 0 padder_.p0.byte_num ; keccak.v:91.7-91.112|padder1.v:27.23-27.31|padder.v:71.13-71.34
1107 uext 5 6 0 padder_.p0.in ; keccak.v:91.7-91.112|padder1.v:26.23-26.25|padder.v:71.13-71.34
1108 uext 5 1066 0 padder_.p0.out ; keccak.v:91.7-91.112|padder1.v:28.23-28.26|padder.v:71.13-71.34
1109 uext 3 211 0 f_ack ; keccak.v:40.24-40.29
1110 uext 14 15 0 f_out ; keccak.v:41.24-41.29
1111 uext 3 860 0 f_out_ready ; keccak.v:42.24-42.35
1112 state 455 i
1113 slice 204 15 1599 1088
1114 uext 204 1113 0 out1 ; keccak.v:43.24-43.28
1115 uext 214 365 0 padder_out ; keccak.v:37.24-37.34
1116 uext 214 215 0 padder_out_1 ; keccak.v:38.24-38.36
1117 uext 3 12 0 padder_out_ready ; keccak.v:39.24-39.40
1118 state 3 state
1119 const 3 1
1120 sort bitvec 17
1121 slice 1120 11 16 0
1122 concat 10 1121 1119
1123 not 3 211 $flatten\padder_.$not$padder.v:55$13 ; keccak.v:91.7-91.112|padder.v:55.36-55.43
1124 concat 1 1123 1123
1125 concat 575 1123 1124
1126 concat 849 1123 1125
1127 sort bitvec 5
1128 concat 1127 1123 1126
1129 concat 542 1123 1128
1130 concat 823 1123 1129
1131 concat 16 1123 1130
1132 concat 443 1123 1131
1133 concat 514 1123 1132
1134 sort bitvec 11
1135 concat 1134 1123 1133
1136 sort bitvec 12
1137 concat 1136 1123 1135
1138 sort bitvec 13
1139 concat 1138 1123 1137
1140 concat 619 1123 1139
1141 concat 504 1123 1140
1142 concat 19 1123 1141
1143 concat 1120 1123 1142
1144 concat 10 1123 1143
1145 and 10 1122 1144 $flatten\padder_.$and$padder.v:55$14 ; keccak.v:91.7-91.112|padder.v:55.14-55.45
1146 or 3 211 1094 $flatten\padder_.$or$padder.v:54$12 ; keccak.v:91.7-91.112|padder.v:54.16-54.30
1147 ite 10 1146 1145 11 $auto$ff.cc:504:unmap_ce$412
1148 const 10 000000000000000000
1149 ite 10 9 1148 1147 $auto$ff.cc:524:unmap_srst$414
1150 next 10 11 1149 $flatten\padder_.$auto$ff.cc:266:slice$381 ; keccak.v:91.7-91.112|padder.v:51.5-55.46
1151 ite 14 212 838 15 $auto$ff.cc:504:unmap_ce$396
1152 const 14 0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
1153 ite 14 9 1152 1151 $auto$ff.cc:524:unmap_srst$398
1154 next 14 15 1153 $flatten\f_permutation_.$auto$ff.cc:266:slice$368 ; keccak.v:94.7-94.91|f_permutation.v:64.5-68.26
1155 slice 3 1112 22 22
1156 ite 3 1155 1119 207 $auto$ff.cc:504:unmap_ce$416
1157 ite 3 9 842 1156 $auto$ff.cc:524:unmap_srst$418
1158 next 3 207 1157 $auto$ff.cc:266:slice$376 ; keccak.v:84.5-88.24
1159 not 3 715 $flatten\f_permutation_.$not$f_permutation.v:42$30 ; keccak.v:94.7-94.91|f_permutation.v:42.35-42.42
1160 and 3 209 1159 $flatten\f_permutation_.$and$f_permutation.v:42$31 ; keccak.v:94.7-94.91|f_permutation.v:42.27-42.43
1161 or 3 1160 211 $flatten\f_permutation_.$or$f_permutation.v:42$32 ; keccak.v:94.7-94.91|f_permutation.v:42.26-42.53
1162 ite 3 9 842 1161 $auto$ff.cc:524:unmap_srst$390
1163 next 3 209 1162 $flatten\f_permutation_.$auto$ff.cc:266:slice$373 ; keccak.v:94.7-94.91|f_permutation.v:40.5-42.54
1164 concat 16 1076 1070
1165 concat 5 1081 1164
1166 slice 353 215 543 0
1167 concat 214 1166 1165
1168 ite 214 1094 1167 215 $auto$ff.cc:504:unmap_ce$408
1169 const 214 000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
1170 ite 214 9 1169 1168 $auto$ff.cc:524:unmap_srst$410
1171 next 214 215 1170 $flatten\padder_.$auto$ff.cc:266:slice$383 ; keccak.v:91.7-91.112|padder.v:45.5-49.36
1172 sort bitvec 22
1173 slice 1172 659 21 0
1174 concat 455 1173 211
1175 const 455 00000000000000000000000
1176 ite 455 9 1175 1174 $auto$ff.cc:524:unmap_srst$388
1177 next 455 659 1176 $flatten\f_permutation_.$auto$ff.cc:266:slice$374 ; keccak.v:94.7-94.91|f_permutation.v:36.5-38.41
1178 ite 3 715 1119 860 $auto$ff.cc:504:unmap_ce$392
1179 concat 1 211 9
1180 redor 3 1179 $flatten\f_permutation_.$auto$opt_dff.cc:254:combine_resets$371
1181 ite 3 1180 842 1178 $auto$ff.cc:524:unmap_srst$394
1182 next 3 860 1181 $flatten\f_permutation_.$auto$ff.cc:266:slice$372 ; keccak.v:94.7-94.91|f_permutation.v:48.5-54.24
1183 ite 3 8 1119 1069 $auto$ff.cc:504:unmap_ce$400
1184 ite 3 9 842 1183 $auto$ff.cc:524:unmap_srst$402
1185 next 3 1069 1184 $flatten\padder_.$auto$ff.cc:266:slice$387 ; keccak.v:91.7-91.112|padder.v:59.5-63.20
1186 and 3 1069 12 $flatten\padder_.$and$padder.v:68$17 ; keccak.v:91.7-91.112|padder.v:68.16-68.33
1187 ite 3 1186 1119 1092 $auto$ff.cc:504:unmap_ce$404
1188 ite 3 9 842 1187 $auto$ff.cc:524:unmap_srst$406
1189 next 3 1092 1188 $flatten\padder_.$auto$ff.cc:266:slice$385 ; keccak.v:91.7-91.112|padder.v:65.5-69.19
1190 and 3 1118 211 $and$keccak.v:54$23 ; keccak.v:54.24-54.37
1191 slice 1172 1112 21 0
1192 concat 455 1191 1190
1193 ite 455 9 1175 1192 $auto$ff.cc:524:unmap_srst$424
1194 next 455 1112 1193 $auto$ff.cc:266:slice$379 ; keccak.v:50.5-54.39
1195 ite 3 8 1119 1118 $auto$ff.cc:504:unmap_ce$420
1196 ite 3 9 842 1195 $auto$ff.cc:524:unmap_srst$422
1197 next 3 1118 1196 $auto$ff.cc:266:slice$378 ; keccak.v:56.5-60.20
; end of yosys output