Partha S Roop
email: p.roop@ec.auckland.ac.nz

Alain Girault
email: alain.girault@inria.fr

Gregor Goessler
email: gregor.goessler@inria.fr

Roopak Sinha

Specification Enforcing Refinement for Convertibility Verification

Keywords: Protocol conversion, forced simulation, discrete controller synthesis

Protocol conversion deals with the automatic synthesis of an additional component, often referred to as an adaptor or a converter, to bridge mismatches between interacting components, often referred to as protocols. A formal solution, called convertibility verification, has been recently proposed, which produces such a converter, so that the parallel composition of the protocols and the converter also satisfies some desired specification. A converter is responsible for bridging different kinds of mismatches such as control, data, and clock mismatches. Mismatches are usually removed by the converter by disabling undesirable paths in the protocol composition (similar to controllers in supervisory control of Discrete Event Systems (DES)).

We generalize this convertibility verification problem by using a new refinement called specification enforcing refinement (SER) between a protocol composition and a desired specification. The existence of such a refinement is shown to be a necessary and sufficient condition for the existence of a suitable converter. We also synthesize automatically the converter if a SER refinement relation exists. The proposed converter is capable of the usual disabling actions to remove undesirable paths in the protocol composition. In addition, the converter can perform forcing actions when disabling alone fails to find a converter to satisfy the desired specification. Forcing allows the generation of control inputs in one protocol that are not provided by the other protocol. Forcing induces state-based hiding, an operation not achievable using DES control theory.

Introduction

System-on-Chip (SoC) [START_REF] Chang | Surviving the SoC Revolution: A guide to platform based design[END_REF] design involves the interconnection of many pre-designed components, called IPs. While, a Partha Roop was supported by research and study leave from Auckland University and a research fellowship for experienced researchers from the Alexander von Humboldt foundation. Alain Girault was supported by a Marie Curie International Outgoing Fellowship within the 7th European Community Framework Programme. set of selected IPs may meet the functional requirements, their protocols may not be consistent, leading to several kinds of mismatches. The most common types of such mismatches are control, data, and clock mismatches. Control mismatches happen when the sequencing of control signals between protocols is inconsistent. Data mismatches happen when the data-widths of the two protocols differ and additional buffers are needed to manage loss-less data communication. Clock mismatches are common between IPs having different clock frequencies. The first approach to demonstrate the problem and some informal steps for a solution was proposed in [START_REF] Green | Protocol conversion[END_REF]. Many techniques have been proposed since then to solve one or more of these incompatibilities using automated algorithmic techniques [START_REF] Lam | Protocol conversion[END_REF]- [START_REF] Narayan | Interfacing incompatible protocols using interface process generation[END_REF]. Their goal is to synthesize some additional glue logic, termed as a converter/interface/adaptor (from now on termed converter) to bridge these mismatches. While these techniques were automated, they failed to address several questions. These include how to formally model protocols and their interaction, and when such models are available, how to determine if a converter exists for a given set of protocols? Moreover, once the existence of a converter is determined, how to synthesize it? More recently, a set of formal techniques have been proposed [START_REF] Kumar | Protocol conversion using supervisory control techniques[END_REF]- [START_REF] Sinha | Multi-clock SoC design using protocol conversion[END_REF] to address these questions. Table 1 compares these approaches over a range of features. The features listed as columns of Table 1 are: the modelling language for protocols, the language for describing desired specifications, multiple protocols (two and more than two), type of conversion algorithm, whether the approach can handle uncontrollable events, event buffering, whether data-width mismatches are handled, whether clock mismatches are handled, and finally the type of control action used. Among the proposed techniques, most approaches use Labeled Transition Systems (LTS) to describe both protocols and specifications, except [START_REF] Sinha | Multi-clock SoC design using protocol conversion[END_REF] where CTL temporal logic is used for the specification part. Also, except the approach of [START_REF] Silva | Synchronous protocol automata: A framework for modelling and verification of SoC communication architectures[END_REF]- [START_REF] Sinha | Multi-clock SoC design using protocol conversion[END_REF] which use oversampling [START_REF] Halbwachs | Synchronous Programming of Reactive Systems[END_REF] to bridge clock mismatches, all other techniques ignore clock mismatches.

Central to protocol conversion is the use of a suitable controller that is used to remove undesirable paths in the protocol composition. This is done using the well known idea of disabling from Discrete Event Systems (DES) control theory [START_REF] Ramadge | The control of discrete event systems[END_REF]. Here, a supervisor or controller is synthesized to control a plant so that the controlled system (composition of the controller and the plant) satisfies the desired specification. The role of the controller is to disable all controllable paths that violate the specification while leaving uncontrollable transitions untouched. In this domain, the plant and the specification are described as labelled transition systems (LTS) over an alphabet partitioned into controllable and uncontrollable events. While a converter is like a DES controller, the convertibility verification problem is not identical to DES supervisory control. Firstly, in convertibility verification there is a need to buffer events as an event generated by one protocol may be needed by another protocol at a later time. Secondly, there may be data and clock mismatches between protocols that are specific problems not addressed by DES supervisory control. Yet, both domains need to deal with controllable and uncontrollable events. Kumar and Nelvagal proposed a formulation mapping the convertibility verification problem to the DES supervisory control problem [START_REF] Kumar | Protocol conversion using supervisory control techniques[END_REF] in a simplistic setting. Passerone et al. [START_REF] Passerone | Convertibility verification and converter synthesis: Two faces of the same coin[END_REF] developed a game theoretic formulation to solve the convertibility verification problem. Subsequently, in D'Silva et al. [START_REF] Silva | Synchronous protocol automata: A framework for modelling and verification of SoC communication architectures[END_REF] a refinement based solution is developed for checking protocol compatibility. Recently, Sinha et al. [START_REF] Sinha | Multi-clock SoC design using protocol conversion[END_REF] proposed a module checking based solution to the convertibility verification problem. Unlike earlier approaches, this approach bridges control, data-width and clock mismatches. Finally, Tivoli et al. [START_REF] Tivoli | Adaptor synthesis for real-time components[END_REF] proposed a contrasting solution to the same problem that they termed as adaptor synthesis. This formulation ensures that timing constraints are met, events between protocols are adequately buffered, and that the composition is deadlock free. Also, while all other formulation presented in Table 1 use 1-place buffers for event buffering, the approach of [START_REF] Tivoli | Adaptor synthesis for real-time components[END_REF] generalizes this to arbitrary N -place buffers.

