An Implementation of Constructive Synchronous Programs in POLIS.
Design tools for embedded reactive systems commonly use a model of computation that employs both synchronous and asynchronous communication styles. We form a junction between these two with an implementation of synchronous languages and circuits (Esterel) on asynchronous networks (POLIS). We implement fact propagation, the key concept of synchronous constructive semantics, on an asynchronous non-deterministic network: POLIS nodes (CFSMs) save state locally to deduce facts, and the network globally propagates facts between them. The result is a correct implementation of the synchronous input/output behavior of the program. Our model is compositional, and thus permits implementations at various levels of granularity from one CFSM per circuit gate to one CFSM per circuit. This allows one to explore various tradeoffs between synchronous and asynchronous implementations.
Introduction
Our purpose is to reduce the gap between two distinct models of concurrency that are fundamental
in the embedded systems framework, the synchronous and asynchronous models, with
application to systems written in the Esterel synchronous programming language and implemented
in the POLIS system developed at UC Berkeley and Cadence.
The synchronous or zero-delay model is used in circuit design and in synchronous programming
languages such as Esterel [6], Lustre [12], Signal [10], and SyncCharts [2] (a synchronous
version of Statecharts [13]), see [11] for a global overview. In this model, all bookkeeping actions
such as control transmission and signal broadcasting are conceptually performed in zero-
time, only explicit delays taking time. Thus, a conceptual global clock controls precisely when
statements simultaneously compute and exchange messages. The model makes it possible to
base design on deterministic concurrency, which is much easier to deal with than classical non-deterministic
concurrency. Compiling, optimizing, and verifying programs is done using powerful
Boolean computation techniques, see [5].
The synchronous model is well-suited for direct speci-cation and implementation of comparatively
compact programs such as protocols, controllers, human-machine interface drivers,
and glue logic. In this case, one can build a global clock slow enough to react to each possible
environmental input.
In an asynchronous model, processes exchange information through messages with non-zero
travel time. Asynchronous models are well-suited for network-based distributed systems speci-
-cation and for hardware/software codesign, where the relative speed of components may vary
This work was begun while the -rst author was visiting Cadence Berkeley Laboratories, August 1998.
widely. There are many asynchronous formalisms with varied communication policies. For ex-
ample, CSP processes [14] communicate by rendezvous, while data-AEow processes [15] exchange
data through queues or buoeers.
The POLIS [3] mixed synchronous/asynchronous model has been developed at UC Berkeley
and Cadence, with primary focus on codesign. It is a Globally Asynchronous Locally Synchronous
(GALS) model, in which synchronous nodes called CFSMs (Codesign Finite State
Machines) are arranged in an asynchronous network and communicate using non-blocking 1-
place buoeers, and through a synthesized real-time operating system (RTOS) for the software
part. The CFSMs can be programmed in a concurrent synchronous language such as Esterel,
thus taking maximal advantage of the synchronous model at the node level. The model can be
eOEciently simulated and implemented in hardware and/or software; notice that 1-place buoeers
are much simpler to implement than FIFOs, especially at the hardware/software boundaries.
However, POLIS networks have much less intrinsic semantic safety than FIFO-based dataAEow
Kahn networks [15], which are behaviorally deterministic, and their behavior must be carefully
controlled. In particular, buoeer overwriting in POLIS can lead to non-deterministic behaviors
that can be hard to analyze and prove correct.
Here, we show that the behavior of a synchronous circuit or program can be nicely implemented
in a POLIS network. Of course, one can implement a synchronous program in a single
CFSM node in a straightforward way. Here, we are interested in distributed implementations
where the synchronous behavior is split between asynchronously communicating units, without
a global clock. In practice, this is useful when the application behavior is naturally synchronous
but the execution architecture is distributed and possibly heterogeneous, with physical inputs
and outputs linked to dioeerent computing units. We retain the synchronous philosophy when
specifying an application and we bene-t from the AEexibility and eOEciency of CFSM networks
in the implementation. We propose a solution in which the CFSM granularity can be chosen at
will: any part of the synchronous program can be implemented in a single synchronous CFSM,
which makes it possible to partition the program according to the architecture constraints and
the best synchrony/asynchrony compromise.
Other authors have proposed such distributed implementations of synchronous programs on
asynchronous networks, see for example [9, 8], and we draw much from their work. However, our
implementation takes maximal advantage of the semantics of the objects we deal with and it is
presented dioeerently, with a trivial correctness proof. Technically speaking, we present a POLIS
implementation of constructive synchronous circuits [5, 18], which is a class of well-behaved cyclic
circuits that generalizes the usual class of acyclic circuits. Since Esterel programs are translated
into constructive circuits [4], this implementation handles Esterel as well.
The key of any implementation of synchronous programs is the realization of a conceptual
zero-delay reaction to an input assignment. In a distributed asynchronous network, this must
be done by a series of message exchanges. In our implementation, the messages are CFSM-
events that carry proven facts about synchronous circuit wire or expression values. Such facts
are exactly the logical information quanta on which the constructive semantics are based. The
CFSM nodes generate output facts from input facts according to the semantic deduction rules.
This is done over a series of computations since conceptually simultaneous facts now arrive at
dioeerent times.
For a single reaction of a program, the number of events is uniformly bounded. No buoeer
overwrite can occur in the network. Although the internal behavior is non-deterministic, the
overall behavior respects the synchronous semantics of the original program and thus is de-
terministic. This is true independently of the schedule employed by the RTOS. In addition,
execution of successive synchronous reactions can be pipelined.
Finally, the implementation takes full advantage of the mathematical properties of the constructive
semantics. In particular, the compositionality property makes it possible to arbitrarily
group elementary circuit gates into CFSM nodes: this allows any level of granularity, from one
single CFSM for the program at one extreme to one CFSM per individual gate at the other.
Clearly, there are many applications for which using only the synchronous formalism at spec-
i-cation level makes no sense, in which case our results are not directly applicable. Nevertheless,
we think that they show that the apparent distance between synchrony and (controlled) asyn-
IJYXFigure

