Search

This software is dedicated to the simulation, analysis, and static scheduling of Event/Marked Graphs, SDF and KRG extensions. A graphical interface allows to edit the Process Networks and their time annotations (latency, ...). Symbolic simulation and graph-theoretic analysis methods allow to compute and optimize static schedules, with best throughputs and minimal buffer sizes. In the case of KRG the (ultimately k-periodic) routing patterns can also be provided and transformed for optimal combination of switching and scheduling when channels are shared. KPASSA also allows for import/export of specific description formats such as UML-MARTE, to and from our other TimeSquare tool.

International audience; Application Architecture Adequacy (AAA) aims at tuning an application to a given hardware architecture. However it is still a difficult and error prone activity. As like as in Hardware/Software co-design, it requires a model of both the application and the architecture. With the new highly-parallel architectures, AAA should also allow a fast exploration of different software mapping granularity in order to leverage better the hardware resources without sacrifying too much productivity. The main contribution of this paper is to extract from a case study a methodology based on dataflow modeling to make the software both faster to develop and suited to the target. Then we show how this methodology can solve some of these issues.

The UML Profile for Modeling and Analysis of Real-Time and Embedded systems promises a general modeling framework to design and analyze systems. Lots of works have been published on the modeling capabilities offered by MARTE, much less on verification techniques supported. The Clock Constraint Specification Language (CCSL), first introduced as a companion language for MARTE, was devised to offer a formal support to conduct causal and temporal analyses on MARTE models. This work introduces formally a state-based semantics for CCSL operators.

This paper presents a novel approach to the design verification of Software Product Lines(SPL). The proposed approach assumes that the requirements and designs are modeled as finite state machines with variability information. The variability information at the requirement and design levels are expressed differently and at different levels of abstraction. Also the proposed approach supports verification of SPL in which new features and variability may be added incrementally. Given the design and requirements of an SPL, the proposed design verification method ensures that every product at the design level behaviorally conforms to a product at the requirement level. The conformance procedure is compositional in the sense that the verification of an entire SPL consisting of multiple features is reduced to the verification of the individual features. The method has been implemented and demonstrated in a prototype tool SPLEnD (SPL Engine for Design Verification) on a couple of fairly large case studies.; Ce papier présente une approche nouvelle de vérification pour les lignes de produits logiciels (LPL). L'approche proposée considère que la spécification et la conception de LPL peuvent être abstraites comme des automates à états finis comprenant des informations sur la variabilité. Ces informations sont exprimées différemment aux niveaux spécification et conceptions. Sous ces hypothèses, l'approche proposée supporte la vérification de LPLs dans lesquelles des fonctionnalités peuvent être ajoutées incrémentalement. A partir de la spécification et de la conception d'une LPL, la méthode de vérification proposée assure que chaque produit au niveau conception se conforme, comportementalement parlant, à un produit au niveau spécification. La procédure de conformité est compositionnelle car la vérification de la LPL en entier se réduit à la vérification des fonctionnalités qui la compose individuellement. La méthode a été implantée dans un outil appelé ''SPLEnD'' et essayée sur deux cas d'étude relativement larges.

A cellular automaton (CA) is an infinite array of cells, each containing the same automaton. The dynamics of a CA is distributed over the cells where each computes its next state as a function of the previous states of its neighborhood. Thus, the transmission of such states between neighbors is considered as feasible directly, in no time. When considering the implementation of a cellular automaton on a many-cores System-on-Chip (SoC), this state transmission is no longer abstract and instantaneous, but has to follow the interconnection medium of the SoC. It is usually a grid or a mesh matching the underlying topology of the CA but finite. In order to consider such constraints at a higher level, we propose a refinement of the classical model of CA where the topology is considered as the communication medium. If the state of a cell depends on its neighbors up to a certain distance, then a given state must be broadcasted to all its neighbors at the same distance, as they all require it to compute their next state. It means routing and duplicating the state in the topology. We study the routing patterns needed to efficiently implement such state broadcasting algorithm. We provide a solution by which each router can locally predict where to redirect the states to correctly and efficiently implement this broadcasting algorithm.; Un automate cellulaire (AC) est un tableau infini de cellules, chacune contenant le même automate. La dynamique d'un AC est distribuée entre les cellules, chacune calcule son prochain état comme une fonction des états de ses voisins. Donc, la transmission d'un état entre deux cellules est donc considérée comme faisable directement et instantanément. Quand on s'intéresse à l'implémentation d'un AC sur un système sur puce à plusieurs cores, on ne peut plus considérer la transmission d'un état comme une action abstraite et instantanée. Cette transmission doit suivre le medium d'interconnexion du système sur puce. Ce dernier est habituellement une grille ou un mesh (grille dans laquelle les extrémités opposées sont connectées) correspondant à la topologie logique de l'AC mais finie. Afin de prendre en compte la notion de medium d'interconnexion à un niveau d'abstraction supérieur, par rapport à l'implémentation, nous proposons un raffinement du modèle classique des AC dans lequel la topologie est considérée comme le medium d'interconnexion. Si l'état d'une cellule dépend de son entourage jusqu'à une certaine distance, alors cet état doit être diffusé à tous les voisins jusqu'à cette même distance puis ce que chacun d'eux en a besoin pour calculer son nouvel état. Cela signifie router et diffuser l'état en question dans la topologie. Nous étudions le schéma de routage nécessaire pour mettre en oeuvre efficacement cet algorithme de diffusion d'état. Dans cette solution, chaque router peut localement prédire où envoyer les états en transit afin de garantir la justesse de l'algorithme.