Table 1 summarizes the features of all these formal approaches to convertibility verification. A key feature of the existing formal solutions (rows 1 to 5) is that they are based on disabling-based controllers. The last row of the table compares the existing solutions to the solution proposed in this paper. We extend the capability of the controller to allow, not only disabling actions, but also forcing actions [START_REF] Roop | Forced simulation: A technique for automating component reuse in embedded systems[END_REF]. Forcing actions are introduced to solve specific needs of the problem domain, namely the need for state based hiding, which is not possible using conventional disabling-only controllers. We will elaborate on this aspect through a motivating example in the next section.

Example and method overview

Figure 1 shows an overview of the convertibility verification problem. The actual protocols and their composition is shown in Fig. 2. We use CCS [START_REF] Milner | Communication and Concurrency[END_REF] style primed and unprimed symbols to indicate outputs and inputs respectively. E.g., in Figure 1, a is produced by the handshake protocol and read by the serial protocol. At each instant, a protocol can perform an input or output action (e.g., a or a ), or perform a T event, standing for the absence of input and output (written T 1 for P 1 and T 2 for P 2 ). Compared to the example in [START_REF] Passerone | Convertibility verification and converter synthesis: Two faces of the same coin[END_REF], the handshake protocol P 1 has an additional initialization step through an input b that is needed prior to establishing a handshake. Once initialized, P 1 outputs the signal a in the next instant. It then outputs the signal b after some random number of T events, modelled using self loops labelled by T 1 . On the other hand, the serial protocol P 2 expects to read input b immediately in the instant following the reception of a. The synchronous parallel composition of P 1 and P 2 , noted P 1 P 2 , is also depicted in the same figure. We used synchronous parallel composition along with T events to indicate that a given protocol just delays. Other kinds of products, such as the interleaved parallel of CCS [START_REF] Milner | Communication and Concurrency[END_REF], were not considered to avoid non-determinism.

We provide a desired specification as shown in Fig. 3. This specification has a notion of completed transactions through the introduction of marked states (depicted by a double circle). This specification enforces that every input must be preceded by its corresponding output (either in the same or a previous step). Moreover, the transmission and reception of a must precede that of b.

T 1 , T 2 q 0 q 2 T 1 , T 2 T 1 , T 2 a , T 2 q 3 T 1 , T 2 q 4 T 1 , T 2 T 1 , a b , T 2 b , b T 1 , b q 1 a , a

Overview of the proposed methodology:

The handshakeserial protocol pair is a mismatched protocol because of the following reasons:

• Initialization input b required by P 1 is not provided by P 2 at all. • After an a is output by P 1 , P 2 expects a b immediately while P 1 may produce b after any number of T 1 events. Given such mismatching protocols and a desired specification, the goal of convertibility verification is to determine the existence of a converter that can bridge the mismatches, so that the overall system with the converter satisfies the desired specification. The converter can buffer inputs and forward them when necessary; it can also disable controllable paths in the composition. In the example of Fig. 2, P 2 requires a b immediately after having read the input a. Hence, when the protocol composition is in state (s 1 , t 0 ), the converter reads the a produced by P 1 , and forces P 2 to make a T 2 transition during this step. During the next transition, the converter transmits this a to P 2 , while P 1 does a T 1 transition. We therefore say that the converter buffers the event a. In addition to buffering a, the converter also disables all other transitions of (s 1 , t 0 ). In the proposed setting, we limit ourselves to 1-place buffers only for efficient synthesis considerations.

Note that by relying only on the usual converter actions (buffering and disabling), we would not be able to generate a converter for the handshake-serial protocol pair. This is because this protocol pair requires a (b, T 2 ) input in its initial state, while the specification allows the input of b only after the generation and consumption of a has been completed. Also note that the input (b, T 2 ) is not present in the converter's buffers initially. Thus, using conventional techniques based on DES supervisory control, we would fail to produce a correct converter. Hence, we propose a new way to control the protocol composition using a converter, as shown in Figure 4(a). The converter first forces the transition from (s 0 , t 0 ) to (s 1 , t 0 ) by generating the (b, T 2 ) input. These are inputs required by the protocols and are not present in the buffers. Forced inputs are marked within square brackets "[ ]" in the converter to distinguish them from other inputs that are either read from the converters buffers (events generated by the protocols in the past and not been consumed yet), or are directly read from the other protocol in the current instant. Since forced inputs are not produced by any of the protocols and have not been consumed from the buffers, they can be hidden by the composition of the protocols and the converter, thus satisfying the specification.