1: Circuit C 1
chrony can be reduced, and we hope that the technology we present can serve as a basis for
future mixed-mode language developments.
We start in Section 2, by presenting the logical, semantical, and electrical views of constructive
circuits. In Section 3, we brieAEy present the POLIS CFSM network model of computation. Our
implementation of constructive circuits in this model is presented in Section 4, We discuss possible
applications and synchrony/asynchrony tradeooes in Section 5, and we conclude in Section 6.
Constructive Circuits
Constructive circuits are iwell-behavedj possibly cyclic circuits that generalize the class of acyclic
circuits. Acyclic circuits can be viewed in two dioeerent ways:
ffl as Boolean equation systems, then de-ning a Boolean function that associates an output
value assignment with each input value assignment.
ffl as electrical devices made of wires and gates that propagate voltages and have certain
delays: if the inputs are kept electrically stable long enough to one of two binary voltages
(say 0V and 3V), the outputs stabilize to one of the binary voltages.
Relating the Boolean and electrical approaches is easy for acyclic circuits: when the outputs electrically
stabilize, they take the voltages corresponding to the results of the Boolean input/output
function. Constructive circuits have exactly the same characteristics even in the presence of cycles

2.1 The Behavior of Cyclic Circuits
A circuit has input, output, and internal wires; the latter we also call local variables. In our
examples, we use the letters I ; J for the inputs and X;Y for the outputs and locals, making it
precise which are the outputs where necessary. Each output or local variable is de-ned by an
equation is an expression built using variables and the operators : (negation),
- (conjunction), an - (disjunction). For simplicity, we assume that an expression E is either a
variable, the negation of a variable, or a single n-ary operator - or - applied to variables or the
negation of variables. Any circuit can be put into this form by adding enough auxiliary variables.
A circuit can also be considered as a network of gates, as pictured in Figure 1. Each wire
has a single source and multiple targets. The gates correspond to the operators.
As a running example, we shall consider the following circuit C 1
, with outputs X and Y :
ae
Notice that C 1 is cyclic: Y appears in the equation of X and conversely.
2.1.1 Circuits as Boolean Equations
In the Boolean view, we try to solve the circuit equations using Boolean values 0 and 1. An
input assignment i associates 0 or 1 with some input variables. An input assignment is complete
if it associates a value with any input variable. For a complete assignment i, A Boolean solution
of the circuit is an assignment of values 0 or 1 to the other variables that satis-es the equations.
An acyclic circuit has exactly one Boolean solution for each complete input assignment. A
cyclic circuit may have zero, one or several solutions for a given complete input assignment. For
example, consider the case where there is no input and one output X . For there is no
solution. For there is a unique solution there are two solutions
For
, there is a unique solution if The solution is
the equations reduce to
and there are two solutions,
2.1.2 Circuits as Electrical Devices
In the electrical view, one preferably uses the graphical presentation and vocabulary. Wires
associated with variables carry two dioeerent voltages, also called 0 and 1 for simplicity, and
logic gates implement the Boolean operators. Wires and gates can have propagation delays.
We shall not be very accurate here about delays; technically, the delay model we refer to is the
up-bounded inertial delay model described in [7, 17]. A complete input assignment is realized
by keeping the input wires stable over time at the appropriate voltages. Voltages propagate in
the circuit wires according to the laws of electricity, and the property we are interested in is
wire voltage stabilization after a bounded time. The non-input wires are assumed to be initially
unstable.
Outputs of acyclic circuits always stabilize. Outputs of cyclic circuits may or may not stabi-
lize. For example, the output of stabilizes, while that of
0 and 1. The output of remains unstable. When wires stabilize, their values always
satisfy the equations.
Stabilization may depend on delays. For example, in the Hamlet circuit 1 de-ned by
, the output X stabilizes to 1 for some delays and does not stabilize for others, see [5].
Stabilization may also depend on the input assignment: for C 1
, outputs stabilize to the right
Boolean values unless I in which the behavior is delay-dependent, with no stabilization
for some delays.
2.2 Constructive Boolean Logic
Notice that the perfect match between Boolean and electrical solution is lost for cyclic circuits:
for Hamlet, the Boolean output function is well-de-ned and yields
electrical stabilization may not occur. Hamlet has a unique Boolean solution because 1 happens
to be a solution while 0 is not. Finding the solution involves propagating non-causal information
and this cannot be done by non-soothsaying electrons in wires. Fortunately, Boolean logic can
be weakened into constructive Boolean logic, in which the solution to Hamlet is rejected,
thereby rendering the Boolean and electrical results the same: no solution exists. Constructive
Boolean Logic precisely models electrical behavior.
2.2.1 Facts and Proofs
Constructive Boolean logic deals with facts and proofs. A fact has the form
where E is a Boolean expression. An input fact is I = 0 or I = 1 for an input variable I . An
input assignment i is a set of input facts. Facts are deduced from other facts by deduction rules.
There are deduction rules for each type of gate and one rule to handle equations. Here are the
rules for the - conjunction operator:
1 Think of X as to be.
(l-and)
(r-and)
(b-and)
The facts above the horizontal bar are the premises and the fact below the bar is the conclusion.
Rule (b-and) reads as follows: from the facts 1. The rules
for - (or-gate) are dual. The rules for negation are:
Notice that X - Y behaves as :(:X - :Y ), just as in classical Boolean logic. The rules for a
circuit equation are
where b can be either 0 or 1.
A proof is a sequence of facts that starts by the facts of an input assignment and such that
any other fact can be deduced from the previous facts using a rule. The following consistency
lemma shows the soundness of the proof system. It is easily shown by induction on the length
of the proof.
Lemma 1 If there exists a proof of a fact 1), then there is no proof of
2.2.2 Proof Examples
We give some proof examples for C 1
. We present them in annotated proof form, writing at each
step the deduced fact, the premises, and the applied deduction rule. Here is an annotated proof
for
with complete input assignment I = 0;
from (1) by (l-and)
from (2) and (5) by (b-and)
Here is the dual proof
for
from (1) by (l-and)
from (2) and (5) by (b-and)
Notice that the deduction ordering is X -rst, Y next in P 01
, while it is the reverse ordering Y
-rst, X next in P 10
. This is the main dioeerence between acyclic and constructive circuits: in
acyclic circuits, one can -nd a data-independent variable ordering valid for all input assignments.
In constructive circuits, such an ordering exists for each input assignment, but it may be data-dependent

