| 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 |
|
| 82 |
|
| 83 | // Premise: i == j and (in2 - in1 == (j - i))
|
| 84 | // Conclusion: out2 - out1 == (j - i)
|
| 85 | wire [31:0] diffin2in1;
|
| 86 | wire [31:0] diffij;
|
| 87 | wire [31:0] diffout2out1;
|
| 88 | assign diffin2in1 = (in[63:32] - in[31:0]);
|
| 89 | assign diffij = (j - i);
|
| 90 | assign diffout2out1 = (out[63:32] - out[31:0]);
|
| 91 |
|
| 92 | wire di2i1_eq_dij;
|
| 93 | wire do2o1_eq_dij;
|
| 94 | wire i_eq_j;
|
| 95 | assign di2i1_eq_dij = &(~(diffin2in1 ^ diffij));
|
| 96 | assign do2o1_eq_dij = &(~(diffout2out1 ^ diffij));
|
| 97 | assign i_eq_j = &(~(i ^ j));
|
| 98 |
|
| 99 | wire implication1;
|
| 100 | assign implication1 = ~(i_eq_j & di2i1_eq_dij) | do2o1_eq_dij;
|
| 101 |
|
| 102 | wire all_implications_hold;
|
| 103 | assign all_implications_hold =
|
| 104 | implication1;
|
| 105 |
|
| 106 | assign error = ~all_implications_hold;
|
| 107 |
|
| 108 | endmodule
|
| 109 |
|