(s2, t1), q3 (s1, t0), q0 [b, T2] (a , T2) (s2, t0), q2 (s0, t0), q0 (T1, a) (a , a) (T1, T2) (s0, t0), q1 (b , b) (a) Converter for handshake-serial example. cs3 cs1 cs2 cs0 τ (a , T2) (a , a) (T1, T2) (T1, a) (b , b) cs4 (b)
Converter composed with the protocols.

Figure 4. A sample converter and its composition with the protocols

The composition of the converter with the protocols is shown in Fig. 4(b). Note that the forced transition from (s 0 , t 0 ) to (s 1 , t 0 ) is hidden in the composition (hence labelled by τ ). Forcing enables state based hiding, different from global hiding achieved by DES supervisory control (based on the hiding operator of CCS [START_REF] Milner | Communication and Concurrency[END_REF]). For instance, in the composed system of Fig. 4(b), the event b is hidden in the initial state cs0, while it is visible later in the state cs3. This is not directly achievable using DES controllers.

Forcing guides a controlled system to a successor state whenever the current state fails to satisfy the requirements of the specification. Like in DES supervisory control, where only controllable transitions may be disabled, only forceable transitions can be forced, and the user must specify a subset of inputs that can be forced. We elaborate on details of forcing in the next section.

We solve the convertibility verification problem as follows. A protocol pair (P 1 , P 2 ) is said to satisfy a specification S when the language accepted by the synchronous parallel composition of the protocols, L(P 1 , P 2 ) is a subset the specification's one, L(S). We only look at visible traces when checking this, because of forcing actions. Otherwise, the protocols are mismatching. In this case, we propose a new refinement relation from the composite protocols P 1 P 2 to the specification S. We also show that the existence of such a refinement relation is a necessary and sufficient condition for the existence of the converter. Finally, we provide an algorithm to synthesize the converter given such a relation. Our method for protocol conversion is based on DES supervisory control [START_REF] Ramadge | The control of discrete event systems[END_REF] and forced simulation [START_REF] Roop | Forced simulation: A technique for automating component reuse in embedded systems[END_REF]. While we have motivated the proposed method using the case of two protocols, the proposed approach generalizes straightforwardly to an arbitrary number of protocols.

Convertibility verification using specification enforcing refinement

Preliminaries

Error-free communication between protocols implies that traces in the protocol composition always respect the event sequencing described in the specification. We start by introducing the models of the protocols and of the specification.

We model protocols with labelled transition systems (LTS).

Definition 1: An LTS is a tuple

P = Σ, Q, → , q • , where Σ is the alphabet of actions, Q is the set of states, → ⊆ Q × Σ × Q is the transition relation, and q • ∈ Q is the initial state.
The transition relation is also written as q a → q iff (q, a, q ) ∈ →. The language L(P ) is the set of all finite and infinite words generated by the LTS P .

In the case of a protocol, the alphabet Σ is partitioned into the set of input actions Σ I , the set of output actions Σ O , and the singleton {T }: Σ = Σ I Σ O {T }. The event T models the absence of input and output actions. Output events are emitted by the components while input events are received. We use primed symbols to represent output events and unprimed symbols to represent input events. Fig. 2 depicts the LTS of the handshake protocol to the left and that of the serial protocol at the top. The handshake protocol awaits for event b in state s 0 and outputs event a in state s 1 . We term all the events labeling the outgoing transitions from a given state q as Label(q) = {a|∃q s.t. q a → q }. Protocol interaction is defined with the synchronous parallel composition of LTSs. The parallel composition of handshake and serial protocols is depicted in Fig. 2.

Definition 2:

Let P 1 = Σ 1 , Q 1 , → 1 , q • 1 and P 2 = Σ 2 , Q 2 , → 2 , q •
2 be two LTSs. The synchronous product of P 1 and P 2 , noted P 1 P 2 , is the LTS defined as:

P 1 P 2 def = Σ 1 × Σ 2 , Q 1 × Q 2 , → , (q • 1 , q • 2 )
where

(q 1 , q 2 ) (a,b) → (q 1 , q 2 ) iff q 1 a → 1 q 1 and q 2 b → 2 q 2 .
A specification describes the desirable interaction between protocols; it is represented as an LTS with a set of marked states [START_REF] Ramadge | The control of discrete event systems[END_REF]. Marked states specify completed transactions between protocols. A specification of the desired behaviour between the handshake and serial protocols is shown in Fig. 3; q 0 is its initial state and q 1 is its sole marked state.

Definition 3:

Let P 1 = Σ 1 , Q 1 , → 1 , q • 1 and P 2 = Σ 2 , Q 2 , → 2 , q • 2 be two protocols. A specification over the pair P 1 , P 2 is a tuple S = Σ 1 × Σ 2 , Q S , → S , q • s , Q m S such that Σ 1 × Σ 2 , Q S , → S , q •
s is an LTS. The subset Q m S ⊆ Q S is the set of the marked states. The language L(S) is the set of all finite words that terminate in Q m S or infinite words that pass through states of Q m S infinitely often.