2.2.3 Example of Non-Provable Circuits
The circuits are both rejected as having no output proof, and for the very
same reason: there is no way to start a proof. Notice that the existence or non-existence of a
Boolean solution is not relevant. The circuit for example, has two Boolean solutions:
1. However, to verify either solution one would have to -rst make an assumption
about the solution, and then verify the validity of the assumption. Constructive proofs must
only propagate facts; they are not allowed to make assumptions
Constructive Boolean logic rejects the Hamlet circuit which no output fact
can be proven. As above, there is no way to start a proof without making an assumption. The
law of excluded middle X - does not hold in constructive logic, unless X has already
been proved to be 0 or 1.
2.2.4 Output Proofs and Complete Proofs
An output proof is a proof that proves a fact for each output variable. A complete proof is a
proof that proves a fact for each variable. A circuit is output constructive w.r.t. a complete input
assignment i if there is an output proof starting with the facts in i. The circuit is completely
constructive w.r.t. i if there is a complete proof starting with the facts in i.
The dioeerence is that no fact is needed for an intermediate variable in an output proof if
this variable is not needed to prove the output facts. It is even allowed that no fact about this
variable can be proved. Consider for example only X is an output. If
no fact for Y can be proved. The circuit is output constructive but not
completely constructive for this input assignment.
Although output constructiveness seems more general, we shall deal with complete construc-
tiveness in the sequel since it is much easier to handle. Complete constructiveness is also required
by the semantics of Esterel [4].
2.2.5 Constructive Logic Matches Delay Independence
Constructive Boolean logic exactly represents delay independence: given a complete input as-
signment, a circuit electrically stabilizes its output wires (resp. all its wires) for any gate and
wire delays if and only if it is output constructive (resp. completely constructive). This fundamental
result is shown in [18, 17] using techniques originally developed for asynchronous circuit
analysis [7].
Notice that a given fact can have several proofs. Delay assignments actually select proofs.
Consider is the output. For there are two
proofs of 0: the -rst one deduces the second one deduces the same fact
from deduced from Electrically speaking, the -rst proof occurs
when propagates through X's and gate before while the second proof occurs if
there is a long delay on the I input wire, long enough for to propagate through X's and
gate before I = 0.
2.3 Scott's Fixpoint Semantics
The classical model of Boolean logic is binary, variables taking values in 1g. Constructive
Boolean logic has a natural ternary semantic model.
2.3.1 The Ternary Model
The ternary domain is 1g. The unde-ned value ? (read bottom) represents absence or
non-provability of information. The domain is partially ordered by Scott's information ordering
the total values 0 and 1 being incomparable 2 . Tuples
are partially
ordered componentwise: x - y ioe x k - y k for all k. Functions are required to be monotonic
must have f(x) - f(y) in B n
? . A
composition of monotonic functions is monotonic. Functions are partially ordered by f - g if
2.3.2 The Fixpoint Theorem
The key result in Scott's semantics is the -xpoint theorem, which we state here in a simple case.
? be monotonic, and let a -xpoint of f be an element x of B n
? such that
x. The theorem states that f has a least -xpoint lfp(f), which is the (-nite) limit of the
increasing sequence
The function lfp that associates the least -xpoint lfp(f) with f is itself monotonic.
2.3.3 The Basic Ternary Operators
The Boolean operators are extended as follows to the ternary logic. There is no choice for
negation, which must be monotonically de-ned by
-, we choose the parallel extension, which is the least monotone function such that
closely corresponds to electrical gate behavior and to our proof rules. The
extension of disjunction - is dual.
Other possible extensions of - are the strict extension such that 0 -
the left sequential extension such that and the symmetrical right
sequential extension. They are de-nable from the parallel extension in constructive logic (hint:
the expression X-:X has value 1 if and only if X is de-ned).See [16, 1] for a complete discussion
of these extensions. It is interesting to note that the parallel extension cannot be de-ned in
sequential languages such as C and requires a parallel interpretation mechanism, hence its name.
2.3.4 Circuits as Fixpoint Operators
A circuit with input vector
? and other variables in vector x
? de-nes an equation
of the form where the k-th component of f is given by the right-hand-side of the
equation for x k . Given an input assignment i, let us write f i
from B n
? to itself. We call a solution of the circuit w.r.t. i the least -xpoint lfp(f i ) of f i . For
example, in circuit C 1 , the least -xpoint for input I = 0; while the least
-xpoint for
The next theorem shows that the constructively deducible facts exactly correspond to the
-xpoint solution.
Theorem 1 Given a circuit C de-ning a function f and an input assignment i, a fact
constructively provable if and only if the X-component of the least -xpoint of f i
has value b.
Unfortunately, some authors use f0; to mean the same thing!
The proof is standard and left to the reader (use inductions on term size and proof length).
Notice that the theorem does not require the input assignment to be complete. It is also
valid when some inputs are ?. Then, no fact for these inputs can be used in deductions.
This concludes the theory of constructive circuits: electrically stabilizing in a delay-independent
way is the same as being provable in constructive Boolean logic or as having a non-? value in
the least -xpoint.
2.4 Algorithms for Circuit Constructiveness
There are algorithms to detect whether a circuit is constructive for a given input assignment
or for all complete input assignments. Here, we present a linear-time algorithm that works
for one complete input assignment. It is used in the Esterel v5 compiler, for interpretation
mode (option -I). Algorithms checking constructiveness for all inputs or for some input classes
are much more complex. The BDD-based algorithm used in the Esterel v5 compiler (option
-causal) is presented in [18, 17, 19]. It will not be considered here.
2.4.1 An Interpretation Algorithm
The running data structure of the algorithm is composed of two sets of facts called
and TODO and of an array PRED of integer values indexed by non-input variable names.
The TODO set initially contains the input facts, and the DONE set is initially empty. The
array entry PRED[X ] is initialized to the number of predecessors of X , which is the number of
variable occurrences in the de-nition equation of X , also called the fanin number in the electrical
presentation.
The algorithm successively takes a fact from TODO, puts it in DONE, and propagates its
constructive consequences, which may add new facts to TODO and decrement the predecessor
counts. Propagating the consequences of a fact works as follows:
ffl All variables that refer to V in their de-nition decrement their predecessor count according
to the number of occurrences of V in their de-nition.
immediately determines that then that fact is added to TODO. This occurs
de-ned by a conjunction where V appears positively, in which case
or by a disjunction where V appears negatively, in which case (symmetrically if
1). This fact propagation rule corresponds to deduction rules such as (l-and) and
(r-and ), possibly combined with (not-0 ) and (not-1 ).
ffl If the predecessor count of a variable W falls to 0 and the value of W is not yet determined,
a new fact is added to TODO, where c is the identity of the de-nition operator of
W , i.e. 1 for - and 0 for -. This corresponds to rules such as (b-and ).
2.4.2 Execution Example
For
with inputs I = 0; we start in the following state:
We remove I = 0 from TODO and put it in DONE. We decrement the predecessor count of X .
immediately implies we add that fact to TODO:
We now process 1. The only consequence is that the number of predecessors of Y is
decremented, since does not determine Y by itself:
We now process This fact does not directly determine the value of Y , but it exhausts its
predecessor list:
We can now deduce that the value of Y is 1 since Y is an empty conjunction. We add this fact
to TODO:
We have computed all the facts we need. However, it is useful to perform the last step, which will
bring us back to a nice clean state. Processing puts this fact in DONE and decrements
X's predecessor count:
Since we build proofs, the result of the algorithm does not depend on the order in which we pick
facts in TODO.
For the input I = 0; here is a run where the output values are computed faster but
cleanup is longer:
For the non-constructive input I = rapidly reach a deadlock:
There are no remaining facts in TODO, and yet no fact has been established for X or Y and
their predecessor counts are positive.
The following result shows that our algorithm is correct and complete:
Theorem 2 Let C be a circuit with n variables and i be a complete input assignment. The
circuit is output constructive w.r.t. i if and only if the algorithm starts with i and computes a
fact for each output variable. The circuit is completely constructive w.r.t. I if and only if the
algorithm terminates with all predecessor counts 0.
For a completely constructive circuit, the algorithm always takes the same number of steps,
which is the sum of all the fanin counts.
3 POLIS and the CFSM model
Recall our goal is to implement synchronous circuits within the POLIS system. POLIS [3]
is a software tool developed at UC Berkeley for the synthesis of control-dominated reactive
systems that are targeted for mixed hardware/software implementations. The primary feature of
POLIS is its underlying CFSM model of computation; it is within this model that we implement
synchronous circuits.
3.1

