// ************************************************************************** // // // // 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 subtraction of radix-B numbers. The leading// // digit s[N] of the sum is either 0 or 1, where 1 indicates an underflow, // // while 0 denotes a correct difference. The circuit has depth O(N) and is // // therefore not optimal. // // ************************************************************************** // macro B = 4; // base of the radix numbers macro N = 4; // number of digits used macro natval(x,m) = sum(i=0..m-1) (x[i] * exp(B,i)); module NatSubCRA([N]nat{B} ?x,?y,[N+1]nat{B} s) { [N+1]nat{2} c; // carry digits c[0] = 0; for(i=0..N-1) { event int{B} sm; sm = +x[i] - (y[i] + c[i]); c[i+1] = -(sm / B); s[i] = sm % B; } s[N] = c[N]; if(natval(x,N) >= natval(y,N)) assert(natval(s,N+1) == natval(x,N) - natval(y,N)); assert(s[N]==0 <-> natval(x,N) >= natval(y,N)); assert(s[N]==1 <-> natval(x,N) < natval(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; } }