Thanks to the associativity of the synchronous product, our formalization generalizes straightforwardly to an arbitrary number of protocols. The only restriction is that communications between the protocols are point-to-point; formally, for each LTS protocol

P i = Σ i , Q i , → i , q • i such that Σ i = Σ Ii Σ Oi {T },
and for each e ∈ Σ Ii , there exists a unique protocol P j such that j = i and e ∈ Σ Oj (and vice-versa).

Refinement Relation

We now provide a solution for convertibility verification using a new refinement relation. In this section, we define the refinement that enforces a desired specification over a protocol composition to ensure error free communication of the two components. We use the well known idea as surveyed in [START_REF] Kern | Formal verification in hardware design: a survey[END_REF] that an implementation (denoted M ) respects a specification (denoted S) whenever a refinement exists from M to S. In this event, each observable behaviour of M is also an observable behaviour of S. We start by defining the notion of satisfaction of a specification for a given protocol composition model. This is similar in spirit to [START_REF] Abadi | The existence of refinement mappings[END_REF].

Definition 4: A model of two interacting protocols,

M = P 1 P 2 , satisfies a specification, denoted M |= S, iff L(M ) ⊆ L(S).
Since forcing leads to some actions being hidden in the resulting system, we weaken the classical definition of spec-ification satisfaction of [START_REF] Ramadge | The control of discrete event systems[END_REF], [START_REF] Abadi | The existence of refinement mappings[END_REF] to deal with these hidden transitions (with internal τ actions) in the composition. This is similar in spirit to the approach taken in [START_REF] Maretti | Mechanized verification of refinement[END_REF] where an interface protocol is introduced.

Definition 5: An LTS M = (Σ, Q, →, q 0 ) weakly satisfies a specification S, denoted M |= w S if and only if L([M ]) ⊆ L(S) where L([M ]) = {α|α ∈ L(M )}, and α is the word obtained by deleting all τ actions from the word α. Now, we introduce a new refinement relation, called specification enforcing refinement (SER), from P 1 P 2 to a specification S. We will subsequently show that this refinement guarantees the existence of a converter. For notational clarity, we represent P 1 P 2 as an LTS M that is equal to the composition of the two protocols:

