| 1 | module Decrementer_Check(in,i,j,out,error);
|
| 2 | input [63:0] in;
|
| 3 | input [31:0] i;
|
| 4 | input [31:0] j;
|
| 5 | input [63:0] out;
|
| 6 | output error;
|
| 7 |
|
| 8 | wire [30:0] in1;
|
| 9 | wire [30:0] in2;
|
| 10 | wire [30:0] out1;
|
| 11 | wire [30:0] out2;
|
| 12 | wire sign_in1;
|
| 13 | wire sign_in2;
|
| 14 | wire sign_out1;
|
| 15 | wire sign_out2;
|
| 16 |
|
| 17 | assign in1 = in[30:0];
|
| 18 | assign in2 = in[62:32];
|
| 19 | assign out1 = out[30:0];
|
| 20 | assign out2 = out[62:32];
|
| 21 |
|
| 22 | assign sign_in1 = in[31];
|
| 23 | assign sign_in2 = in[63];
|
| 24 | assign sign_out1 = out[31];
|
| 25 | assign sign_out2 = out[63];
|
| 26 |
|
| 27 | wire in1_or_reduced;
|
| 28 | wire in1_eq_zero;
|
| 29 | wire in1_lt_zero;
|
| 30 | wire in1_gt_zero;
|
| 31 | wire in1_eq_min;
|
| 32 | assign in1_or_reduced = |in1;
|
| 33 | assign in1_eq_zero = ~sign_in1 & ~in1_or_reduced;
|
| 34 | assign in1_lt_zero = sign_in1;
|
| 35 | assign in1_gt_zero = ~sign_in1 & in1_or_reduced;
|
| 36 | assign in1_eq_min = sign_in1 & ~in1_or_reduced;
|
| 37 |
|
| 38 | wire in2_or_reduced;
|
| 39 | wire in2_eq_zero;
|
| 40 | wire in2_lt_zero;
|
| 41 | wire in2_gt_zero;
|
| 42 | wire in2_eq_min;
|
| 43 | assign in2_or_reduced = |in2;
|
| 44 | assign in2_eq_zero = ~sign_in2 & ~in2_or_reduced;
|
| 45 | assign in2_lt_zero = sign_in2;
|
| 46 | assign in2_gt_zero = ~sign_in2 & in2_or_reduced;
|
| 47 | assign in2_eq_min = sign_in2 & ~in2_or_reduced;
|
| 48 |
|
| 49 | wire out1_or_reduced;
|
| 50 | wire out1_and_reduced;
|
| 51 | wire out1_eq_zero;
|
| 52 | wire out1_lt_zero;
|
| 53 | wire out1_gt_zero;
|
| 54 | wire out1_eq_min;
|
| 55 | assign out1_or_reduced = |out1;
|
| 56 | assign out1_and_reduced = &out1;
|
| 57 | assign out1_eq_zero = ~sign_out1 & ~out1_or_reduced;
|
| 58 | assign out1_lt_zero = sign_out1;
|
| 59 | assign out1_gt_zero = ~sign_out1 & out1_or_reduced;
|
| 60 | assign out1_eq_min = sign_out1 & ~out1_or_reduced;
|
| 61 |
|
| 62 | wire out2_or_reduced;
|
| 63 | wire out2_and_reduced;
|
| 64 | wire out2_eq_zero;
|
| 65 | wire out2_lt_zero;
|
| 66 | wire out2_gt_zero;
|
| 67 | wire out2_eq_min;
|
| 68 | assign out2_or_reduced = |out2;
|
| 69 | assign out2_and_reduced = &out2;
|
| 70 | assign out2_eq_zero = ~sign_out2 & ~out2_or_reduced;
|
| 71 | assign out2_lt_zero = sign_out2;
|
| 72 | assign out2_gt_zero = ~sign_out2 & out2_or_reduced;
|
| 73 | assign out2_eq_min = sign_out2 & ~out2_or_reduced;
|
| 74 |
|
| 75 | // has to be of the form (0)*(1)+
|
| 76 | wire [30:0] in1_xor_out1;
|
| 77 | wire [30:0] in2_xor_out2;
|
| 78 | assign in1_xor_out1 = (in1 ^ out1);
|
| 79 | assign in2_xor_out2 = (in2 ^ out2);
|
| 80 |
|
| 81 | wire dec1_mincase_correct;
|
| 82 | wire dec1_signflip_correct;
|
| 83 | wire dec1_deccase_correct;
|
| 84 | wire dec1_correct;
|
| 85 | wire dec2_mincase_correct;
|
| 86 | wire dec2_signflip_correct;
|
| 87 | wire dec2_deccase_correct;
|
| 88 | wire dec2_correct;
|
| 89 |
|
| 90 | assign dec1_mincase_correct = ~in1_eq_min | out1_eq_min;
|
| 91 | assign dec1_signflip_correct = ~(sign_in1 ^ sign_out1) | (in1_eq_zero & out1_and_reduced);
|
| 92 | assign dec2_mincase_correct = ~in2_eq_min | out2_eq_min;
|
| 93 | assign dec2_signflip_correct = ~(sign_in2 ^ sign_out2) | (in2_eq_zero & out2_and_reduced);
|
| 94 |
|
| 95 | // only allow '01' transitions, not '10', LSB must be set
|
| 96 | assign dec1_deccase_correct = ((sign_in1 ^ sign_out1) | in1_eq_min) | ( in1_xor_out1[0]
|
| 97 | & ( ~(in1_xor_out1[1] ^ in1_xor_out1[0]) | in1_xor_out1[0] )
|
| 98 | & ( ~(in1_xor_out1[2] ^ in1_xor_out1[1]) | in1_xor_out1[1] )
|
| 99 | & ( ~(in1_xor_out1[3] ^ in1_xor_out1[2]) | in1_xor_out1[2] )
|
| 100 | & ( ~(in1_xor_out1[4] ^ in1_xor_out1[3]) | in1_xor_out1[3] )
|
| 101 | & ( ~(in1_xor_out1[5] ^ in1_xor_out1[4]) | in1_xor_out1[4] )
|
| 102 | & ( ~(in1_xor_out1[6] ^ in1_xor_out1[5]) | in1_xor_out1[5] )
|
| 103 | & ( ~(in1_xor_out1[7] ^ in1_xor_out1[6]) | in1_xor_out1[6] )
|
| 104 | & ( ~(in1_xor_out1[8] ^ in1_xor_out1[7]) | in1_xor_out1[7] )
|
| 105 | & ( ~(in1_xor_out1[9] ^ in1_xor_out1[8]) | in1_xor_out1[8] )
|
| 106 | & ( ~(in1_xor_out1[10] ^ in1_xor_out1[9]) | in1_xor_out1[9] )
|
| 107 | & ( ~(in1_xor_out1[11] ^ in1_xor_out1[10]) | in1_xor_out1[10] )
|
| 108 | & ( ~(in1_xor_out1[12] ^ in1_xor_out1[11]) | in1_xor_out1[11] )
|
| 109 | & ( ~(in1_xor_out1[13] ^ in1_xor_out1[12]) | in1_xor_out1[12] )
|
| 110 | & ( ~(in1_xor_out1[14] ^ in1_xor_out1[13]) | in1_xor_out1[13] )
|
| 111 | & ( ~(in1_xor_out1[15] ^ in1_xor_out1[14]) | in1_xor_out1[14] )
|
| 112 | & ( ~(in1_xor_out1[16] ^ in1_xor_out1[15]) | in1_xor_out1[15] )
|
| 113 | & ( ~(in1_xor_out1[17] ^ in1_xor_out1[16]) | in1_xor_out1[16] )
|
| 114 | & ( ~(in1_xor_out1[18] ^ in1_xor_out1[17]) | in1_xor_out1[17] )
|
| 115 | & ( ~(in1_xor_out1[19] ^ in1_xor_out1[18]) | in1_xor_out1[18] )
|
| 116 | & ( ~(in1_xor_out1[20] ^ in1_xor_out1[19]) | in1_xor_out1[19] )
|
| 117 | & ( ~(in1_xor_out1[21] ^ in1_xor_out1[20]) | in1_xor_out1[20] )
|
| 118 | & ( ~(in1_xor_out1[22] ^ in1_xor_out1[21]) | in1_xor_out1[21] )
|
| 119 | & ( ~(in1_xor_out1[23] ^ in1_xor_out1[22]) | in1_xor_out1[22] )
|
| 120 | & ( ~(in1_xor_out1[24] ^ in1_xor_out1[23]) | in1_xor_out1[23] )
|
| 121 | & ( ~(in1_xor_out1[25] ^ in1_xor_out1[24]) | in1_xor_out1[24] )
|
| 122 | & ( ~(in1_xor_out1[26] ^ in1_xor_out1[25]) | in1_xor_out1[25] )
|
| 123 | & ( ~(in1_xor_out1[27] ^ in1_xor_out1[26]) | in1_xor_out1[26] )
|
| 124 | & ( ~(in1_xor_out1[28] ^ in1_xor_out1[27]) | in1_xor_out1[27] )
|
| 125 | & ( ~(in1_xor_out1[29] ^ in1_xor_out1[28]) | in1_xor_out1[28] )
|
| 126 | & ( ~(in1_xor_out1[30] ^ in1_xor_out1[29]) | in1_xor_out1[29] ) );
|
| 127 |
|
| 128 | // only allow '01' transitions, not '10', LSB must be set
|
| 129 | assign dec2_deccase_correct = ((sign_in2 ^ sign_out2) | in2_eq_min) | ( in2_xor_out2[0]
|
| 130 | & ( ~(in2_xor_out2[1] ^ in2_xor_out2[0]) | in2_xor_out2[0] )
|
| 131 | & ( ~(in2_xor_out2[2] ^ in2_xor_out2[1]) | in2_xor_out2[1] )
|
| 132 | & ( ~(in2_xor_out2[3] ^ in2_xor_out2[2]) | in2_xor_out2[2] )
|
| 133 | & ( ~(in2_xor_out2[4] ^ in2_xor_out2[3]) | in2_xor_out2[3] )
|
| 134 | & ( ~(in2_xor_out2[5] ^ in2_xor_out2[4]) | in2_xor_out2[4] )
|
| 135 | & ( ~(in2_xor_out2[6] ^ in2_xor_out2[5]) | in2_xor_out2[5] )
|
| 136 | & ( ~(in2_xor_out2[7] ^ in2_xor_out2[6]) | in2_xor_out2[6] )
|
| 137 | & ( ~(in2_xor_out2[8] ^ in2_xor_out2[7]) | in2_xor_out2[7] )
|
| 138 | & ( ~(in2_xor_out2[9] ^ in2_xor_out2[8]) | in2_xor_out2[8] )
|
| 139 | & ( ~(in2_xor_out2[10] ^ in2_xor_out2[9]) | in2_xor_out2[9] )
|
| 140 | & ( ~(in2_xor_out2[11] ^ in2_xor_out2[10]) | in2_xor_out2[10] )
|
| 141 | & ( ~(in2_xor_out2[12] ^ in2_xor_out2[11]) | in2_xor_out2[11] )
|
| 142 | & ( ~(in2_xor_out2[13] ^ in2_xor_out2[12]) | in2_xor_out2[12] )
|
| 143 | & ( ~(in2_xor_out2[14] ^ in2_xor_out2[13]) | in2_xor_out2[13] )
|
| 144 | & ( ~(in2_xor_out2[15] ^ in2_xor_out2[14]) | in2_xor_out2[14] )
|
| 145 | & ( ~(in2_xor_out2[16] ^ in2_xor_out2[15]) | in2_xor_out2[15] )
|
| 146 | & ( ~(in2_xor_out2[17] ^ in2_xor_out2[16]) | in2_xor_out2[16] )
|
| 147 | & ( ~(in2_xor_out2[18] ^ in2_xor_out2[17]) | in2_xor_out2[17] )
|
| 148 | & ( ~(in2_xor_out2[19] ^ in2_xor_out2[18]) | in2_xor_out2[18] )
|
| 149 | & ( ~(in2_xor_out2[20] ^ in2_xor_out2[19]) | in2_xor_out2[19] )
|
| 150 | & ( ~(in2_xor_out2[21] ^ in2_xor_out2[20]) | in2_xor_out2[20] )
|
| 151 | & ( ~(in2_xor_out2[22] ^ in2_xor_out2[21]) | in2_xor_out2[21] )
|
| 152 | & ( ~(in2_xor_out2[23] ^ in2_xor_out2[22]) | in2_xor_out2[22] )
|
| 153 | & ( ~(in2_xor_out2[24] ^ in2_xor_out2[23]) | in2_xor_out2[23] )
|
| 154 | & ( ~(in2_xor_out2[25] ^ in2_xor_out2[24]) | in2_xor_out2[24] )
|
| 155 | & ( ~(in2_xor_out2[26] ^ in2_xor_out2[25]) | in2_xor_out2[25] )
|
| 156 | & ( ~(in2_xor_out2[27] ^ in2_xor_out2[26]) | in2_xor_out2[26] )
|
| 157 | & ( ~(in2_xor_out2[28] ^ in2_xor_out2[27]) | in2_xor_out2[27] )
|
| 158 | & ( ~(in2_xor_out2[29] ^ in2_xor_out2[28]) | in2_xor_out2[28] )
|
| 159 | & ( ~(in2_xor_out2[30] ^ in2_xor_out2[29]) | in2_xor_out2[29] ) );
|
| 160 |
|
| 161 | assign dec1_correct = dec1_mincase_correct & dec1_signflip_correct & dec1_deccase_correct;
|
| 162 | assign dec2_correct = dec2_mincase_correct & dec2_signflip_correct & dec2_deccase_correct;
|
| 163 |
|
| 164 | wire all_implications_hold;
|
| 165 | assign all_implications_hold =
|
| 166 | dec1_correct &
|
| 167 | dec2_correct;
|
| 168 |
|
| 169 | assign error = ~all_implications_hold;
|
| 170 |
|
| 171 | endmodule
|
| 172 |
|
