```pascal
program P18 :
output S1_and_S2,
      S1_and_not_S2,
      not_S1_and_S2,
      not_S1_and_not_S2;
loop
    trap T1 in
        signal S1 in
            pause;
            emit S1;
            exit T1
        ||
    loop
        trap T2 in
            signal S2 in
                pause;
                emit S2;
                exit T2
        ||
    loop
        present S1 then
            present S2 then
                emit S1_and_S2
            else
                emit S1_and_not_S2
        end present
        else
            present S2 then
                emit not_S1_and_S2
            else
                emit not_S1_and_not_S2
        end
    end present;
    pause
end loop
end signal
end trap
end loop
end signal
end trap
end loop
```

<caption>Figure 12.6: Multiple incarnations: program P18</caption>
The example can be extended to *n* signals, in which case the innermost
signal has *n* + 1 incarnations. Although such programs rarely occur in prac-
tice and can even look pathological, they are constructively correct and they
must be correctly translated<fnref n="2" />.

12.7 Curing Schizophrenia

To correctly translate examples such as P18, we must duplicate logic as many times as required by the number of possible incarnations. The solution we present here is based on the idea of always keeping the surface(s) and depth disjoint to be able to correctly translate loops by straightforward feedback. It has the drawback that logic is duplicated even if there are no loops, but it is semantically very clear. (A different solution based on duplicating logic only when translating loops is presented in [30].) In the worst case, the size of the logic will be square of the size of the source program. However, the squaring factor only shows up for artificial programs such as P18, and it is not a problem in practice. To minimize logic, the Esterel v5 compiler uses static analysis techniques to avoid duplication for non-schizophrenic parallels or local signals. We shall not present this optimization here.

12.7.1 Incarnation Indices

The key ingredient of our solution is the use of integer indices to name incarnations. In P16, page 130, and P17, page 132, we used indices 0 for the surface wires and 1 for the depth wires. We extend this numbering scheme to more complex examples such as P18, page 138. In the analysis of P18, we informally named the three incarnations of S2 “depth–depth”, “depth–surface”, and “surface–surface”, in the constructive order in which they appeared. We can abbreviate these names into words *dd*, *ds*, and *ss*. In this naming, we neglected the parallel statement that encloses “*signal S2*”; when taking this parallel into account, we get the exact naming *ddd*, *dds*, and *sss*. Notice that there can be no name such as *sds* where a *d* follows an *s*: by definition, the depth of a statement is included in the depth of all statements that enclose it. Therefore, we can further simplify the names and replace them by integer *incarnation indices* 2, 1, and 0, simply counting the number of occurrences of *d* in the name.

<footnote n="2">²The reader may question this point and wonder whether reincarnation is of any prac-
tical interest. The answer is yes, although we shall not try to prove this statement here.
For an example, see [16] where reincarnation is nicely used to handle menus in a menubar.</footnote>
In the final translation, we create separate logic for each incarnation
index. The reason why this way of duplicating logic works is easy to explain:
if a program *P* is constructive, then, for any substatement *p*, each indexed
incarnation of *p* can be executed only once in a reaction. Intuitively, given a
constructive proof of a reaction of *P* to an input, one can label each transition
in the proof by the index at which the transition occurs. The only way to
have two transitions of a substatement *p* at the same index would be to start
a loop at this index and to loop the loop. This would imply that the body
of the loop terminates instantaneously when started, which is forbidden by
the semantics (see rules (*loop*) in the behavioral semantics and (*r-do-loop*) in
the state semantics). Technically, this property is not trivial to prove, and
the proof is deferred to Chapter 13. In P18, one notices that looping a loop
always strictly decreases the incarnation level, as we shall explain in greater
detail in Section 12.7.4.

12.7.2 Translation Sketch

Before giving the final translation in Chapter 13, let us explain it intuitively and revisit examples. Let *P* be a program and *p* be a substatement of *P*. We translate *p* as in the basic translation, except that we replace the original *GO*, *KILL*, *K*, *S*, and *S'* wires by arrays of wires indexed by incarnation indices. The *RES*, *SUSP*, and *SEL* wires need not be indexed since they concern only the depth of statements and are not reincarnated. For *GO[i]*, *KILL[i]*, and *Kk[i]* completion wires, the incarnation index *i* ranges from 0 to *l*, where the *level* *l* of *p* is the number of parallel statements and local signal declarations of *P* in which *p* is contained (the other statements cannot provoke schizophrenia and do not trigger logic duplication). For local signal input and output wires *S[i]* and *S'[i]*, the index *i* ranges from 0 to *l'* if *l'* is the level of the body of the declaration of *S*, i.e. the level of the declaration plus one. Gates that receive wire arrays are replicated for each index. The wire driven by a *pause* register of level *l* is indexed by *l* since it is a typical depth wire.