M = Σ 1 × Σ 2 , Q 1 × Q 2 , → M , (q • 1 , q • 2 ) with q M σ → q M iff (q 1 , q 2 ) (a,b)
→ (q 1 , q 2 ) and σ is a shorthand for (a, b). Exactly like in the framework of DES supervisory control, we partition the set Σ M into two subsets: the subset Σ Mc of controllable events and the subset Σ Mu of uncontrollable events. We introduce two additional subsets: the subset Σ Mb of buffered events and the subset Σ Mf of forceable events. While Σ Mc and Σ Mu are static sets (i.e., they don't change over time), Σ Mb is a dynamic set since it depends on the current set of inputs in the converter's buffers. The set Σ Mf is obtained by removing all current buffered inputs from the set of controllable inputs Σ Mc , i.e., Σ Mf = Σ Mc -Σ Mb . This is because buffered inputs have been produced in the environment; hence, they are visible and can't be hidden through forcing by the converter. Like Σ Mb , Σ Mf is also a dynamic set (i.e., its contents change over time). In the current setting, only outputs are uncontrollable, because the converter can not exert any influence on their generation. We now formally define these sets. We introduce a predicate inBuff that returns true when a given input event is in the converter's buffers.

Definition 6: Given an LTS M = P 1 P 2 , the subset Σ Mc of the controllable events of M is

Σ Mc = {σ|σ = (a, b)∧a ∈ Σ I1 ∧b ∈ Σ I2 }, the subset Σ Mu of uncontrollable events is Σ Mu = Σ-Σ Mc , the subset Σ Mb of buffered events is Σ Mb = {σ|σ ∈ Σ Mc ∧inBuff (σ)}, and finally, the subset Σ Mf of forceable events is Σ Mc -Σ Mb .
We now define the new refinement relation.

Definition 7: Let M = Σ M , Q M , → M , q • M and S = Σ S , Q S , → S , q • S , Q m S
be the LTS of the protocol composition and the specification respectively.

A relation R ⊆ Q M × Q S × Σ *
Mc is called a specification enforcing refinement (SER) from M to S, if the three conditions below hold. The notation q M R s q S is used as a shorthand for (q M , q S , s) ∈ R, where s is any word over Σ Mc whose maximum length is bounded by |Q M |.

• [Matched-state]: If q M R ε q S , then there exists σ ∈ Label(q M ) ∩ Label(q S ), q M ∈ Q M , q S ∈ Q S , and

s ∈ Σ * Mc such that q M σ → q M and q S σ → q S , and q M R s q S . • [Forced-state]: If q M R σs q S for σs ∈ Σ + Mc , then σ ∈ Σ Mf and there exists q M ∈ Q M such that q M σ → q M and q M R s q S . • [Init-state]: q • M R s q • S for some s ∈ Σ * Mc .
According to Definition 7 above, there are two ways how states q M ∈ Q M and q S ∈ Q S can be related via an SER R: 1. q M and q S are directly related if q M has at least one transition having the same label as a transition from q S (a matching transition pair). Moreover, for the matching transition pair q M σ → q M in M and q S σ → q S in S, the successor states q M and q S are also related via some forcing sequence

s ∈ Σ * Mc . Hence, q M R ε q S . q M q M q S q S σ σ R s R ε
2. q M and q S are related via some forcing sequence σ.s if there exists a successor state q M in M such that q M is reachable from q M via a forceable event σ where q M and q S are related via R. In this case, q M R σ.s q S .

q M q M q S R σ.s

R s σ

These possibilities are formalized in the first two conditions of Definition 7. In addition, the start states are required to be related via some forcing sequence s, which corresponds to the third condition. Note that the length of the forcing sequence is bounded by the size of the model. This restriction is needed to ensure that we have only bounded forcing steps. Unbounded forcing steps are possible if the converters have forcing cycles. We forbid such converters since our application domain requires converters to be synthesizable.

Between the handshake-serial example in Fig. 2 (M ) and the specification shown in Fig. 3 (S), an SER exists as follows: R = {((s 0 , t 0 ), q 0 , [b, T 2 ]), ((s 1 , t 0 ), q 0 , ε), ((s 2 , t 0 ), q 2 , ε), ((s 2 , t 1 ), q 3 , ε), ((s 0 , t 0 ), q 1 , ε)}

In general, there may be many SER relations between M and S. For example, R = {((s 0 , t 0 ), q 0 , ε, )} is also a valid SER relation between M and S.

Marked compatibility

The goal of convertibility verification is to determine the conditions under which a suitable converter between M and S exists. Note that an SER refinement between M and S alone doesn't guarantee the existence of such a converter. For example, consider the model M of the composite protocols as shown in Fig. 2 and the specification as shown in Fig. 3. We can define an SER R = {((s 0 , t 0 ), q 0 , ε)}. The corresponding trivial converter will just enable the self-loop transition in the initial states of the two protocols. However, such a converter doesn't ensure completed transactions in the protocols. Marked states (e.g., state q 1 in Fig. 3) in the specification are used to represent completed transactions.

To prevent synthesis of trivial converters, we define marked compatible SERs.

Definition 8: Let R be an SER relation between M and S. A path q M → q M1 → q M2 ... → q Mn in M is a compatible path to a path q S → q S1 → q S2 ... → q Sn in S if (q M , q S , s) ∈ R for some s ∈ Σ *

Mc and for all i ∈ [1.

.n]: (q Mi , q Si , s i ) ∈ R for some s i ∈ Σ * Mc . Definition 9: An SER relation R between M and S is marked compatible if for every (q M , q S , s) ∈ R there exists (q M , q S , s ) ∈ R such that there exists a path from q M to q M and a compatible path from q S to q S ∈ Q m S , i.e., q S is a marked state of S.

Definition 10: Let M and S be a model of protocol composition and a specification, respectively. M SER S if there exists a specification enforcing refinement from M and S that is marked compatible.

Converters

We now synthesize converters between protocols. A converter is an LTS whose role is to appropriately guide the protocols so that the composite system satisfies the desired specification. The role of the converter is to act as an intermediary so that all protocol communications are consistent with the specification. We only consider converters with a bounded number of states since our application domain is embedded systems (SoCs) and in this domain it is important that we are able to synthesize the generated converters. In our framework, a converter can perform the following actions:

1) Disabling a transition of the protocols: Remove undesirable communication paths that violate the specification. This operation is identical to the controllers in DES [START_REF] Ramadge | The control of discrete event systems[END_REF]. The disabled transitions must be controllable. 2) Forcing a transition of the protocols: Automatically guide the protocols to a successor state from its current state so that the future state is consistent with a specification state. This is done by generating the suitable forceable inputs on a path.

3) Buffering a communication between the protocols: If a

given input generated by one of the protocols cannot be consumed by the receiving protocol, a converter can buffer this event so that it can be forwarded in the future.

Converter Synthesis from an SER Relation

Converters can be derived automatically once an SER is established between M and S. Given an SER R, the states of the converter Q C are exactly the elements of R. We now formalize the relationship between an SER relation and a corresponding converter. We start by defining precisely-forced SERs so as to ensure that forcing is always performed in a unique fashion from any forced state. Definition 11: An SER relation R is precisely-forced iff (q M , q S , s 1 ) ∈ R and (q M , q S , s 2 ) ∈ R implies that s 1 = s 2 .

Given an SER R, a precisely-forced SER R can be automatically derived from R and always exists. From a precisely-forced SER, we now build a converter that derives from it:

Definition 12: Let R be a precisely-forced SER between a model M and a specification S. The converter derived from R is the LTS

C R = Σ M ∪ [Σ Mc ], R, → C , ((q • M , q • S ), s 0 ) , where [Σ Mc ] = { [σ] | σ ∈ Σ Mc } and [σ]
denotes the forced action over event σ, and → C is defined by the following two rules:

• [Matched-event]: If (q M , q S , ε) ∈ R ∧ (q M , q S , s ) ∈ R ∧ q M σ → q M ∧ q S σ → q S , then (q M , q S , ε) σ → (q M , q S , s ). • [Forced-event]: If (q M , q S , α.s) ∈ R∧q M α → q M , then (q M , q S , α.s) [α]
→ (q M , q S , s).

For the handshake-serial protocol pair shown in Fig. 2 and the specification S shown in Fig. 3, a converter generated by our approach is shown in Fig. 4(a). It first forces the transition from (s 0 , t 0 ) to (s 1 , t 0 ) by generating the events [b, T 2 ]. Subsequently, it reads the a produced by P 1 and buffers it while allowing P 2 to remain in its initial state through a T 2 transition. It then forwards the buffered a to the P 2 while allowing P 1 to remain in its current state through a T 1 transition. Note that there is also the choice of directly allowing the (a , a) transition in the state cs1 instead of first buffering a and later forwarding a. Hence, the generated converter keeps all possibilities.

