--- source: tests/btor2_test.rs expression: sys.serialize_to_str(&ctx) --- sha3_keccak.w2.replace_variables input byte_num : bv<2> input is_last : bv<1> input in_ready : bv<1> input in : bv<32> input reset : bv<1> input clk : bv<1> output out_ready : bv<1> = i[22] output buffer_full : bv<1> = 1'b0 output out : bv<512> = concat(f_out[1543:1536], concat(f_out[1551:1544], concat(f_out[1559:1552], concat(f_out[1567:1560], concat(f_out[1575:1568], concat(f_out[1583:1576], concat(f_out[1591:1584], concat(f_out[1599:1592], concat(f_out[1479:1472], concat(f_out[1487:1480], concat(f_out[1495:1488], concat(f_out[1503:1496], concat(f_out[1511:1504], concat(f_out[1519:1512], concat(f_out[1527:1520], concat(f_out[1535:1528], concat(f_out[1415:1408], concat(f_out[1423:1416], concat(f_out[1431:1424], concat(f_out[1439:1432], concat(f_out[1447:1440], concat(f_out[1455:1448], concat(f_out[1463:1456], concat(f_out[1471:1464], concat(f_out[1351:1344], concat(f_out[1359:1352], concat(f_out[1367:1360], concat(f_out[1375:1368], concat(f_out[1383:1376], concat(f_out[1391:1384], concat(f_out[1399:1392], concat(f_out[1407:1400], concat(f_out[1287:1280], concat(f_out[1295:1288], concat(f_out[1303:1296], concat(f_out[1311:1304], concat(f_out[1319:1312], concat(f_out[1327:1320], concat(f_out[1335:1328], concat(f_out[1343:1336], concat(f_out[1223:1216], concat(f_out[1231:1224], concat(f_out[1239:1232], concat(f_out[1247:1240], concat(f_out[1255:1248], concat(f_out[1263:1256], concat(f_out[1271:1264], concat(f_out[1279:1272], concat(f_out[1159:1152], concat(f_out[1167:1160], concat(f_out[1175:1168], concat(f_out[1183:1176], concat(f_out[1191:1184], concat(f_out[1199:1192], concat(f_out[1207:1200], concat(f_out[1215:1208], concat(f_out[1095:1088], concat(f_out[1103:1096], concat(f_out[1111:1104], concat(f_out[1119:1112], concat(f_out[1127:1120], concat(f_out[1135:1128], concat(f_out[1143:1136], f_out[1151:1144]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) node f_permutation_.accept : bv<1> = ite(__synth_change_variable_19, ite(__synth_variable_135, buffer_full, ite(__synth_variable_134, buffer_full, ite(__synth_variable_133, state, ite(__synth_variable_132, out_ready, ite(__synth_variable_131, buffer_full, ite(__synth_variable_130, is_last, ite(__synth_variable_129, in_ready, ite(__synth_variable_128, reset, clk)))))))), buffer_full) node f_permutation_.round_.in : bv<1600> = ite(f_permutation_.accept, concat(xor(ite(__synth_change_variable_17, 576'x0, 576'x0), f_out[1599:1024]), f_out[1023:0]), f_out) node f_permutation_.round_.a[24] : bv<64> = f_permutation_.round_.in[63:0] node f_permutation_.round_.a[23] : bv<64> = f_permutation_.round_.in[383:320] node f_permutation_.round_.a[22] : bv<64> = f_permutation_.round_.in[703:640] node f_permutation_.round_.a[21] : bv<64> = f_permutation_.round_.in[1023:960] node f_permutation_.round_.a[20] : bv<64> = f_permutation_.round_.in[1343:1280] node f_permutation_.round_.b[4] : bv<64> = xor(xor(xor(xor(f_permutation_.round_.a[20], f_permutation_.round_.a[21]), f_permutation_.round_.a[22]), f_permutation_.round_.a[23]), f_permutation_.round_.a[24]) node %1902 : bv<64> = concat(f_permutation_.round_.b[4][62:0], f_permutation_.round_.b[4][63]) node f_permutation_.round_.a[14] : bv<64> = f_permutation_.round_.in[191:128] node f_permutation_.round_.a[13] : bv<64> = f_permutation_.round_.in[511:448] node f_permutation_.round_.a[12] : bv<64> = f_permutation_.round_.in[831:768] node f_permutation_.round_.a[11] : bv<64> = f_permutation_.round_.in[1151:1088] node f_permutation_.round_.a[10] : bv<64> = f_permutation_.round_.in[1471:1408] node f_permutation_.round_.b[2] : bv<64> = xor(xor(xor(xor(f_permutation_.round_.a[10], f_permutation_.round_.a[11]), f_permutation_.round_.a[12]), f_permutation_.round_.a[13]), f_permutation_.round_.a[14]) node f_permutation_.round_.a[16] : bv<64> = f_permutation_.round_.in[1087:1024] node f_permutation_.round_.c[16] : bv<64> = xor(xor(f_permutation_.round_.a[16], f_permutation_.round_.b[2]), %1902) node f_permutation_.round_.d[16] : bv<64> = concat(f_permutation_.round_.c[16][8:0], f_permutation_.round_.c[16][63:9]) node f_permutation_.round_.a[19] : bv<64> = f_permutation_.round_.in[127:64] node f_permutation_.round_.a[18] : bv<64> = f_permutation_.round_.in[447:384] node f_permutation_.round_.a[17] : bv<64> = f_permutation_.round_.in[767:704] node f_permutation_.round_.a[15] : bv<64> = f_permutation_.round_.in[1407:1344] node f_permutation_.round_.b[3] : bv<64> = xor(xor(xor(xor(f_permutation_.round_.a[15], f_permutation_.round_.a[16]), f_permutation_.round_.a[17]), f_permutation_.round_.a[18]), f_permutation_.round_.a[19]) node %1928 : bv<64> = concat(f_permutation_.round_.b[3][62:0], f_permutation_.round_.b[3][63]) node f_permutation_.round_.a[9] : bv<64> = f_permutation_.round_.in[255:192] node f_permutation_.round_.a[8] : bv<64> = f_permutation_.round_.in[575:512] node f_permutation_.round_.a[7] : bv<64> = f_permutation_.round_.in[895:832] node f_permutation_.round_.a[6] : bv<64> = f_permutation_.round_.in[1215:1152] node f_permutation_.round_.a[5] : bv<64> = f_permutation_.round_.in[1535:1472] node f_permutation_.round_.b[1] : bv<64> = xor(xor(xor(xor(f_permutation_.round_.a[5], f_permutation_.round_.a[6]), f_permutation_.round_.a[7]), f_permutation_.round_.a[8]), f_permutation_.round_.a[9]) node f_permutation_.round_.c[10] : bv<64> = xor(xor(f_permutation_.round_.a[10], f_permutation_.round_.b[1]), %1928) node f_permutation_.round_.d[10] : bv<64> = concat(f_permutation_.round_.c[10][1:0], f_permutation_.round_.c[10][63:2]) node %1947 : bv<64> = concat(f_permutation_.round_.b[2][62:0], f_permutation_.round_.b[2][63]) node f_permutation_.round_.a[4] : bv<64> = f_permutation_.round_.in[319:256] node f_permutation_.round_.a[3] : bv<64> = f_permutation_.round_.in[639:576] node f_permutation_.round_.a[2] : bv<64> = f_permutation_.round_.in[959:896] node f_permutation_.round_.a[1] : bv<64> = f_permutation_.round_.in[1279:1216] node f_permutation_.round_.a[0] : bv<64> = f_permutation_.round_.in[1599:1536] node f_permutation_.round_.b[0] : bv<64> = xor(xor(xor(xor(f_permutation_.round_.a[0], f_permutation_.round_.a[1]), f_permutation_.round_.a[2]), f_permutation_.round_.a[3]), f_permutation_.round_.a[4]) node f_permutation_.round_.c[9] : bv<64> = xor(xor(f_permutation_.round_.a[9], f_permutation_.round_.b[0]), %1947) node f_permutation_.round_.d[9] : bv<64> = concat(f_permutation_.round_.c[9][61:0], f_permutation_.round_.c[9][63:62]) node %1967 : bv<64> = concat(f_permutation_.round_.b[1][62:0], f_permutation_.round_.b[1][63]) node f_permutation_.round_.c[3] : bv<64> = xor(xor(f_permutation_.round_.a[3], f_permutation_.round_.b[4]), %1967) node f_permutation_.round_.d[3] : bv<64> = concat(f_permutation_.round_.c[3][22:0], f_permutation_.round_.c[3][63:23]) node %1979 : bv<64> = concat(f_permutation_.round_.b[0][62:0], f_permutation_.round_.b[0][63]) node f_permutation_.round_.c[22] : bv<64> = xor(xor(f_permutation_.round_.a[22], f_permutation_.round_.b[3]), %1979) node f_permutation_.round_.d[22] : bv<64> = concat(f_permutation_.round_.c[22][24:0], f_permutation_.round_.c[22][63:25]) node f_permutation_.round_.c[1] : bv<64> = xor(xor(f_permutation_.round_.a[1], f_permutation_.round_.b[4]), %1967) node f_permutation_.round_.d[1] : bv<64> = concat(f_permutation_.round_.c[1][27:0], f_permutation_.round_.c[1][63:28]) node f_permutation_.round_.c[20] : bv<64> = xor(xor(f_permutation_.round_.a[20], f_permutation_.round_.b[3]), %1979) node f_permutation_.round_.d[20] : bv<64> = concat(f_permutation_.round_.c[20][36:0], f_permutation_.round_.c[20][63:37]) node f_permutation_.round_.c[19] : bv<64> = xor(xor(f_permutation_.round_.a[19], f_permutation_.round_.b[2]), %1902) node f_permutation_.round_.d[19] : bv<64> = concat(f_permutation_.round_.c[19][7:0], f_permutation_.round_.c[19][63:8]) node f_permutation_.round_.c[13] : bv<64> = xor(xor(f_permutation_.round_.a[13], f_permutation_.round_.b[1]), %1928) node f_permutation_.round_.d[13] : bv<64> = concat(f_permutation_.round_.c[13][48:0], f_permutation_.round_.c[13][63:49]) node f_permutation_.round_.c[7] : bv<64> = xor(xor(f_permutation_.round_.a[7], f_permutation_.round_.b[0]), %1947) node f_permutation_.round_.d[7] : bv<64> = concat(f_permutation_.round_.c[7][53:0], f_permutation_.round_.c[7][63:54]) node f_permutation_.round_.c[11] : bv<64> = xor(xor(f_permutation_.round_.a[11], f_permutation_.round_.b[1]), %1928) node f_permutation_.round_.d[11] : bv<64> = concat(f_permutation_.round_.c[11][57:0], f_permutation_.round_.c[11][63:58]) node f_permutation_.round_.c[5] : bv<64> = xor(xor(f_permutation_.round_.a[5], f_permutation_.round_.b[0]), %1947) node f_permutation_.round_.d[5] : bv<64> = concat(f_permutation_.round_.c[5][62:0], f_permutation_.round_.c[5][63]) node f_permutation_.round_.c[4] : bv<64> = xor(xor(f_permutation_.round_.a[4], f_permutation_.round_.b[4]), %1967) node f_permutation_.round_.d[4] : bv<64> = concat(f_permutation_.round_.c[4][45:0], f_permutation_.round_.c[4][63:46]) node f_permutation_.round_.c[23] : bv<64> = xor(xor(f_permutation_.round_.a[23], f_permutation_.round_.b[3]), %1979) node f_permutation_.round_.d[23] : bv<64> = concat(f_permutation_.round_.c[23][55:0], f_permutation_.round_.c[23][63:56]) node f_permutation_.round_.c[17] : bv<64> = xor(xor(f_permutation_.round_.a[17], f_permutation_.round_.b[2]), %1902) node f_permutation_.round_.d[17] : bv<64> = concat(f_permutation_.round_.c[17][38:0], f_permutation_.round_.c[17][63:39]) node f_permutation_.round_.c[21] : bv<64> = xor(xor(f_permutation_.round_.a[21], f_permutation_.round_.b[3]), %1979) node f_permutation_.round_.d[21] : bv<64> = concat(f_permutation_.round_.c[21][43:0], f_permutation_.round_.c[21][63:44]) node f_permutation_.round_.c[15] : bv<64> = xor(xor(f_permutation_.round_.a[15], f_permutation_.round_.b[2]), %1902) node f_permutation_.round_.d[15] : bv<64> = concat(f_permutation_.round_.c[15][35:0], f_permutation_.round_.c[15][63:36]) node f_permutation_.round_.c[14] : bv<64> = xor(xor(f_permutation_.round_.a[14], f_permutation_.round_.b[1]), %1928) node f_permutation_.round_.d[14] : bv<64> = concat(f_permutation_.round_.c[14][2:0], f_permutation_.round_.c[14][63:3]) node f_permutation_.round_.c[8] : bv<64> = xor(xor(f_permutation_.round_.a[8], f_permutation_.round_.b[0]), %1947) node f_permutation_.round_.d[8] : bv<64> = concat(f_permutation_.round_.c[8][18:0], f_permutation_.round_.c[8][63:19]) node f_permutation_.round_.c[2] : bv<64> = xor(xor(f_permutation_.round_.a[2], f_permutation_.round_.b[4]), %1967) node f_permutation_.round_.d[2] : bv<64> = concat(f_permutation_.round_.c[2][60:0], f_permutation_.round_.c[2][63:61]) node f_permutation_.round_.c[6] : bv<64> = xor(xor(f_permutation_.round_.a[6], f_permutation_.round_.b[0]), %1947) node f_permutation_.round_.d[6] : bv<64> = concat(f_permutation_.round_.c[6][19:0], f_permutation_.round_.c[6][63:20]) node f_permutation_.round_.c[0] : bv<64> = xor(xor(f_permutation_.round_.a[0], f_permutation_.round_.b[4]), %1967) node f_permutation_.round_.c[24] : bv<64> = xor(xor(f_permutation_.round_.a[24], f_permutation_.round_.b[3]), %1979) node f_permutation_.round_.d[24] : bv<64> = concat(f_permutation_.round_.c[24][49:0], f_permutation_.round_.c[24][63:50]) node f_permutation_.round_.c[18] : bv<64> = xor(xor(f_permutation_.round_.a[18], f_permutation_.round_.b[2]), %1902) node f_permutation_.round_.d[18] : bv<64> = concat(f_permutation_.round_.c[18][42:0], f_permutation_.round_.c[18][63:43]) node f_permutation_.round_.c[12] : bv<64> = xor(xor(f_permutation_.round_.a[12], f_permutation_.round_.b[1]), %1928) node f_permutation_.round_.d[12] : bv<64> = concat(f_permutation_.round_.c[12][20:0], f_permutation_.round_.c[12][63:21]) node %519 : bv<1> = f_permutation_.i[21] node %517 : bv<1> = f_permutation_.i[19] node %515 : bv<1> = f_permutation_.i[14] node %513 : bv<1> = f_permutation_.i[13] node %511 : bv<1> = f_permutation_.i[12] node %509 : bv<1> = f_permutation_.i[11] node %507 : bv<1> = f_permutation_.i[9] node %505 : bv<1> = f_permutation_.i[6] node %503 : bv<1> = f_permutation_.i[5] node %501 : bv<1> = f_permutation_.i[4] node %499 : bv<1> = f_permutation_.i[3] node f_permutation_.round_.f[0] : bv<64> = xor(f_permutation_.round_.c[0], and(not(f_permutation_.round_.d[6]), f_permutation_.round_.d[12])) node %538 : bv<1> = f_permutation_.i[18] node %536 : bv<1> = f_permutation_.i[17] node %534 : bv<1> = f_permutation_.i[15] node %529 : bv<1> = f_permutation_.i[10] node %527 : bv<1> = f_permutation_.i[7] node %524 : bv<1> = f_permutation_.i[1] node %525 : bv<1> = or(f_permutation_.i[0], %524) node %526 : bv<1> = or(%525, %499) node %554 : bv<1> = f_permutation_.i[22] node %545 : bv<1> = f_permutation_.i[8] node %567 : bv<1> = f_permutation_.i[20] node %564 : bv<1> = f_permutation_.i[16] node %571 : bv<1> = f_permutation_.i[2] node f_permutation_.reset : bv<1> = ite(__synth_change_variable_16, ite(__synth_variable_119, buffer_full, ite(__synth_variable_118, buffer_full, ite(__synth_variable_117, buffer_full, ite(__synth_variable_116, state, ite(__synth_variable_115, out_ready, ite(__synth_variable_114, buffer_full, ite(__synth_variable_113, is_last, ite(__synth_variable_112, in_ready, clk)))))))), reset) node padder_.reset : bv<1> = ite(__synth_change_variable_7, ite(__synth_variable_62, buffer_full, ite(__synth_variable_61, buffer_full, ite(__synth_variable_60, buffer_full, ite(__synth_variable_59, state, ite(__synth_variable_58, out_ready, ite(__synth_variable_57, buffer_full, ite(__synth_variable_56, is_last, ite(__synth_variable_55, in_ready, clk)))))))), reset) node padder_.out_ready : bv<1> = ite(__synth_change_variable_11, ite(__synth_variable_87, buffer_full, ite(__synth_variable_86, buffer_full, ite(__synth_variable_85, buffer_full, ite(__synth_variable_84, state, ite(__synth_variable_83, out_ready, ite(__synth_variable_82, is_last, ite(__synth_variable_81, in_ready, ite(__synth_variable_80, reset, clk)))))))), buffer_full) node padder_.f_ack : bv<1> = ite(__synth_change_variable_14, ite(__synth_variable_103, buffer_full, ite(__synth_variable_102, buffer_full, ite(__synth_variable_101, state, ite(__synth_variable_100, out_ready, ite(__synth_variable_99, buffer_full, ite(__synth_variable_98, is_last, ite(__synth_variable_97, in_ready, ite(__synth_variable_96, reset, clk)))))))), buffer_full) node %1796 : bv<1> = not(padder_.f_ack) node %1819 : bv<1> = not(padder_.out_ready) state i : bv<23> [next] ite(ite(__synth_change_variable_0, ite(__synth_variable_7, buffer_full, ite(__synth_variable_6, buffer_full, ite(__synth_variable_5, buffer_full, ite(__synth_variable_4, state, ite(__synth_variable_3, out_ready, ite(__synth_variable_2, buffer_full, ite(__synth_variable_1, is_last, ite(__synth_variable_0, in_ready, clk)))))))), reset), 23'x0, concat(i[21:0], and(ite(__synth_change_variable_1, ite(__synth_variable_15, buffer_full, ite(__synth_variable_14, buffer_full, ite(__synth_variable_13, buffer_full, ite(__synth_variable_12, out_ready, ite(__synth_variable_11, buffer_full, ite(__synth_variable_10, is_last, ite(__synth_variable_9, in_ready, ite(__synth_variable_8, reset, clk)))))))), state), ite(__synth_change_variable_2, ite(__synth_variable_23, buffer_full, ite(__synth_variable_22, buffer_full, ite(__synth_variable_21, state, ite(__synth_variable_20, out_ready, ite(__synth_variable_19, buffer_full, ite(__synth_variable_18, is_last, ite(__synth_variable_17, in_ready, ite(__synth_variable_16, reset, clk)))))))), buffer_full)))) state f_out : bv<1600> [next] ite(f_permutation_.reset, 1600'x0, ite(or(f_permutation_.calc, f_permutation_.accept), concat(xor(f_permutation_.round_.f[0][63], or(or(or(or(or(or(or(or(or(or(or(or(%524, %571), %503), %505), %511), %513), %515), %534), %564), %538), %517), %567), %554)), concat(f_permutation_.round_.f[0][62:32], concat(xor(f_permutation_.round_.f[0][31], or(or(or(or(or(or(or(or(or(%571, %501), %503), %507), %529), %509), %538), %517), %519), %554)), concat(f_permutation_.round_.f[0][30:16], concat(xor(f_permutation_.round_.f[0][15], or(or(or(or(or(or(or(or(or(or(or(or(or(%525, %571), %499), %503), %505), %507), %509), %513), %515), %534), %536), %517), %567), %554)), concat(f_permutation_.round_.f[0][14:8], concat(xor(f_permutation_.round_.f[0][7], or(or(or(or(or(or(or(or(or(%526, %503), %527), %545), %509), %511), %513), %564), %517), %567)), concat(f_permutation_.round_.f[0][6:4], concat(xor(f_permutation_.round_.f[0][3], or(or(or(or(or(or(or(or(or(or(or(or(%524, %499), %505), %527), %545), %507), %529), %509), %511), %513), %536), %538), %554)), concat(f_permutation_.round_.f[0][2], concat(xor(f_permutation_.round_.f[0][1], or(or(or(or(or(or(or(or(%526, %527), %529), %509), %511), %515), %534), %536), %538)), concat(xor(f_permutation_.round_.f[0][0], or(or(or(or(or(or(or(or(or(or(or(f_permutation_.accept, %499), %501), %503), %505), %507), %509), %511), %513), %515), %517), %519)), concat(xor(f_permutation_.round_.d[6], and(not(f_permutation_.round_.d[12]), f_permutation_.round_.d[18])), concat(xor(f_permutation_.round_.d[12], and(not(f_permutation_.round_.d[18]), f_permutation_.round_.d[24])), concat(xor(f_permutation_.round_.d[18], and(not(f_permutation_.round_.d[24]), f_permutation_.round_.c[0])), concat(xor(f_permutation_.round_.d[24], and(not(f_permutation_.round_.c[0]), f_permutation_.round_.d[6])), concat(xor(f_permutation_.round_.d[15], and(not(f_permutation_.round_.d[21]), f_permutation_.round_.d[2])), concat(xor(f_permutation_.round_.d[21], and(not(f_permutation_.round_.d[2]), f_permutation_.round_.d[8])), concat(xor(f_permutation_.round_.d[2], and(not(f_permutation_.round_.d[8]), f_permutation_.round_.d[14])), concat(xor(f_permutation_.round_.d[8], and(not(f_permutation_.round_.d[14]), f_permutation_.round_.d[15])), concat(xor(f_permutation_.round_.d[14], and(not(f_permutation_.round_.d[15]), f_permutation_.round_.d[21])), concat(xor(f_permutation_.round_.d[5], and(not(f_permutation_.round_.d[11]), f_permutation_.round_.d[17])), concat(xor(f_permutation_.round_.d[11], and(not(f_permutation_.round_.d[17]), f_permutation_.round_.d[23])), concat(xor(f_permutation_.round_.d[17], and(not(f_permutation_.round_.d[23]), f_permutation_.round_.d[4])), concat(xor(f_permutation_.round_.d[23], and(not(f_permutation_.round_.d[4]), f_permutation_.round_.d[5])), concat(xor(f_permutation_.round_.d[4], and(not(f_permutation_.round_.d[5]), f_permutation_.round_.d[11])), concat(xor(f_permutation_.round_.d[20], and(not(f_permutation_.round_.d[1]), f_permutation_.round_.d[7])), concat(xor(f_permutation_.round_.d[1], and(not(f_permutation_.round_.d[7]), f_permutation_.round_.d[13])), concat(xor(f_permutation_.round_.d[7], and(not(f_permutation_.round_.d[13]), f_permutation_.round_.d[19])), concat(xor(f_permutation_.round_.d[13], and(not(f_permutation_.round_.d[19]), f_permutation_.round_.d[20])), concat(xor(f_permutation_.round_.d[19], and(not(f_permutation_.round_.d[20]), f_permutation_.round_.d[1])), concat(xor(f_permutation_.round_.d[10], and(not(f_permutation_.round_.d[16]), f_permutation_.round_.d[22])), concat(xor(f_permutation_.round_.d[16], and(not(f_permutation_.round_.d[22]), f_permutation_.round_.d[3])), concat(xor(f_permutation_.round_.d[22], and(not(f_permutation_.round_.d[3]), f_permutation_.round_.d[9])), concat(xor(f_permutation_.round_.d[3], and(not(f_permutation_.round_.d[9]), f_permutation_.round_.d[10])), xor(f_permutation_.round_.d[9], and(not(f_permutation_.round_.d[10]), f_permutation_.round_.d[16]))))))))))))))))))))))))))))))))))))), f_out)) state __synth_variable_104 : bv<1> [next] __synth_variable_104 state __synth_variable_105 : bv<1> [next] __synth_variable_105 state __synth_variable_106 : bv<1> [next] __synth_variable_106 state __synth_variable_107 : bv<1> [next] __synth_variable_107 state state : bv<1> [next] ite(ite(__synth_change_variable_3, ite(__synth_variable_31, buffer_full, ite(__synth_variable_30, buffer_full, ite(__synth_variable_29, buffer_full, ite(__synth_variable_28, state, ite(__synth_variable_27, out_ready, ite(__synth_variable_26, buffer_full, ite(__synth_variable_25, is_last, ite(__synth_variable_24, in_ready, clk)))))))), reset), buffer_full, ite(ite(__synth_change_variable_4, ite(__synth_variable_39, buffer_full, ite(__synth_variable_38, buffer_full, ite(__synth_variable_37, buffer_full, ite(__synth_variable_36, state, ite(__synth_variable_35, out_ready, ite(__synth_variable_34, buffer_full, ite(__synth_variable_33, in_ready, ite(__synth_variable_32, reset, clk)))))))), is_last), 1'b1, state)) state __synth_variable_108 : bv<1> [next] __synth_variable_108 state __synth_variable_109 : bv<1> [next] __synth_variable_109 state __synth_variable_110 : bv<1> [next] __synth_variable_110 state __synth_variable_111 : bv<1> [next] __synth_variable_111 state __synth_change_variable_15 : bv<1> [next] __synth_change_variable_15 state __synth_variable_112 : bv<1> [next] __synth_variable_112 state __synth_variable_113 : bv<1> [next] __synth_variable_113 state __synth_variable_114 : bv<1> [next] __synth_variable_114 state __synth_variable_115 : bv<1> [next] __synth_variable_115 state __synth_variable_116 : bv<1> [next] __synth_variable_116 state __synth_variable_117 : bv<1> [next] __synth_variable_117 state __synth_variable_118 : bv<1> [next] __synth_variable_118 state __synth_variable_119 : bv<1> [next] __synth_variable_119 state __synth_change_variable_16 : bv<1> [next] __synth_change_variable_16 state __synth_change_variable_17 : bv<1> [next] __synth_change_variable_17 state __synth_variable_120 : bv<1> [next] __synth_variable_120 state __synth_variable_121 : bv<1> [next] __synth_variable_121 state __synth_variable_122 : bv<1> [next] __synth_variable_122 state __synth_variable_123 : bv<1> [next] __synth_variable_123 state __synth_variable_124 : bv<1> [next] __synth_variable_124 state __synth_variable_125 : bv<1> [next] __synth_variable_125 state __synth_variable_126 : bv<1> [next] __synth_variable_126 state __synth_variable_127 : bv<1> [next] __synth_variable_127 state __synth_change_variable_18 : bv<1> [next] __synth_change_variable_18 state __synth_variable_128 : bv<1> [next] __synth_variable_128 state __synth_variable_129 : bv<1> [next] __synth_variable_129 state __synth_variable_130 : bv<1> [next] __synth_variable_130 state __synth_variable_131 : bv<1> [next] __synth_variable_131 state __synth_variable_132 : bv<1> [next] __synth_variable_132 state __synth_variable_133 : bv<1> [next] __synth_variable_133 state __synth_variable_134 : bv<1> [next] __synth_variable_134 state __synth_variable_135 : bv<1> [next] __synth_variable_135 state __synth_change_variable_19 : bv<1> [next] __synth_change_variable_19 state __synth_variable_136 : bv<1> [next] __synth_variable_136 state __synth_variable_137 : bv<1> [next] __synth_variable_137 state __synth_variable_138 : bv<1> [next] __synth_variable_138 state __synth_variable_139 : bv<1> [next] __synth_variable_139 state __synth_variable_140 : bv<1> [next] __synth_variable_140 state __synth_variable_141 : bv<1> [next] __synth_variable_141 state __synth_variable_142 : bv<1> [next] __synth_variable_142 state __synth_variable_143 : bv<1> [next] __synth_variable_143 state __synth_change_variable_20 : bv<1> [next] __synth_change_variable_20 state f_permutation_.i : bv<23> [next] ite(f_permutation_.reset, 23'x0, concat(f_permutation_.i[21:0], f_permutation_.accept)) state f_permutation_.calc : bv<1> [next] ite(f_permutation_.reset, buffer_full, or(and(f_permutation_.calc, not(%554)), f_permutation_.accept)) state __synth_variable_47 : bv<1> [next] __synth_variable_47 state __synth_variable_48 : bv<1> [next] __synth_variable_48 state __synth_variable_49 : bv<1> [next] __synth_variable_49 state __synth_variable_50 : bv<1> [next] __synth_variable_50 state __synth_variable_51 : bv<1> [next] __synth_variable_51 state __synth_variable_52 : bv<1> [next] __synth_variable_52 state __synth_variable_53 : bv<1> [next] __synth_variable_53 state __synth_variable_54 : bv<1> [next] __synth_variable_54 state __synth_change_variable_6 : bv<1> [next] __synth_change_variable_6 state __synth_variable_55 : bv<1> [next] __synth_variable_55 state __synth_variable_56 : bv<1> [next] __synth_variable_56 state __synth_variable_57 : bv<1> [next] __synth_variable_57 state __synth_variable_58 : bv<1> [next] __synth_variable_58 state __synth_variable_59 : bv<1> [next] __synth_variable_59 state __synth_variable_60 : bv<1> [next] __synth_variable_60 state __synth_variable_61 : bv<1> [next] __synth_variable_61 state __synth_variable_62 : bv<1> [next] __synth_variable_62 state __synth_change_variable_7 : bv<1> [next] __synth_change_variable_7 state __synth_variable_63 : bv<1> [next] __synth_variable_63 state __synth_change_variable_8 : bv<1> [next] __synth_change_variable_8 state __synth_variable_64 : bv<1> [next] __synth_variable_64 state __synth_variable_65 : bv<1> [next] __synth_variable_65 state __synth_variable_66 : bv<1> [next] __synth_variable_66 state __synth_variable_67 : bv<1> [next] __synth_variable_67 state __synth_variable_68 : bv<1> [next] __synth_variable_68 state __synth_variable_69 : bv<1> [next] __synth_variable_69 state __synth_variable_70 : bv<1> [next] __synth_variable_70 state __synth_variable_71 : bv<1> [next] __synth_variable_71 state __synth_change_variable_9 : bv<1> [next] __synth_change_variable_9 state __synth_variable_72 : bv<1> [next] __synth_variable_72 state __synth_variable_73 : bv<1> [next] __synth_variable_73 state __synth_variable_74 : bv<1> [next] __synth_variable_74 state __synth_variable_75 : bv<1> [next] __synth_variable_75 state __synth_variable_76 : bv<1> [next] __synth_variable_76 state __synth_variable_77 : bv<1> [next] __synth_variable_77 state __synth_variable_78 : bv<1> [next] __synth_variable_78 state __synth_variable_79 : bv<1> [next] __synth_variable_79 state __synth_change_variable_10 : bv<1> [next] __synth_change_variable_10 state __synth_variable_80 : bv<1> [next] __synth_variable_80 state __synth_variable_81 : bv<1> [next] __synth_variable_81 state __synth_variable_82 : bv<1> [next] __synth_variable_82 state __synth_variable_83 : bv<1> [next] __synth_variable_83 state __synth_variable_84 : bv<1> [next] __synth_variable_84 state __synth_variable_85 : bv<1> [next] __synth_variable_85 state __synth_variable_86 : bv<1> [next] __synth_variable_86 state __synth_variable_87 : bv<1> [next] __synth_variable_87 state __synth_change_variable_11 : bv<1> [next] __synth_change_variable_11 state __synth_change_variable_12 : bv<1> [next] __synth_change_variable_12 state __synth_variable_96 : bv<1> [next] __synth_variable_96 state __synth_variable_97 : bv<1> [next] __synth_variable_97 state __synth_variable_98 : bv<1> [next] __synth_variable_98 state __synth_variable_99 : bv<1> [next] __synth_variable_99 state __synth_variable_100 : bv<1> [next] __synth_variable_100 state __synth_variable_101 : bv<1> [next] __synth_variable_101 state __synth_variable_102 : bv<1> [next] __synth_variable_102 state __synth_variable_103 : bv<1> [next] __synth_variable_103 state __synth_change_variable_14 : bv<1> [next] __synth_change_variable_14 state padder_.state : bv<1> [next] ite(padder_.reset, buffer_full, ite(ite(__synth_change_variable_10, ite(__synth_variable_79, buffer_full, ite(__synth_variable_78, buffer_full, ite(__synth_variable_77, buffer_full, ite(__synth_variable_76, state, ite(__synth_variable_75, out_ready, ite(__synth_variable_74, buffer_full, ite(__synth_variable_73, in_ready, ite(__synth_variable_72, reset, clk)))))))), is_last), 1'b1, padder_.state)) state padder_.done : bv<1> [next] ite(padder_.reset, buffer_full, ite(and(padder_.state, padder_.out_ready), 1'b1, padder_.done)) state padder_.i : bv<18> [next] ite(padder_.reset, 18'x0, ite(or(padder_.f_ack, and(or(and(and(not(padder_.state), ite(__synth_change_variable_9, ite(__synth_variable_71, buffer_full, ite(__synth_variable_70, buffer_full, ite(__synth_variable_69, buffer_full, ite(__synth_variable_68, state, ite(__synth_variable_67, out_ready, ite(__synth_variable_66, buffer_full, ite(__synth_variable_65, is_last, ite(__synth_variable_64, reset, clk)))))))), in_ready)), %1819), and(padder_.state, %1819)), not(padder_.done))), and(concat(padder_.i[16:0], 1'b1), concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, concat(%1796, %1796)))))))))))))))))), padder_.i)) state __synth_variable_95 : bv<1> [next] __synth_variable_95 state __synth_variable_94 : bv<1> [next] __synth_variable_94 state __synth_variable_93 : bv<1> [next] __synth_variable_93 state __synth_variable_92 : bv<1> [next] __synth_variable_92 state __synth_variable_91 : bv<1> [next] __synth_variable_91 state __synth_variable_90 : bv<1> [next] __synth_variable_90 state __synth_variable_89 : bv<1> [next] __synth_variable_89 state __synth_variable_88 : bv<1> [next] __synth_variable_88 state __synth_variable_46 : bv<1> [next] __synth_variable_46 state __synth_variable_45 : bv<1> [next] __synth_variable_45 state __synth_variable_44 : bv<1> [next] __synth_variable_44 state __synth_variable_43 : bv<1> [next] __synth_variable_43 state __synth_variable_42 : bv<1> [next] __synth_variable_42 state __synth_variable_41 : bv<1> [next] __synth_variable_41 state __synth_variable_40 : bv<1> [next] __synth_variable_40 state __synth_variable_39 : bv<1> [next] __synth_variable_39 state __synth_variable_38 : bv<1> [next] __synth_variable_38 state __synth_variable_37 : bv<1> [next] __synth_variable_37 state __synth_variable_36 : bv<1> [next] __synth_variable_36 state __synth_variable_35 : bv<1> [next] __synth_variable_35 state __synth_variable_34 : bv<1> [next] __synth_variable_34 state __synth_variable_33 : bv<1> [next] __synth_variable_33 state __synth_variable_32 : bv<1> [next] __synth_variable_32 state __synth_variable_31 : bv<1> [next] __synth_variable_31 state __synth_variable_30 : bv<1> [next] __synth_variable_30 state __synth_variable_29 : bv<1> [next] __synth_variable_29 state __synth_variable_28 : bv<1> [next] __synth_variable_28 state __synth_variable_27 : bv<1> [next] __synth_variable_27 state __synth_variable_26 : bv<1> [next] __synth_variable_26 state __synth_variable_25 : bv<1> [next] __synth_variable_25 state __synth_variable_24 : bv<1> [next] __synth_variable_24 state __synth_variable_23 : bv<1> [next] __synth_variable_23 state __synth_variable_22 : bv<1> [next] __synth_variable_22 state __synth_variable_21 : bv<1> [next] __synth_variable_21 state __synth_variable_20 : bv<1> [next] __synth_variable_20 state __synth_variable_19 : bv<1> [next] __synth_variable_19 state __synth_variable_18 : bv<1> [next] __synth_variable_18 state __synth_variable_17 : bv<1> [next] __synth_variable_17 state __synth_variable_16 : bv<1> [next] __synth_variable_16 state __synth_variable_15 : bv<1> [next] __synth_variable_15 state __synth_variable_14 : bv<1> [next] __synth_variable_14 state __synth_variable_13 : bv<1> [next] __synth_variable_13 state __synth_variable_12 : bv<1> [next] __synth_variable_12 state __synth_variable_11 : bv<1> [next] __synth_variable_11 state __synth_variable_10 : bv<1> [next] __synth_variable_10 state __synth_variable_9 : bv<1> [next] __synth_variable_9 state __synth_variable_8 : bv<1> [next] __synth_variable_8 state __synth_variable_7 : bv<1> [next] __synth_variable_7 state __synth_variable_6 : bv<1> [next] __synth_variable_6 state __synth_variable_5 : bv<1> [next] __synth_variable_5 state __synth_variable_4 : bv<1> [next] __synth_variable_4 state __synth_variable_3 : bv<1> [next] __synth_variable_3 state __synth_variable_2 : bv<1> [next] __synth_variable_2 state __synth_variable_1 : bv<1> [next] __synth_variable_1 state __synth_variable_0 : bv<1> [next] __synth_variable_0 state __synth_change_variable_13 : bv<1> [next] __synth_change_variable_13 state __synth_change_variable_5 : bv<1> [next] __synth_change_variable_5 state __synth_change_variable_4 : bv<1> [next] __synth_change_variable_4 state __synth_change_variable_3 : bv<1> [next] __synth_change_variable_3 state __synth_change_variable_2 : bv<1> [next] __synth_change_variable_2 state __synth_change_variable_1 : bv<1> [next] __synth_change_variable_1 state __synth_change_variable_0 : bv<1> [next] __synth_change_variable_0