// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // This is an unrolling of Rivest with N=5 together with an acyclic version. // // ************************************************************************** // module Rivest05(event [5]bool ?x, event [10]bool y) { loop{ y[0] = x[0]&y[9]; y[1] = x[1]|y[0]; y[2] = x[2]&y[1]; y[3] = x[3]|y[2]; y[4] = x[4]&y[3]; y[5] = x[0]|y[4]; y[6] = x[1]&y[5]; y[7] = x[2]|y[6]; y[8] = x[3]&y[7]; y[9] = x[4]|y[8]; assert(y[0] == (x[0]&x[4] | x[0]&x[2]&x[3] | x[0]&x[1]&x[3])); assert(y[2] == (x[1]&x[2] | x[0]&x[2]&x[4] | x[0]&x[2]&x[3])); assert(y[4] == (x[3]&x[4] | x[1]&x[2]&x[4] | x[0]&x[2]&x[4])); assert(y[6] == (x[0]&x[1] | x[1]&x[3]&x[4] | x[1]&x[2]&x[4])); assert(y[8] == (x[2]&x[3] | x[0]&x[1]&x[3] | x[1]&x[3]&x[4])); assert(y[1] == (x[1] | x[0]&x[4] | x[0]&x[2]&x[3])); assert(y[3] == (x[3] | x[1]&x[2] | x[0]&x[2]&x[4])); assert(y[5] == (x[0] | x[3]&x[4] | x[1]&x[2]&x[4])); assert(y[7] == (x[2] | x[0]&x[1] | x[1]&x[3]&x[4])); assert(y[9] == (x[4] | x[2]&x[3] | x[0]&x[1]&x[3])); pause; } } drivenby { bv{5} w; for(i=0..31) { pause; w = nat2bv(i,5); for(j=0..4) x[j] = w{j}; } }