Overview

The model of computation consists of a network of communicating Codesign Finite State Machines
(CFSMs). The communication style is called GALS: globally asynchronous locally syn-
chronous. At the node level, each CFSM has synchronous semantics: when run, a CFSM reads
inputs, computes, and writes outputs instantaneously. At the network level, the CFSMs communicate
asynchronously: communication is done via data transmission through buoeers, and no
assumptions are made about the relative delays of the computations performed by each CFSM
or about the delays of the data transmission.
3.2 CFSM Communication
Each CFSM has a set of inputs and outputs, and CFSMs are connected with nets. A net
associates an output of one CFSM to some inputs of other CFSMs. The information transmitted
between CFSMs is composed of a status and a value which are stored in 1-place communication
buoeers. For each net, there is one associated value buoeer and multiple status buoeers, one for
each attached CFSM input. Thus, each CFSM has a local copy of the status of each of its inputs,
while the value is stored in a shared buoeer. A CFSM input buoeer is composed of the local status
buoeer and the shared value buoeer. 3 The status buoeer stores either 1 or 0, representing presence
or absence of valid data in the value buoeer.
A CFSM input assignment is the set of values stored in the input buoeers for a CFSM. It
is equivalent to the circuit input assignment given in Section 2.1.1. A CFSM input assignment
may be complete or partial. A captured input assignment corresponds to the statuses and values
that are actually read from the buoeers when a CFSM in run.
3.3 CFSM Computation
A CFSM computation is called a CFSM execution or CFSM run. When a CFSM executes, it
reads its inputs, makes its computation, writes its outputs, and resets (consumes) its inputs.
Input reading: A CFSM atomically reads and resets the status buoeers: it simultaneously
reads all status buoeers and sets them to 0, ready for the arrival of new inputs. 4
It subsequently reads the values of the present inputs. This determines the captured input
assignment.
Computation: The CFSM uses the captured input assignment to make its computation: it
computes its outputs and next states based on the values given in its state transition table. The
computation is done synchronously, which means that the CFSM reacts precisely to the captured
input assignment, regardless of whether the inputs change while the CFSM is computing.
Output writing: For each output, a CFSM writes the value buoeer and subsequently atomically
sets the status buoeers for each associated CFSM input. 5
A CFSM-event consists of an output emitting its data and the corresponding input status
buoeers being set to 1.
3.4 CFSM Network Computation
A network computation is called a network execution or network run and corresponds to several
CFSM executions.
Each CFSM network has an associated scheduler(s). The scheduler continuously reads the
current input assignments, determines which CFSMs are runnable, and chooses the order in
3 Note that in [3], the word event is used both for the status alone and for the status/value pair.
In POLIS, a CFSM may have an empty execution, which means that it does not react to its current inputs.
In this case, the current inputs are saved, and any inputs that are received while the CFSM is determining its
empty reaction are added to the input assignment, which is restored and thus read at the next run. We do not
use this feature here.
5 Atomic reads and writes are more expensive, since they require an implementation that guarantees that these
actions can happen simultaneously. The decision was made in POLIS to make status buoeer reading and writing
atomic, and not value-buoeer reading and writing, because atomically reading and writing of short bit strings can
be implemented eOEciently, and because this guarantees certain desirable behavioral properties in the system.
which to run them. 6 A CFSM is runnable if it has at least one input status buoeer set to 1. A
CFSM is run by the scheduler sometime after it is runnable.
Typically, an input assignment is given to the network, and the scheduler runs the CFSMs
according to its schedule until there are no further changes in the communication buoeers. This
is called a complete network execution.
Time eoeectively passes when control is returned to the scheduler, and thus instantaneous
communication between CFSM modules is not possible.
Implementing Constructive Circuits in CFSM Networks
In this section, we explain our realization of the synchronous behavior of a circuit on a CFSM
network. To facilitate the exposition, we restrict ourselves to the extreme case of one CFSM per
gate. More realistic levels of granularity will be handled in Section 5.
In Section 2.4, we presented an algorithm to compute the behavior of a circuit for a given
circuit input assignment. The essential ingredients were a set TODO of facts to propagate, a
set DONE of established facts, and a predecessor counter for each variable. The basic idea of
the CFSM network implementation presented here is to distribute a similar algorithm over a
network of CFSMs, associating a CFSM with each circuit gate (equation).
We start by studying the reaction to a single input assignment and then present various ways
of chaining reactions to handle circuit input assignment sequences, to obtain the cyclic behavior
characteristic of synchronous systems.
4.1 Fact propagation in a CFSM network
We implement each gate as a CFSM that reads and write facts, which are encoded in POLIS
CFSM-events sent by one gate to its fanouts. The arrival of a fact at a gate makes the gate
runnable, and, when run, if there is a provable output fact from the facts received so far, the
gate CFSM outputs it. Fact propagation between gates is directly performed by the underlying
POLIS scheduling and CFSM-event broadcasting mechanisms. A POLIS execution schedule is
thus precisely a proof (fact propagation) ordering.
Facts arrive sequentially at a gate CFSM. Therefore, a combinational circuit gate must be
implemented by a sequential CFSM that remembers which facts it has received so far. The sequential
state of a gate CFSM encodes the number of predecessors of the interpretation algorithm
of Section 2.4.
4.2 The Basic Gate CFSM
For ease of exposition, we write the gate CFSMs in Esterel. This makes the gate speci-cation
very AEexible, which will be useful in the next sections. No preliminary knowledge of Esterel is
required.
To handle our running example
, it suOEces to describe the AndNot gate
Other gates are similar. The Esterel program for AndNot has the following interface:
module AndNot :
Here, A, B, and C are Esterel signals of type boolean, the values of which are called true and
false. Esterel signals are just like POLIS buoeers, with some additional notation. An event of a
boolean-valued signal such as A has two components: a binary presence status component, also
written A, which can take values present and absent , and a value component of type boolean,
written ?A. We choose to encode the fact present with value true (resp.
6 In POLIS, scheduler is automatically synthesized with parameters, such as the type of scheduling algorithm,
given by the user.
false) 7 . Notice that we use two pieces of information, the status and the value, to represent a
fact, i.e. the stable value of a wire. A present status component indicates stability, i.e. that a
fact has been propagated to this point, and the value component represents the Boolean value
of the fact.
Like a POLIS captured input assignment, An Esterel input assignment de-nes the presence
status of each input signal and the value of each present signal. For instance, for AndNot,
A(true).B(false) is an Esterel input assignment in which A is present with value true and B
is present with value false, encoding the facts is an input
assignment where A is present with value false and B is absent, encoding the fact
Like a CFSM, an Esterel program repeatedly reacts to an externally provided input assignment
by generating an output assignment. The processing of an input assignment is also called
a reaction or an instant. In POLIS, a run of an Esterel CFSM triggers exactly one reaction of
the Esterel program, with the same input assignment.
Unlike in POLIS, communication in Esterel is instantaneous: a signal emitted by a statement
is instantaneously received by all the statements that listen to it. Similarly, control propagation
is instantaneous; for example, in a sequence 'p; q', q immediately starts when p terminates. The
only statements that break the AEow of control are explicit delays such as iawait Sj that waits
for the next occurrence of a signal S.
Finally, in Esterel, signal presence status is not memorized from reaction to reaction, but
value is : the value of the Esterel expression ?A of A in a reaction where A is absent is the one it
had in the previous reaction. Notice that the value of a signal may change only when the signal
is present.
Our -rst attempt to write the Esterel body of AndNot is:
await A;
if not ?A then emit C(false) end if
if ?B then emit C(false) end if
if (?A and not ?B) then emit C(true) end if
The program reads as follows. First, we start two parallel threads. The -rst thread waits for
the presence of A, and the second threads waits for the presence of B. The -rst input assignment
can have A present, B present, or both (an empty assignment with neither A nor B present would
leave the program in the same state; such an assignment is permitted in Esterel but will never
be generated by the POLIS scheduler). If A is absent, the -rst thread continues waiting. If A
is present, the -rst thread immediately checks A's value ?A and immediately outputs C(false)
if ?A is false, thus mimicking the (l-and) deduction rule; the thread terminates immediately in
either case. The second thread behaves symmetrically but checks for the truth of ?B to emit
C(false). If both A and B are present, the threads evolve simultaneously.
The Esterel parallel construct '-' terminates immediately when both branches have termi-
nated. Therefore, the above parallel statement terminates exactly when both A and B have been
received, either simultaneously or in successive input assignments. In that instant, C(true) is
emitted if the possibly memorized values ?A and ?B are respectively true and false, mimicking
the (b-and) deduction rule with negated second argument.
4.2.1 Avoiding Double Output
Our gate CFSM almost works, but not quite, since C(false) can be emitted twice (possibly at
dioeerent instants) if ?A is false and ?B is true. The gate should output C only once. To correct
this problem, we use an auxiliary Boolean signal Caux:
7 Other equivalent encodings can be considered. One can for example use a pair of pure signals for each
variable, one for presence and one for value. The encoding we use makes a clear dioeerence between availability
and value.
Sd