Having established the relationship between a given SER and the associated converter, we now define well-formed converters. Well-formed converters ensure that protocols always complete their transactions.

Definition 13: Let R be a SER between a model M and a specification S.

A converter C = Σ C , Q C , → C , q • C
derived from R is said to be well-formed if the two following conditions hold:

• [Forced-alone]: For all q, q ∈ Q C and α ∈ Σ C such that q [α] → C q , if q σ → C q and q [β]
→ C q for some q , q ∈ Q C and some σ, β ∈ Σ C , then σ = [α], q = q , β = α, and q = q .

• [Marked-path]: For any state q ∈ Q C , there always exists a path to a state q ∈ Q C such that q = (q M , q S , s) and q S ∈ Q m S . The state graph of a well-formed converter has only one successor for states where forcing is performed. Other states may have more than one successor. Moreover, from every state of a well formed converter, a marked state can always be reached. A state in the converter is called a marked state if the corresponding component of R is of the form (q M , q S , s) such that q S is a marked state. It is easy to note that any converter C derived from a deterministic and marked compatible SER is always well-formed.

In our framework, event buffering is achieved thanks to the state space of the converter. This is the case of the event a in the converter of Figure 4.

Lemma 1: Let R be a precisely-forced SER between a model M and a specification S, and let C R be the converter derived from R. If R is marked compatible, then C R is well-formed.

Proof:

Let C R = Σ C , Q C , → C , q • C be the converter derived from R. Proof of Condition [Forced-alone]: Let q, q ∈ Q C and α ∈ Σ C such that q [α] → C q . We prove by contradiction that q = q ∈ Q C and σ = α ∈ Σ C such that q σ → C q . Since [α] is a forced action, Rule [Forced-event] implies that q = (q M , q S , α.s) ∈ R. Furthermore, since q σ → C q , Rule [Matched-event] implies that (q M , q S , ε) ∈ R.
Hence, according to Definition 11, we conclude α.s = ε, which is a contradiction.

Similarly, it can be show by contradiction that q = q ∈ Q C and β = α ∈ Σ C such that q

[β] → C q . This follows directly from the fact that R is precisely-forced.

Proof of Condition [Marked-path]: Direct consequence of Definition 9.

We now define the product operation for composing a converter C with a pair of protocols represented as an LTS M .

Definition 14:

Let C = Σ C , Q C , → C , q • C and M = Σ M , Q M , → M , q •
M be a converter and a model respectively. The forced composition C // M of C and M is

C // M def = Σ M ∪ {τ }, Q C × Q M , → , (q • C , q • M )
, where → is defined by the following two rules: The next result states that a marked compatible SER relation between M and S is a necessary and sufficient condition for the existence of a correct converter.

• [Tau-trans]: (q C , q M ) τ → (q C , q M ) if q C [α] → C q C and q M α → M q M for some α ∈ Σ Mf . • [Event-trans]: (q C , q M ) σ → (q C , q M ) if q C σ → C q C and q M σ → M q M for all σ ∈ Σ M .
Theorem 1: Let M and S be deterministic LTSs of the model and the specification respectively. There exists a wellformed and deterministic converter C such that C//M |= w S if and only if M SER S.

Proof: Sufficient Condition: The proof is constructive. Given M SER S, there exists a precisely-forced and marked compatible SER R. We can construct a converter C using Definition 12. Since R is marked compatible C is well formed (Lemma 1). Also, C is deterministic since both M and S are deterministic. Thus, C // M is also deterministic. Now it is easy to see that all τ -projected traces of C // M are contained in the trace set of S.

Necessary Condition: Given a well-formed converter C such that C // M |= w S, we need to prove that M SER S. Since L([C // M]) ⊆ L(S) and as C is well-formed and C, M and S are deterministic, this result follows.

Prototype tool and results

A local, on-the-fly tableau construction algorithm, similar to [START_REF] Cleaveland | Tableau-based model checking in the propositional mu-calculus[END_REF], [START_REF] Sinha | An approach for resolving control and data mismatches in SoCs[END_REF], is used for converter synthesis. The recursive algorithm is shown in Alg. 1 and is described as follows.

A tableau is a table of assertions which is organized as a graph in the proposed algorithm. Each assertion is of the form (q M ,buf, q S ) which is true when the states q M and q S (of the synchronous composition M of the given protocols and specification S respectively) are related via a SER. The set buf is used to describe the events contained in the buffers of the converter (being generated) under which the assertion must hold. Each assertion is described as a vertex of the graph (tableau), called a node. A node's attributes are the states q M and q S , the set buf, and a variable type that can be either "Disabling" or "Forcing". The type is used to avoid forcing cycles in the converter and is described later. A node can have outgoing edges to other nodes in the graph, which are called its children nodes. The assertion represented by a node holds if and only if the sub-assertions represented by its children nodes hold.

The inputs to the recursive algorithm checkSER are states q M and q S of a model and a specification, a set buf of signals assumed to be contained in the converter's buffers, and h, an ordered list of nodes that have been visited before the current call to checkSER is made. The first call to the algorithm is made with the parameters q • m , buf = ∅, q • s , and h = ∅. This forms the initial assertion of the tableau and requires that the initial states q • m and q • s of the model and specification be related to each other via a SER relation under the assumption that the converter contains no events in its buffers initially (h is empty because no previous call has been made).