Due to the increasing scaling of digital system, System-on-Chip (SoC) design deals with latencies problem on long wire interconnection through the whole chip. A SoC is a set of IP components communicating together. While the communication inside the IP component can still be considered synchronous (abstracted as instantaneous action), the communication between IP components should not. Many clock cycles occur between sending and reception of a data on an interconnexion wire. The theory of Latency Insensitive Design (LID) created by L. Carloni and A. Sangiovanni-Vincentelli solves this problem by implementing a communication protocol based on segmentation of interconnection wire and back pressure in case of local traffic jam. In the first time, we'll give theoretical basis of LID theory by formally linking it to the deterministic model of Marked/Event graph (conflict free subset of Petri net), and limiting the capacity of places by 2; which naturally implement the back pressure protocol. This model drive us to the main problem of this work: How to minimize the size of memory resources used as buffer through the interconnection wires? Because their quantity and location should become critical at implementation. Then we'll study this problem with the natural hypothesis of determinism. This allow the system to have regular and periodic behaviour. The goal of this work is to modify the LID theory by taking care of this hypothesis. the study of deterministic systems and previous results lead us to a first modification step called: Equalization. Next step consist in statically schedule these system. We chose to explicitly represent schedule of each element of the system using periodic binary word (1 for activity, 0 for stalling) such M. Pouzet and al. introduce it in "N-synchronous Kahn network". A study of different classes of binary word (Sturm, Christoffel, Lyndon, Mechanical words) was prior to their association to LID theory and {\em Equalization} process. We obtained statically scheduled systems which answered to the main problem of this work.; Du fait de la miniaturisation grandissante des circuits électroniques, la conception de système sur puce actuelle, se heurte au problème des latences sur les fils d'interconnexions traversant tout le circuit. Un système sur puce est un ensemble de blocs de calculs (les composants IP) qui s'échangent des données. Alors que la communication à l'intérieur de ces blocs de calculs peut toujours se faire de manière synchrone, c'est à dire s'abstraire comme une action instantanée, la communication d'un bloc de calculs à un autre prend un temps qui n'est pas négligeable. Il s'écoule plusieurs cycles d'horloge entre l'émission d'une donnée sur un fil d'interconnexion et sa réception. La théorie du Latency Insensitive Design créée par Luca Carloni et Alberto Sangiovanni-Vincentelli permet entre autre de résoudre ce problème en implantant un protocole de communication basé sur la segmentation des fils d'interconnexions et sur le principe de rétroaction en cas d'embouteillage. Dans un premier temps, nous avons donné un fondement théorique à cette théorie en la rapprochant formellement d'une modélisation par Marked/Event graph (Sous ensemble sans conflit des Réseaux de Pétri) et avec des places de capacité ; ce qui génère naturellement le protocole de contrôle de flux. Cette modélisation nous amène à la problématique principale de cet ouvrage: comment, et sous quelles conditions, peut on minimiser la taille des ressources de mémorisation utilisées comme tampons intermédiaires au long de ces fils d'interconnexions? Car leur nombre et leur position peuvent se révéler critique à l'implantation matérielle. Nous allons ensuite étudier cette question sous une hypothèse naturelle de déterminisme, ce qui permet d'obtenir des régimes de fonctionnement périodiques et réguliers. Le but de cette thèse est de modifier le protocole mis en place dans la théorie du Latency Insensitive Design en prenant en compte cette hypothèse. L'étude des systèmes déterministes et des résultats existant nous a permis une première phase de modification appelée: égalisation. L'étape suivante consiste à ordonnancer statiquement ces systèmes. Pour cela, nous avons choisi de représenter explicitement l'ordonnancement de chacun des éléments du système comme un mot binaire périodique où les "1" représentent les instants d'activités et les "0" d'inactivités tel que M. Pouzet et al. l'ont introduit dans le "N-synchronous Kahn network". Une étude approfondie des différentes classes de mots binaires existants (mot de Sturm, de Christoffel, de Lyndon ou encore mécaniques) a précédé leur association à la théorie du Latency Insensitive Design et au processus d'égalisation pour obtenir des systèmes déterministes ordonnancés statiquement.