Figure

2: Partial state transition graph for module AndNot
signal Caux : combine boolean with and in
await A;
if not ?A then emit Caux(false) end if
if ?B then emit Caux(false) end if
if (?A and not ?B) then emit Caux(true) end if
await Caux;
emit C(?Caux)
signal
The -rst branch of the outermost parallel behaves as before but emits Caux instead of C. The
second branch waits for Caux to emit C with the same value, and immediately terminates. If Caux
is emitted twice in succession by the -rst branch, the second emission is simply unused since the
iawait Cauxj statement has already terminated. The icombine boolean with andj declaration
smoothly handles simultaneous double emission, also called collision. For this example, collision
occurs if A(false) and B(true) occur simultaneously, in which case both iemit C(false)j
statements are simultaneously executed. The combine declaration speci-es that the result value
?Caux is the conjunction of the separately emitted values. Here, we could as well use disjunction,
for only false values will be combined.
4.2.2 The Gate CFSM State Graph
The gate CFSM state transition graph (STG) is partially shown in Figure 2. The transitions are
shown for the cases in which A is received before B, the other cases (B arriving -rst or A and B
arriving simultaneously) are similar and not pictured. This partial STG is shown to help visualize
the sequential state traversal in a familiar syntax, but is not a practical input mechanism for
reactive modules compared to the Esterel language. For example, a module that waits for n
signals concurrently will have 2 n states, while the Esterel description has size n. Note also that
the C aux signal is shown in the output list for visualization purposes; it is an internal signal that
is not seen by any other module.
4.2.3 Gate CFSM Execution Example
To become familiar with the Esterel semantics, let us run the AndNot program on two dioeerent
input assignment sequences. We start in state S 0
where we are waiting for the inputs A and B
and internally for Caux, pictured by underlining the active await statements:
signal Caux : combine boolean with and in
await A;
if not ?A then emit Caux(false) end if
if ?B then emit Caux(false) end if
if (not ?A and ?B) then emit Caux(true) end if
await Caux
emit C(?Caux)
signal
Assume the -rst gate input assignment is A(true) and B absent. Then, iawait Aj terminates,
and we execute the test for inot ?Aj; since the test fails, the -rst parallel branch terminates
without emitting Caux. We then reach state S 1
, in which we continue waiting for B and Caux:
signal Caux : combine boolean with and in
await A;
if not ?A then emit Caux(false) end if
if ?B then emit Caux(false) end if
if (?A and not ?B) then emit Caux(true) end if
await Caux;
emit C(?Caux)
signal
If we now input B(false), we execute the ?B test, which also fails. Since the second parallel
branch terminates, the parallel statement terminates immediately; we execute the i?A and not ?Bj
test, which succeeds. We emit Caux(true), which makes the iawait Cauxj statement instantaneously
terminate; the output C(true) is emitted, since We reach the dead state
S d where no signal is awaited.
Assume now that the -rst gate input assignment is A(false) and B absent. Then, starting
from S 0
, we execute the -rst test, which succeeds and emits Caux(false). The iawait Cauxj
statement immediately terminates and C(false) is emitted. We continue waiting for B, in the
following
signal Caux : combine boolean with and in
await A;
if not ?A then emit Caux(false) end if
if ?B then emit Caux(false) end if
if (?A and not ?B) then emit Caux(true) end if
await Caux;
emit C(?Caux)
signal
Then, when B occurs in a later input assignment, the iawait Bj statement terminates and the
program reaches the dead state S d . If ?B is true, the emission of Caux(false) is performed but
unused. This last step of waiting for B mimics the last cleanup step of the propagation algorithm
of Section 2.4. It will be essential to chain cycles in Section 4.4.
If A and B occur together in the -rst input assignment, then AndNot immediately emits C
with the appropriate value and transitions directly from state S 0
to dead state S d .
Notice that the number of predecessor waited for in the algorithm of Section 2.4 is exactly
the number of underlined statements among iawait Aj and await Bj.
Scheduler
A
A
Y
I

