// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // Find the first element of an array that has a certain property. In the case// // below, the property has already been applied to form a boolean array, and // // thus, we seek the index of the first "true" in the array. // // Note that algorithm FirstOne requires time O(1) using O(N^2) processors. // // The algorithm below applies FirstOne twice to reduce the number of required// // processors to O(N) while still requiring time O(1). // // ************************************************************************** // macro M = 4; macro N = M*M; module FirstOneOpt([N]bool ?a,nat{N} index, event !rdy) { [N]bool x; [M]bool y; nat{M} yindex; // use O(N) processors to copy a to x; one might apply a desired property // to a[i] before copying, so that arbitrary properties can be checked for(i=0..N-1) x[i] = a[i]; // use O(M^2) = O(N) processors to check in which groups of size M there // are true bits for(i=0..M-1) for(j=0..M-1) if(x[i*M+j]) y[i] = true; // apply FirstOne to determine the first index of a group holding a true bit // this requires O(M^2)=O(N) processors and O(1) time for(i=0..M-2) for(j=i+1..M-1) if(y[i] & y[j]) next(y[j]) = false; w1: pause; // now, at most one y[i] is true; if so, i is the desired index for(i=0..M-1) if(y[i]) yindex = i; // we now know that the first true bit is in x[yindex*M..yindex*M+M-1] // thus, apply FirstOne again to this subsequence to determine the index for(i=0..M-2) for(j=i+1..M-1) if(x[yindex*M+i] & x[yindex*M+j]) next(x[yindex*M+j]) = false; w2: pause; // now, at most one x[i] in x[yindex*M..yindex*M+M-1]is true; // if so, this i is the desired index for(i=0..M-1) if(x[yindex*M+i]) index = yindex*M+i; emit(rdy); } drivenby { for(i=0..N-1) a[i] = i==5 | i==7 | i==9 | i==11; await(rdy); assert(a[index] -> forall(i=0..N-1) (i<index -> !a[i])); }