The algorithm, given the arguments q M , buf, q S , and h, proceeds as follows. It first creates a node curr with the attributes q M , buf, and q S . Next, it checks if a similar node anc is contained in h (line 3). If such a node anc is found, this means that a cycle in the converter (being generated) is found. In this case, the algorithm checks if the trace from anc to curr contains a node nxt where nxt.q S is a final state in the specification (q S ∈ Q m S ) and also that nxt.q M and nxt.q S are related directly (via ε). If such a node is found, the cycle is acceptable (is marked compatible and has no forcing cycles), and the algorithm returns anc (line 7). Otherwise, it returns nil signifying that the cycle is either not marked compatible or contains forcing cycles (line 11). Algorithm 1 node checkSER(q M , buf, q S , h) 1: curr := createNode(q M , buf, q S ); 2: //FINITIZE: Check for Cycles 3: if curr = anc for some anc ∈ h then nodes are not resolved further. For example, in Fig. 5, the nodes A2 and A8 are not resolved further because they are identical to the previously processed node A1. A2 returns failure because the path from A1 to A2 does not contain any node corresponding to the marked state q 1 , whereas A8 returns success because the path from A1 to A8 contains a node (A7) that corresponds to q 1 . A5 is resolved in the same manner as A6, and returns success because (A6) has already returned success. The algorithm exits when the initial assertion (A1) returns success to indicate that a successful tableau has been generated. Each node in a successful tableau corresponds to a unique state in the converter. For example, each node in the tableau shown in Fig. 5 corresponds to a unique state in the converter shown in Fig. 4(a), (and the initial node A1 corresponds to the initial state of the converter). If checkSER succeeds, the returned node, called the root node of the tableau, is passed to the procedure extractConverter to generate the converter. extractConverter operates as follows. It first creates a data structure MAP that maps nodes in the tableau to states in the converter (MAP is initially empty). It then calls the recursive algorithm extract and passes to it the root node of the tableau. In extract, we first checked if the argument curr is contained in the MAP. If so, the corresponding converter state is returned. Otherwise, a new converter state q C is created and map is adjusted to remember the correspondence between curr and q C (line 4-5). Then, each child node nxt of curr is processed by calling extract to obtain its corresponding state q C and a transition from q C to q C is created.

Algorithm 2 STATE extractConverter(root)

Implementation Results

Tab. 2 shows a set of results obtained by executing the SER algorithm over some well-known conversion problems described in literature [START_REF] Kumar | Protocol conversion using supervisory control techniques[END_REF]- [START_REF] Silva | Synchronous protocol automata: A framework for modelling and verification of SoC communication architectures[END_REF], [START_REF] Lam | Protocol conversion[END_REF], [START_REF] Sinha | An approach for resolving control and data mismatches in SoCs[END_REF]. Each entry in the table describes the protocols and specification involved and the types converters obtained by using classical approaches and the SER conversion algorithm (D=disabling, DF=disabling and forcing). Problem 1 is the handshake-serial problem Algorithm 3 STATE extract(curr) presented in [START_REF] Passerone | Convertibility verification and converter synthesis: Two faces of the same coin[END_REF] while problem 1A is an extension of problem 1 that involves an extra input transition in the handshake protocol (see Fig. 2). Problems 2, 3, 4, and 5, that are taken from other articles on protocol conversion, are extended in similar fashion to problems 2A, 3A, 4A, and 5A. While classical techniques can handle problems 1, 2, 3, 4, and 5 only, we could generate converters for these problems as well as their variants 1A, 2A, 3A, 4A, and 5A. Although the implementation does not address the question of finding optimal converters (those with minimum number of forcing steps), it can generate all possible converters. The algorithm not only finds converters where previous approaches fail, it also preserves the full design space by finding all possible solutions.

Conclusions

Protocol conversion is required while creating a complex system (such as a System-on-Chip) from pre-designed components (called IPs) which have mismatching communication protocols. Convertibility verification automatically determines if a suitable glue-logic, called a converter, exists to bridge such mismatches. Converters are inspired by controllers from DES supervisory control theory and hence bridge mismatches through disabling of undesirable communication paths while also performing additional control actions such as event buffering. This paper presents a more generalized converter synthesis technique that performs forcing of actions in addition to the conventional disabling. Forcing actions are used to hide extra control sequences that are required by the protocols but not by the desired specification. Forcing induces state-based hiding that is not possible using standard hiding operators in DES supervisory control.

We have proposed a new refinement relation, called specification enforcing refinement (SER), between a given protocol composition and a desired specification. We have also shown that the existence of this relation is a necessary and sufficient condition for the existence of a suitable converter that enforces the desired specification over the protocols. The proposed approach generalizes existing approaches to convertibility verification, and we have demonstrated it by finding converters for many protocol mismatches that can't

2 Figure 1 .

 21 Figure 1. Overview of convertibility verification

Figure 2 .

 2 Figure 2. Handshake and serial protocols and their synchronous parallel composition

Figure 3 .

 3 Figure 3. A desired specification with a marked state

