// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // The subtraction of B-complement numbers requires a special full adder to // // add the most significant digits of the B-complement numbers. These digits // // are given as unsigned integers of type nat{B}, but they are interpreted by // // function alpha given below as signed integers of type int{B/2}. Hence, the // // intended values for cout and s must satisfy the following equation: // // alpha(x)-(alpha(y)+cin) == alpha(cout) * B + s. // // These values are obviously computed by the reference implementation: // // // // module FullSubBC(nat{B} ?x,?y,nat{2} ?cin,nat{B} cout,nat{B} s) { // // event int{B} sm; // // sm = alpha(x) - (alpha(y) + cin); // // s = sm % B; // // cout = gamma(sm / B); // // } // // // // To show the correctness of the implementation given below, abbreviate the // // values xa:=alpha(x) and ya:=alpha(y). Then, the following bounds can be // // easily derived for sm=xa-(ya+cin) // // // // (1) xa>=0 and ya>=0 --> sm is in {0,…,b-1}-({0,…,b-1}+{0,1})={-b,…,b-1} // // (2) xa>=0 and ya<0 --> sm is in {0,…,b-1}-({-b,…,-1}+{0,1})={0,…,2b-1} // // (3) xa<0 and ya>=0 --> sm is in {-b,…,-1}-({0,…,b-1}+{0,1})={-2b,…,-1} // // (4) xa<0 and ya<0 --> sm is in {-b,…,-1}-({-b,…,-1}+{0,1})={-b,…,b-1} // // // // Thus, in case (2), we have (xa-(ya+cin))/B=0 and therefore cout=0, and in // // case (3), we have (xa-(ya+cin))/B=-1, and therefore cout=B-1. In cases (1) // // and (4), the value of (xa-(ya+cin))/B depends on the sign of sm. As can be // // seen, the sum sm fits into a machine word in these cases, so that variable // // s holds this value in these cases. Finally, note that x<b holds if and only// // if alpha(x)>=0 holds. // // ************************************************************************** // macro B = 8; macro b = 4; macro alpha(x) = (x<b ? +x : +x-B); macro gamma(y) = (y<0 ? y+B : y); // note that addition/subtraction of signed and unsigned numbers yields the same // results on a processor; only the definition of overflow is different macro uadd(x,y) = (x+y)%B; macro usub(x,y) = (+x-y)%B; module IntFullSub(nat{B} ?x,?y,nat{2} ?cin,nat{B} cout,s) { s = usub(x,uadd(y,cin)); if(x<b) if(y<b) // (1) alpha(x)>=0 & alpha(y)>=0 cout = (s<b ? 0 : B-1); else // (2) alpha(x)>=0 & alpha(y)<0 cout = 0; else if(y<b) // (3) alpha(x)<0 & alpha(y)>=0 cout = B-1; else // (4) alpha(x)<0 & alpha(y)<0 cout = (s<b ? 0 : B-1); assert(alpha(x)-(alpha(y)+cin) == alpha(cout) * B + s); }