Consider a parallel statement *p*|*q* of level *l*. Then *p* and *q* are at level *l' = l + 1*. A surface of the parallel statement is characterized by an index *i* such that 0 ≤ *i* ≤ *l*, and it is made of a pair of surfaces of *p* and *q* synchronized by a specific synchronizer *SYN[i]*. It is started by the wire *GO[i]*, which is passed to *p* and *q* as in Figure 11.10. No surface is generated at index *l'*. The depth of the parallel statement is made of all the wires driven by the *pause* registers of *p* and *p'*, which have index *l'*, and of a depth synchronizer *SYN[l']*. The surfaces and depth are kept disjoint as requested. Finally, we set *KILL[l'] =*
`KILL[l]` to propagate trap exits to the depth, and we union the completion wires of level *l* and *l'* to correctly propagate depth completion to the enclosing statement at level *l*.

For a local signal declaration of level *l*, the construction is similar. A surface has an index *i* such that 0 ≤ *i* ≤ *l* and uses a pair *S[i]*, *S'[i]* of signal wires, while the depth has index *l' = l + 1* and uses a distinct pair of wires *S[l']*, *S'[l']*.

### 12.7.3 Simple Examples

In P16, all wires in the top surface synchronizer have index 0, and all wires in the bottom depth synchronizer have index 1. Consider the following slightly more elaborate example P19.

```pascal
module P19:
input I;
output O;
signal S in
    present I then emit O else pause end;
[
    emit S
]
||
pause; emit S
]
end signal
```

Let us first analyze control propagation. The `signal S` statement opens one level, and the parallel statement opens another level. The `present` statement is translated at indices 0 and 1. Here, the depth incarnation of index 1 is useless since there is no way to start the `present` statement at resumption time: since `GO[1] = 0`, the incarnation of index 1 disappears by constant propagation<fnref n="3" />. The `emit O` statement in the `then` branch is translated with index 0 and its termination wire has the form `KO[0]`. The `pause` statement in the `else` branch generates two completion wires: the `K1[0]` wire, which reports pausing at start time, and the `KO[1]` wire, which reports termination at resumption time. The termination wire index

<footnote n="3">³In the Esterel v5 compiler, instead of generating and simplifying the depth incarnation, we do not generate it at all.</footnote>
is 1 since the **pause** statement is at level 1. The parallel statement has three incarnations 0, 1, and 2, with two surface synchronizers **SYN**[0] and **SYN**[1] and one depth synchronizer **SYN**[2].

* Incarnation 0 is of type surface-surface. It is active when both the **signal** and parallel statements are started. In our example, this happens at boot time if I is present. The **GO**[0] start wire of the parallel statement is the **KO**[0] termination wire of "**emit O**". The **GO**[0] wire is connected to the **LO**[0] entry of the **SYN**[0] synchronizer through the first "**emit S**" statement and to the **R1**[0] entry of **SYN**[0] through the **K1**[0] completion wire of the second **pause** statement, which indicates pausing. If **GO**[0] is set, **SYN**[0] reports pausing by setting its own completion wire **K1**[0].

* Incarnation 1 is of type depth-surface. It is active when the "**signal S**" statement is resumed and the parallel statement is started. This happens when the first **pause** statement is selected and resumed, i.e. in the second instant if I was absent in the first instant. The **GO**[1] start wire is the termination wire **KO**[1] of the first **pause** statement. As before, the **GO**[1] wire is connected to the **LO**[1] and **R1**[1] entries of **SYN**[1], which reports pausing by setting **K1**[1].

* The **SYN**[2] synchronizer is of type depth-depth. It is active when the parallel statement is resumed, which can occur only when the **signal** statement is resumed. In our example, this happens in the second instant if I was present in the first instant, and in the third instant otherwise. There is no **GO** wire at index 2 since the depth is solely driven by the **RES** resumption wire. The termination wire of the second **pause** statement is **KO**[2] since this statement is at level 2. It is connected to the **RO**[2] entry of **SYN**[2]. The first branch is not connected to **SYN**[2] since its depth is empty.

The **Kk**[1] and **Kk**[2] completion wires of **SYN**[1] and **SYN**[2] are *or*-ed at level 1, since they are all in the depth of the enclosing **signal** statement. This way, the parallel statement reports pausing and termination as if it was not internally split.

Let us now analyze signals. The toplevel **I** and **O** signals have only one incarnation indexed by 0. The input wire **I**[0] is connected to the **present** statement *and* gates. The output wire **O'**[0] is equal to the **GO**[0] input of "**emit O**", i.e. to the output of the first *and* gate of the **present** statement.
The S local signal has two incarnations 0 and 1. The surface "emit S" in the first parallel branch is translated at indices 0 and 1. Its GO[0] and GO[1] start wires respectively reach the or-gates of S'[0] and S'[1]. The depth "emit S" in the second branch acts only at index 2 since it follows a pause statement of level 2. Its GO[2] wire is connected to the S'[1] or-gate: the index 2 is transformed into 1 = min(1, 2) since the level of S is 1.

12.7.4 Correct Translation of P18

Consider now the program P18, page 138. The maximum level is 4 since
new levels are opened by the nested "signal S1", "||", "signal S2", and
"||" statements. The first pause statement has level 2 since it is enclosed in
the first signal declaration and the first parallel statement, while the second
and third ones have level 4. The S1 signal has two incarnations, the first
parallel statement has three, the S2 signal has four, and the second parallel
statement has five.

The "signal S1" declaration generates two input-output wire pairs: S1[0] and S1'[0] for surface incarnation, and S1[1] and S1'[1] for depth incarnation. At boot time, no "emit S1" statement is executed, which implies that S1'[0] and S1[0] have constant value 0. Being driven by the first pause statement of level 2, the "emit S1" statement connects its GO[2] input to S'[1], which is itself connected to S[1] by a buffer. Notice that the index 2 of the GO wire is decreased to 1, which is the maximal index for S1.

The first parallel statement has three synchronizers, only SYN[0] and SYN[2] being of interest. The surface-surface SYN[0] synchronizer is used when entering the parallel statement at boot time or when looping the outermost loop. It then reports pausing. The depth-depth SYN[2] synchronizer is used in all instants except boot to synchronize the termination of the branch resumptions. It then reports exiting trap T1 by setting K2[2]. Since there is no possibility to start the parallel from a pause statement of level 1, all inputs to the depth-surface SYN[1] synchronizer are 0, and SYN[1] disappears by constant propagation.

The "signal S2" declaration generates four pairs of wires correspond-
ing to indices 0 to 3. No "emit S2" statement can be executed at in-
dices 0, 1, and 2, which implies that S2'[0], S2[0], S2'[1], S2[1], S2'[2],
and S2[2] have constant value 0. The "emit S2" statement is started by a
pause statement of level 4. It connects its GO[4] input to S2'[3], and one
has S2[3] = S2'[3] = GO[4].

The innermost parallel statement has five synchronizers ranging from SYN[0]
to SYN[4], two of them being useless. The surface-surface SYN[0] synchronizer is used when entering the parallel statement at boot time or when looping the outermost loop. It then reports pausing by setting K1[0]. The SYN[2] synchronizer is used when the second loop loops. It then reports pausing by setting K1[2]. The SYN[4] synchronizer is used for proper resumption of the parallel depth. It then reports exiting T2 by setting K2[4]. The SYN[1] and SYN[3] synchronizers are useless and disappear by constant propagation.

The `present` statement also has also five incarnations, the ones indexed by 1 and 3 being useless since $GO[1] = GO[3] = 0$.

At boot time, the `SYN[0]` synchronizers all report pausing by setting their `K1[0]` outputs. No local signal is emitted, and the surface 0 incarnation of the `present` statement executes `"emit not S1_and_not S2"`, which sets `not S1_and_not S2'[0]`. In the next instants, execution is as follows.

* The three `pause` registers set their respective termination outputs `K0[2]`, `K0[4]`, and `K0[4]`, which provokes setting `S1'[1]` and `S2'[3]` and executing the `present` statement at index 4. The `present` statement tests for the depth `S1[1]` and `S2[3]` incarnations, which are set. Therefore, `"emit S1_and_S2"` is executed and `S1_and_S2'[0]` is set. The first branch of the innermost parallel executes `"exit T2"` and sets the `L2[4]` input of `SYN[4]`, while the second branch executes `pause` and sets the `R1[4]` input of `SYN[4]`. Therefore, `SYN[4]` propagates the exit by setting its `K2[4]` output wire. This wire reaches the `"trap T2"` statement output `or`-gate, which sets the termination wire `K0[2]` of the trap statement, which has depth 2.

* The surrounding loop sets `GO[2]` that traverses the `"signal S2"` declaration and starts the incarnation 2 of the innermost parallel. The first branch reports pausing to `SYN[2]` by setting `L1[2]`. The second branch executes the `present` test at index 2. This time, the signals tested for are `S1[1] = 1` and `S2[2] = 0`, and `S1_and_not_S2'[0]` is set. The second branch reports pausing to `SYN[2]` by setting the `R1[2]` input, and `SYN[2]` sets its `K1[2]` output. Pausing is reported to the `R1[2]` input of the depth `SYN[2]` synchronizer of the first parallel.

* In parallel, the first branch of the outermost parallel asks for exiting `T1` by setting the `L2[2]` input of the `SYN[2]` depth synchronizer. Since `L2[2]` and `R1[2]` are set, the `SYN[2]` synchronizer sets
its completion wire K2[2], which sets the termination wire K0[0] of
the "trap T1" statement.

* The outermost loop sets `GO[0]` and starts the surface incarnations. All `pause` statements report pausing to `SYN[0]` synchronizers. The incarnation 0 of the `present` statement is executed. It tests for `S1[0]` and `S2[0]`, which are both unset. The `"emit not_S1_and_not_S2"` circuit is executed and sets `not_S1_and_not_S2[0]`.

This all happens in one instant.
# Chapter 13

## The Formal Translation to Hardware

We now formally present the final correct translation of Esterel programs into circuits, using the textual presentation of circuits as sets of definitions and making heavy use of the syntactic extensions described in Section 10.4.

### 13.1 Translation Environments

For simplicity, we assume that all local signals have distinct names in the Esterel source program. This can be achieved by a suitable renaming.

The translation function takes as argument an *environment* $\rho$ composed of several constants and wires. The environment is used to determine the input and output wires of the current statement and some numerical auxiliaries. It contains the following fields:

* An integer $\kappa$ that denotes the maximal completion code available when translating the current statement, i.e. the number of traps in which the statement is included plus one.

* An integer $l$ that denotes the level of the current statement, i.e. the number of local signal and parallel statements in which the statement is enclosed.

* A vector $GO$ of *start wires* $GO[i]$, indexed by incarnation indices $i$ such that $0 \le i \le l$.

* A *resumption wire* RES.
* A suspension wire SUS.

* A vector KILL of kill wires KILL[i], indexed by incarnation indices i such that $0 \le i \le l$.

* A selection wire SEL.

* A matrix K of completion wires K[k, i], indexed by completion codes k such that $0 \le k \le \kappa$ and by incarnation indices i such that $0 \le i \le l$. In the formal translation, we write K[3, 2] instead of the K3[2] of Chapter 12.

* A set E of input signal vectors S[i] and a set E' of output signal vectors S'[i], each set containing one vector for each signal s visible in the current scope. For a vector S[i] or S'[i], the index i is an incarnation index such that $0 \le i \le l(s)$, where the level l(s) of a signal s declared by $p \setminus s$ is the level of p, i.e. the level of $p \setminus s$ plus one.

We use the classical record field notation to retrieve environment components. For instance, $\rho.G\mathit{O}[i]$ denotes an incoming control wire. Unless confusion is possible, we simply abbreviate $\rho.G\mathit{O}[i]$ by $G\mathit{O}[i]$.

Given an environment $\rho$, we shall often need to consider another environment $\rho'$ that differs from $\rho$ by the value of one field, say by changing $\rho.G\mathit{O}[i]$ into some wire $w$. We then write $\rho' = \rho[w/G\mathit{O}[i]]$. The notation extends naturally when changing several fields.

### 13.1.1 The Global Environment

To translate a program, we first allocate the following global wires:

* A global selection wire GSEL to be defined by the circuit.

* A global resumption wire GRES defined by $GRES = 1$.

* A global suspension wire GSUS defined by $GSUS = 0$.

* A global kill wire GKILL defined by $GKILL = 0$.

* A global start GGO wire defined by $GGO = \neg BOOTREG$, where the auxiliary boot register `BOOTREG` is defined by `BOOTREG := 1`.

* A matrix GK made of two global continuation wires GK[0, 0] and GK[1, 0], which respectively correspond to global termination and pause.
* A set $\mathcal{I}$ of input signal wires, and a set $\mathcal{O}$ of output signal wires. For each input signal $i$, there is an input wire $\mathbf{I}$, and for each signal $o$ there is an output wire $\mathbf{O}$. Being an input, $\mathbf{I}$ has no definition. Since the body of a program is at level 0, we use $\mathbf{I}[0]$ and $\mathbf{O}[0]$ as synonyms for $\mathbf{I}$ and $\mathbf{O}$.

We translate the module body in the global environment

$$g\rho = (1, 0, \mathbf{GGO}, \mathbf{GRES}, \mathbf{GSUS}, \mathbf{GKILL}, \mathbf{GSEL}, \mathbf{GK}, \mathcal{I}, \mathcal{O})$$

## 13.2 Translation Rules

For a completion code different from 1, we replicate the design of Figure 11.2 at all incarnation indices.

$$\text{for } k \neq 1, \quad C(k, \rho) = \mathbf{K}[k, i] \underset{0 \le i \le l}{\rightleftharpoons} \mathbf{GO}[i]$$

In the translation of a `pause` statement, we replicate the surface part of Figure 11.3, and the register drives the $\mathbf{K}[0, l]$ depth termination output.

$$C(1, \rho) = \left\{ \begin{array}{ll} \text{local REG} & \\ \text{REG} := & (\text{SUS} \land \text{REG} \land \neg\text{KILL}[l]) \\ & \lor \lor (\text{GO}[i] \land \neg\text{KILL}[i]) \\ & 0 \le i \le l \\ \text{SEL} \leftarrow \text{REG} & \\ \mathbf{K}[1, i] \leftarrow\leftarrow \text{GO}[i] & \\ \mathbf{K}[0, l] \leftarrow \text{REG} \land \text{RES} & \end{array} \right.$$

For a signal emission, we replicate Figure 11.4 at all indices. If $i > l(s)$, we are in the depth of the definition of $s$, and the wire to be set is $S'[l(s)]$. We use the notation $m \downarrow n$ as a short-hand for $\min(m, n)$.

$$C(!s, \rho) = \left\{ \begin{array}{ll} \mathbf{K}[0, i] & \leftarrow\leftarrow \mathbf{GO}[i] \\ S'[i \downarrow l(s)] & \leftarrow\leftarrow \mathbf{GO}[i] \\ 0 \le i \le l & \\ 0 \le i \le l & \end{array} \right.$$
For a signal presence test, we replicate Figure 11.5 at all indices. If $i > l(s)$, we are in the depth of the definition of $s$, and the wire to be tested for is $S[l(s)]$. All the or-gates that gather the outputs of the subcircuits in Figure 11.5 are implicitly created, since the subcircuits are instantiated in the same output environment and since the output wires are locally defined by implications in the subcircuits.

$$ C((s \ ? \ p, q), \rho) = \left\{ \begin{array}{l} \text{local } GO_1[0..l], GO_2[0..l] \\ C(p, \rho [GO_1 / GO]) \\ C(q, \rho [GO_2 / GO]) \\ GO_1[i] \quad 0 \le i \le l \\ GO_2[i] \quad 0 \le i \le l \end{array} \right. \quad \begin{array}{l} GO[i] \wedge S[i \downarrow l(s)] \\ GO[i] \wedge \neg S[i \downarrow l(s)] \end{array} $$

The translations of a suspension or of a watchdog are trivial since only the depth is of interest.

$$ C(s \supset p, \rho) = \left\{ \begin{array}{l} \text{local NRES, NSUS} \\ C(p, \rho [\text{NRES / RES, NSUS / SUS}]) \\ \text{NRES} = \text{RES} \wedge \neg S[l(s)] \\ \text{NSUS} = \text{SUS} \vee (\text{RES} \wedge \text{SEL} \wedge S[l(s)]) \\ \text{K}[1, l] \Leftarrow \text{RES} \wedge \text{SEL} \wedge S[l(s)] \end{array} \right. $$

$$ C(s \gg p, \rho) = \left\{ \begin{array}{l} \text{local NRES} \\ C(p, \rho [\text{NRES / RES}]) \\ \text{NRES} = \text{RES} \wedge \neg S[l(s)] \\ \text{K}[0, l] \Leftarrow \text{RES} \wedge S[l(s)] \end{array} \right. $$

In the translation of a sequence $p$; $q$, we chain $p$ and $q$ at all incarnation indices, as in Figure 11.8. The output or-gates are implicitly generated by implications, as for $s \ ? \ p, q$.

$$ C(p; q, \rho) = \left\{ \begin{array}{l} \text{local } \text{SEQ}[0..l] \\ C(p, \rho [\text{SEQ}[i] / \text{K}[0, i]]) \\ \qquad 0 \le i \le l \\ C(q, \rho [\text{SEQ} / GO]) \end{array} \right. $$
For a loop, we feedback the depth termination wire to the depth $GO[l]$ start wire.

$$C(p*, \rho) = \begin{cases} \text{local INLOOP, OUTLOOP} \\ C(p, \rho [\text{INLOOP} / \text{GO}[l], \text{OUTLOOP} / \text{K}[0, l]]) \\ \text{INLOOP} = \text{GO}[l] \lor \text{OUTLOOP} \end{cases}$$

Notice that the wires $K[0, i]$ are left pending for $i \neq l$. This works only for loop-safe programs defined in Section 6.6, for which these wires are guaranteed to always have value 0. A translation that also handles loop-unsafe programs will be presented in Section 13.4.

We now translate the parallel statement. We increment the level and declare the selection, left and right completion, and synchronizer wires. We translate the left and right substatements in the appropriate environments, and we build the selection wire and the synchronizers, as in Figures 11.10 and 11.11. The output or-gates are created implicitly by implications. To translate the substatements, we use an auxiliary environment $\rho'$ such that $l' = l + 1$, $\rho \cdot GO[l'] = 0$, since there should be no surface at depth level $l'$, and $\rho' \cdot KILL[l'] = \rho \cdot KILL[l]$ since the input depth kill wire must be propagated to the new depth to handle exceptions. Given an array $A$ of size $n$, call $A \cdot v$ the array of size $n + 1$ obtained by adding $v$ to $A$ at position $n$. Then $\rho' = \rho [l' / l, GO \cdot 0 / GO, KILL \cdot KILL[l] / KILL]$. The formal translation is
$$
\begin{equation*}
C(p | q, \rho) =
\left\{
\begin{array}{ll}
\text{local } l' = l + 1 & \\
\quad \text{LSEL, RSEL,} & \\
\quad \text{L}[0..\kappa, 0..l'], \text{R}[0..\kappa, 0..l'], & \\
\quad \text{LMIN}[0..\kappa, 0..l'], \text{RMIN}[0..\kappa, 0..l'], \text{UNION}[0..\kappa, 0..l'] & \\
C(p, \rho' [\text{LSEL} / \text{SEL}, \text{L} / \text{K}]) & \\
C(q, \rho' [\text{RSEL} / \text{SEL}, \text{R} / \text{K}]) & \\
SEL \leftarrow \text{LSEL} & \\
SEL \leftarrow \text{RSEL} & \\
\text{UNION}[k, i] & = \text{L}[k, i] \lor \text{R}[k, i] \\
\phantom{\text{UNION}[k, i] =} 0 \le k \le \kappa \\
\phantom{\text{UNION}[k, i] =} 0 \le i \le l' \\
\text{LMIN}[0, l'] & \leftarrow \neg \text{LSEL} \\
\text{LMIN}[0, i] & \iff \text{L}[0, i] \\
\text{LMIN}[k + 1, i] & = \text{LMIN}[k, i] \lor \text{L}[k + 1, i] \\
\phantom{\text{LMIN}[k + 1, i] =} 0 \le k < \kappa \\
\phantom{\text{LMIN}[k + 1, i] =} 0 \le i \le l' \\
\text{RMIN}[0, l'] & \leftarrow \neg \text{RSEL} \\
\text{RMIN}[0, i] & \iff \text{R}[0, i] \\
\text{RMIN}[k + 1, i] & = \text{RMIN}[k, i] \lor \text{R}[k + 1, i] \\
\phantom{\text{RMIN}[k + 1, i] =} 0 \le k < \kappa \\
\phantom{\text{RMIN}[k + 1, i] =} 0 \le i \le l' \\
K[k, l \downarrow i] & \iff \text{LMIN}[k, i] \land \text{UNION}[k, i] \land \text{RMIN}[k, i] \\
\phantom{K[k, l \downarrow i] =} 1 \le k \le \kappa \\
\phantom{K[k, l \downarrow i] =} 0 \le i \le l'
\end{array}
\right.
\end{equation*}
$$

Notice that the last implication implicitly performs the union of $K[k, l]$ and $K[k, l + 1]$,
which is necessary to report depth completion at the level at which the par-
allel is translated. Such a completion is either the completion of the surface
of index *l* or a completion of the parallel depth proper.
Trap and shift are translated as in Figures 11.12 and 11.13 at all indices.

$$ C(\{p\}, \rho) = \left\{ \begin{array}{ll} \text{local } \kappa' = \kappa + 1 & \\ \quad \text{NKILL}[0..l] & \\ \quad \text{NK}[0..\kappa', 0..l] & \\ \quad C(p, \rho[\kappa' / \kappa, \text{NKILL} / \text{KILL}, \text{NK} / \text{K}]) & \\ \text{NKILL}[i] \underset{0\le i\le l}{=} \text{KILL}[i] \lor \text{NK}[2, i] & \\ \quad K[0, i] \underset{0\le i\le l}{\Longleftrightarrow} \text{NK}[0, i] \lor \text{NK}[2, i] & \\ \quad K[1, i] \underset{0\le i\le l}{\Longleftrightarrow} \text{NK}[1, i] & \\ \quad K[k, i] \underset{\begin{array}{l} 2\le k\le \kappa \\ 0\le i\le l \end{array}}{\Longleftrightarrow} \text{NK}[k+1, i] & \\ \end{array} \right. $$

$$ C(\uparrow p, \rho) = \left\{ \begin{array}{ll} \text{local } \kappa' = \kappa - 1 & \\ \quad \text{NK}[0..\kappa', 0..l] & \\ \quad C(p, \rho[\kappa' / \kappa, \text{NK} / \text{K}]) & \\ \quad K[\uparrow k, i] \iff \text{NK}[k, i] & \\ \quad \begin{array}{l} 0\le k<\kappa \\ 0\le i\le l \end{array} & \\ \end{array} \right. $$

To translate a $p$s statement, we increment $l$ and feed back the signal wires at all incarnation indices. As for the parallel statement, we use the environment $\rho' = \rho[l'/l, GO \cdot 0 / GO, \text{KILL} \cdot \text{KILL}[l] / \text{KILL}]$. The translation is:

$$ C(p\backslash s, \rho) = \left\{ \begin{array}{ll} \text{local } l' = l + 1 & \\ \quad \mathbf{S}[0..l'], \mathbf{S}'[0..l'] & \\ \quad \text{NK}[0..\kappa, 0..l'] & \\ \quad C(p, \rho[\mathbf{E} \cdot \mathbf{S} / \mathbf{E}, \mathbf{E}' \cdot \mathbf{S}' / \mathbf{E}', \text{NK} / \text{K}]) & \\ \quad \mathbf{S}[i] \underset{0\le i\le l'}{=} \mathbf{S}'[i] & \\ \quad K[k, l \downarrow i] \underset{0\le i\le l'}{=} \text{NK}[k, i] & \\ \end{array} \right. $$
## 13.3 Correctness of the Translation

Let $P$ be a program of body $q$, let $p = 1$; $q$ be the base statement of the states of $P$, and let $C = C(P)$ be the generated circuit. Registers in $C$ are in bijection with **pause** statements in $p$. With each state $\hat{p}$ of $P$ we associate a state $R(\hat{p})$ of $C$. In $R(\hat{p})$, a register has value 1 if and only if the corresponding **pause** statement is selected in $\hat{p}$, except for the boot register, which is inverted and has value 0 if the auxiliary boot statement is selected; this inversion is needed since all registers are assumed to have initial value 0 while the boot statement is originally selected. Note that the terminated extended statement $p$ corresponds to the circuit state where the boot register has value 1 and all other **pause** registers have value 0, which is characterized by $GSEL = 0$ in $C$.

The main equivalence theorem shows that our circuit translation exactly implements the constructive behavioral semantics for loop-safe programs.

**Theorem 6** For any state $\hat{p}$ of a loop-safe program $P$ and for any input event $I$, one has $\hat{p} \stackrel{O}{\rightleftharpoons}_I \hat{p}'$ in the state constructive semantics if and only if one has $R(\hat{p}) \stackrel{O}{\rightleftharpoons}_I R(\hat{p}')$ in the constructive circuit semantics.

## 13.4 Extension to Loop-Unsafe Programs

We briefly indicate how to extend the translation to all programs, including loop-unsafe ones.

Consider a loop $q*$ of level $l$ in a program $P$. For $i < l$, the termination wire $K[0, i]$ of $q$ is generated by the surface of $q$, which cannot terminate instantaneously if $P$ is loop-safe. In this case, $K[0, i]$ always has value 0 and can be ignored. For loop-unsafe programs, we must dynamically check for $K[0, i] = 0$. One way to do this is to introduce an artificial combinational loop using an auxiliary wire $INSTLOOP[i]$ defined by

$$ \mathit{INSTLOOP}[i] = \mathit{INSTLOOP}[i] \wedge \mathit{K}[0, i] \qquad (13.1) $$

Then, the value of $\mathit{INSTLOOP}[i]$ can be constructively computed to be 0 if and only if $K[0, i] = 0$. If $K[0, i] = 1$, we get $\mathit{INSTLOOP}[i] = \mathit{INSTLOOP}[i]$ and the circuit is not constructive, which is detected by the Esterel compiler. This is fine for $i < l$ since $K[0, i]$ is a surface wire, and the extension of the translation is trivial. However, at level $l$, $K[0, l]$ handles both the surface of index $l$ and the depth of $q$. To use the same trick, we have to distinguish
between surface and depth completion wires and to use only the surface
completion wire in the definition of **INSTLOOP**[*l*]. This requires an easy but
tedious modification of the translation, which we leave to the reader.
Chapter 14

Conclusion

We have presented the new constructive semantics of Pure Esterel and we
have shown the equivalence between three styles of semantics: the construc-
tive behavioral semantics, where reactions are defined by single synchronous
transitions, the constructive operational semantics, where reactions are de-
fined by sequences of elementary microsteps, and the electrical semantics
that uses a translation into constructive digital circuits.

On the theoretical side, the main result is the equivalence of construc-
tiveness of a program and electrical stabilization of its circuit. This result
is important since it relates a logical notion to a truly physical one. It gives
us additional confidence in the relevance of the constructive semantics. On
the practical side, the constructive semantics is implemented in the Esterel
v5 compiler to software or hardware, and it is also used in other tools such
as symbolic debuggers, see the Esterel v5 manual [12].

There are many more things to be studied. In this book, we have not
studied compositionality issues. It turns out that the logical semantics has
a weird behavior w.r.t. program composition, while the constructive seman-
tics is compositional by nature, being a least fixpoint semantics (neverthe-
less, compositionality issues are never trivial in synchronous languages). We
have also not discuss optimization issues. The interested reader can refer
to [36, 37]. We are also lacking an axiomatic semantics, which should be
useful for studying program equivalence. Finally, we are looking for very
efficient algorithms to show constructiveness for all possible inputs. The
ones we presently use are not that bad, but they can surely be dramatically
improved.
Bibliography

[1] C. André. Representation and analysis of reactive behaviors: a syn-
chronous approach. In *Proc CESA '96, IEEE-SMC, Lille, France*, 1996.

[2] G. Berry. Real-time programming: General purpose or special-purpose languages. In G. Ritter, editor, *Information Processing 89*, pages 11–17. Elsevier Science Publishers B.V. (North Holland), 1989.

[3] G. Berry. Programming a digital watch in Esterel v3.2. Rapport de recherche 08/91, Centre de Mathématiques Appliquées, Ecole des Mines de Paris, Sophia-Antipolis, 1991.

[4] G. Berry. Esterel on hardware. *Philosophical Transactions Royal Society of London A*, 339:87–104, 1992.

[5] G. Berry. Preemption and concurrency. In *Proc. FSTTCS 93*, Lecture Notes in Computer Science 761, pages 72–93. Springer-Verlag, 1993.

[6] G. Berry. The semantics of pure Esterel. In M. Broy, editor, *Program Design Calculi*, volume 118 of *Series F: Computer and System Sciences*, pages 361–409. NATO ASI Series, 1993.

[7] G. Berry. *The Esterel Primer*. http://www.inria.fr/meije/esterel, 1998.

[8] G. Berry. The foundations of Esterel. In G. Plotkin, C. Stirling, and M. Tofte, editors, *Proof, Language, and Interaction: Essays in Honour of Robin Milner*. MIT Press, to appear.

[9] G. Berry and L. Cosserat. The synchronous programming languages Esterel and its mathematical semantics. In S. Brookes and G. Winskel, editors, *Seminar on Concurrency*, pages 389–448. Springer Verlag Lecture Notes in Computer Science 197, 1984.
[10] G. Berry and G. Gonthier. Incremental development of an hdlc entity in Esterel. *Comp. Networks and ISDN Systems*, 22:35–49, 1991.

[11] G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. *Science Of Computer Programming*, 19(2):87–152, 1992.

[12] G. Berry and the Esterel Team. *The Esterel v5 System Manual*. http://www.inria.fr/meije/esterel, 1998.

[13] F. Boussinot. Programming a reflex game in Esterel v3.2. Rapport de recherche 07/91, Centre de Mathématiques Appliquées, Ecole des Mines de Paris, Sophia-Antipolis, 1991.

[14] F. Boussinot and R. de Simone. The Esterel language. *Another Look at Real Time Programming, Proceedings of the IEEE*, 79:1293–1304, 1991.

[15] J. Brzozowski and C.-J. Seger. *Asynchronous Circuits*. Springer-Verlag, 1996.

[16] D. Clément and J. Incerpi. Programming the behavior of graphical objects using Esterel. In *TAPSOFT '89, Springer-Verlag LNCS 352*, 1989.

[17] J-Y. Girard, Yves Lafont, and Paul Taylor. *Proofs And Types*. Cambridge University Press, 1989.

[18] G. Gonthier. Sémantique et modèles d'exécution des langages réactifs synchrones; application à Esterel. Thèse d'informatique, Université d'Orsay, 1988.

[19] The Esterel Group. The Esterel v5 documentation. Technical report, Ecole des Mines de Paris / INRIA.

[20] P. Le Guernic, M. Le Borgne, T. Gauthier, and C. Le Maire. Programming real time applications with Signal. *Another Look at Real Time Programming, Proceedings of the IEEE, Special Issue*, Sept. 1991.

[21] G. D. Hachtel and F. Somenzi. *Logic Synthesis and Verification Algorithms*. Kluwer Academic Publishers, 1996.

[22] N. Halbwachs. *Synchronous Programming of Reactive Systems*. Kluwer, 1993.
[23] N. Halbwachs, P. Caspi, and D. Pilaud. The synchronous dataflow programming language Lustre. *Another Look at Real Time Programming, Proceedings of the IEEE, Special Issue*, Sept. 1991.

[24] N. Halbwachs and F. Maraninchi. On the symbolic analysis of combinational loops in circuits and synchronous programs. In *Euromicro'95*, Como (Italy), September 1995.

[25] D. Harel. Statecharts: a visual approach to complex systems. *Science of Computer Programming*, 8:231-274, 1987.

[26] D. Harel, A. Pnueli, J.P. Schmidt, and R. Sherman. On the formal semantics of Statecharts. In *Proc. Logic in Computer Science*, 1986.

[27] L. Jategaonkar Jagadeesan, C. Puchol, and J. E. Von Olnhausen. A formal approach to reactive systems software: a telecommunications application in Esterel. *Formal Methods in Systems Design*, 8(2), 1996.

[28] S. Malik. Analysis of cyclic combinational circuits. *IEEE Trans. Computer-Aided Design*, 13(7):950-956, 1994.

[29] Florence Maraninchi. The Argos language: Graphical representation of automata and description of reactive systems. In *Proc. IEEE Conf. on Visual Languages, Kobe, Japan*, 1991.

[30] F. Mignard. Compilation du langage Esterel en systèmes d'équations booléennes. Thèse d'informatique, Ecole des Mines de Paris, 1994.

[31] R. Milner. *Communication and Concurrency*. Series in Computer Science. Prentice Hall, 1989.

[32] G. Murakami and Ravi Sethi. Terminal call processing in Esterel. In *Proc. IFIP 92 World Computer Congress, Madrid, Spain*, 1992.

[33] G. Plotkin. Lcf considered as a programming language. *Theoretical Computer Science*, 5(3):223-256, 1977.

[34] G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, University of Aarhus, 1981.

[35] V. A. Saraswat, R. Jagadeesan, and V. Gupta. Default timed concurrent constraint programming. In *Proc. POPL'95, San Francisco, USA*, pages 272-285, 1995.
[36] E. Sentovich, H. Toma, and G. Berry. Latch optimization in circuits generated from high-level descriptions. In *Proc. International Conf. on Computer-Aided Design (ICCAD)*, 1996.

[37] E. Sentovich, H. Toma, and G. Berry. Efficient latch optimization using exclusive sets. In *Proc. Digital Automation Conference (DAC)*, 1997.

[38] T. Shiple and G. Berry. Constructive analysis of cyclic circuits. In *Proc. International Design and Test Conference ITDC 96, Paris, France*, 1996.

[39] Thomas R. Shiple, Vigyan Singhal, Gérard Berry, Robert K. Brayton, and Alberto L. Sangiovanni-Vincentelli. Analysis of combinational cycles. Technical Report UCB/ERL M96, Electronics Research Laboratory, College of Engineering, University of California, Berkeley, 1996.

[40] The COQ Team. The COQ system. Technical report, INRIA, http://pauillac.inria.fr/coq.

[41] H. Touati and G. Berry. Optimized controller synthesis using Esterel. In *Proc. International Workshop on Logic Synthesis IWLS'93, Lake Tahoe*, 1993.

[42] J. Vuillemin. On circuits and numbers. *IEEE Transactions on Computers*, 43:8:868:27-79, 1994.