Jean-Pierre Talpin

Paul Le Guernic

Sandeep Kumar

Frédéric Doucet

Rajesh Gupta

Formal Refinement Checking in a System-level Design Methodology

Rising complexity, increasing performance requirements, and shortening time-to-market demands necessitate newer design paradigms for embedded system design. Such newer design methodologies require raising the level of abstraction for design entry, reuse of intellectual property blocks as virtual components, refinement based design, and formal verification to prove correctness of refinement steps. The problem of combining various components from different designers and companies, designed at different levels of abstraction, and embodying heterogeneous models of computation is a difficult challenge for the designer community today. Moreover, one of the gating factors for widespread adoption of the system-level design paradigm is the lack of formal models, method and tools to support refinement. In the absence of provably correct and adequate behavioral synthesis techniques, the refinement of a system-level description towards its implementation is primarily a manual process. Furthermore, proving that the implementation preserves the properties of the higher system-level design-abstraction is an outstanding problem.

In this paper, we address these issues and define a formal refinement-checking methodology for system-level design. Our methodology is based on a polychronous model of computation of the multi-clocked synchronous formalism SIGNAL. This formalism is implemented in the POLYCHRONY workbench. We demonstrate the effectiveness of our approach by the experimental case study of a SPECC modeling example. First, we define a technique to systematically model SPECC programs in the SIGNAL formalism. Second, we define a methodology to compare system-level models of SPECC programs and to validate behavioral equivalence relations between these models at different levels of abstraction. Although we use SPECC modeling examples to illustrate our technique, our methodology is generic and language-independent and the model that supports it conceptually minimal by offering a scalable notion and a flexible degree of abstraction.

Introduction

Rising complexity and performances, shortening time-to-market demands, stress high-level embedded system design as a prominent research topic Ad-hoc design methodologies, that lifts modeling to higher levels of abstraction, the concept of intellectual property, that promotes reuse of existing components, are essential steps to manage design complexity, gain performance, accelerate design cycle. However, the issue of compositional correctness arises with these steps. Given components from different manufacturers, designed at different levels of abstraction and with heterogeneous models of computation, combining them in a correct-by-construction manner is a difficult challenge.

A gating factor for widespread adoption of the system-level design paradigm is a lack of formal models, method and tools to support refinement. In the absence of adequate behavioral synthesis techniques, the refinement of a system-level description toward its implementation is primarily a manual process. Furthermore, proving that the implementation preserves the properties of the higher system-level design abstraction is an unsolved problem.

In this aim, system design based on the so-called "synchronous hypothesis" [START_REF] Benveniste | The synchronous languages twelve years later[END_REF] consists of abstracting the non-functional implementation details of a system away and let one benefit from a focused reasoning on the logics behind the instants at which the system functionalities should be secured. From this point of view, synchronous design models and languages provide intuitive models for integrated circuits. This affinity explains the ease of generating synchronous circuits and verify their functionalities using compilers and related tools that implement this approach.

In the relational model of the POLYCHRONY workbench [START_REF]The Polychrony workbench[END_REF], this affinity goes beyond the domain of purely synchronous circuits to embrace the context of globally asynchronous locally synchronous (GALS) architectures. The unique features of this model are to provide a scalable capability to describe partially clocked specifications or multi-clocked architectures and to support a formal notion of design refinement, from the early stages of requirements specification, to the later stages of deployment and synthesis, using formal verification.

We address the issue of conformance checking in system design by considering the polychronous model of computation of the POLYCHRONY workbench to define a formal refinement-checking methodology. Our approach builds upon previous work on the multi-clocked synchronous paradigm of SIG-NAL [START_REF] Benveniste | Synchronous programming with events and relations: the SIGNAL language and its semantics[END_REF] and verification using the related model-checking tool SIGALI [START_REF] Marchand | Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller[END_REF] (the POLYCHRONY workbench). We put the polychronous model of computation [START_REF] Le Guernic | Polychrony for system design[END_REF] to work in the context of emerging highlevel design languages such as SPECC [START_REF] Gajski | SPECC: Specification Language and Methodology[END_REF] by the study of refinement relations between system design levels in SPECC (Figure 1). Outline This paper is organized as follows. We start with an overview of the polychronous model of computation in Section 2. In Section 3, we provide an informal introduction to the SIGNAL dataflow notation of the POLYCHRONY workbench. Starting from this presentation, Section 4 develops a methodology aimed at checking design refinement relations correct within the POLYCHRONY workbench by introducing a suitable notion of flow-preservation. This model and methodology are put to work in Section 5 in the context of system design using SPECC. A simple design example of an even-parity checker (EPC) is used as a vehicle to explain our methodology. We outline a technique to automatically derive a model of SPECC specifications in the POLYCHRONY workbench and apply our methodology to checking the refinement of the EPC correct from its specification level design to its RTL-level design. This exercise demonstrates the capability of POLYCHRONY to support high-level design transformations operated on SPECC programs with the validation services offered by the POLYCHRONY workbench.

A Polychronous Model of Computation

We start with a brief overview of the polychronous model of computation, proposed in [START_REF] Le Guernic | Polychrony for system design[END_REF]. The polychronous model of computation consists of a domain of traces and of semi-lattice structures that render synchrony and asynchrony using timing equivalence relations: clock equivalence relates traces in the synchronous structure and flow equivalence relates traces in the asynchronous structure.

Domain of polychrony

We consider a partially-ordered set (T , ≤, 0) of tags. A tag t ∈ T denotes a symbolic period in time. The relation ≤ denotes a partial order. Its minimum is noted 0. We note C ∈ C a (possibly infinite) chain of tags. Events, signals, behaviors and processes are defined as follows:

Definition 2.1. (polychrony) -An event e ∈ E = T × V is the pair of a value and a tag. -A signal s ∈ S = C → V is a function from a chain of tags to a set of values.

-A behavior b ∈ B is a function from names x ∈ X to signals s ∈ S.

-A process p ∈ P is a set of behaviors that have the same 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 1 . Even tags of y, e.g. t 2 , are ordered along its chain, e.g. x :

• t 1 • • y : • t 1 • t 2 • • • z : • t 3 • • • Figure 2.
A behavior in the polychronous model of computation

In the remainder, we write tags(s) and tags(b) = ∪ x∈vars(b) tags (b(x)) for the tags of a signal s and of a behavior b, b| X for the projection of a behavior b on X ⊂ X and b/X = b| vars(b)\X for its complementary, vars(b) and vars(p) for the domains of b and p. We write B| X for the set of all behaviors defined on the set of variables X.

Synchronous composition is noted p | | q and defined by the union of all behaviors b (from p) and c (from q) which are synchronous: all signals they share, i.e. in I = vars(p) ∩ vars(q), are equal.