Figure

3: CFSM network for circuit C 1
4.3 Performing a Single Reaction on a Network of Gates
Given a circuit C, the CFSM network for C is obtained by creating an input buoeer for each
input signal in C, an output buoeer for each output signal, and a gate CFSM for each equation
in C. Gate CFSM outputs are broadcast to the gate CFSMs that use them, as speci-ed by the
circuit equations.
To run the network for a given circuit input assignment i, it suOEces to put the input values
de-ned by i in each of the network input buoeers. Then, the gate CFSMs directly connected
to inputs become runnable. As soon as a gate has computed its result, it puts it in its output
buoeer, the result's value is automatically transferred to all fanout CFSM input buoeers by the
network, and these CFSMs become runnable.
4.3.1 An Execution Example
Consider the network for C 1 , pictured in Figure 3, where the CFSMs for X and Y are called
CX and CY. The rectangular buoeers are the 1-place buoeers used to communicate CFSM-events
between modules. Note that there are two information storage mechanisms at work during the
execution of this circuit:
1. The CFSM-gates as implemented by the Esterel modules internally store which signals
they have received and thus which they are still waiting for using their implicit states.
2. The CFSM-network as implemented in POLIS stores a copy of each CFSM-event, one for
each fanout of that event, using the 1-place buoeers.
Consider the input assignment I = 0 and -rst put false in I's buoeer and true in
J's buoeer. The CFSMs CX and CY become runnable. Assume CX is run -rst. Then it captures the
partial input assignment A(false) and B absent, which encodes I = 0. The CX CFSM outputs
C(false), which is the encoding for goes to state S 1
. The false event is made
visible at CY's B input buoeer after some time.
ffl Assume -rst that CY is run before the arrival of CX's output. Then CY captures the partial
input assignment A(true) and B absent, which encodes the fact 1. The CY CFSM
emits no output and continues waiting for its B input, in state S 2
. When X's false
value is written in CY's B input buoeer, CY is made runnable and runs with captured input
assignment A absent and B(false); it emits C(true), which encodes Y = 1, and goes to
the dead state.
ffl Assume instead that CX's false output is written in CY's input buoeer B before CY is run.
Then, when CY is later run, it captures the complete input assignment A(true):B(false),
which encodes the facts It emits C(true) and goes directly to the dead
state.
Once CY has emitted its output C(true), the true value is written in CX's input buoeer B, and
CX is made runnable again. Then, CX is run with input assignment B(true) and A absent, which
encodes goes to the dead state.
4.3.2 Correctness of the CFSM Implementation
The CFSM network computes a proof in the same way as the interpretation algorithm of Section
2.4, but with dynamic and concurrent scheduling of fact propagation. Building a new fact
is equivalent to generating a CFSM-event. Propagating a fact is equivalent to broadcasting the
CFSM-event to the fanouts and running the fanout CFSMs, which is exactly what the network
automatically provides.
The following theorem summarizes the results:
Theorem 3 Let C be a circuit. Let n be the number of output or local variables (fanouts), and
let f be the number of variable occurrences in the right-hand-sides of C's equations (fanins). Let
i be a circuit input assignment. For any run of the network associated with C initialized with i,
the following holds:
1. The number of created CFSM-events is bounded by n, and the number of CFSM runs is
bounded by f . No buoeer overwrite can occur.
2. If, in some complete network execution sequence, exactly n CFSM-events have been created,
then the implemented circuit is completely constructive w.r.t. i, and the output gate CFSM
generated events are the encodings of the output values of C w.r.t. i. All complete execution
sequences give the same result independent of the schedule, and all gate CFSMs terminate
in the dead state once all CFSM-events have been processed.
3. If, for some complete run, less than n CFSM-events have been created, then this is true
for all runs and C is not completely constructive w.r.t. i.
Output constructive circuits can be handled by a slight modi-cation of the result, but loosing
the nice fact that all gate CFSMs terminate in the dead state, which if useful when chaining
reactions, which we demonstrate in the next section.
4.4 Chaining Reactions
A synchronous circuit or program is meant to be used sequentially, the user or RTOS providing
a sequence of input assignments and reading a sequence of output assignments. In our POLIS
implementation, the user alternates writing circuit input assignments in the network input buoeers
and reading the computed circuit output assignments in the network output buoeers. Since POLIS
uses 1-place buoeers for communication, we must make sure that no buoeer overwrite occurs in the
network. In particular, we cannot let the user overwrite an input buoeer until its value has been
completely processed by the gates connected to it. Here are four possible user-level protocols:
ffl Wait for a given amount of time. This is the technique used for single-clocked electrical
circuits. Since the number of operations to be performed is uniformly bounded, if
the underlying machinery (CPUs, network, etc.) has predictable performance, we are

Figure

