|
| 1 | +Instructions: |
| 2 | + SRL rd_ptr = 1, rs1_ptr = 3, rs2 = 1, rs2_as = 0 |
| 3 | + SLL rd_ptr = 2, rs1_ptr = 3, rs2 = 31, rs2_as = 0 |
| 4 | + OR rd_ptr = 3, rs1_ptr = 1, rs2 = 2, rs2_as = 1 |
| 5 | + |
| 6 | +APC advantage: |
| 7 | + - Main columns: 142 -> 26 (5.46x reduction) |
| 8 | + - Bus interactions: 68 -> 18 (3.78x reduction) |
| 9 | + - Constraints: 174 -> 5 (34.80x reduction) |
| 10 | + |
| 11 | +Symbolic machine using 26 unique main columns: |
| 12 | + from_state__timestamp_0 |
| 13 | + reads_aux__0__base__prev_timestamp_0 |
| 14 | + reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 |
| 15 | + writes_aux__base__prev_timestamp_0 |
| 16 | + writes_aux__base__timestamp_lt_aux__lower_decomp__0_0 |
| 17 | + writes_aux__prev_data__0_0 |
| 18 | + writes_aux__prev_data__1_0 |
| 19 | + writes_aux__prev_data__2_0 |
| 20 | + writes_aux__prev_data__3_0 |
| 21 | + a__0_0 |
| 22 | + a__1_0 |
| 23 | + a__2_0 |
| 24 | + a__3_0 |
| 25 | + b__0_0 |
| 26 | + b__1_0 |
| 27 | + b__2_0 |
| 28 | + b__3_0 |
| 29 | + writes_aux__base__prev_timestamp_1 |
| 30 | + writes_aux__base__timestamp_lt_aux__lower_decomp__0_1 |
| 31 | + writes_aux__prev_data__0_1 |
| 32 | + writes_aux__prev_data__1_1 |
| 33 | + writes_aux__prev_data__2_1 |
| 34 | + writes_aux__prev_data__3_1 |
| 35 | + a__3_1 |
| 36 | + a__3_2 |
| 37 | + is_valid |
| 38 | + |
| 39 | +// Bus 0 (EXECUTION_BRIDGE): |
| 40 | +mult=is_valid * -1, args=[0, from_state__timestamp_0] |
| 41 | +mult=is_valid * 1, args=[12, from_state__timestamp_0 + 9] |
| 42 | + |
| 43 | +// Bus 1 (MEMORY): |
| 44 | +mult=is_valid * -1, args=[1, 3, b__0_0, b__1_0, b__2_0, b__3_0, reads_aux__0__base__prev_timestamp_0] |
| 45 | +mult=is_valid * -1, args=[1, 1, writes_aux__prev_data__0_0, writes_aux__prev_data__1_0, writes_aux__prev_data__2_0, writes_aux__prev_data__3_0, writes_aux__base__prev_timestamp_0] |
| 46 | +mult=is_valid * -1, args=[1, 2, writes_aux__prev_data__0_1, writes_aux__prev_data__1_1, writes_aux__prev_data__2_1, writes_aux__prev_data__3_1, writes_aux__base__prev_timestamp_1] |
| 47 | +mult=is_valid * 1, args=[1, 1, a__0_0, a__1_0, a__2_0, a__3_0, from_state__timestamp_0 + 6] |
| 48 | +mult=is_valid * 1, args=[1, 2, 0, 0, 0, a__3_1, from_state__timestamp_0 + 7] |
| 49 | +mult=is_valid * 1, args=[1, 3, a__0_0, a__1_0, a__2_0, a__3_2, from_state__timestamp_0 + 8] |
| 50 | + |
| 51 | +// Bus 3 (VARIABLE_RANGE_CHECKER): |
| 52 | +mult=is_valid * 1, args=[reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0, 17] |
| 53 | +mult=is_valid * 1, args=[15360 * reads_aux__0__base__prev_timestamp_0 + 15360 * reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 + 15360 - 15360 * from_state__timestamp_0, 12] |
| 54 | +mult=is_valid * 1, args=[writes_aux__base__timestamp_lt_aux__lower_decomp__0_0, 17] |
| 55 | +mult=is_valid * 1, args=[15360 * writes_aux__base__prev_timestamp_0 + 15360 * writes_aux__base__timestamp_lt_aux__lower_decomp__0_0 - (15360 * from_state__timestamp_0 + 15360), 12] |
| 56 | +mult=is_valid * 1, args=[7864320 * a__3_1 - 1006632960 * b__0_0, 7] |
| 57 | +mult=is_valid * 1, args=[writes_aux__base__timestamp_lt_aux__lower_decomp__0_1, 17] |
| 58 | +mult=is_valid * 1, args=[15360 * writes_aux__base__prev_timestamp_1 + 15360 * writes_aux__base__timestamp_lt_aux__lower_decomp__0_1 - (15360 * from_state__timestamp_0 + 61440), 12] |
| 59 | + |
| 60 | +// Bus 6 (BITWISE_LOOKUP): |
| 61 | +mult=is_valid * 1, args=[a__3_0, a__3_1, 2 * a__3_2 - (a__3_0 + a__3_1), 1] |
| 62 | +mult=is_valid * 1, args=[a__0_0, a__1_0, 0, 0] |
| 63 | +mult=is_valid * 1, args=[a__2_0, 0, 0, 0] |
| 64 | + |
| 65 | +// Algebraic constraints: |
| 66 | +(b__0_0 + 256 * b__1_0 + 65536 * b__2_0 + 16777216 * b__3_0 - (2 * a__0_0 + 512 * a__1_0 + 131072 * a__2_0 + 33554432 * a__3_0)) * (b__0_0 + 256 * b__1_0 + 65536 * b__2_0 + 16777216 * b__3_0 - (2 * a__0_0 + 512 * a__1_0 + 131072 * a__2_0 + 33554432 * a__3_0 + 1)) = 0 |
| 67 | +(b__1_0 + 256 * b__2_0 + 65536 * b__3_0 - (2 * a__1_0 + 512 * a__2_0 + 131072 * a__3_0)) * (b__1_0 + 256 * b__2_0 + 65536 * b__3_0 - (2 * a__1_0 + 512 * a__2_0 + 131072 * a__3_0 + 1)) = 0 |
| 68 | +(b__2_0 + 256 * b__3_0 - (2 * a__2_0 + 512 * a__3_0)) * (b__2_0 + 256 * b__3_0 - (2 * a__2_0 + 512 * a__3_0 + 1)) = 0 |
| 69 | +(b__3_0 - 2 * a__3_0) * (b__3_0 - (2 * a__3_0 + 1)) = 0 |
| 70 | +is_valid * (is_valid - 1) = 0 |
0 commit comments