// ************************************************************************** // // // // 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 constructive cyclic program is due to Riedel [Ried04]. The assertions // // indicate an equivalent acyclic version. // // ************************************************************************** // module Riedel1(event ?x1,?x2,?x3,y1,y2,y3) { event w1,w2,w3,w4,w5,w6; always{ w1 = x1 & y1; w2 = !x1 & y2; w3 = x2 & w5; w4 = !x2 & w6; w5 = x1 | y3; w6 = !x1 | y3; y1 = x3 | w3; y2 = !x3 | w4; y3 = !(w1 | !w2); assert(y1 == (x2 | x3)); assert(y2 == (!x3 | !x1 & !x2)); assert(y3 == (!x1 & !(x2&x3))); } } drivenby { bv{3} w; for(i=0..7) { pause; w = nat2bv(i,3); x1 = w{0}; x2 = w{1}; x3 = w{2}; } }