p | | q = {b ∪ c | (b, c) ∈ p × q, I = vars(p) ∩ vars(q), b| I = c| I }
Figure 3 depicts the synchronous composition, right, of the behaviors b, left, and the behavior c, middle, of two processes p and q. Notice that the signal y, shared by p and q, must carry the same tags and the same values in both p and q in order for b ∪ c, right, to belong to p | | q.

  

x :

• t 1 • y : • t 1 • t 2 • •    | |    y : • t 1 • t 2 • • z : • t 3 • •    =    x : • t 1 • y : • t 1 • t 2 • • z : • t 3 • •    Figure 3. Synchronous composition of b ∈ p and c ∈ q
Scheduling structure To render constraints between the occurrence of events during a period t, we refine the domain of polychrony with a scheduling relation. Figure 4 depicts a scheduling relation superimposed to the signals x and y of Figure 2. The relation y t 1 → x t 1 denotes a scheduling constraint: y should be calculated before x at the period t 1 .

x :

• t 1 • • ↑ ↑ ↑ y : • t 1 • t 2 • • • Figure 4.
Scheduling relations between simultaneous events

The pair x t of a time tag t and of a signal name x renders the date d of the event occurring at the symbolic period t along the signal x. The tag t represents the period during which multiple events take place to form a reaction. It corresponds to an equivalence class between dates d, as in the synchronous structures [START_REF] Nowak | Synchronous structures[END_REF].

Definition 2.2. (scheduling relation)

The scheduling relation → b is a pre-order defined on dates D = X × T for a behavior b which satisfies:

∀b ∈ B, ∀x ∈ vars(b), ∀t, t ∈ tags(b(x)), t < t ⇒ x t → b x t ∧ x t → b x t ⇒ ¬(t < t)
When no ambiguity is possible on the identity of b in x → b y, we write it x → y. A scheduling relation is implicitly transitive (x t → b y t → b z t implies x t → b z t ) and its closure for restriction b/X is defined by x t → b/X y t iff x t → b y t and x, y ∈ X.

Synchronous structure Building upon the domain of polychrony, we define the semi-lattice structure which relationally denotes synchronous behaviors. The intuition behind this relation is depicted figure 5. 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 and 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 the figure 5, the time scale of x and y change but the partial timing and scheduling relations are preserved. Stretching is a partial-order relation which defines clock equivalence (definition 2.3).

x :

• t 1 • • ↑ ↑ ↑ y : • t 1 • t 2 • • • ≤ x : • t 3 • • ↑ ↑ ↑ y : • t 3 • t 4 • • • Figure 5.
Relating synchronous behaviors by stretching.

Definition 2.3. (clock equivalence)

A behavior c is a stretching of b, written b ≤ c, iff vars(b) = vars(c) and there exists a bijection on tags x has been shifted (and its scheduling constraint with an initially synchronous event along y lost) as the effect of delaying its transmission using e.g. a FIFO buffer.