4: Circuit C 1
guaranteed that the reaction is complete after a maximal (predictable) time and that no
buoeer overwriting occurs. This solution is often used in cycled-based control systems implemented
in software and in Programmable Logic Controllers (PLCs). This protocol can
be realized in our implementation with the addition of performance estimation, in order
to compute the frequency with which new inputs can be fed to the synchronous circuit.
ffl Compute and return a termination signal. If the circuit is completely constructive w.r.t.
the input, we know that the computation has -nished when all the gate CFSMs have read
all their inputs, i.e. when the network has processed a given number of CFSM-events.
We can either modify the scheduler to have it report completion to the user or build an
explicit termination signal by having each gate output a separate CFSM-event when it has
processed all inputs. These CFSM-events are gathered by an auxiliary gate that generates
a termination event for the user when all its input have arrived. These centralized solutions
are not in the spirit of distributed systems.
ffl Implement a local AEow control protocol at each gate CFSM. This is a much more natural
solution in a distributed setting and it makes it possible to pipeline the execution: for each
input, the user may enter a new value as soon as the AEow-control protocol says so, without
waiting for the reaction to be complete. The protocol must ensure that an input for a
conceptual synchronous cycle never interferes with values for other cycles.
ffl Queue input events: this solution is used in [9, 8]. It implies that the user can always write
new inputs and is never blocked. In our implementation, the same AEow control problem is
simply pushed inside the network, since CFSMs do not communicate using queues.
We now present a AEow-control protocol that supports pipelining. The reactions remain globally
well-ordered as required by the synchronous model: the n-th value of input I is processed in the
same conceptual synchronous cycle as the n-th value of input J ; however, because of pipelining,
internal network CFSM scheduling and CFSM-event generation can occur in intricate orderings.
To make the gate reusable, is suOEces to embed their bodies into an Esterel iloop.endj
in-nite loop. Then, instead of going to the dead state, a gate CFSM returns to its initial state.
This is why it is much easier to handle complete proofs. To deal with more general output
proofs, we should add complicated gate reset mechanism, while reset is automatically performed
by complete proofs.
Thanks to the AEexibility of Esterel code, the protocol only requires a slight modi-cation of
our basic gate code, and the addition of a new module. The corresponding CFSM network is
shown in Figure 4.
Consider an output X of a CFSM M, read for example by two other CFSMs N and P. With
X and N (resp. P) we associate a signal X-Free-N (resp. X-Free-P) that is written by N (resp.
P). With X and M we associate a signal X-Free-M read by M and written by an auxiliary module
X-CFSM which consumes X-Free-N and X-Free-P and writes X-Free-M when both X-Free-N and
X-Free-P have received a value. The buoeers in Figure 4 for each signal are those used by POLIS;
the actual information determining when the signal X is free to be written by M is contained in
the implicit states of X-CFSM. The new module is written as follows:
module X-CFSM:
input X-Free-N, X-Free-P;
output X-Free-M;
loop
await X-Free-N
await X-Free-P
emit X-Free-M
loop
module
Similarly, for a network input I broadcast to N and P, we generate a network output buoeer
I-Free -lled by the auxiliary CFSM reading I-Free-N and I-Free-P, and for any network
output O a network input buoeer O-Free -lled by the user when it is ready to accept a new value
of O.
We require M to write its X output only when X-Free-M holds 0, then consuming that value.
We require N (resp. P) to write 0 in X-Free-N (resp. X-Free-P) when it reads its local copy of
the input X. The AndNot CFSM is modi-ed as follows:
module AndNot :
output A-Free, B-Free;
input C-Free;
loop
signal Caux : combine boolean with and in
await A;
emit A-Free;
if not ?A then emit Caux(false) end if
emit B-Free;
if ?B then emit Caux(false) end if
if (?A and not ?B) then emit Caux(true) end if
await Caux;
await C-Free
emit C(?Caux)
signal
loop
The output C is emitted only when the last of Caux and C-Free has been received.
When the gate CFSM is instantiated at a node M, the A-Free, B-Free, and C-Free buoeers
must be appropriately renamed A-Free-M, B-Free-M, and C-Free-M, to avoid name clashes.
The AEow-control mechanism acts in two ways. First, it prevents buoeer overwriting. Second,
it makes pipelining possible. Given a circuit input assignment i n at cycle n, the new value of a
circuit input I for cycle can be written in I's network input buoeer as soon as I-Free is
full. Therefore, it is not necessary to wait for the global end of a cycle to locally start a new one.
We have a last technical problem to solve. Assume that an AndNot gate CFSM starts circuit
cycle n. Assume that the gate CFSM receives an A input event, say A(false) with B absent.
The gate sends back A-Free. From then on, the gate can receive two inputs:
ffl The B input event that holds B's value in cycle n. This input should be processed normally
since the gate CFSM is currently processing cycle n.
ffl The out-of-order A input event that holds A's value for cycle n + 1. Processing this input
should be deferred until B has been processed.
In the current POLIS network model, a CFSM is made runnable as soon as it receives an input
event. Therefore, the gate can be made runnable with input A for cycle while it is still
processing cycle n. At this point, the gate should either internally memorize A's value or rewrite
it in the A buoeer, leaving in both cases the A-Free AEow control buoeer empty until it has -nished
cycle n. Both solutions are expensive and somewhat ugly.
We suggest a slight modi-cation to the POLIS scheduling policy. A CFSM should tell the
scheduler which input buoeers it is currently interested in, and the scheduler should not make the
CFSM runnable if none of these buoeers holds an event. When the CFSM is run, its captured
input assignment should only contain the events in the buoeers the CFSM is explicitly waiting for,
leaving the rest in their input buoeers. In the above example, the gate CFSM tells the scheduler
it is only waiting for B. If the new value of A comes in, the CFSM is not made runnable. When B
occurs, the gate is made runnable, and it will run with input B only. Once the gate has processed
B, it tells the scheduler that it is now waiting for both A and B. Since A is already there, the gate
can be immediately made runnable again.
The -nal version of the gate CFSM involves the auxiliary Wait signals sent to the scheduler
to implement this mechanism:
module AndNot :
output A-Free, B-Free;
output A-Wait, B-Wait;
input C-Free;
output C-Free-Wait;
loop
signal Caux : combine boolean with and in
abort
sustain A-Wait
when A;
emit A-Free;
if not ?A then emit Caux(false) end if
abort
sustain B-Wait
when B;
emit B-Free;
if ?B then emit Caux(false) end if
if (?A and not ?B) then emit Caux(true) end if
await Caux;
abort
sustain C-Free-Wait
when C-Free
emit C(?Caux)
signal
loop
The iAwait Aj statement has become iabort sustain A-Wait when Aj. The isustain A-Waitj
statement emits A-Wait in each clock cycle. the iabort p when Aj aborts its body p right away
when A occurs, not executing p at abortion time. Therefore, A-Wait is emitted until A is received,
that instant excluded.
5 Mixed Synchronous/Asynchronous Implementation
We now have two very dioeerent levels of granularity for implementing an Esterel program in
POLIS: compiling the program into a single CFSM node or building a separate CFSM for each
gate of the program circuit. The -rst does not support distribution, while the second is clearly too
ineOEcient: the associated overhead is unacceptable for large programs since it involves scheduling
each individual gate CFSM multiple times.
We now brieAEy explain how we can deal with many other implementation choices with dioeer-
ent levels of granularity, using the compositional and incremental character of the constructive
semantics. When doing so, we retain the full synchronous semantics of the program, but we
trade ooe synchrony and asynchrony in the implementation.
The idea as one moves to a larger granularity implementation is to partition the set of gates
into gate clusters G 1
Each cluster G k groups its gates into a single CFSM, the clusters
being connected by the POLIS network as before. The partition can be arbitrary, and chosen
to match any locality or performance constraints. Facts are processed both synchronously and
asynchronously, but again their proofs are derived from the synchronous constructive semantics.
In particular, synchronous fact processing is done within a cluster using the algorithm of Section
2.4, in a single CFSM and in one computation of that CFSM; asynchronous fact processing
is done across the network and thus between CFSMs. Some facts will be both synchronously
and asynchronously processed, e.g. an output from gate g 1
that is an input to another gate g 0in the same cluster G 1
and to g 2
in another cluster G 2
What makes this possible is the ability of our centralized and distributed algorithms to deal
with partial deduction: given a partial input assignment i, both algorithms generate all the facts
that can be deduced from i. If a new fact is added to i, the algorithms incrementally deduce its
consequences. Therefore, it does not matter whether facts are handled synchronously in a gate
cluster or asynchronously in the POLIS cluster network.
Consider for example the following circuit C 2
obtained by adding an output Z to C 1
Consider -rst the clusters G fZg. Assume that we receive the fact
deduces outputs that fact to G 2
, which can make a local transition to
reach the state S 1
where it waits only for Y
also internally remembers in its local state that
Y has lost a predecessor. Thus, synchronously propagated to Y in the same cluster,
and asynchronously propagated to Z in the other cluster through another call to a CFSM,. If we
now receive sends that fact to G 2 , which can now output
With the same input sequence, consider the clusters G g. When receiving
instantaneously generates the facts determined
synchronously. The fact asynchronously propagated to G 2 by the network, and G 2 's
CFSM transitions to a state where it waits only for J . When occurs, the CFSM outputs
that fact is propagated to G 1
's CFSM, which goes back to its initial state.
Optimal solutions to the problem of determining a set of clusters is beyond the scope of
this paper. A number of clustering algorithms exist in the literature, and the design may be
entered in a partitioned fashion that leads to a natural clustering as well. In our case, clustering
according to the source code module structure is an obvious candidate for a clustering
heuristic, as well as clustering according to the frequency of use of signals (like clocks in Lus-
tre). Here, we simply point out that our algorithms and the semantics behind them permit
any level of granularity: from individual gates implemented as separate CFSMs, to an entire
synchronous program implemented as a single CFSM. Thus, the tradeooe between synchronous
and asynchronous implementation of a synchronous program can be fully explored.
6 Conclusions and Future Work
We have described a method for implementing synchronous Esterel programs or circuits on
globally asynchronous locally synchronous (GALS) POLIS networks. The method is based on
fact propagation algorithms that directly implement the constructive semantics of synchronous
programs. We have developed AEow-control techniques that automatically ensure that no POLIS
buoeer can be overwritten and that make pipelining possible.
Initially, we have associated a POLIS CFSM with each circuit gate, which is unrealistic in
practice. However, our method is fully compositional, and fact propagation can be performed
either synchronously in a node or asynchronously between nodes. This makes it possible to
cluster gates into bigger synchronous nodes and to explore the tradeooe between synchronous
and asynchronous implementation.
For simplicity, we have only dealt with the pure fragment of Esterel where signals carry
no value. Extension to full value-passing Esterel constructs raises no particular diOEculty. A
complete implementation is currently being developed.



