| ... | ... | @@ -194,26 +194,30 @@ a * b + c = d |
|
|
|
|
|
|
|
### Layout
|
|
|
|
|
|
|
|
| hi | lo | hi | lo | cnt | u16_0 | u16_1 | u16_2 | u16_3 | u16_4 |
|
|
|
|
| ---------------------- | -------------- | -------------- | -------------- | ---- | ------------------------------------------------------------ | ------ | ------ | ------ | ------ |
|
|
|
|
| | | | | 17 | d_lo_0 | | | | |
|
|
|
|
| | | | | 16 | d_hi_0 | | | | |
|
|
|
|
| | | | | 15 | c_lo_0 | | | | |
|
|
|
|
| a_com_lt | | | | 14 | c_hi_0 | | | | |
|
|
|
|
| c_sum_carry_hi | c_sum_carry_lo | d_sum_carry_hi | d_sum_carry_lo | 13 | b_hi_0 | | | | |
|
|
|
|
| a_sum_carry_hi | a_sum_carry_lo | b_sum_carry_hi | b_sum_carry_lo | 12 | a_hi_0 (因为a,b 都是输入，我们不用约束它们，这里hi主要是给lt使用) | | | | |
|
|
|
|
| a_lt_carry_hi | b_lt_carry_hi | c_lt_carry_hi | d_lt_carry_hi | 11 | a_diff | | | | |
|
|
|
|
| | | | | 10 | cb_diff_lo_0(c,d 约束因为c,d 非输入值。并且我们要计算c + c_com = 1<<256) | | | | |
|
|
|
|
| cb_diff_hi(cb 指c < b) | cb_diff_lo | cb_carry_hi | | 9 | cb_diff_hi_0 | | | | |
|
|
|
|
| mul_carry_hi | mul_carry_lo | | | 8 | mul_carry_lo_0 | | | | |
|
|
|
|
| | | | | 7 | d_com_lo_0 | | | | |
|
|
|
|
| | | | | 6 | d_com_hi_0 | a_diff | a_diff | a_diff | a_diff |
|
|
|
|
| | | | | 5 | c_com_lo_0 | | | | |
|
|
|
|
| | | | | 4 | c_com_hi_0 | | | | |
|
|
|
|
| c_com_hi | c_com_lo | d_com_hi | d_com_lo | 3 | b_com_lo_0 | | | | |
|
|
|
|
| a_com_hi | a_com_lo | b_com_hi | b_com_lo | 2 | b_com_hi_0 | | | | |
|
|
|
|
| c_hi | c_lo | d_hi | d_lo | 1 | a_com_lo_0 | | | | |
|
|
|
|
| a_hi | a_lo | b_hi | d_lo | 0 | a_com_hi_0 | | | | |
|
|
|
|
(因为a,b 都是输入不需要进行范围约束，但是因为我们需要判断a,b的符号，所以只需要对a_hi,b_hi进行范围约束。因为c,d 属于非输入值，并且我们要计算c + c_com = 1<<256。
|
|
|
|
所以我们需要对c,d进行范围约束)
|
|
|
|
其中u_16 具有8列，这里为了表现清晰，我们做了简便处理。
|
|
|
|
|
|
|
|
| hi | lo | hi | lo | cnt | u16_0 | u16_1 | u16_2 | u16_3 | u16_4 |
|
|
|
|
| ---------------------- | -------------- | -------------- | -------------- | ---- |----------------|--------|--------|--------|------------|
|
|
|
|
| | | | | 17 | d_lo_0 | | | | |
|
|
|
|
| | | | | 16 | d_hi_0 | | | | |
|
|
|
|
| | | | | 15 | c_lo_0 | | | | |
|
|
|
|
| a_com_lt | | | | 14 | c_hi_0 | | | | |
|
|
|
|
| c_sum_carry_hi | c_sum_carry_lo | d_sum_carry_hi | d_sum_carry_lo | 13 | b_hi_0 | | | | |
|
|
|
|
| a_sum_carry_hi | a_sum_carry_lo | b_sum_carry_hi | b_sum_carry_lo | 12 | a_hi_0 | | | | |
|
|
|
|
| a_lt_carry_hi | b_lt_carry_hi | c_lt_carry_hi | d_lt_carry_hi | 11 | a_diff | b_diff | c_diff | d_diff | a_com_diff |
|
|
|
|
| | | | | 10 | cb_diff_lo_0 | | | | |
|
|
|
|
| cb_diff_hi(cb 指c < b) | cb_diff_lo | cb_carry_hi | | 9 | cb_diff_hi_0 | | | | |
|
|
|
|
| mul_carry_hi | mul_carry_lo | | | 8 | mul_carry_lo_0 | | | | |
|
|
|
|
| | | | | 7 | d_com_lo_0 | | | | |
|
|
|
|
| | | | | 6 | d_com_hi_0 | | | | |
|
|
|
|
| | | | | 5 | c_com_lo_0 | | | | |
|
|
|
|
| | | | | 4 | c_com_hi_0 | | | | |
|
|
|
|
| c_com_hi | c_com_lo | d_com_hi | d_com_lo | 3 | b_com_lo_0 | | | | |
|
|
|
|
| a_com_hi | a_com_lo | b_com_hi | b_com_lo | 2 | b_com_hi_0 | | | | |
|
|
|
|
| c_hi | c_lo | d_hi | d_lo | 1 | a_com_lo_0 | | | | |
|
|
|
|
| a_hi | a_lo | b_hi | d_lo | 0 | a_com_hi_0 | | | | |
|
|
|
|
|
|
|
|
## AddMod
|
|
|
|
|
| ... | ... | |
