From 2beeace98a59036e7f405731301ec883c28b84a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 29 Nov 2023 11:31:13 -0500 Subject: [PATCH] synth: test sha3 testbench --- synthesizer/src/maltese/app/Btor2MC.scala | 5 +- .../test/synth/TestbenchSimulatorTests.scala | 16 + .../synth/benchmarks/keccak.original.btor | 1199 +++++++++++++++++ 3 files changed, 1218 insertions(+), 2 deletions(-) create mode 100644 synthesizer/test/synth/benchmarks/keccak.original.btor diff --git a/synthesizer/src/maltese/app/Btor2MC.scala b/synthesizer/src/maltese/app/Btor2MC.scala index 8f55bc9..b56c945 100644 --- a/synthesizer/src/maltese/app/Btor2MC.scala +++ b/synthesizer/src/maltese/app/Btor2MC.scala @@ -5,9 +5,9 @@ package maltese.app import java.io.File - import maltese.mc._ import maltese.smt +import maltese.smt.BitwuzlaSMTLib /** simple interface to all supported model checkers */ object Btor2MC extends App { @@ -16,7 +16,8 @@ object Btor2MC extends App { } else { val filename = os.pwd / args.head val sys = Btor2.load(filename) - val checker = new BtormcModelChecker + //val checker = new BtormcModelChecker + val checker = new SMTModelChecker(BitwuzlaSMTLib) check(checker, sys, kMax = -1) } diff --git a/synthesizer/test/synth/TestbenchSimulatorTests.scala b/synthesizer/test/synth/TestbenchSimulatorTests.scala index a961850..9e2ad0d 100644 --- a/synthesizer/test/synth/TestbenchSimulatorTests.scala +++ b/synthesizer/test/synth/TestbenchSimulatorTests.scala @@ -50,6 +50,22 @@ class TestbenchSimulatorTests extends AnyFlatSpec { Testbench.save(CirFixDir / "opencores" / "i2c" / "fixed_x_prop_tb.csv", fixed) } + it should "correctly execute the sha3 test" in { + val tb = Testbench.load(CirFixDir / "opencores" / "sha3" / "low_throughput_core" / "keccak_tb.csv") + + assert(tb.length == 358) + + val sys = Btor2.load(BenchmarkDir / "keccak.original.btor") + + // initialize everything to zero + val seed: Long = 1 + val rnd = new scala.util.Random(seed) + val initialized = initSys(sys, ZeroInit, rnd) + + val r = Testbench.run(initialized, tb, verbose = true, vcd = Some(os.pwd / "dump.vcd")) + assert(!r.failed) + } + } private object XInputConversion { diff --git a/synthesizer/test/synth/benchmarks/keccak.original.btor b/synthesizer/test/synth/benchmarks/keccak.original.btor new file mode 100644 index 0000000..2d3098c --- /dev/null +++ b/synthesizer/test/synth/benchmarks/keccak.original.btor @@ -0,0 +1,1199 @@ +; 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