// ************************************************************************** // // // // 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 equality checking for radix-B numbers. // // The algorithm has depth O(log(N)) since the Quartz compiler converts // // generic expressions into balanced binary trees. // // ************************************************************************** // 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 NatEqu([N]nat{B} ?x,?y,bool eq) { eq = forall(i=0..N-1) (x[i]==y[i]); assert(eq <-> 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; } }