f which satisfies ∀t, t ∈ tags(b), t ≤ f (t) ∧ (t < t ⇔ f (t) < f (t )) ∀x, y ∈ vars(b), ∀t ∈ tags(b(x)), ∀t ∈ tags(b(y)), t x → b t y ⇔ f (t) x → c f (t ) y ∀x ∈ vars(b), tags(c(x)) = f (tags(b(x))) ∧ ∀t ∈ tags(b(x)), b(x)(t) = c(x)(f (
x : Asynchronous composition is noted p q and defined by considering the partial-order structure induced by the relaxation relation. The parallel composition of p and q consists of behaviors d that are relaxations of behaviors b and c from p and q along shared signals I = vars(p) ∩ vars(q) and that are stretching of b and c along the independent signals of p and q.

• t 1 • • ↑ ↑ ↑ y : • t 1 • t 2 • • • x : • t 3 • • y : • t 4 • t 5 • • •
p q = d ∈ B| vars(p)∪vars(q) | ∃(b, c) ∈ p × q, d/I ≥ b/I ∧ d/I ≥ c/I ∧ b| I d| I ∧ d| I c| I }
Figure 7 depicts the asynchronous composition, right, of the behavior b ∈ p, left, and of the behavior c ∈ q, middle. Notice that the signal x and y are alternated in p, left, and synchronous in q, middle. Asynchronous composition allows for these signals to be independently stretched in both p and q in order to find a common flow in the asynchronously composed process, right.

  

x :

• t 1 • t 3 y : • t 2 • t 4       x : • t 1 • t 2 y : • t 1 • t 2 z : • • •    =    x : • • y : • • z : • • •   

A Polychronous Design Language

In the POLYCHRONY workbench, the polychronous model of computation is implemented by the multiclocked synchronous data-flow notation SIGNAL [START_REF] Benveniste | Synchronous programming with events and relations: the SIGNAL language and its semantics[END_REF]. It will serve as the specification formalism used for the case study of the present article.

Core syntax and semantics

In SIGNAL, a process P consists of the composition of simultaneous equations x := f (y, z) over signals x, y, z. A signal x ∈ X is a possibly infinite flow values v ∈ V sampled at a discrete clock noted ^x.

P, Q ::= x := y f z | P/x | P | | Q (SIGNAL process)
In the polychronous model of computation, Section 2, the denotation of a clock ^x is the domain of the signal associated to x: a chain of tags. We note [[P ]] for the denotation of a process P . The synchronous composition of processes P | | Q consists of the simultaneous solution of the equations in P and in Q. The process P/x restricts the signal x to the lexical scope of P . Native combinators SIGNAL requires four primitive combinators to perform delay x := y$1 init v, sampling x := y when z, merge x = y default z and specify scheduling constraints x → y when ^z, Figure 8. The equation x := y$1 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$1 init v are synchronous: they share the same set of tags t 1 , t 2 , . . . . Initially, at t 1 , the signal x takes the declared value v and then, at tag t n , the value of y at tag t n-1 .

[[P | | Q]] = [[P ]] | | [[Q]]
[ The equation x → y when ^z forces x to occur before y when z is present. In the equation y → x when ^z, for instance, there is no scheduling relation required from x to y unless both x, y, z are present, e.g. at tag t.

[x → y when ^z]]={b ∈ B| x,y,z | ∀t ∈ tags(b(x)) ∩ tags(b(y)) ∩ tags(b(z)), x t → y t } [[x := y$1 init v]]= b ∈ B| x,y tags(b(x)) = tags(b(y)) = C ∈ C, b(x)(min(C)) = v ∀t ∈ C \ min(C), b(x)(t) = b(y)(pred C (t)) [[x := y when z]]= b ∈ B| x,y,z tags(b(x)) = {t ∈ tags(b(y)) ∩ tags(b(z)) | b(z)(t) = true } ∀t ∈ tags(b(x)), b(x)(t) = b(y)(t) ∧ y t → x t ∧ z t → x t [[x := y default z]]=      b ∈ B| x,y,z tags(b(y)) ∪ tags(b(z)) = tags(b(x)) ∈ C ∀t ∈ tags(b(y)), b(x)(t) = b(y)(t) ∧ y t → x t ∀t ∈ tags(b(x))\tags(b(y)), b(x)(t) = b(z)(t) ∧ z t → x t     
y • t 1 ,v 1 • t 2 ,v 2 • t 3 ,v 3 . . . (x := y$1 init v) x • t 1 ,v • t 2 ,v 1 • t 3 ,v 2 . . . y • • • t . . . ↓ (y → x when ^z) x • • t . . . z • • t . . .
The equation 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 1 at t 1 then x holds (t 1 , v 1 ). If y is present (at t 2 or t 3 ) then x holds its value whether z is present (at t 2 ) or not (at t 3 ). The equation 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 2 at t 2 only if y is present with v 2 at t 2 and if z is present at t 2 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 t 2 → x t 2 ← z t 2 . y • • t 2 ,v 2 . . . ↓ (x := y when z) x • t 2 ,v 2 . . . ↑ z • • t 1 ,0 • t 2 ,1 . . . y • t 2 ,v 2 • t 3 ,v 3 . . . ↓ ↓ (x := y default z) x • t 1 ,v 1 • t 2 ,v 2 • t 3 ,v 3 . . . ↑ z • t 1 ,v 1 • . . .

Syntax and semantics of clocks

In SIGNAL, the presence of a value along a signal x is the proposition noted ^x that is true when x is present and that is absent otherwise. The syntax of clock expressions e and clock relations E is a particular subset of SIGNAL that is defined by the induction grammar of Figure 9.

The clock expression ^x can be defined by the boolean operation x = x (i.e. y := ^x= def y := (x = x)).

Referring to the polychronous model of computation, it represents the set of tags at which the signal holds a value. Clock expression naturally represent control, the clock when x represents the time tags at which the boolean signal x is present and true (i.e. y := when x= def y := true when x). The clock when not x represents the time tags at which the boolean signal x is present and false. We write 0 for the empty clock (the empty set of tags).

Hierarchization

The clock and scheduling constraints E of a process P hold the necessary information to decide the property of endochrony [START_REF] Le Guernic | Polychrony for system design[END_REF]. The process accepts flow-equivalent inputs x and y (left). Inputs are processed by p in clock equivalent ways (middle) so as to produce the same outputs in the same order at clock-equivalent rates (right). Clock constraints determine the order in which events are processed endochronously, definition 3.1. Rule 1 defines equivalence classes for signals of equivalent clocks. Rule 2 constructs elementary partial orders relations: the clock when x is smaller than ^x. Rule 3 defines the insertion of a partial order of maximum e 3 under a clock e e 3 . The insertion algorithm, specified in [START_REF] Amagbegnon | Implementation of the data-flow synchronous language SIGNAL[END_REF], yields a canonical representation of the corresponding partial order by observing that there exists a unique minimum clock e below e such that 3 holds. We write E ⇒ E iff E is a proposition that is deductible from E in the semi-lattice of clocks.

x :• • • ↓ y : •••• • input buffer • • • ↓ ↓ ↓ • • • • • endochronous process p • • • : z x :• • • y : •• • • • input buffer • • • ↓ ↓ ↓ • • • • • endochronous process p • • • : z
E is hierarchical iff its clock relation has a minimum, written min E ∈ vars(E), so that ∀x ∈ vars(E), ∃y ∈ vars(E), y

x. H is acyclic iff E ⇒ x → x when e implies E ⇒ e^= 0 (for all x ∈ vars(E)). In [START_REF] Le Guernic | Polychrony for system design[END_REF], we show that if P : E and if E is acyclic and hierarchical, then P is endochronous. Example The implications of definition 3.1 can be outlined by considering a simple SIGNAL program, Figure 12, left. Process buffer implements two functionalities. One is the process current. It defines a cell in which values are stored at the input clock ^i and loaded at the output clock ^o. cell is a predefined SIGNAL operation defined by:

x := y cell z init v def = (m := x$1 init v | | x := y default m | | ^x^= ^y ^+ ^z) /m
The other functionality is the process alternate which desynchronizes the Some more concrete syntax In addition to the core syntax of SIGNAL presented so far, we make extensive use of process declarations and partial equations for the purpose of modeling our case study. In SIGNAL, a partial equation x ::= y f z when e is the partial definition of the variable x by the operation y f z at the clock denoted by the expression e. The default equation x ::= defaultvalue v defines the value of the variable x when it is present but no corresponding partial equation x ::= y f z when e applies (because e is absent). Let x be a variable defined using n partial equations and a default value v: x := (x 1 when e 1 ) default . . . default (x n when e n ) default v

In SIGNAL, the declaration of a process P of name f , input signals

x 1 , . . . x m , output signals x m+1 , . . . x n is noted process f = (? x 1 , . . . x m ! x m+1 , . . . x n ) (| P |);
Once declared, process f may be called (y m+1 , . . . y n ) := f (y 1 , . . . y m ) with its actual parameters y 1 , . . . y n and behave as P with x 1,...n substituted by y 1,...n . A variant declaration is that of a foreign function f , accessible, e.g. from a separately compiled C library. Its call can be wrapped into SIGNAL by declaring its interface and by declaring an abstraction E of its behavior (consists of scheduling and clock constraints).

process f = (? x 1 , . . . x m ! x) spec (| E |) pragmas C CODE"&x = f(&x 1 , . . . &x m )" end pragmas;

A Refinement Checking Methodology

The definition of the polychronous model of computation [START_REF] Le Guernic | Polychrony for system design[END_REF] accurately renders the synchronous hypothesis implemented in the multi-clocked data-flow notation SIGNAL and relates it to architectures using communication with unbounded delay. In an embedded architecture, however, the flow of a signal usually slides from another as the result of finite delays incurred by resource-bounded protocols, e.g. fifo buffers. In this section, we seek towards a formulation of the formal properties implied by this practice to check correctness of a concrete design refinement methodology.

Finite relaxation

We start from the model of a one-place fifo buffer in SIGNAL, Figure 13, which we will use to draw the spectrum of possible timing relations considered, modelled and checked in the context of the present case study. The processing of process fifo is decomposed into two functionalities. One is the process access which defines the necessary timing constraints on the input signal i and output signal o via the delayed value of the boolean signal b: fifo can accepts an input at the next time sample iff b is true.

y := fifo(x) d(x) : • • • ↓ ↓ ↓ d(m) : • • •→• ↓ ↓ d(y) = c(x) : • • • Figure 14.
Relation between events through a one-place FIFO buffer Definition 4.1 formalizes this relation and accounts for the behavior of fifo by implying a series of (reflexive-anti-symmetric) relations N (for N > 0) which yields the (series of) reflexive-symmetric flow relations ≈ N to identify processes of same flows up to a flow-preserving first-in-first-out buffer of size N . In Definition 4.1, we write pred C (t) (resp. succ C (t)) for the immediate predecessor (resp. successor) of the tag t in the chain C. This guarantees the independence or exclusion between the clocks of i and o. Each tag t i of an event along o can only happen strictly between the tags t i and t i+1 of two consecutive events along i, i.e. t i < t i < t i+1 , and vice-versa. (

∀t ∈ C, t ∈ tags(d(x)) ⇒ d(m)(t) = d(x)(t) t ∈ tags(d(x)) ⇒ d(m)(t) = d(m)(pred C (t)) t ∈ tags(c(x)) ⇒ c(x)(t) = d(m)(t) and satisfying ∀t ∈ tags(c(x))∃t ∈ {t, succ C (t)}, c(x)(t ) = d(x)(t).
process alternate = (? i, o ! ) (| b := not (b$1 init true) | i ^= when b | o ^= when not b |) / b process buffer = (? i ! o) (| alternate (i, o) | o := current (i) |) i: • • b: • • • • o: • •
(x) = (t i , v i ) i≥0 , c(x) = (t i , v i ) i≥0 and, for all i ≥ 0, t i < t i < t i+1 .
) ∀b ∈ [[x := fifo(y)]], [z → b(y)] z 1 [z → b(x)] (2) ∀b ∈ [[x := buffer(y)]], [z → b(y)] z [z → b(x)] 1
Formal properties The series of relations (≈ n ) n≥0 defines a spectrum between synchrony and asynchrony that can be modeled using the SIGNAL formalism. It is hence tempting to interpret the asynchronous partial-order as the (inaccessible) limit or union ∪ N ≥0 N of this series.

(finite flow-invariance)

The refinement of p by q is finitely flow-invariant, written p * q, iff I ⊂ vars(p) = vars(q) and ∀(b, c) ∈ p × q, (b|

I )≈(c| I ) ⇒ b ≈ * c.
The property of finite flow-invariance is a very general methodological criterion. It is reflexive (p * p) and transitive (p * q * r ⇒ p * r) for all flow-preserving processes (p, q, r). For instance, it can be applied to the characterization of correctness criteria for model transformations such as protocol insertion or desynchronization.

Verification methodology Property 4.1 provides all necessary elements to define an observer giving sufficient conditions for finite flow-preservation to hold and be provable by model checking. To this end, we consider the template SIGNAL process observer of Figure 16. It is parameterized by the notation {P, Q} over two processes named P and Q which we want to check finitely flow-equivalent. The observer receives an input signal i. This input signal is used to generate two desynchronized signals (i.e. satisfying the hypothesis b| i ≈ c| i ) by using the process buffer. The flows b| i and c| i are injected to P and Q and the outputs collected by using fifo to avoid the synchronization of the outputs performed by the comparison =. If the output of the observer is always true then the equality is an invariant. For the sake of simplicity, process observer is displayed Figure 16 for two processes P and Q that have only one input and one output signal and with a fifo buffer of length 1. Extending the observer to accept processes with m inputs, n outputs and a buffer of lenght k is obtained by structural induction starting from fifo and buffer. Theorem 4.1 formalizes the implication of processobserver for refinement checking by considering flow-preserving processes P and Q of same cardinality i.e. vars(P ) = vars(Q) and in(P ) = in(Q).

Formal Methods for Refinement-Based Besign in SPECC

The model and method presented in Sections 2 and 4 are applied to checking refinements between design abstraction-levels correct. Section 5.2 proposes a technique to automatically represent SPECC programs in the POLYCHRONY workbench. Section 5.3 applies the methodology of Section 4 to formally establish the correctness of design refinements (Figure 17). We consider a simple SPECC programming example as case study to illustrate our methodology. It demonstrate the usability of the POLYCHRONY workbench to provide the needed model, method and tool to automatically derive conditions on specifications, verifiable by static checking or model checking, and under which the refinement of a high-level specification by its lower-level implementation can be formally checked, in a manner that is independent of a particular formalism (we consider SPECC in [START_REF] Talpin | Polychrony for formal refinementchecking in a system-level design methodology[END_REF], JAVA in [START_REF] Talpin | Hard real-time implementation of embedded software in JAVA[END_REF], SYSTEMC in [START_REF] Talpin | A behavioral type inference system for compositional system design[END_REF]). Larger case studies applied to concrete examples (e.g. a finite input response filter and an ARM bus) are currently under way to demonstrate the capability of our technique to provide modular verification and an environmnent for co-simulation. In particular, modular verification is envisaged by considering the verification of a property in a system by checking it against the model of the very components that affects it while considering a static abstraction (in terms of clock and scheduling constraints) of all other components in the system under validation. Cosimulation is being investigated by considering the controller synthesis techniques provided in the POLYCHRONY workbench and with the aim of applying them to the generation of optimized and control-sensitive simulators for large SYSTEMC designs.

Refinement-Based Design in SPECC

The SPECC system-level design methodology is depicted in Figure 18. It is based on the concept of refinement: an initial system model is gradually refined through transformations performed at several levels of abstraction: specification, architecture, communication, and implementation. System design starts with a set of requirements and constraints, both in terms of functionality and quality, possibly captured in different models of computation.

The specification level describes the system functionality in a unified way as a starting point for system synthesis. At the architecture level, the system functionality is partitioned and partitions are assigned to different components. In the process, the computational parts of the system are ordered based on execution times and a scheduling of computation on each component. At the communication level, components are refined into bus-functional representations, which accurately describe the timing of events on the wires of the busses. Finally, at the implementation level, the components are defined in terms of their register-transfer or instruction-set architecture.

Modeling SPECC Behaviors in SIGNAL

The formal grammar of SPECC programs under consideration, Table 19, is represented in static singleassignment intermediate form akin to that of the Tree-SSA package of the GCC project [START_REF]The GCC Tree-SSA Branch[END_REF]. SSA provides a language-independent, locally optimized intermediate representation (Tree-SSA currently accepts C, C++, Fortran 95, and Java inputs) in which language-specific syntactic sugar is absent. SSA transforms a given programming unit (a function, a method or a thread) into a structure in which all variables are read and written once and all native operations are represented by 3-address instructions.

An intermediate representation A program pgm consists of a sequence of labeled blocks L:blk . Each block consists of a label L and of a sequence of statements stm terminated by a return statement rtn. In the remainder, a block always starts with a label and finishes with a return statement: stm 1 ; L:stm 2 is rewritten as stm 1 ; goto L; L:stm 2 . A wait is always placed at the beginning of a block: stm 1 ; wait v; stm 2 is rewritten as stm 1 ; goto L; L:wait v; stm 2 . Block instructions consist of native method invocations x = f (y * ), lock monitoring and branches if x goto L. Blocks are returned from by either a goto L, a return or an exception throw x. The declaration catch x from L 1 to L 2 using L 3 that matches an exception x raised at block L 1 activates the exception handler L 3 and continues at block L 2 . We depict the structure of the SSA for a typical SPECC program by considering the core of the EPC, Figure 20. The behavior ones counts the number of bits set to 1 in a bit-array data. It consists of three blocks. The block labeled L1 waits for the lock istart before initializing the local state variable idata to the value of the input signal data and icount to 0. Label L2 corresponds to a loop that shifts idata right and adds its right-most bit to icount until termination (condition T2). Finally, in the block L3, icount is sent to the signal ocount and idone is unlocked before going back to L1. 22, implements the translation from SSA to SIG-NAL. It was first developed for the JIMPLE intermediate representation of JAVA [START_REF] Talpin | Hard real-time implementation of embedded software in JAVA[END_REF], then redesigned and adapted to the wider spectrum of programming languages admitting the SSA intermediate representation [START_REF]The GCC Tree-SSA Branch[END_REF] and its used exemplified for SYSTEMC in [START_REF] Talpin | A behavioral type inference system for compositional system design[END_REF].

To each block of label L ∈ L f , the function I[[pgm]] associates an input clock x L and an output clock x exit L . The clock x L is true iff L has been activated in the previous transition. The boolean signal x exit L is true iff execution of block L is terminates. The default activation condition of a block is hence x L $1 (equation (1) of Table 22). For a return instruction or for a block, function I returns a type P . For a block instruction stm, function I[[stm]] e 1 L = P e 2 takes three arguments: an instruction stm, the label L of the block it belongs to, and an input clock e 1 . It returns the type P of the instruction and its output clock e 2 . The output clock of stm corresponds to the input clock of the instruction that immediately follows it in the execution sequence of the block.

For instance, consider block L2 of behavior ones, Figure 21. The instruction T1 = idata, left, is associated with the partial equation T1 ::= idata$1 when L2$1, right. It means that, if the label L2 is being executed, then T1 is equal to idata$1. Next, consider instruction if T2 goto L3. It corresponds to the partial equation L3 ::= true when T2. It means that control is passed to L3 when T2 is true. Instructions that follow are conditioned by the negative not T2 to means: "in the block L2 and not in its branch going to L3". (1) The generic type of f is taken from an environment E(f ). It is given the name of the result x, of the actual parameters y 1...n and of the input clock e to obtain the type of x = f (y 1...n ).

I[[L:blk ; pgm]] =I[[blk ]] x L $1 L | | I[[pgm]] (2) I[[stm; blk ]] e L =let P e 1 = I[[stm]] e L in P | | I[[blk ]] e 1 L (3) I[[x = f (y 1...n )]] e L = E(f )(x 1...n e) e (
For instance, Figure 23 depicts the translation of native operations in block L2 of behavior ones. The assignment of icount to the local variable T3 is translated by the partial equation T3 ::= icount$1 when not T2 which assigns the previous value of icount to the temporary T3 at the clock not T2 (i.e. when T1 is not 0, Figure 21). The input and output clocks of an instruction may differ. This is the case, rule (4), for an if x goto L 1 instruction in a block L. Let e be the input clock of the instruction and define the fresh signal name y by the equation y := x when e. When y is false, then control is passed to the rest of the block: the output clock is not y. Otherwise, the control is passed to the block L 1 at the clock y. The wait-notify protocol, rules (5 -6), is modeled using a boolean flip-flop variable x. Method notify, rule (5), defines the next value of the lock x by the negation of its current value at the input clock e. The wait method, rule (6), activates its output clock y iff the value of the lock x has changed at the input clock e. Otherwise, control goes back to L.

For example, consider the wait-notify protocol at the blocks labeled L1 and L3 in the ones counter. The wait instruction receives control at the clock x L1 . If the value of istart changes (i.e. when not T0) then icount and idata are initialized and the control is passed to the block L2. Otherwise, at the clock when T0, a transition back to L1 is scheduled. of the current block L by their input clock e. This is the right place to do that: e defines the very condition upon which the block actually reaches its return statement. A goto L 1 instruction, rule [START_REF] Benveniste | Synchronous programming with events and relations: the SIGNAL language and its semantics[END_REF], passes control to block L 1 unconditionally at the input clock e. A return instruction, rule [START_REF] Berry | The ESTEREL synchronous programming language: design, semantics, implementation[END_REF], sets the exit clock x f to true at clock e to inform the caller that f is terminated. A throw x statement in block L, rule (9), triggers the exception signal x at the input clock e by x ::= true when e. The matching catch statement, of the form catch x from L to L 1 using L 2 passes the control to the handler L 2 and then to the block L 1 upon termination of the handler. This requires, first, to activate L 2 from L when x is present and then to pass control to L 1 upon termination of the handler.

Completion Table 22 requires all entry clocks x L and x f to be simultaneously present when the f is being executed. Each signal x L holds the value true iff the block L is active during a transition currently being executed. Otherwise, x L is set to false by L ::= defaultvalue false. The same holds for local variables T with the default equation T ::= defaultvalue T$1. The SIGNAL compiler guarantees the completion of the next-state logic by aggregating partial equations. The translation technique proposed in [START_REF] Talpin | Hard real-time implementation of embedded software in JAVA[END_REF][START_REF] Talpin | A behavioral type inference system for compositional system design[END_REF] is modular (block-wise), conceptually simple (one equation perinstruction) and language-independent (SSA is the input formalism). The host formalism, SIGNAL, supports a scalable notion and a flexible degree of abstraction. Notice that the structure of the original program is represented by program labels L which play an essential role during modeling as they represent clocks, i.e. the data-structure used by the POLYCHRONY workbench to represent the control flow of programs. This information is propagated during modeling, verification and transformation. As a result, traceability is easily provided by this information to relate an error to its original block, in addition to the name of all variables it implies.

A Case Study: the Even-Parity Checker

We focus on a simple SPECC programming example: an even-parity checker (EPC, figure 26), to illustrate our refinement-based methodology. We shows how the specification of the EPC can be refined toward a GALS implementation with the help of the tool POLYCHRONY, showing in what respects and at which critical design stages formal methods matter for engineering its architecture. This example demonstrates the capabilities of the polychronous model of computation of SIGNAL to provide formal modeling and verification support for the capture of behavioral abstractions of high-level system descriptions. The even-parity checker (EPC), Figure 26, consists of three functionalities: an interface thread IO, a master test thread even and a slave counting thread ones (gray elements are SPECC-specific). Numbers are sent from IO to even via the input port In. Then, IO notifies start to even which forwards In to ones via the data port. Upon notification istart, ones counts the number of bits set to one in data and returns it to even via the ocount port. Upon notification idone, even forwards the result to IO via port Out and notifies done.

Specification-Level Design in SPECC

In SPECC, the design level of specification defines the functionalities and behavior of a system composed of hardware and software by means of parallel threads (called behaviors) of computations exchanging data via ports and synchronized by wait and notify events. Behavior ones, Figure 27, first waits the event istart before to load data from the input port data into the variable idata. Then, it iteratively scans idata to count the number of bits set to one in it. This is done by shifting the bits in idata right and by comparing the right-most one to 1. When the data is processed (it equals 0 and there is no more bit to shift and count) the internal count icount is returned to the ocount port and the event idone is notified. The behavior even passes values from port In to port data, notifies istart, waits idone, and returns either 0 (if ocount is odd) or 1 (it is even) along the port Out before to notify Done. In state L1, behavior ones waits for istart. It receives it at clock when not T0 and initializes idata to data, icount to 0 and steps to state L2. While in state L2 (at clock when not T2) it adds the right-most bit of idata to icount, shifts idata right and goes back to L2. If idata is zero (at At specification-level, data exchange between the behaviors ones and even is performed by shared variables and arbitrated by a wait-notify protocol. At architecture-level, this protocol is refined by a double handshake protocol defined by the methods send and recv of the module ChMP, figure 29. The channel encapsulates the wait and notify operations performed in the specification model together with locally shared variables ack and ready.

Model of the Specification-Level Design in SIGNAL

Model of the Architecture Refinement in SIGNAL

The SIGNAL model of the send method, Figure 30, of the recv method, of the architecture-layer refinement of the EPC, are obtained in the very same way as for the behaviors even and ones of the specification level. The send method of the ChMP module assigns the current value of the input In to the shared variable data, sets the shared ready flag to true and waits for the notification eAck from the recv process until the shared flag ack becomes true. The same transaction is repeated to wait until the transmission of its return data to ready a new transaction.

Process send receives two parameters L1 and L7 in addition to its input data In. The boolean signal L1 is true when send receives control from its caller. The boolean signal L7 is true when send returns control to its caller. Appendix B gives the complete listing of the send and recv functionalities of the channel ChMP which were checked endochronous using the POLYCHRONY workbench to qualify for validation using our refinement checking methodology.

Validation of the Specification-to-Architecture Refinement

The installation of a channel between the processes even and ones incurs an additional desynchronization of the transmission between the In and Out signals. Showing that the refinement of the EPC from the specification level, process epc1, to the architecture level, process epc2, is correct requires checking that the refinement is finitely flow-invariant: epc1 * epc2.

The verification of this property amounts to proving that, for all behaviors b and c of epc1 and epc2, flow equivalence of the input signal In, i.e. b| In ≈ c| In implies flow equivalence of the output signal Out, i.e. b| Out ≈ c| Out .

(

) : ∀b ∈ [[epc1]], ∀c ∈ [[epc2]], b| In ≈ c| In ⇒ b| Out ≈ c| Out 1
Preliminary observations are in order to facilitate the proof of equation [START_REF] Abramsky | Interaction categories and the foundations of typed concurrent programming[END_REF]. The architecture model of the EPC only differs from the specification model by the introduction of a channel in place of a wait-notify protocol to synchronize concurrent accesses to shared variables. By contrast, the architecture model epc2 uses the double handshake protocol of the send and recv functionality of the module ChMP.

Figure 31 isolates the pattern specif that characterizes the wait-notify protocol in the specification model. The variables of the EPC models specif and archi are interfaced to signals In and Out for the purpose of verification. The producer and consumer processes prod1 and cons1 are defined by infinite loops that wrap the patterns of interest. Figure 32 isolates the matching communication pattern of the architecture model wrapped in the process archi. In Figure 31, the presence of an input In triggers a wait-notify protocol that synchronizes the transmission of data from even to ones. In Figure 32, this synchronization is embedded in the call to the send and recv methods. Control to and from send and recv is provided by the labels L2 and L3. The additional label L1 closes the infinite loop.

Conclusive Remarks

By considering a simple SPECC programming example, featuring all salient aspects of the language, we demonstrated the capability of the POLYCHRONY workbench to model the functionalities and the architecture of a system and to provide the necessary services to express model transformations and check them correct. The methodology of finite-flow invariance we employ is directly derived from previous work pertaining on the design of globally asynchronous locally synchronous architectures. The present case study departs from the very spectrum of GALS design by showing that imperative programs in the style of communicating sequential processes are equally covered. In other words, flow equivalence does not define the spectrum of architectures that are covered by our methodological principles but the very criterion for checking design refinements correct.

Naturally, other criteria can be designed and other properties checked. The POLYCHRONY workbench provides scalable abstraction of SPECC design for verification. Previous results and case studies span from the use theorem-proving [START_REF] Kerboeuf | The steam-boiler problem in SIGNAL-COQ[END_REF][START_REF] Nowak | Co-inductive axiomatization of a synchronous language[END_REF][START_REF] Kerboeuf | Formal proof of a polychronous protocol for loosely timetriggered architectures[END_REF] to prove properties on concrete models, model checking [START_REF] Benveniste | A protocol for loosely time-triggered architectures[END_REF][START_REF] Talpin | Polychrony for formal refinementchecking in a system-level design methodology[END_REF] to prove properties on models abstracted by finite-state machines, static checking [START_REF] Nowak | An ML-like module system for the synchronous language Signal[END_REF][START_REF] Talpin | A behavioral type inference system for compositional system design[END_REF] to prove properties over state-less boolean model abstractions. POLYCHRONY further provides means to optimally reuse, adapt, transform pre-defined system components and modules: hierarchization (combines several threads into one), distributed protocol synthesis (split synchronous threads into a network of communicating threads). Its current limitations are the absence of support for reasoning on dynamic resources management (memory or threads) and the lake of connexions to other models of computation (untimed, real-timed, continuous).

Related Works

Synchronous programming being a computational model which is popular in hardware design, and desynchronization being a technique to convert that computational model into a more general, globally asynchronous and locally synchronous computational model, suitable for system-on-chip design, one may naturally consider investigating further the links between these two models understood as Ptolemy domains [START_REF] Buck | Ptolemy: A Framework for Simulating and Prototyping Heterogeneous Systems[END_REF] and study the refinement-based design of GALS architectures starting from polychronous specifications captured from heterogeneous elementary components.

Models of computation

The aim of capturing both synchrony and asynchrony in a unifying model of computation is shared by several approaches: the interaction categories of Abramsky et al. in [START_REF] Abramsky | Interaction categories and the foundations of typed concurrent programming[END_REF], the communicating sequential processes of Hoare [START_REF] Hoare | Communicating sequential processes[END_REF] and Kahn networks [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF] (communicating data-flow functions) that is one of the models supported by Ptolemy [START_REF] Lee | A framework for comparing models of computation[END_REF] and the methodology of latency insensitive protocols of Carloni et al. [START_REF] Carloni | Latency-Insensitive Protocols[END_REF] and its extension to real-time [START_REF] Benveniste | Heterogeneous Reactive Systems Modeling and Correct-by-Construction Deployment[END_REF]. All related models can be categorized as stratified, in the sense that they dissociate the semantics structure representing synchronous islands (the predefined pearls or IPs) from the one representing asynchrony. For instance, the heterogeneous model of [START_REF] Benveniste | Heterogeneous Reactive Systems Modeling and Correct-by-Construction Deployment[END_REF] is layered into a model of tag-less asynchrony and of tagged synchrony (where tags model stuttering equivalence in a way akin to clock equivalence yet without scheduling). The polychronous model of computation does not feature such a decoupling between its synchronous and asynchronous structures.

Refinement-checking Most of the existing formal frameworks to refinement-checking, such as B [START_REF] Abrial | The B Book -Assigning Programs to Meanings[END_REF], Unity [START_REF] Chandy | Parallel Program Design: A Foundation[END_REF], CSP [START_REF] Hoare | Communicating sequential processes[END_REF][START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF], are essentially specification-based, in that modeling, transformation and verification are entirely envisaged within the framework of a formal notation and its companion methods and tools. By contrast, our data-flow oriented approach to refinement-checking is novel and allows us to combine a programatic approach (of SPECC) with the scalable modeling and verification techniques of the polychronous model of computation: theorem-proving [START_REF] Kerboeuf | The steam-boiler problem in SIGNAL-COQ[END_REF][START_REF] Nowak | Co-inductive axiomatization of a synchronous language[END_REF][START_REF] Kerboeuf | Formal proof of a polychronous protocol for loosely timetriggered architectures[END_REF], model checking [START_REF] Benveniste | A protocol for loosely time-triggered architectures[END_REF][START_REF] Talpin | Polychrony for formal refinementchecking in a system-level design methodology[END_REF], static checking [START_REF] Nowak | An ML-like module system for the synchronous language Signal[END_REF][START_REF] Talpin | A behavioral type inference system for compositional system design[END_REF]. Being combined to a language-independent translation technique enabling the capture of high-level system descriptions in general purpose languages such as C orJAVA, our workbench departs from specification-oriented approaches, by combining software model-checking capabilities with aggressive optimization services present in this workbench for the purpose of accelerated simulation and synthesis.

Conclusions

Until now, the refinement of a system-level description toward its implementation, in SPECC or SYS-TEMC was primarily envisaged as a manual process and proving conformance from the system-level abstraction to the implementation an unsolved issue. To solve it, we proposed a formal refinement-checking methodology for system-level design formalized within the polychronous model of computation of the multi-clocked synchronous formalism SIGNAL. We demonstrated the effectiveness of our approach by the experimental case study of a SPECC programming example, showing the benefits of our approach to give an accurate model of successive design abstractions of the system: functional, architecture, communication. We introduced, proved and applied a refinement-checking criterion allowing for comparing and validating behavioral equivalence relations between these successive refinements. Our methodology relies on an automated modeling technique that is conceptually minimal and supports a scalable notion and a flexible degree of abstraction. Our presentation targets SPECC yet with a generic and languageindependent method. Applications of our technique range from the detection of local design errors to the compositional design refinement and conformance checking.

Figure 1 .

 1 Figure 1. Checking conformance of a design refinement

Figure 2

 2 Figure 2 depicts a behavior b over three signals named x, y and z in the domain of polychrony. Two frames depict timing domains formalized by chains of tags. Signal 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 1 . Even tags of y, e.g. t 2 , are ordered along its chain, e.g. t 1 < t 2 , but absent from x. Signal z belongs to a different timing domain. Its tags, e.g. t 3 are not ordered with respect to the chain of y, e.g. t 1 ≤ t 3 and t 3 ≤ t 1 .

  t)) b and c are clock-equivalent, written b ∼ c, iff there exists a behavior d s.t. d ≤ b and d ≤ c. Asynchronous structure The asynchronous structure of polychrony is modeled by weakening the clock-equivalence relation to allow for comparing behaviors w.r.t. the sequences of values signals hold regardless of the time at which they hold these values. The relaxation relation allows to individually stretch the signals of a behavior in a way preserving scheduling constraints. Relaxation is a partial-order relation which defines flow-equivalence (definition 2.4). Two behaviors are flow-equivalent iff their signals hold the same values in the same order. Definition 2.4. (flow equivalence) A behavior c is a relaxation of b, written b c, iff vars(b) = vars(c) and, for all x ∈ vars(b), b| {x} ≤ c| {x} . b and c are flow-equivalent, written b ≈ c, iff there exists a behavior d s.t. d b and d c.

Figure 6

 6 Figure 6 depicts two asynchronously equivalent behaviors related by relaxation. The first event alongx has been shifted (and its scheduling constraint with an initially synchronous event along y lost) as the effect of delaying its transmission using e.g. a FIFO buffer.

Figure 6 .

 6 Figure 6. Relating asynchronous behaviors by relaxation.

Figure 7 .

 7 Figure 7. Asynchronous composition of b ∈ p and c ∈ q

  and [[P/x]] = [[P ]]/x = {c ≤ b/{x} | b ∈ [[P ]]} An equation x := y f z denotes a relation between the input signals y and z and an output signal x by a combinator f . An equation is usually a ternary and infixed relation noted x := y f z but it can in general be an m + n-ary relation noted (x 1 , . . . x m ) := f (y 1 , . . . y n ).

Figure 8 .

 8 Figure 8. Semantics of polychronous operators

Figure 9 .Figure 10 .

 910 Figure 9. Clock and scheduling constraints

Figure 11 .

 11 Figure 11. Endochrony: from flow-equivalent inputs to clock-equivalent outputs

Definition 3 . 1 .

 31 The partial order of E is the largest relation satisfying 1. if E ⇒ ^x^= ^y then x y (and y x). 2. if E ⇒ ^x^= when y or E ⇒ ^x^= when not y then y x.3. if y x w and H⇒ ^z = ^yf ^w for any f ∈ { ^+ , ^* , ^-} then x z.x and y are equivalent, written x≺ y, iff x y and y x.

  signals i and o by synchronizing them to the true and false values of an alternating boolean signal b. Clock inference (Figure 12, middle) applies the clock inference system of Figure 10 to the process buffer to determine three synchronization classes. We observe that b, c b, zb, zo are synchronous and define the master clock synchronization class of buffer. There are two other synchronization classes, c i and c o, that corresponds to the true and false values of the boolean flip-flop variable b, respectively. Recalling Definition 3.1, we write: b≺ c b≺ zb≺ zo and b c i≺ i and b c o≺ o This defines three nodes in the control-flow graph of the generated code, Figure 12, right. At the main clock c b, b and c o are calculated from zb. At the sub-clock b, the input signal i is read. At the sub-clock c o the output signal o is written. Finally, zb is determined. Notice that the sequence of instructions follows the scheduling constraints determined during clock inference.

  Figure 12. Specification, clock analysis and code generation

  x ::= x 1 when e 1 | | . . . | | x ::= x n when e n | | x ::= defaultvalue v Once parsed, the SIGNAL compiler processes this definition by first checking the clock expressions e 1 , . . . e n mutually exclusive and then handling the definition as the equivalent equation:

Figure 13 .

 13 Figure13. A one-place first-in first-out buffer in SIGNAL

Definition 4 . 1 .

 41 (finite relaxation) The behavior c is a 1-relaxation of x in b, written b x 1 c iff vars(b) = vars(c) and there exists d/m ≥ b such that d/x = c/x and a chain C = tags(d(m)) = tags(d(x)) ∪ tags(c(x)) such that:

  We write b 1 c iff b x 1 c for all x ∈ vars(b), and, for all n > 0, b n+1 c iff there exists d such that b 1 d n c. Desynchronization Now, recall the process buffer of Figure 12. It essentially differs from process fifo by the policy implemented by process alternate. Process alternate synchronizes i and o to the true and false values of an alternating signal b.

Figure 15 .

 15 Figure 15. A desynchronization buffer in SIGNAL

  The relation between Definitions 4.1 and 4.2 and the implementation of fifo and buffer of Figure13and 15are brought together by the following proposition. The proof of property (1) consists of formulating the four requirements of definition 4.1 by observers written in SIGNAL and of checking them against the model of fifo. Property (2) is proved by observing that all tags of i and o satisfy t i < t i by induction on i and that t i and t i form two disjoint sub-chains of the domain of b. Proposition 4.1.

Lemma 4. 1 .

 1 -b ∼ b implies b ≈ 1 b , -b ≈ n b implies b ≈ b , for all n > 0 -b ≈ m b ≈ n b implies b ≈ m+n b , for all m and n Instead, we focus on the largest equivalence relation that can be modeled using SIGNAL. It consists of behaviors equal up to a timing deformation performed by a finite FIFO protocol. Definition 4.3. (finite flow-equivalence) b and c are finitely flow-equivalent, written b ≈ * c, iff there exists n > 0 and d s.t. d n b and d n c.We say that a process P is finitely flow-preserving iff given finitely flow-equivalent inputs, it can only produce behaviors that are finitely flow equivalent. Example of finitely flow-preserving processes are endochronous processes. An endochronous process which receives finitely flow equivalent inputs produces clock-equivalent outputs. Definition 4.4. (finite flow-preservation) p is finitely flow-preserving with I ⊂ vars(p) iff ∀b, c ∈ p, (b| I )≈(c| I ) ⇒ b ≈ * c. A refinement-based design methodology based on the property of finite flow-preservation consists of characterizing sufficient invariants for a given model transformation to preserve flows. Definition 4.5.

Figure 16 .

 16 Figure 16. Observer function for the property of finite flow-equivalence

Theorem 4 . 1 .

 41 (refinement checking) Let P and Q be finitely flow-preserving processes of same cardinality m = |in(P )| = |in(Q)|. If, for all b ∈ [[x := observer{P, Q}(y 1 , . . . y m )]] and, for all t ∈ tags(b(x)), b(x)(t) = true , then P * Q. Let p = [[P ]] and q = [[Q]] be two flow-preserving processes and let I = in(p) = in(q) be the input signals. By definition of process observer, Figure 16, and by Property 4.1, we have: (1) : ∀b ∈ B| I , ∀(c, d) ∈ p × q, b I c| I ∧ b I d| I ⇒ c ≈ 1 d By hypothesis, p and q are both finitely flow-preserving. By definition 4.4, this requires that c| I ≈ d| I implies c ≈ * d for all (c, d) ∈ p 2 as well as all (c, d) ∈ q 2 . Applied to (1), this hypothesis means that c| I ≈ d| I also implies c ≈ 1 d for all (c, d) ∈ p × q. By lemma 4.1, this yields the result expected in Theorem 4.1, as c ≈ 1 d implies c ≈ * d.

Figure 17 .

 17 Figure 17. Checking conformance of a design refinement

Figure 18 .

 18 Figure 18. SPECC design methodology[START_REF] Gajski | SPECC: Specification Language and Methodology[END_REF]

Figure 19 .

 19 Figure 19. SSA intermediate representation for SPECC programs

Figure 20 .

 20 Figure 20. From SPECC to static single assignment

Figure 21 .

 21 Figure 21. From SSA to SIGNAL

2 Figure 22 .

 222 Figure 22. Modeling of SSA expressions into SIGNAL

Figure 23 .

 23 Figure 23. Translating bative operations in SIGNAL

1 Figure 24 .

 124 Figure 24. Model of wait-notify in the EPC

Figure 25 .

 25 Figure 25. Completion of the next-state-logic for the EPC

Figure 26 .

 26 Figure 26. Functional architecture of an even-parity checker (EPC).

Figure 27 .

 27 Figure 27. Specification-level design of the EPC in SPECC.

Figure 28

 28 Figure 28 gives a model of behavior ones in SIGNAL. It displays partial equations obtained from the translation algorithm of Figure 22. An endochronous SIGNAL program which implements the specification model of the EPC is given Appendix A. It is obtained from Figure 28 by completion of the next-state logics and by the synchronization of local variables.In state L1, behavior ones waits for istart. It receives it at clock when not T0 and initializes idata to data, icount to 0 and steps to state L2. While in state L2 (at clock when not T2) it adds the right-most bit of idata to icount, shifts idata right and goes back to L2. If idata is zero (at

Figure 30 .

 30 Figure 30. Model of the architecture-level channel (send method) in SIGNAL.

Figure 31 .

 31 Figure 31. Isolation of the synchronization protocol in the specification model

Figure 32 .

 32 Figure 32. Isolation of the synchronization protocol in the architecture model

clock when T2), ones steps to L3, passes the value of icount to ocount, notifies idone and goes to L1. Process even depicts a similar decomposition of the SPECC behavior in SSA form.

Architecture-Level Design Refinement

The translation of the even-parity checker of Section 31 demonstrates the capability of SIGNAL to model components for specification-level SPECC designs. The typical SPECC design-flow starts with the capture of IP-blocks represented as C functions and automatic partitioning according to an appropriate cost function. After partitioning, double handshake protocols (message sequence below), or other appropriate HW-SW protocols (request-acknowledge) are inserted between the functional units. since neither In nor Out interfere with control in specif and archi. We obtain the formulation of the appropriate observer function (see appendix C). It is be checked invariant by SIGALI and yields the expected proof of conformance, by application of Theorem 4.1.

(3) : cqfd := observer {specif, archi} (In)

Refinement of the Architecture Model Toward Implementation

The communication layer of the EPC, Figure 33, consists of a refinement of the data structures manipulated in the ChMP channel and of modeling (in SPECC) the behavior of the actual bus of the architecture in place of the channel abstraction ChMP. The model of the bus consists of the decomposition of the methods send and receive into sub-processes that implement the bus read and write methods.

Showing this refinement correct reduces to proving that the model of the channel's ChMP methods send and recv are flow-equivalent to the methods read and write of the bus model. The control structure of the bus model in SIGNAL is identical to that of the channel, except for the implementation of the input/output integer signals as bit-vectors. Compared to the communication model of Figure 33, the RTL or implementation model of the EPC in SPECC, Figure 34, consists of a cycle-accurate implementation of the EPC that is materialized the