--R

Domains and Lambda-Calculi


The Constructive Semantics of Esterel.
The Foundations of Esterel.
The Esterel Synchronous Programming Language: Design
asynchronous Circuits.
Distributing automata for asynchronous networks of processors.
Distributing reactive systems.
Programming Real-Time Applications with Signal
Synchronous Programming of Reactive Systems.
The Synchronous DataAEow Programming Language Lustre.
A Visual Approach to Complex Systems.
Communicating Sequential Processes.
The Semantics of a Simple Language for Parallel Programming.
LCF as a programming language.
Formal Analysis of Cyclic Circuits.
Constructive Analysis of Cyclic circuits.
Analyse Constructive et Optimisation S
--TR
Communicating sequential processes
Statecharts: A visual formalism for complex systems
The ESTEREL synchronous programming language
Formal verification of embedded systems based on CFSM networks
Hardware-software co-design of embedded systems
Domains and lambda-calculi
The foundations of Esterel
Synchronous Programming of Reactive Systems
Constructive Analysis of Cyclic Circuits
Formal analysis of synchronous circuits

--CTR
Gerald Lttgen , Michael Mendler, The intuitionism behind Statecharts steps, ACM Transactions on Computational Logic (TOCL), v.3 n.1, p.1-41, January 2002
Mohammad Reza Mousavi , Paul Le Guernic , Jean-Pierre Talpin , Sandeep Kumar Shukla , Twan Basten, Modeling and Validating Globally Asynchronous Design in Synchronous Frameworks, Proceedings of the conference on Design, automation and test in Europe, p.10384, February 16-20, 2004
Stephen A. Edwards , Olivier Tardieu, SHIM: a deterministic model for heterogeneous embedded systems, Proceedings of the 5th ACM international conference on Embedded software, September 18-22, 2005, Jersey City, NJ, USA
Stephen A. Edwards , Edward A. Lee, The semantics and execution of a synchronous block-diagram language, Science of Computer Programming, v.48 n.1, p.21-42, July
embedded systems;finite state machines;synchronous programming;asynchronous networks