// ************************************************************************** // // // // 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 module below implements an algorithm for checking equality of binary // // signed digit numbers. It is based on the reduction x==y <-> x-y==0 and the // // fact that 0 has uniquely representation. The subtraction can be done in // // depth O(1), but checking whether all digits are 0 requires time O(log(N)). // // Note that the subtraction algorithm requires floor(B/2)+1 <= D < B which // // is not possible for B=2. // // ************************************************************************** // macro D = 3; // digit set is -D,...,-1,0,1,...,D macro B = 5; // base of the radix numbers macro N = 4; // number of digits used for the addition // macro to evaluate a signed digit number macro sgnval(x,k) = sum(i=0..k-1) (x[i] * exp(B,i)); module SgnEqu([N]int{D+1} ?x,?y,bool eqq) { [N+1]int{2} t; // transfer digits [N+1]int{D+1} s; // sum digits of a-b // compute sum and transfer digits in parallel t[0] = 0; for(i=0..N-1) let(ds = x[i]-y[i]) { t[i+1] = (ds>=D?+1:(ds<=-D?-1:0)); s[i] = ds + t[i] - t[i+1] * B; } s[N] = t[N]; eqq = forall(i=0..N) (s[i]==0); assert(eqq <-> (sgnval(x,N) == sgnval(y,N))); }