// ************************************************************************** // // // // 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 module implements the following SIGNAL program: // // // // x +-------+ x1 +-----+ // // ---->| CpyIn |-----o------->| | x5 +--------+ // // +-------+ | | Add |----| CpyOut |---> y // // | +---->| | +--------+ // // +-----+ x2 | | +-----+ // // +->| Buf |---+ | +--------+ // // | +-----+ | | +-----+ | x4 // // x3 | | +->| | | // // | +-----+ | | Whn |--+ // // +--| Not |<--o----->| | // // +-----+ +-----+ // // // // This program can be used to study various phenomena: First of all, observe // // that x2 will produce a stream of boolean values that toggle (if that stream// // will be generated at all). Thus, x4 requires values from x1 in every even // // step. Thus, if x has values in other steps than these, the program will not// // be clock-consistent, and this is seen in that output driven execution of // // the When node will enforce clk(x2)=val(x2)=true while the negation assigns // // val(x2)=false, thus yielding a write conflict. // // On the other hand, using an input stream where x has values only at even // // points of time, we will see an underspecified behavior: Then, neither x1 // // nor x5, nor y, and neither x4 will then have values at these points of time// // and that leaves clk(x2) unknown. // // ************************************************************************** // import BasicNodes.*; macro val(x) = x.0; macro clk(x) = x.1; module Signal03(event(int* bool) ?x,event ?clk_y,event int !val_y) { event(int * bool) x1,x4,x5; event(bool * bool) x2,x3; CpyIn(x,x1); || BufBool(x3,x2,true); || Not(x2,x3); || When(x1,x2,x4); || Add(x1,x4,x5); || CpyOut(clk(x5),clk_y,val(x5),val_y); || loop { // check clock consistency assert(clk(x) -> clk(x1)); assert(clk(x3) <-> clk(x2)); assert(clk(x4) <-> (clk(x1) & clk(x2) & val(x2))); assert(clk(x5) <-> clk(x1)); assert(clk(x5) <-> clk(x4)); assert(clk_y -> clk(x5)); asp: pause; } } // ************************************************************************** // // This input trace is not clock consistent and will lead to val(x2)=⊤ in the // // second macro step of the Quartz program. // // ************************************************************************** // drivenby t1 { val(x) = 1; clk(x) = true; clk_y = true; pause; val(x) = 2; clk(x) = true; clk_y = true; pause; val(x) = 3; clk(x) = true; clk_y = true; pause; val(x) = 4; clk(x) = true; clk_y = true; pause; val(x) = 5; clk(x) = true; clk_y = true; } // ************************************************************************** // // This input trace is clock consistent, and could produce (in theory) values // // at every even point of time (with finite memory). However, clk(x2) will be // // unknown, since if neither clk(x1) nor clk(x4) holds, then clk(x2) is not // // determined (only by the mutually dependent assignments of Buf and Not). // // Thus, we have a lack of causality here. // // ************************************************************************** // drivenby t2 { val(x) = 1; clk(x) = true; clk_y = true; pause; clk(x) = false; clk_y = false; pause; val(x) = 3; clk(x) = true; clk_y = true; pause; clk(x) = false; clk_y = false; pause; val(x) = 5; clk(x) = true; clk_y = true; }