Due to the increasing scaling of digital system, System-on-Chip (SoC) design deals with latencies problem on long wire interconnection through the whole chip. A SoC is a set of IP components communicating together. While the communication inside the IP component can still be considered synchronous (abstracted as instantaneous action), the communication between IP components should not. Many clock cycles occur between sending and reception of a data on an interconnexion wire. The theory of Latency Insensitive Design (LID) created by L. Carloni and A. Sangiovanni-Vincentelli solves this problem by implementing a communication protocol based on segmentation of interconnection wire and back pressure in case of local traffic jam. In the first time, we'll give theoretical basis of LID theory by formally linking it to the deterministic model of Marked/Event graph (conflict free subset of Petri net), and limiting the capacity of places by 2; which naturally implement the back pressure protocol. This model drive us to the main problem of this work: How to minimize the size of memory resources used as buffer through the interconnection wires? Because their quantity and location should become critical at implementation. Then we'll study this problem with the natural hypothesis of determinism. This allow the system to have regular and periodic behaviour. The goal of this work is to modify the LID theory by taking care of this hypothesis. the study of deterministic systems and previous results lead us to a first modification step called: Equalization. Next step consist in statically schedule these system. We chose to explicitly represent schedule of each element of the system using periodic binary word (1 for activity, 0 for stalling) such M. Pouzet and al. introduce it in "N-synchronous Kahn network". A study of different classes of binary word (Sturm, Christoffel, Lyndon, Mechanical words) was prior to their association to LID theory and {\em Equalization} process. We obtained statically scheduled systems which answered to the main problem of this work.; Du fait de la miniaturisation grandissante des circuits électroniques, la conception de système sur puce actuelle, se heurte au problème des latences sur les fils d'interconnexions traversant tout le circuit. Un système sur puce est un ensemble de blocs de calculs (les composants IP) qui s'échangent des données. Alors que la communication à l'intérieur de ces blocs de calculs peut toujours se faire de manière synchrone, c'est à dire s'abstraire comme une action instantanée, la communication d'un bloc de calculs à un autre prend un temps qui n'est pas négligeable. Il s'écoule plusieurs cycles d'horloge entre l'émission d'une donnée sur un fil d'interconnexion et sa réception. La théorie du Latency Insensitive Design créée par Luca Carloni et Alberto Sangiovanni-Vincentelli permet entre autre de résoudre ce problème en implantant un protocole de communication basé sur la segmentation des fils d'interconnexions et sur le principe de rétroaction en cas d'embouteillage. Dans un premier temps, nous avons donné un fondement théorique à cette théorie en la rapprochant formellement d'une modélisation par Marked/Event graph (Sous ensemble sans conflit des Réseaux de Pétri) et avec des places de capacité ; ce qui génère naturellement le protocole de contrôle de flux. Cette modélisation nous amène à la problématique principale de cet ouvrage: comment, et sous quelles conditions, peut on minimiser la taille des ressources de mémorisation utilisées comme tampons intermédiaires au long de ces fils d'interconnexions? Car leur nombre et leur position peuvent se révéler critique à l'implantation matérielle. Nous allons ensuite étudier cette question sous une hypothèse naturelle de déterminisme, ce qui permet d'obtenir des régimes de fonctionnement périodiques et réguliers. Le but de cette thèse est de modifier le protocole mis en place dans la théorie du Latency Insensitive Design en prenant en compte cette hypothèse. L'étude des systèmes déterministes et des résultats existant nous a permis une première phase de modification appelée: égalisation. L'étape suivante consiste à ordonnancer statiquement ces systèmes. Pour cela, nous avons choisi de représenter explicitement l'ordonnancement de chacun des éléments du système comme un mot binaire périodique où les "1" représentent les instants d'activités et les "0" d'inactivités tel que M. Pouzet et al. l'ont introduit dans le "N-synchronous Kahn network". Une étude approfondie des différentes classes de mots binaires existants (mot de Sturm, de Christoffel, de Lyndon ou encore mécaniques) a précédé leur association à la théorie du Latency Insensitive Design et au processus d'égalisation pour obtenir des systèmes déterministes ordonnancés statiquement.

