Goals and Scientific Foundations

Context and motivations

High-level embedded system design has gained prominence in the face of rising technological complexity, increasing performance requirements and shortening time to market demands for electronic equipments. Today, the installed base of intellectual property (IP) further stresses the requirements for adapting existing components with new services within complex integrated architectures, calling for appropriate mathematical models and methodological approaches to that purpose.

However, they are usually not amenable to direct engineering use nor seem to satisfy the present industrial demand. As a matter of fact, the attention of the industry tends to shift to modeling frameworks based on general-purpose programming language variants, in response to a growing industry demand for higher abstraction-levels in the system design process and an attempt to fill the so-called  productivity gap.

Project-team Espresso aims at this convergence by considering the formal modeling framework of the Polychrony toolbox to serve as pivot formalism to import, transform, validate and export heterogeneous formalisms and languages.

The polychronous approach

Despite overwhelming advances in embedded systems design, existing techniques and tools merely provide ad-hoc solutions to the challenging issue of the productivity gap. The pressing demand for design tools has sometimes hidden the need to lay mathematical foundations below design languages.  Many illustrating examples can be found, e.g. the variety of very different formal semantics found in  state-diagram formalisms.  Even though these design languages benefit from decades of programming practice, they still give rise to some diverging interpretations of their semantics.

The need for higher abstraction-levels and the rise of stronger market constraints now make the need for unambiguous design models more obvious.  This challenge requires models and methods to translate a high-level system specification into a distribution of purely sequential programs and to implement semantics-preserving transformations and high-level optimizations such as hierarchization (sequentialization) or desynchronization (protocol synthesis).

In this aim, system design based on the so-called ``synchronous hypothesis'' has focused the attention of many academic and industrial actors. The synchronous paradigm consists of abstracting the non-functional implementation details of a system and lets one benefit from a focused reasoning on the logics behind the instants at which the system functionalities should be secured.

With this point of view, synchronous design models and languages provide intuitive models for embedded systems [5]. This affinity explains the ease of generating systems and architectures and verify their functionalities using compilers and related tools that implement this approach.

In the relational mathematical model behind the design language Signal, the supportive data-flow notation of Polychrony, this affinity goes beyond the domain of purely sequential systems and synchronous circuits and embraces the context of complex architectures consisting of synchronous circuits and desynchronization protocols: globally asynchronous and locally synchronous architectures (GALS).

This unique feature is obtained thanks to the fundamental notion of polychrony: the capability to describe systems in which components obey to multiple clock rates.  It provides a mathematical foundation to a notion of refinement: the ability to model a system from the early stages of its requirement specifications (relations, properties) to the late stages of its synthesis and deployment (functions, automata).

The notion of polychrony goes beyond the usual scope of a programming language, allowing for specifications and properties to be described. As a result, the Signal design methodology draws a continuum from synchrony to asynchrony, from specification to implementation, from abstraction to refinement, from interface to implementation.  Signal gives the opportunity to seamlessly model embedded systems at multiple levels of abstraction while reasoning within a simple and formally defined mathematical model.

The inherent flexibility of the abstract notion of signal handled in Signal invites and favors the design of correct-by-construction systems by means of well-defined model transformations that preserve the intended semantics and stated properties of the architecture under design.

Scientific Foundations

Scientific Foundations

Embedded systems are not new, but their pervasive introduction in ordinary-life objects (cars, telephone, home appliances) brought a new focus onto design methods for such systems. New development techniques are needed to meet the challenges of productivity in a competitive environment. Synchronous languages rely on the synchronous hypothesis, which lets computations and behaviors be divided into a discrete sequence of computation steps which are equivalently called reactions or execution instants. In itself this assumption is rather common in practical embedded system design.

But the synchronous hypothesis adds to this the fact that, inside each instant, the behavioral propagation is well-behaved (causal), so that the status of every signal or variable is established and defined prior to being tested or used. This criterion, which may be seen at first as an isolated technical requirement, is in fact the key point of the approach. It ensures strong semantic soundness by allowing universally recognized mathematical models to be used as supporting foundations. In turn, these models give access to a large corpus of efficient optimization, compilation, and formal verification techniques. The synchronous hypothesis also guarantees full equivalence between various levels of representation, thereby avoiding altogether the pitfalls of non-synthesizability of other similar formalisms. In that sense the synchronous hypothesis is, in our view, a major contribution to the goal of model-based design of embedded systems.

We shall describe the synchronous hypothesis and its mathematical background, together with a range of design techniques enpowered by the approach. Declarative formalisms implementing the synchronous hypothesis can be cast into a model of computation [1] consisting of a domain of traces or behaviors and of semi-lattice structure that renders the synchronous hypothesis using a timing equivalence relation: clock equivalence. Asynchrony can be superimposed on this model by considering a flow equivalence relation as well as heterogeneous systems  [2] by parameterizing composition with arbitrary timing relations.

