// ************************************************************************** // // // // 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 |------->| | x4 +--------+ // // +-------+ | Add |----| CpyOut |---> y // // +->| | +--------+ // // +-----+ x3 | +-----+ // // +->| Buf |---o---+ // // | +-----+ | // // x2 | | // // | +-----+ | // // +--| Inc |<--+ // // +-----+ // // // // Note here that the mutual recursive definition of x2 and x3 alone would not// // have a reason to compute anything at all. However, the definition of Add is// // made such that the clock tick of one input also demands a clock tick of the// // other one, and that also a clock tick of the output stream demands clock // // ticks of the argument streams. // // ************************************************************************** // import BasicNodes.*; macro val(x) = x.0; macro clk(x) = x.1; module Signal01(event(int* bool) ?x,event ?clk_y,event int !val_y) { event(int * bool) x1,x2,x3,x4; CpyIn(x,x1); || Buf(x2,x3,0); || Inc(x3,x2); || Add(x1,x3,x4); || CpyOut(clk(x4),clk_y,val(x4),val_y); || loop { // check clock consistency assert(clk(x1) <-> clk(x3)); assert(clk(x1) <-> clk(x4)); assert(clk(x3) <-> clk(x2)); assert(clk(x4) <-> clk_y); pause; } } // ************************************************************************** // // The input driver below produces the following trace: // // // // -------------------------------------------- // // step : 0 1 2 3 4 // // -------------------------------------------- // // x.0 : 0 0 0 4 6 // // x.1 : True False False True True // // x1.0 : 0 0 0 4 6 // // x1.1 : True True True True True // // x2.0 : 1 2 3 4 5 // // x2.1 : True True True True True // // x3.0 : 0 1 2 3 4 // // x3.1 : True True True True True // // x4.0 : 0 1 2 7 10 // // x4.1 : True True True True True // // val_y : 0 1 2 7 10 // // clk_y : True True True True True // // // // ************************************************************************** // drivenby { val(x) = 0; clk(x) = true; clk_y = true; pause; clk(x) = false; clk_y = true; pause; clk(x) = false; clk_y = true; pause; val(x) = 4; clk(x) = true; clk_y = true; pause; val(x) = 6; clk(x) = true; clk_y = true; }