[8] | 1 | #include "mdd.h" |
---|
| 2 | |
---|
| 3 | /*---------------------------------------------------------------------------*/ |
---|
| 4 | /* Static function prototypes */ |
---|
| 5 | /*---------------------------------------------------------------------------*/ |
---|
| 6 | |
---|
| 7 | EXTERN void addition_block_build(mdd_manager *mgr, mdd_t **A, mdd_t **B, bvar_type *bx_ptr, bvar_type *by_ptr, bvar_type *bz_ptr); |
---|
| 8 | EXTERN void one_var_and_carry_add_block(mdd_manager *mgr, mdd_t **A, mdd_t **B, bvar_type *bz_ptr, bvar_type *blv_ptr); |
---|
| 9 | |
---|
| 10 | |
---|
| 11 | void |
---|
| 12 | addition_block_build( |
---|
| 13 | mdd_manager *mgr, |
---|
| 14 | mdd_t **A, |
---|
| 15 | mdd_t **B, |
---|
| 16 | bvar_type *bx_ptr, |
---|
| 17 | bvar_type *by_ptr, |
---|
| 18 | bvar_type *bz_ptr) |
---|
| 19 | { |
---|
| 20 | mdd_t *zero; |
---|
| 21 | mdd_t *C, *D, *E, *F, |
---|
| 22 | *G, *H, *I; |
---|
| 23 | |
---|
| 24 | zero = mdd_zero(mgr); |
---|
| 25 | |
---|
| 26 | G = mdd_ite( by_ptr->node, zero , *A , 1, 1, 1 ); |
---|
| 27 | H = mdd_ite( by_ptr->node, *A , *B , 1, 1, 1 ); |
---|
| 28 | I = mdd_ite( by_ptr->node, *B , zero, 1, 1, 1 ); |
---|
| 29 | |
---|
| 30 | C = mdd_ite( bx_ptr->node, zero, G , 1, 1, 1 ); |
---|
| 31 | D = mdd_ite( bx_ptr->node, G , H , 1, 1, 1 ); |
---|
| 32 | E = mdd_ite( bx_ptr->node, H , I , 1, 1, 1 ); |
---|
| 33 | F = mdd_ite( bx_ptr->node, I , zero, 1, 1, 1 ); |
---|
| 34 | |
---|
| 35 | *A = mdd_ite( bz_ptr->node, D , C , 1, 1, 1 ); |
---|
| 36 | *B = mdd_ite( bz_ptr->node, F , E , 1, 1, 1 ); |
---|
| 37 | |
---|
| 38 | mdd_free(G); |
---|
| 39 | mdd_free(H); |
---|
| 40 | mdd_free(I); |
---|
| 41 | mdd_free(C); |
---|
| 42 | mdd_free(D); |
---|
| 43 | mdd_free(E); |
---|
| 44 | mdd_free(F); |
---|
| 45 | mdd_free(zero); |
---|
| 46 | |
---|
| 47 | return; |
---|
| 48 | } |
---|
| 49 | |
---|
| 50 | |
---|
| 51 | void |
---|
| 52 | one_var_and_carry_add_block( |
---|
| 53 | mdd_manager *mgr, |
---|
| 54 | mdd_t **A, |
---|
| 55 | mdd_t **B, |
---|
| 56 | bvar_type *bz_ptr, |
---|
| 57 | bvar_type *blv_ptr) |
---|
| 58 | { |
---|
| 59 | mdd_t *C, *D, *E; |
---|
| 60 | mdd_t *zero; |
---|
| 61 | |
---|
| 62 | zero = mdd_zero(mgr); |
---|
| 63 | |
---|
| 64 | C = mdd_ite( blv_ptr->node, zero, *A, 1, 1, 1); |
---|
| 65 | D = mdd_ite( blv_ptr->node, *A, *B, 1, 1, 1); |
---|
| 66 | E = mdd_ite( blv_ptr->node, *B, zero, 1, 1, 1); |
---|
| 67 | |
---|
| 68 | *A = mdd_ite( bz_ptr->node, D, C, 1, 1, 1); |
---|
| 69 | *B = mdd_ite( bz_ptr->node, zero, E, 1, 1, 1); |
---|
| 70 | |
---|
| 71 | mdd_free(C); |
---|
| 72 | mdd_free(D); |
---|
| 73 | mdd_free(E); |
---|
| 74 | |
---|
| 75 | mdd_free(zero); |
---|
| 76 | |
---|
| 77 | return; |
---|
| 78 | } |
---|
| 79 | |
---|
| 80 | /* in1 + in2 = sum */ |
---|
| 81 | mdd_t * |
---|
| 82 | mdd_add_s( |
---|
| 83 | mdd_manager *mgr, |
---|
| 84 | int sum_id, |
---|
| 85 | int mvar_id1, |
---|
| 86 | int mvar_id2) |
---|
| 87 | { |
---|
| 88 | mdd_t *one, *zero; |
---|
| 89 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 90 | array_t *bvar_list = mdd_ret_bvar_list(mgr); |
---|
| 91 | int config, |
---|
| 92 | no_common_to_all_bits, |
---|
| 93 | no_common_in_bits, i; |
---|
| 94 | |
---|
| 95 | bvar_type bx, by, bz, z_carry, blv; |
---|
| 96 | mvar_type x, y, z, long_var; |
---|
| 97 | mdd_t *A, *B, *range_check; |
---|
| 98 | mdd_t *result = NIL(mdd_t); /* initialize for lint */ |
---|
| 99 | |
---|
| 100 | |
---|
| 101 | |
---|
| 102 | x = array_fetch(mvar_type, mvar_list, mvar_id1); |
---|
| 103 | y = array_fetch(mvar_type, mvar_list, mvar_id2); |
---|
| 104 | z = array_fetch(mvar_type, mvar_list, sum_id); |
---|
| 105 | |
---|
| 106 | /* Ensures that the i_th bit of x has smaller index |
---|
| 107 | than the i_th bit of y */ |
---|
| 108 | |
---|
| 109 | if ( ( mdd_ret_bvar_id(&x,x.encode_length) ) > |
---|
| 110 | ( mdd_ret_bvar_id(&y,y.encode_length) ) ) { |
---|
| 111 | y = array_fetch(mvar_type, mvar_list, mvar_id1); |
---|
| 112 | x = array_fetch(mvar_type, mvar_list, mvar_id2); |
---|
| 113 | } |
---|
| 114 | |
---|
| 115 | one = mdd_one(mgr); |
---|
| 116 | zero = mdd_zero(mgr); |
---|
| 117 | |
---|
| 118 | no_common_in_bits = MIN(x.encode_length,y.encode_length); |
---|
| 119 | no_common_to_all_bits = MIN(no_common_in_bits, z.encode_length); |
---|
| 120 | |
---|
| 121 | A = mdd_dup(one); |
---|
| 122 | B = mdd_dup(zero); |
---|
| 123 | |
---|
| 124 | for (i = 1; i <= no_common_to_all_bits; i++){ |
---|
| 125 | |
---|
| 126 | bx = mdd_ret_bvar(&x,x.encode_length-i,bvar_list); |
---|
| 127 | by = mdd_ret_bvar(&y,y.encode_length-i,bvar_list); |
---|
| 128 | bz = mdd_ret_bvar(&z,z.encode_length-i,bvar_list); |
---|
| 129 | addition_block_build( mgr, &A, &B, &bx, &by, &bz); |
---|
| 130 | } |
---|
| 131 | |
---|
| 132 | |
---|
| 133 | if ( z.encode_length > no_common_to_all_bits ){ |
---|
| 134 | if ( x.encode_length != y.encode_length ){ |
---|
| 135 | if ( x.encode_length == no_common_in_bits ){ |
---|
| 136 | long_var = y; |
---|
| 137 | /* short_var = x; */ |
---|
| 138 | } |
---|
| 139 | else { |
---|
| 140 | long_var = x; |
---|
| 141 | /* short_var = y; */ |
---|
| 142 | } |
---|
| 143 | |
---|
| 144 | if ( z.encode_length > long_var.encode_length) { |
---|
| 145 | config = 1; |
---|
| 146 | } |
---|
| 147 | else |
---|
| 148 | { |
---|
| 149 | config = 2; |
---|
| 150 | } |
---|
| 151 | } |
---|
| 152 | else |
---|
| 153 | config = 3; |
---|
| 154 | } |
---|
| 155 | else |
---|
| 156 | config = 4; |
---|
| 157 | |
---|
| 158 | |
---|
| 159 | switch (config) { |
---|
| 160 | |
---|
| 161 | case 1: /* z > long_var , short_var */ |
---|
| 162 | |
---|
| 163 | for ( i = no_common_to_all_bits + 1; i <= long_var.encode_length; i++){ |
---|
| 164 | |
---|
| 165 | z_carry = mdd_ret_bvar(&z,z.encode_length-i,bvar_list); |
---|
| 166 | blv = mdd_ret_bvar(&long_var,long_var.encode_length-i,bvar_list); |
---|
| 167 | |
---|
| 168 | one_var_and_carry_add_block(mgr, &A, &B, &bz, &blv); |
---|
| 169 | } |
---|
| 170 | |
---|
| 171 | z_carry = mdd_ret_bvar(&z,z.encode_length - long_var.encode_length - 1, bvar_list); |
---|
| 172 | |
---|
| 173 | A = mdd_ite( z_carry.node, B, A, 1, 1, 1); |
---|
| 174 | |
---|
| 175 | for ( i = long_var.encode_length + 2; i <= z.encode_length; i++){ |
---|
| 176 | z_carry = mdd_ret_bvar(&z,z.encode_length-i, bvar_list); |
---|
| 177 | A = mdd_ite( z_carry.node, zero, A, 1, 1, 1); |
---|
| 178 | } |
---|
| 179 | result = mdd_dup(A); |
---|
| 180 | break; |
---|
| 181 | |
---|
| 182 | case 2: /* short_var < z < long_var */ |
---|
| 183 | |
---|
| 184 | for ( i = no_common_to_all_bits + 1; i <= z.encode_length; i++){ |
---|
| 185 | |
---|
| 186 | z_carry = mdd_ret_bvar(&z,z.encode_length-i,bvar_list); |
---|
| 187 | blv = mdd_ret_bvar(&long_var,long_var.encode_length-i,bvar_list); |
---|
| 188 | |
---|
| 189 | one_var_and_carry_add_block(mgr, &A, &B, &bz, &blv); |
---|
| 190 | |
---|
| 191 | } |
---|
| 192 | |
---|
| 193 | result = mdd_or(A,B,1,1); |
---|
| 194 | break; |
---|
| 195 | |
---|
| 196 | case 3: /* z> long_var = short_var */ |
---|
| 197 | |
---|
| 198 | z_carry = mdd_ret_bvar(&z,z.encode_length - no_common_to_all_bits - 1,bvar_list); |
---|
| 199 | A = mdd_ite( z_carry.node, B, A, 1, 1, 1); |
---|
| 200 | |
---|
| 201 | for ( i = no_common_to_all_bits + 2; i <= z.encode_length; i++){ |
---|
| 202 | z_carry = mdd_ret_bvar(&z, z.encode_length - i, bvar_list); |
---|
| 203 | A = mdd_ite( z_carry.node, zero, A, 1, 1, 1); |
---|
| 204 | } |
---|
| 205 | |
---|
| 206 | result = mdd_dup(A); |
---|
| 207 | break; |
---|
| 208 | |
---|
| 209 | case 4: /* z <= long_var, z <= short_var */ |
---|
| 210 | result = mdd_or(A,B,1,1); |
---|
| 211 | break; |
---|
| 212 | } |
---|
| 213 | |
---|
| 214 | mdd_free(A); |
---|
| 215 | mdd_free(B); |
---|
| 216 | |
---|
| 217 | |
---|
| 218 | mdd_free(one); |
---|
| 219 | mdd_free(zero); |
---|
| 220 | |
---|
| 221 | range_check = build_lt_c(mgr, sum_id, z.values); |
---|
| 222 | result = mdd_and(result, range_check, 1, 1); |
---|
| 223 | |
---|
| 224 | mdd_free(range_check); |
---|
| 225 | |
---|
| 226 | return result; |
---|
| 227 | } |
---|
| 228 | |
---|
| 229 | |
---|