A synchronous model of computation

We consider a partially-ordered set of tags t to denote instants seen as symbolic periods in time during which a reaction takes place. The relation t1 ≤ t2 says that t₁ occurs before t₂. Its minimum is noted 0. A totally ordered set of tags C is called a chain and denotes the sampling of a possibly continuous or dense signal over a countable series of causally related tags. Events, signals, behaviors and processes are defined as follows:

• an event e is a pair consisting of a value v and a tag t,

• a signal s is a function from a chain of tags to a set of values,

• a behavior b is a function from a set of names x to signals,

• a process p is a set of behaviors that have the same domain.

In the remainder, we write tags (s) for the tags of a signal s, vars (b) for the domains of b, b|_X for the projection of a behavior b on a set of names X and b/X for its complementary.

Figure 1 depicts a behavior b over three signals named x, y and z. Two frames depict timing domains formalized by chains of tags. Signals x and y belong to the same timing domain: x is a down-sampling of y. Its events are synchronous to odd occurrences of events along y and share the same tags, e.g. t₁. Even tags of y, e.g. t₂, are ordered along its chain, e.g. t₁<t₂, but absent from x. Signal z belongs to a different timing domain. Its tags, e.g. t₃ are not ordered with respect to the chain of y, e.g. t₁ ¬ ≤ t₃ and t₃ ¬≤ t₁.

Figure 1. Behavior b over three signals x, y and z in two clock domains

Composition

Synchronous composition is noted p || q and defined by the union b ∪ c of all behaviors b (from p) and c (from q) which hold the same values at the same tags b|_I = c|_I for all signal x ∈ I=vars(b) ∩ vars(c) they share. Figure 2 depicts the synchronous composition (Figure 2, right) of the behaviors b (Figure 2, left) and the behavior c (Figure 2  middle). The signal y, shared by b and c, carries the same tags and the same values in both b and c. Hence, b ∪ c defines the synchronous composition of b and c.

Figure 2. Synchronous composition of b ∈ p and c ∈ q

Scheduling

A scheduling structure is defined to schedule the occurrence of events along signals during an instant t. A scheduling → is a pre-order relation between dates x_t where t represents the time and x the location of the event. Figure 3 depicts such a relation superimposed to the signals x and y of Figure 1. The relation y_t1 → x_t1, for instance, requires y to be calculated before x at the instant t₁. Naturally, scheduling is contained in time: if t < t' then x_t →^b x_t' for any x and b and if x_t → ^b x_t' then t' ¬< t.

Figure 3. Scheduling relations between simultaneous events

Structure

A synchronous structure is defined by a semi-lattice structure to denote behaviors that have the same timing structure. The intuition behind this relation is depicted in Figure 4. It is to consider a signal as an elastic with ordered marks on it (tags). If the elastic is stretched, marks remain in the same relative (partial) order but have more space (time) between each other. The same holds for a set of elastics: a behavior. If elastics are equally stretched, the order between marks is unchanged.

In Figure 4, the time scale of x and y changes but the partial timing and scheduling relations are preserved. Stretching is a partial-order relation which defines clock equivalence. Formally, a behavior c is a stretching of b of same domain, written b ≤ c, iff there exists an increasing bijection on tags f that preserves the timing and scheduling relations. If so, c is the image of b by f. Last, the behaviors b and c are said clock-equivalent, written b~c, iff there exists a behavior d s.t. d ≤ b and d ≤ c .

Figure 4. Relating synchronous behaviors by stretching.

A declarative design language

Signal  [3] is a declarative design language expressed within the polychronous model of computation. In Signal, a process P is an infinite loop that consists of the synchronous composition P | | Q of simultaneous equations x = yfz over signals named x, y, z. The restriction of a signal name x to a process P is noted P/x.

Equations x = yfz in Signal more generally denote processes that define timing relations between input and output signals. There are four primitive combinators in Signal:

• delay x = y $ init v, initially defines the signal x by the value v and then by the previous value of the signal y. The signal y and its delayed copy x = y $ init v are synchronous: they share the same set of tags t1,t2,... . Initially, at t₁, the signal x takes the declared value v and then, at tag t_n, the value of y at tag t_n-1.

  

• sampling x = y when z, defines x by y when z is true (and both y and z are present); x is present with the value v₂ at t₂ only if y is present with v₂ at t₂ and if z is present at t₂ with the value true. When this is the case, one needs to schedule the calculation of y and z before x, as depicted by y_t2 → x_t2 ← z_t2.

• merge x = y default z, defines x by y when y is present and by z otherwise. If y is absent and z present with v₁ at t₁ then x holds (t₁, v₁). If y is present (at t₂ or t₃) then x holds its value whether z is present (at t₂) or not (at t₃).

  