Process Networks have long been used as formal Models of Computation in the design of dedicated hardware and software embedded systems and Systems-on-Chip. Choice-less models such as Marked/Event Graphs and their Synchronous Data Flow extensions have been considered to support periodic scheduling analysis. Those models do not hide dependency informations like regular sequential languages: they capture the communication topology through point-to-point channels. Those models are concurrent, formally defined, have a clear semantic but are limited due to static point-to-point channels. Then, further extensions such as Cyclo-Static Data Flow or Boolean-controlled Dataflow (BDF) graphs introduced routing switches, allowing internal choices while preserving conflict-freeness, in the tradition of Kahn Process Networks. We introduce a new model, which we term Kahn-extended Event Graphs (KEG). It can be seen as a specialization of both Cyclo-Static and BDF processes. It consists merely in the addition of Merge/Select routing nodes to former Marked/Event Graphs; but, most importantly, these new nodes are governed by explicit (ultimately periodic) binary-word switching patterns for routing directions. We introduce identities on Merge/Select expressions, and show how they build a full axiomatization for the flow-equivalence between the computation nodes. The transformations carry a strong intuitive meaning, as they correspond to sharing/unsharing the interconnect links. Such interconnect defines each time a precise Network-on-Chip topology, and the switching patterns drive the traffic. One can also compute the buffering space actually required at the various fifo locations. The example of a Sobel edge filter is discussed to illustrate the importance of this model.

Event/Marked Graphs (EG) form a strict subset of Petri Nets. They are fundamental models in Scheduling Theory, mostly because of their absence of alternative behaviors (or conflict-freeness). It was established in the past that, under broad structural conditions, behavior of Timed Event Graphs (TEG) becomes utterly regular (technically speaking: “ultimately k-periodic”). More recently it has been proposed to use this kind of regular schedulings as syntactic types for so-called N-synchronous processes. These types remained essentially user-provided. Elsewhere there have been proposals for adding control in a “light fashion” to TEGs, not as general Petri Nets, but with the addition of Merge/Select nodes switching the data flows. This was much in the spirit of Kahn process networks [8, 9]. But usually the streams of test values governing the switches are left unspecified, which may introduce phenomena of congestion or starvation in the system, as token flow preservation becomes an issue. In the present paper we suggest to restrict the Merge/Select condition streams to (binary) k-periodic patterns as well, and to study their relations with the schedules constructed as before for TEGs, but on the extended model. We call this model Kahn-extended Event Graphs (KEG). The main result is that flow preservation is now checkable (by abstraction into another model of Weighted Marked Graphs, called SDF in the literature). There are many potential applications of KEG models, as for instance in modern Systems-on-Chip (SoC) comprising on-Chip networks. Communication links can then be shared, and the model can represent the (regular) activity schedules of the computing as well as the communicating components, after a strict scheduling has been found. They can also be used as a support to help find the solution.

We revisit the formal modeling of relay stations, which are specific connection elements used in the theory of Latency-Insensitive Design of Globally-Asynchronous/Locally-Synchronous systems. Relay stations are in charge of taking into account the physical mandatory latencies, while handling the regulation of signal/data traffic so as to avoid starvation, deadlock and congestion of local IP synchronous computation blocks. Since proposed by Carloni et al, the structure and behaviors of these relay stations have been amply characterized and analysed. But previous works never provided a fully formal and cycle-accurate description of these mechanisms, amenable to formal verification for instance (instead, mainly simulation models were developed). Due to the needed precision of the whole scheme we feel such a formal description might be needed. We describe such an attempt here. On its way, this work also led us to a number of (hopefully insightful) remarks on favorable and disfavorable graph topologies and initialization features, that are also reported here.