// ************************************************************************** // // // // 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 following module implements comparison of B-complement numbers. // // The depth of the algorithm below is O(N), which can be obviously improved // // to O(log(N)) using a parallel prefix computation. Alternatively, we refer // // to IntSubCLA which has depth O(log(N)) and can also compare numbers. // // ** Note: We are only interested in even values of B ** // // ************************************************************************** // macro B = 4; // base of the radix numbers macro N = 4; // number of digits used macro alpha(x) = (x<B/2 ? +x : +x-B); macro gamma(y) = (y<0 ? y+B : y); macro dval(x,i,k) = (i==k-1 ? alpha(x[i]) : +x[i]); macro intval(x,k) = sum(i=0..k-1) (dval(x,i,k) * exp(B,i)); module IntLes([N]nat{B} ?x,?y,bool les,eqq) { event [N]bool ls,eq; ls[N-1] = alpha(x[N-1]) < alpha(y[N-1]); eq[N-1] = x[N-1] == y[N-1]; for(i=0..N-2) { ls[i] = ls[i+1] | eq[i+1] & x[i]<y[i]; eq[i] = eq[i+1] & x[i]==y[i]; } les = ls[0]; eqq = eq[0]; assert(les <-> intval(x,N) < intval(y,N)); assert(eqq <-> intval(x,N) == intval(y,N)); } drivenby Test01 { for(i=0..N-1) { x[i] = i % B; y[i] = (N+i) % B; } } drivenby Test02 { for(i=0..N-1) { x[i] = (2*i+1) % B; y[i] = (N+2*i) % B; } }