The structuring element of a Signal specification is a process. A process accepts input signals originating from possibly different clock domains to produce output signals when needed. This allows, for instance, to specify a counter where the inputs tick and reset and the output value have independent clocks. The body of counter consists of one equation that defines the output signal value. Upon the event reset, it sets the count to 0. Otherwise, upon a tick event, it increments the count by referring to the previous value of value and adding 1 to it. Otherwise, if the count is solicited in the context of the counter process (meaning that its clock is active), the counter just returns the previous count without having to obtain a value from the tick and reset signals.

    process counter = (? event tick, reset ! integer value)

        (| value := (0 when reset)

            default ((value$ init 0 + 1) when tick)

            default (value$ init 0)

        |);

A Signal process is a structuring element akin to a hierarchical block diagram. A process may structurally contain sub-processes. A process is a generic structuring element that can be specialized to the timing context of its call. For instance, the definition of a synchronized counter starting from the previous specification consists of its refinement with synchronization. The input tick and reset clocks expected by the process counter are sampled from the boolean input signals tick and reset by using the when tick and when reset expressions. The count is then synchronized to the inputs by the equation reset ^= tick ^= count.

    process synccounter = (? boolean tick, reset ! integer value)

        (| value := counter (when tick, when reset)

         | reset ^= tick ^= value

         |);

Compilation of Signal

Sequential code generation starting from a Signal specification starts with an analysis of its implicit synchronization and scheduling relations. This analysis yields the control and data flow graphs that define the class of sequentially executable specifications and allow to generate code.

Synchronization and scheduling specifications

In Signal, the clock ^x of a signal x denotes the set of instants at which the signal x is present. It is represented by a signal that is true when x is present and that is absent otherwise. Clock expressions represent control. The clock when x (resp. when not x) represents the time tags at which a boolean signal x is present and true (resp. false).

The empty clock is written ^0 and clock expressions e combined using conjunction, disjunction and symmetric difference. Clock equations E are Signal processes: the equation e ^= e' synchronizes the clocks e and e^' while  e ^< e'  specifies the containment of e in e^'. Explicit scheduling relations x → y when e allow to schedule the calculation of signals (e.g. x after y at the clock e).

e ::= ^x | when x | when not x |  e^+ e' | e ^* e' | e ^- e' | ^0   (Clock expressions)

E ::= () | e^= e' | e^≤ e' | x → y when e | E | E' | E/x (graph and clock relations)

Synchronization and scheduling analysis

A Signal process P corresponds to a system of clock and scheduling relations E that denotes its timing structure. It can be defined by induction on the structure of P using the inference system P:E of Figure 5.

    x := y$ init v   : ^x ^= ^y

    x := y when z    : ^x ^= ^y when z | y -> x when z

    x := y default z : ^x ^= ^y default ^z | y -> x when ^y | z -> x when ^z ^- ^y

                                                               Figure 5. Clock inference system

Hierarchization [4]

The clock and scheduling relations E of a process P define the control-flow and data-flow graphs that hold all necessary information to compile a Signal specification upon satisfaction of the property of endochrony. A process is said endochronous iff, given a set of input signals and flow-equivalent input behaviors, it has the capability to reconstruct a unique synchronous behavior up to clock-equivalence: the input and output signals are ordered in clock-equivalent ways.

To determine the order in which signals are processed during the period of a reaction, clock relations E play an essential role. The process of determining this order is called hierarchization and consists of an insertion algorithm which hooks elementary control flow graphs (in the form of if-then-else structures) one to the others. Figure 6. right, let h3 be a clock computed using h1 and h2. Let h be the head of a tree from which h1 and h2 are computed (an if-then-else), h3 is computed after h1 and h2 and placed under h.

Figure 6. Hierarchization of clocks

References

[1]

P. Le Guernic , J.-P. Talpin, J.-C. Le Lann.
Polychrony for system design, in: Journal of Circuits, Systems and Computers, Special Issue on Application Specific Hardware Design, 2003.

[2]

A. Benveniste, P. Caspi, L. Carloni, A. Sangiovanni-Vincentelli.
Heterogeneous Reactive Systems Modeling and Correct-by-Construction Deployment, in: Embedded Software Conference (EMSOFT'03), Springer Verlag, 2003.

[3]

A. Benveniste, P. Le Guernic , C. Jacquemot.
Synchronous programming with events and relations: the Signal language and its semantics, in: Science of Computer Programming, 1991, vol. 16, p. 103-149.

[4]

T. P. Amagbegnon, L. Besnard , P. Le Guernic .
Implementation of the Data-flow Synchronous Language Signal, in: Proceedings of the ACM Symposium on Programming Languages Design and Implementation (PLDI'95), ACM, 1995, p. 163–173.

[5]

A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. Le Guernic , R. de Simone.
The Synchronous Languages Twelve Years Later, in: Proceedings of the IEEE Special issue on Modeling and Design of Embedded Systems, 2003, vol. 91(1).