Lemma 2 :

 2 The forced composition C//M is deterministic if both C and M are deterministic and if the converter C is well-formed.Proof: The proof follows directly from the fact that both C and M are deterministic and from the Rules [Tau-trans] and [Event-trans].

4 : 6 : 7 :

 467 nxt := anc; {allow only compatible, non-forcing cycles} 5: while nxt != nil do if nxt.type = Disabling and nxt.qS ∈ Q m S then

Figure 5 .

 5 Figure 5. Tableau for the handshake-serial example

Table 1 .

 1 Features of various protocol conversion approaches

	Approach	Input	(Protocols)	Input (spec.)	Multiple Protocols	Algorithm	Uncontrollable Signals	Buffering	Data	Multi-clock	Control Action
	Kumar et al. [1]	LTS	LTS		supervisory control		×	×	×	disabling
	Passerone et al. [2]	LTS	LTS	×	game-theoretic	×		×	×	disabling
	D'Silva et al. [3]	SPA	×		refinement	×				disabling
	Tivoli et al. [4]	LTS	×		controlled coverability			×	implicit	disabling
	Sinha et al. [5]	LTS	CTL		model-checking					disabling
	SER Refinement	LTS	LTS		refinement			×	×	disabling, forcing

1 :

 1 if curris present in MAP then 2: return map.get(curr) 3: end if 4: create new converter state qC 5: MAP.put(curr, qC ) 6: for each nodenxts.t. curr→ a nxt do

	7: 8:	State q C = extract(nxt) add transition qC a → q C
	9: end for
	10: return MAP.get(curr)

end if 9: nxt := h.getNodeAfter(nxt); return nil; 12: end if 13: h' := h.append(curr); 14: //DISABLING: 15: curr.type := Disabling; 16: common := Label(q M ) ∩ Label(q S ); {can be matched} 17: uncSet := Label(q M ) ∩ ΣMu; {must be matched} 18: if uncSet ⊆ common then 19: for each a ∈ uncSet do 20:

q Ma := q M : q M a → q M ; 21:

q Sa := q S : q S a → q S ; 22: nxt := checkSER(q Ma , adjustBuf(buf, a), q Sa , h'); for each a ∈ common such that a ∈ buf do 32:

q Ma := q M : q M a → q M ; 33:

q Sa := q S : q S a → q S ; 34: nxt := checkSER(q Ma , adjustBuf(buf, a), q Sa , h'); q Ma := q M : q M a → q M ; 47:

nxt := checkSER(q Ma , buf, q S , h'); In case the node curr needs to be expanded further (no cycle is detected), the algorithm adds it to h to form a new history stack h'. The algorithm then attempts to match curr.q M and curr.q S using either the null sequence ε (lines 14-40) or some forcing sequence a (lines 41-53). If both attempts fail, the algorithm returns nil (line 54).

In order to match curr.q M and curr.q S over ε (by possibly disabling one or more transitions in curr.q M ), the algorithm sets curr.type to "Disabling" and computes the sets common and uncSet (lines [START_REF] Kern | Formal verification in hardware design: a survey[END_REF][START_REF] Abadi | The existence of refinement mappings[END_REF][START_REF] Maretti | Mechanized verification of refinement[END_REF]. common contains all events that trigger transitions in both curr.q M and curr.q S whereas uncSet contains events that trigger uncontrollable transitions in curr.q M . A converter must enable all transitions triggered by uncSet in curr.q M and each enabled transition must match a transition curr.q S . Hence, the states cannot be matched if uncSet is not a subset of common because one or more uncontrollable transitions in curr.q M cannot be matched by any transition in curr.q S . Otherwise, the algorithm checks if the states q Ma and q Sa reached from curr.q M and curr.q S via each uncontrollable event a ∈ uncSet are related to each other (lines 19-29). If for any a, q Ma and q Sa are not related (checked via a recursive call to checkSER), curr.q M and curr.q S cannot be related to ε. If however all q Ma and q Sa pairs are related, the algorithm then checks if any other states reached via controllable events (events in the set common-uncSet) are also related to each other (lines 30-38). Each pair that matches is retained as a (successful) sub-assertion. The algorithm then returns curr to indicate that matching over ε is successful.

In case matching over ε fails, the algorithm attempts to apply forcing (lines 41-53). It first resets curr.type to "Forcing" and checks if the state curr.q M is indeed forcible (that is, it has no uncontrollable transitions). Next, it checks if each transition label a of curr.q M can be forced such that the resulting state q Ma is related to curr.q S . Note that an event a is considered only if it is not present in buf. The algorithm returns success when such an event a is found. The resulting (successful) node returned by the recursive call to checkSER is added as the sole child of curr.

In case both disabling and forcing tests fail, the node returns failure (nil). The worst-case complexity of the al- The algorithm is intuitively described by using the tableau shown in Fig. 5 (generated for the handshake-serial example). The inputs to the algorithm are the initial states (s 0 , t 0 ) and q 0 of the model and the specification, and an empty set of buffered events and an empty set of previously visited nodes. These inputs form the initial assertion (node) A1 of the tableau, which is recursively broken down into subassertions (children nodes) using the disabling and forcing rules. A node returns success if its children return success. An infinite resolution of nodes into children nodes is prevented by termination conditions to ensure that duplicate be bridged using existing techniques. Future work will involve extending the formulation to handle data-width and clock mismatches, and finding optimal converters. We will then apply the algorithm to solve protocol mismatches in real SoCs based on standard buses such as the AMBA.