EE290N - Specification and Modeling of Reactive Real-Time Systems

Lecture 24 - November 21, 1996, Scribe: Alain Girault

Signal is a data-flow language (although not in the exact sense of Kahn's process networks). So the objects are flows, i.e., infinite sequences of values. They are called signals. Each signal has a clock which is the sequence of instants where the signal has a value. At any instant of its clock, a signal can be present and have a defined value, or be absent and have the value bot.

Signal is a declarative language. So signals are defined by equations that specify their properties. The order of the equations is irrelevant.

Signal is a synchronous language. So all the events (i.e., the values of all the signals) are totally ordered.

Signal is a relational language. So the way a signal is used can have consequences on the signal itself (actually on its clock).

Unlike in Lustre, there is no global clock. Instead, the notion of clock is local. For instance, the signals (1,2,3,4 ...) and (1,2,bot,3,bot,bot,4 ...) can be the same. Without any other information on their clock, they are the same.

If two signals have the same clock, then whenever one has a value, the other one must also have one, and when one has no value (i.e., a bot), the other one must also have a bot.

Delay operator: Y := U$1 which implies that Y and U have the same clock.

U : (1,2,bot, 3 ,4 ...)
Y : (x,1, 2 ,bot,3,4 ...)
where x is any value.
U : (1,2,3,bot,4 ...)
Y : (x,1,2,bot,3,4 ...)
Note that the bot is now between the 2 and the 3.

Initial value: Y$$0 defines 0 as the initial value of Y.

Down-sampling operator: Y := X when B, where B is a boolean flow. The signals X and B are not required to have the same clock. The value of Y is the value of X iff B is present and has value true, and is bot otherwise.

X : (1, 2 ,bot, 3 ,4,bot, 5 ,6 ...)
B : (t, f , t , f ,t, f ,bot,t ...)
Y : (1,bot,bot,bot,4,bot,bot,6 ...)
Deterministic merge: Y := U default V. The signals U and V are not required to have the same clock. The value of Y is the value of U iff U is present, the value of V iff U is absent and V is present, and otherwise bot. This merge is deterministic in the sense that when both U and V have a value, the value taken is always that of U.
U : ( 1 , 2 ,bot,3,4,bot,5,6,bot ...)
V : (bot,bot, 3 ,4,7,bot,8,9, 3  ...)
Y : ( 1 , 2 , 3 ,3,4,bot,5,6, 3  ...)
Assertions about clocks: X ^= Y constraints the clock of X to be the same as the clock of Y. X ^< Y constraints the clock of X to be less frequent than the clock of Y.

Example of a memory cell: Inputs are X (value to be memorized) and B (request for reading the memory cell). Output is Y.

Y := X default (Y$1);
Y$$0;
Y ^= X default (B when B);
Example of clock inconsistency:
X := A when (A > 0);
Y := A when (A <= 0);
X := X + Y;
This is illegal since the addition of X and Y constraints them to have the same clock, which is false from their definition.

Clock calculus: For a signal Y, we note y its clock. Clocks are sequences of values belonging to GF(3), the Galois Field of three elements. GF(3) = {-1,0,1}. Arithmetic inside GF(3) is the modulo arithmetic:

 0 +  0 =  0
 0 +  1 =  1 + 0 =  1
 0 + -1 = -1 + 0 = -1
 1 +  1 = -1
 1 + -1 = -1 + 1 =  0
-1 + -1 =  1
Subtraction is similar, and multiplication is standard. The meaning of these three values is:
-1 : present and false
 0 : absent
 1 : present and true
Then the clock equations derived from the signal equations are
Y := U + V        =>  y2 = u2 = v2
Y := U when B     =>  y = x(-b -b2)
Y := U default V  =>  y = u + v(1 - u2)      for booleans
                  =>  y2 = u2 + v2(1 - u2)    for non booleans
Y := X$1          =>  y2 = x2
                  =>  sn+1 = (1 - x2)sn + x   where sn is the dynamic state of the delay
When applying the clock calculus to the example above, we find an equation system whose only solution implies that there are no events at all!