Publications of Matthieu Moy (sorted by years)

List publication All in one, By year.

2016

[1] Matthieu Moy, Claude Helmstetter, Tayeb Bouhadiba, and Florence Maraninchi. Modeling Power Consumption and Temperature in TLM Models. Leibniz Transactions on Embedded Systems, Vol 3(No 1):03:1--03:29, June 2016. [ bib | DOI | http | .pdf ]
Keywords: Systemc ; Tlm ; Energy ; atmi
[2] Matthieu Moy and Sébastien Viardot. Chamilotools: a set of tools to interact with a chamilo server. Published as Free Software (CeciLL C License), 2016. [ bib | http ]
[3] Denis Becker, Jérôme Cornet, and Matthieu Moy. SycView: Visualize and Profile SystemC Simulations. In DUHDe, 3rd Workshop on Design Automation for Understanding Hardware Designs, Dresden, Germany, Mar 2016. [ bib | http | .pdf ]
[4] Hamza Rihani, Claire Maiza, and Matthieu Moy. Efficient Execution of Dependent Tasks on Many-Core Processors. In RTSOPS 2016, 7th International Real-Time Scheduling Open Problems Seminar, Toulouse, France, Jul 2016. [ bib | http | .pdf ]
Keywords: WCRT Analysis; Shared Resource Interference; Dependent Tasks; Synchronous Data flow; Many-cores; Scheduling
[5] Hamza Rihani, Matthieu Moy, Claire Maiza, Robert I. Davis, and Sebastian Altmeyer. Response Time Analysis of Synchronous Data Flow Programs on a Many-Core Processor. In RTNS 2016, 24th International Conference on Real-Time Networks and Systems, Brest, France, Oct 2016. [ bib | DOI | http | .pdf ]
Keywords: WCRT Analysis; Shared Resource Interference; Dependent Tasks; Synchronous Data flow; Many-cores; Scheduling
[6] Karine Altisen and Matthieu Moy. Causality problem in real-time calculus. Formal Methods in System Design (Springer), 48(1):1--45, 2016. Rank A CORE ERA2010. [ bib | DOI | http | .pdf ]
[7] Denis Becker, Matthieu Moy, and Jérôme Cornet. Parallel Simulation of Loosely Timed SystemC/TLM Programs: Challenges Raised by an Industrial Case Study. MDPI Electronics, 5(2):22, 2016. [ bib | DOI | http | .pdf ]

2015

[1] Hamza Rihani, Matthieu Moy, Claire Maiza, and Sebastian Altmeyer. WCET analysis in shared resources real-time systems with TDMA buses. In RTNS 2015, 23rd International Conference on Real-Time Networks and Systems, Lille, France, November 2015. [ bib | DOI | http | .pdf ]
Keywords: wcet ; tdma ; worst-case execution time ; bus ; multi-core ; smt
[2] Denis Becker, Matthieu Moy, and Jérôme Cornet. Challenges for the Parallelization of Loosely Timed SystemC Programs. In IEEE International Symposium on Rapid System Prototyping (RSP), 2015. [ bib | http | .pdf ]

2014

[1] Matthieu Moy. High-level Models for Embedded Systems. Habilitation à diriger des recherches (HDR), Univ. Grenoble Alpes, F-38000 Grenoble, France, Verimag, March 2014. [ bib | http | .pdf ]
[2] Matthieu Moy. Compte-rendu d'habilitation : Modélisation à haut niveau d'abstraction pour les systèmes embarqués. Technique et Science Informatiques, 33(3):285--293, 2014. [ bib | http | .pdf ]
Les systèmes embarqués modernes ont atteint un niveau de complexité qui fait qu'il n'est plus possible d'attendre les premiers prototypes physiques pour valider les décisions sur l'intégration des composants matériels et logiciels. Il est donc nécessaire d'utiliser des modèles, tôt dans le flot de conception. Les travaux présentés dans ce document contribuent à l'état de l'art dans plusieurs domaines. Nous présentons dans un premier temps de nouvelles techniques de vérification de programmes écrits dans des langages généralistes comme C, C++ ou Java. Dans un second temps, nous utilisons des outils de vérification formelle sur des modèles écrits en SystemC au niveau transaction (TLM). Plusieurs approches sont présentées, la plupart d'entre elles utilisent des techniques de compilations spécifiques à SystemC pour transformer le programme SystemC en un format utilisable par les outils. La seconde partie du document s'intéresse aux propriétés non-fonctionnelles des modèles : performances temporelles, consommation électrique et température. Dans le contexte de la modélisation TLM, nous proposons plusieurs techniques pour enrichir des modèles fonctionnels avec des informations non-fonctionnelles. Enfin, nous présentons les contributions faites à l'analyse de performance modulaire (MPA) avec le calcul temps-réel (RTC). Nous proposons plusieurs connections entre ces modèles analytiques et des formalismes plus expressifs comme les automates temporisés et le langage de programmation Lustre. Ces connexion posent le problème théorique de la causalité, qui est formellement défini et résolu avec un algorithme nouveau dit de " fermeture causale ".

2013

[1] Tayeb Bouhadiba, Matthieu Moy, Florence Maraninchi, Jérôme Cornet, Laurent Maillet-Contoz, and Ilija Materic. Co-Simulation of Functional SystemC TLM Models with Power/Thermal Solvers. In Virtual Prototyping of Parallel and Embedded Systems (VIPES), Boston, US, May 2013. [ bib | http | .pdf ]
Modern systems-on-chips need sophisticated power-management policies to control their power consumption and temperature. These power-management policies are usually implemented partly in software, with hardware support. They need to be validated early, hence power and temperature-aware simulation techniques at the system-level need to be developed. Existing approaches for system-level power and thermal analysis usually either completely abstract the functionality (allowing only simple scenarios to be simulated), or run the functional simulation independently from the non-functional one. The approach presented in this paper allows a coupled simulation of a SystemC/TLM model, possibly including the actual embedded software, with a power and temperature solver such as ATMI or the commercial tool ACEplorer. Power and temperature analysis is done based on the stimuli sent by the SystemC/TLM platform, which in turn can take decisions based on the non-functional simulation.

[2] Matthieu Moy. Parallel Programming with SystemC for Loosely Timed Models: A Non-Intrusive Approach. In The Design, Automation, and Test in Europe (DATE), Grenoble, France, March 2013. 16.4% accepted as long-paper, Rank A+ GDR SoC-SiP. [ bib | http | .pdf ]
The SystemC/TLM technologies are widely accepted in the industry for fast system-level simulation. An important limitation of SystemC regarding performance is that the reference implementation is sequential, and the official semantics makes parallel executions difficult. As the number of cores in computers increase quickly, the ability to take advantage of the host parallelism during a simulation is becoming a major concern. Most existing work on parallelization of SystemC targets cycle-accurate simulation, and would be inefficient on loosely timed systems since they cannot run in parallel processes that do not execute simultaneously. We propose an approach that explicitly targets loosely timed systems, and offers the user a set of primitives to express tasks with duration, as opposed to the notion of time in SystemC which allows only instantaneous computations and time elapses without computation. Our tool exploits this notion of duration to run the simulation in parallel. It runs on top of any (unmodified) SystemC implementation, which lets legacy SystemC code continue running as-it-is. This allows the user to focus on the performance-critical parts of the program that need to be parallelized.

Keywords: SystemC; TLM; parallelism; multi-core; loosely-timed
[3] Tayeb Bouhadiba, Matthieu Moy, and Florence Maraninchi. System-level modeling of energy in TLM for early validation of power and thermal management. In Design Automation and Test Europe (DATE), Grenoble, France, March 2013. 16.4% accepted as long-paper, Rank A+ GDR SoC-SiP. [ bib | http | .pdf ]
[4] Claude Helmstetter and Matthieu Moy. LIBTLMPWT: Model power-consumption and temperature in systemc/tlm. Published as Free Software (GPL License), 2013. [ bib | http ]
[5] Claude Helmstetter, Jérôme Cornet, Bruno Galilée, Matthieu Moy, and Pascal VIVET. Fast and Accurate TLM Simulations using Temporal Decoupling for FIFO-based Communications. In Design, Automation and Test in Europe (DATE), page 1185, Grenoble, France, Mar 2013. acceptance rate: 302/829 = 36.4% all categories, Rank A+ GDR SoC-SiP. [ bib | http | .pdf ]
Untimed models of large embedded systems, generally written using SystemC/TLM, allow the software team to start simulations before the RTL description is available, and then provide a golden reference model to the verification team. For those two purposes, only a correct functional behavior is required, but users are asking more and more for timing estimations early in the design flow. Because companies cannot afford to maintain two simulators for the same chip, only local modifications of the untimed model are considered. A known approach is to add timing annotations into the code and to reduce the number of costly context switches using temporal decoupling, meaning that a process can go ahead of the simulation time before synchronizing again. Our current goal is to apply temporal decoupling to the TLM platform of a many-core SoC dedicated to high performance computing. Part of this SoC communicates using classic memory-mapped buses, but it can be extended with hardware accelerators communicating using FIFOs. Whereas temporal decoupling for memory-based transactions has been widely studied, FIFO-based communications raise issues that have not been addressed before. In this paper, we provide an efficient solution to combine temporal decoupling and FIFO-based communications.

2012

[1] Jérôme Cornet, Laurent Maillet-Contoz, Ilija Materic, Sylvian Kaiser, Hela Boussetta, Tayeb Bouhadiba, Matthieu Moy, and Florence Maraninchi. Co-Simulation of a SystemC TLM Virtual Platform with a Power Simulator at the Architectural Level: Case of a Set-Top Box. In Design Automation Conference, page SESSION 10U: USER TRACK, San Francisco, US, June 2012. [ bib | http ]
The ability to perform power estimation early in the design flow is becoming more and more critical as power optimization requirements grow. For now, standalone power simulators allow such estimation, based on typical stimuli described in a use-case scenario. We propose a co-simulation of SystemC TLM platforms with a Power model. This way, the Power model benefits from more realistic stimuli. In addition, it is possible to provide real-time information from the Power model back to the SystemC TLM simulation, such as temperature values.

Keywords: power estimation; temperature; systemc; transaction-level modeling
[2] Matthieu Moy. sc-during: tasks with duration for parallel programming in SystemC. Published as Free Software (LGPL License), 2012. [ bib | http ]
[3] Julien Henry, David Monniaux, and Matthieu Moy. Succinct representations for abstract interpretation. In Static analysis Symposium (SAS), 2012. Acceptance rate: 40%, Rank A CORE 2014. [ bib ]
[4] Julien Henry, David Monniaux, and Matthieu Moy. PAGAI: a path sensitive static analyzer. In Bertrand Jeannet, editor, Tools for Automatic Program Analysis (TAPAS), 2012. [ bib ]
We describe the design and the implementation of PAGAI, a new static analyzer working over the LLVM compiler infrastructure, which computes inductive invariants on the numerical variables of the analyzed program. PAGAI implements various state-of-the-art algorithms combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside the control flow graph while avoiding systematic exponential enumerations. It is parametric in the abstract domain in use, the iteration algorithm, and the decision procedure. We compared the time and precision of various combinations of analysis algorithms and abstract domains, with extensive experiments both on personal benchmarks and widely available GNU programs.

2011

[1] Kevin Marquet, Matthieu Moy, and Bertrand Jeannet. Efficient Encoding of SystemC/TLM in Promela. In DATICS-IMECS, Hong-Kong, 03 2011. [ bib | http | .pdf ]
To deal with the ever growing complexity of Systems-on-Chip, designers use models early in the design flow. SystemC is a commonly used tool to write such models. In order to verify these models, one thriving approach is to encode its semantics into a formal language, and then to verify it with verification tools. Various encodings of SystemC into formal languages have already been proposed, with different performance implications. In this paper, we investigate a new, automatic, asynchronous means to formalize models. Our encoding supports the subset of the concurrency and communication constructs offered by SystemC used for high-level modeling. We increase the confidence in the fact that encoded programs have the same semantics as the original one by model-checking a set of properties. We give experimental results on our formalization and compare with previous works.

Keywords: SystemC, Transaction-Level Modeling, Promela, Spin, Model-checking
[2] Giovanni Funchal, Matthieu Moy, Laurent Maillet-Contoz, and Florence Maraninchi. Faithfulness considerations for virtual prototyping of systems-on-chip. In 3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO), Heraklion, Crete, Greece, jan 2011. [ bib | .pdf ]
Virtual prototypes are simulators used in the consumer electronics industry. They enable the development of embedded software before the real, physical hardware is available, hence providing important gains in speed of development and time-to-market. Transaction-level Modeling (TLM) is a widely used technique for designing such virtual prototypes. Its main insight is that many micro-architectural details (i.e. caches, fifos and pipelines) can be omitted from the model as they should not impact the behavior perceived from a software programmer's point-of-view. In this paper, we shall see that this assumption is not always true, specially for low-level software (e.g. drivers). As a result, there may be bugs in the software which are not observable on a TLM virtual prototype, designed according to the current modeling practices. We call this a "faithfulness" issue. Our experience shows that many engineers are not aware of this issue. Therefore, we provide an in-depth and intuitive explanation of the sort of bugs that may be missed. We claim that, to a certain extent, modified TLM models can be faithful without losing the benefits in terms of time-to-market and ease of modeling. However, further investigation is required to understand how this could be done in a more general framework.

[3] Giovanni Funchal and Matthieu Moy. jTLM: an experimentation framework for the simulation of transaction-level models of systems-on-chip. In Design, Automation and Test in Europe (DATE), 2011. acceptance rate : 314/950 = 33%, Rank A+ GDR SoC-SiP. [ bib | .pdf ]
Virtual prototypes are simulators used in the consumer electronics industry. Transaction-level Modeling (TLM) is a widely used technique for designing such virtual prototypes. In particular, they allow for early development of embedded software.

The SystemC modeling language is the current industry standard for developing virtual prototypes. Our experience suggests that writing TLM models exclusively in SystemC leads sometimes to confusion between modeling concepts and their implementation, and may be the root of some known bad practices.

This paper introduces jTLM, an experimentation framework that allow us to study the extent to which common modeling issues come from a more fundamental constraint of the TLM approach. We focus on a discussion of the two modes of simulation scheduling: cooperative and preemptive. We confront the implications of these two modes on the way of designing TLM models, the software bugs exposed by the simulators and the performance.

[4] Matthieu Moy. Efficient and Playful Tools to Teach Unix to New Students. In 16th Annual Conference on Innovation and Technology in Computer Science Education ITiCSE, Darmstadt Allemagne, 06 2011. Acceptance rate : 66/169 = 39%, Rank A CORE 2014. [ bib | http | .pdf ]
Teaching Unix to new students is a common tasks in many higher schools. This paper presents an approach to such course where the students progress autonomously with the help of the teacher. The traditional textbook is complemented with a wiki, and the main thread of the course is a game, in the form of a treasure hunt. The course finishes with a lab exam, where students have to perform practical manipulations similar to the ones performed during the treasure hunt. The exam is graded fully automatically. This paper discusses the motivations and advantages of the approach, and gives an overall view of the tools we developed. The tools are available from the web, and open-source, hence re-usable outside the Ensimag.

Keywords: Unix, Education, Exam, Treasure Hunt
[5] Giovanni Funchal and Matthieu Moy. Modeling of time in discrete-event simulation of systems-on-chip. In ACM/IEEE Ninth International Conference on Formal Methods and Models for Codesign MEMOCODE, Cambridge Royaume-Uni, 07 2011. Acceptance rate : 16/43 = 37%. [ bib | .pdf ]
Today's consumer electronics industry uses modeling and simulation to cope with the complexity and time-to-market challenges of designing high-tech devices. In such context, Transaction-Level Modeling (TLM) is a widely spread modeling approach often used in conjunction with the IEEE standard SystemC discrete-event simulator. In this paper, we present a novel approach to modeling time that distinguishes between instantaneous actions and tasks with a duration. We argue that this distinction should be natural to the user. In addition, we show that it gives us important insight and better comprehension of what actions can overlap in time. We are able to exploit this distinction to parallelize the simulation, achieving an important speedup and exposing subtle software bugs related to parallelism. We propose a set of primitives and discuss the design decisions, expressiveness and semantics in depth. We present a research simulator called jTLM that implements all these ideas.

Keywords: TLM, time, duration, Java, jTLM
[6] Karine Altisen and Matthieu Moy. Causality closure for a new class of curves in real-time calculus. In Proceedings of the 1st International Workshop on Worst-Case Traversal Time, pages 3--10, Vienna, Autriche, 2011. ACM. [ bib | DOI | .pdf | .pdf ]
Real-Time Calculus (RTC) is a framework to analyze heterogeneous real-time systems that process event streams of data. The streams are characterized by arrival curves which express upper and lower bounds on the number of events that may arrive over any specified time interval. System properties may then be computed using algebraic techniques in a compositional way. The property of causality on arrival curves essentially characterizes the absence of deadlock in the corresponding generator. A mathematical operation called causality closure transforms arbitrary curves into causal ones. In this paper, we extend the existing theory on causality to the class Upac of infinite curves represented by a finite set of points plus piecewise affine functions, where existing algorithms did not apply. We show how to apply the causality closure on this class of curves, prove that this causal representative is still in the class and give algorithms to compute it. This provides the tightest pair of curves among the curves which accept the same sets of streams.

Keywords: algorithms, causality, real-time calculus
[7] Matthieu Moy. Unix-training: a set of tools to teach Unix efficiently. Published as Free Software (LGPL License), 2011. [ bib | http ]
[8] Julien Henry, David Monniaux, and Matthieu Moy. PAGAI static analyzer: Path analysis for invariant generation by abstract interpretation. Published as Free Software (CECILL-C License), 2011. [ bib | http ]

2010

[1] Karine Altisen and Matthieu Moy. ac2lus: Bringing SMT-solving and abstract interpretation techniques to real-time calculus through the synchronous language Lustre. In 22nd Euromicro Conference on Real-Time Systems (ECRTS), Brussels, Belgium, July 2010. Acceptance rate: 27/112 = 24%, Rank A CORE 2014. [ bib | .pdf ]
We present an approach to connect the Real-Time Calculus (RTC) method to the synchronous data-flow language Lustre, and its associated tool-chain, allowing the use of techniques like SMT-solving and abstract interpretation which were not previously available for use with RTC.

The approach is supported by a tool called ac2lus. It allows to model the system to be analyzed as general Lustre programs with inputs specified by arrival curves; the tool can compute output arrival curves or evaluate upper and lower bounds on any variable of the components, like buffer sizes.

Compared to existing approaches to connect RTC to other formalisms, we believe that the use of Lustre, a real programming language, and the synchronous hypothesis make the task easier to write models, and we show that it allows a great flexibility of the tool itself, with many variants to fine-tune the performances.

[2] Karine Altisen and Matthieu Moy. Arrival curves for real-time calculus: the causality problem and its solutions. In J. Esparza and R. Majumdar, editors, TACAS, pages 358--372, March 2010. Acceptance rate: 24/110 = 21%, Rank A CORE 2014. [ bib | .pdf ]
The Real-Time Calculus (RTC) is a framework to analyze heterogeneous real-time systems that process event streams of data. The streams are characterized by pairs of curves, called arrival curves, that express upper and lower bounds on the number of events that may arrive over any specified time interval. System properties may then be computed using algebraic techniques in a compositional way. A well-known limitation of RTC is that it cannot model systems with states and recent works studied how to interface RTC curves with state-based models. Doing so, while trying, for example to generate a stream of events that satisfies some given pair of curves, we faced a causality problem: it can be the case that, once having generated a finite prefix of an event stream, the generator deadlocks, since no extension of the prefix can satisfy the curves anymore. When trying to express the property of the curves with state-based models, one may face the same problem.

This paper formally defines the problem on arrival curves, and gives algebraic ways to characterize causal pairs of curves, i.e. curves for which the problem cannot occur. Then, we provide algorithms to compute a causal pair of curves equivalent to a given curve, in several models. These algorithms provide a canonical representation for a pair of curves, which is the best pair of curves among the curves equivalent to the ones they take as input.

[3] Karine Altisen, Yanhong Liu, and Matthieu Moy. Performance evaluation of components using a granularity-based interface between real-time calculus and timed automata. In Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL), Paphos, Cyprus, March 2010. Electronic Proceedings in Theoretical Computer Science. [ bib | .pdf ]
To analyze complex and heterogeneous real-time embedded systems, recent works have proposed interface techniques between real-time calculus (RTC) and timed automata (TA), in order to take advantage of the strengths of each technique for analyzing various components. But the time to analyze a state-based component modeled by TA may be prohibitively high, due to the state space explosion problem. In this paper, we propose a framework of granularity-based interfacing to speed up the analysis of a TA modeled component. First, we abstract fine models to work with event streams at coarse granularity. We perform analysis of the component at multiple coarse granularities and then based on RTC theory, we derive lower and upper bounds on arrival patterns of the fine output streams using the causality closure algorithm of [?]. Our framework can help to achieve tradeoffs between precision and analysis time.

[4] Kevin Marquet and Matthieu Moy. PinaVM: a SystemC front-end based on an executable intermediate representation. In International Conference on Embedded Software, page 79, Scottsdale, USA, 10 2010. Acceptance rate: 29/89 = 32%, Rank A CORE 2014. [ bib | .pdf ]
SystemC is the de facto standard for modeling embedded systems. It allows system design at various levels of ab- stractions, provides typical object-orientation features and incorporates timing and concurrency concepts. A SystemC program is typically processed by a SystemC front-end in order to verify, debug and/or optimize the architecture. Designing a SystemC front-end is a difficult task and existing approaches suffer from limitations. In this paper, we present a new approach that addresses most of these limitations. We detail this approach, based on an executable intermediate representation. We introduce PinaVM, a new, open-source SystemC front-end and implementation of our contributions. We give experimental results on this tool.

Keywords: Modeling, Validation, SystemC, System on Chip
[5] Kevin Marquet, Matthieu Moy, and Bageshri Karkare. A theoretical and experimental review of SystemC front-ends. In Forum for Design Languages (FDL), 2010. B.1.4, C.3 OpenTLM (Projet Minalogic). [ bib | .pdf ]
SystemC is a widely used tool for prototyping Systems-on-a-Chip. Being implemented as a C++ library, a plain C++ compiler is sufficient to compile and simulate a SystemC program. However, a SystemC program needs to be processed by a dedicated tool in order to visualize, formally verify, debug and/or optimize the architecture. In this paper we focus on the tools (called front-ends) used in the initial stages of processing SystemC programs. We describe the challenges in developing SystemC front-ends and present a survey of existing solutions. The limitations and capabilities of these tools are compared for various features of SystemC and intended back-end applications. We present typical examples that front-ends should ideally be able to process, and give theoretical limitations as well as experimental results of existing tools.

Keywords: SystemC, front-end, compilation, review
[6] Kevin Marquet and Matthieu Moy. PinaVM: PinaVM Is Not A Virtual Machine. Published as Free Software (LGPL License), 2010. [ bib | http ]
[7] Giovanni Funchal, Matthieu Moy, Florence Maraninchi, and Laurent Maillet-Contoz. Faithfulness considerations for virtual prototyping of systems-on-chip. Technical report, VERIMAG, 2010. [ bib | .pdf ]
Virtual prototypes are simulators used in the consumer electronics industry. They enable the development of embedded software before the real, physical hardware is available, hence providing important gains in speed of development and time-to-market. Transaction-level Modeling (TLM) is a widely used technique for designing such virtual prototypes. Its main insight is that many micro-architectural details (i.e. caches, fifos and pipelines) can be omitted from the model as they should not impact the behavior perceived from a software programmerś point-of-view. In this paper, we shall see that this assumption is not always true, specially for low-level software (e.g. drivers). As a result, there may be bugs in the software which are not observable on a TLM virtual prototype, designed according to the current modeling practices. We call this a faithfulness issue. Our experience shows that many engineers are not aware of this issue. Therefore, we provide an in-depth and intuitive explanation of the sort of bugs that may be missed. We claim that, to a certain extent, modified TLM models can be faithful without losing the benefits in terms of time-to-market and ease of modeling. However, further investigation is required to understand how this could be done in a more general framework.\n

2009

[1] Loïc Besnard, Thierry Gautier, Matthieu Moy, Jean-Pierre Talpin, Kenneth Johnson, and Florence Maraninchi. Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form. In Ninth International Workshop on Automated Verification of Critical Systems (AVOCS'09). Electronic Communications of the EASST, September 2009. [ bib | .pdf ]
We present an approach for the translation of imperative code (like C, C++) into the synchronous formalism Signal, in order to use a model-checker to verify properties on the source code. The translation uses SSA as an intermediate formalism, and the GCC compiler as a front-end. The contributions of this paper with respect to previous work are a more efficient translation scheme, and the management of parallel code. It is applied successfully on simple SystemC examples.

2008

[1] Florence Maraninchi, Matthieu Moy, Jérôme Cornet, Laurent Maillet-Contoz, Claude Helmstetter, and Claus Traulsen. SystemC/TLM Semantics for Heterogeneous System-on-Chip Validation. In IEEE, editor, 2008 Joint IEEE-NEWCAS and TAISA Conference 2008 Joint IEEE-NEWCAS and TAISA Conference, Montréal Canada, June 2008. B.6.3, D.2.4, D.3.1, F.4.3, F.3.1, B.8.1. [ bib | http ]
SystemC has become a de facto standard for the system-level description of systems-on-a-chip. SystemC/TLM is a library dedicated to transaction level modeling. It allows to define a virtual prototype of a hardware platform, on which the embedded software can be tested. Applying formal validation techniques to SystemC descriptions of SoCs requires that the semantics of the language be formalized. The model of time and concurrency underlying the SystemC definition is intermediate between pure synchrony and pure asynchrony. We list the available solutions for the semantics of SystemC/TLM, and explain how to connect SystemC to existing formal validation tools.

Keywords: SystemC; TLM; lustre; spin; promela; semantics; model-checking; verification; model; SoC; System-on-a-Chip

2007

[1] Claus Traulsen, Jérôme Cornet, Matthieu Moy, and Florence Maraninchi. A SystemC/TLM semantics in Promela and its possible applications. In 14th Workshop on Model Checking Software SPIN, July 2007. [ bib | .pdf ]
SystemC has become a de-facto standard for the modeling of systems-on-a-chip, at various levels of abstraction, including the so-called transaction level (TL). Verifying properties of a TL model requires that SystemC be translated into some formally defined language for which there exist verification back-ends. Since SystemC has no formal semantics, this includes a careful encoding of the SystemC scheduler, which has both synchronous and asynchronous features, and a notion of time. In a previous work, we described LusSy a complete chain from SystemC to a synchronous formalism and its associated verification tools. In this paper, we describe the encoding of the SystemC scheduler into a asynchronous formalism, namely Promela (the input language for Spin). We comment on the possible uses of this new encoding, and compare it with the synchronous encoding.

2006

[1] Matthieu Moy, Florence Maraninchi, and Laurent Maillet-Contoz. LusSy: an open tool for the analysis of systems-on-a-chip at the transaction level. Design Automation for Embedded Systems, 2006. special issue on SystemC-based systems. [ bib | .pdf ]
We describe a toolbox for the analysis of Systems-on-a-chip written in SystemC at the transaction level. The tool is able to extract information from SystemC code, and to build a set of parallel automata that capture the semantics of a SystemC design, including the transaction-level specific constructs. As far as we know, this provides the first executable formal semantics of SystemC. Being implemented as a traditional compiler front-end, it is able to deal with general SystemC designs. The intermediate representation is now connected to existing formal verification tools via appropriate encodings. The toolbox is open and other tools will be used in the future.

[2] Matthieu Moy, V. H. Gupta, and K. Gopinath. Framogr: a FRAMework for the MOdeling and simulation of GRoup protocols. Published as Free Software (LGPL License), 2006. http://download.gna.org/framogr/. [ bib ]
[3] Claude Helmstetter, Florence Maraninchi, Laurent Maillet-Contoz, and Matthieu Moy. Automatic generation of schedulings for improving the test coverage of systems-on-a-chip. FMCAD, pages 171--178, 2006. Acceptance rate: 21/90 = 23%. [ bib | DOI | .pdf ]
SystemC is becoming a de-facto standard for the early simulation of Systems-on-a-chip (SoCs). It is a parallel language with a scheduler. Testing a SoC written in SystemC implies that we execute it, for some well chosen data. We are bound to use a particular deterministic implementation of the scheduler, whose specification is non-deterministic. Consequently, we may fail to discover bugs that would have appeared using another valid implementation of the scheduler. Current methods for testings SoCs concentrate on the generation of the inputs, and do not address this problem at all. We assume that the selection of relevant data is already done, and we generate several schedulings allowed by the scheduler specification. We use dynamic partial-order reduction techniques to avoid the generation of two schedulings that have the same effect on the system’s behavior. Exploring alternative schedulings during testing is a way of guaranteeing that the SoC description, and in particular the embedded software, is scheduler-independent, hence more robust. The technique extends to the exploration of other non-fully specified aspects of SoC descriptions, like timing.

2005

[1] Matthieu Moy. Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level. PhD thesis, INPG, Grenoble, France, December 2005. [ bib | http ]
The work presented in this document deals with the formal verification models of Systems-on-a-Chip at the transaction level (TLM). We present the transaction level and its variants, and remind how this new level of abstraction is today necessary in addition to the register transfer level (RTL) to accommodate the growing constraints of productivity and quality, and how it integrates in the design flow.

We present a new tool, called LusSy, that allows property-checking on transactional models written in SystemC. Its structure is similar to the one of a compiler: A front-end, Pinapa, that reads the source program, a semantic extractor, Bise, into our intermediate formalism HPIOM, a number of optimizations in the component Birth, and code generators for provers like Lustre and SMV.

LusSy has been designed to have as few limitation as possible regarding the way the input program is written. Pinapa uses a novel approach to extract the information from the SystemC program, and the semantic extraction implements several TLM constructs that have not been implemented in any other SystemC verification tool as of now. It doesn't require any manual annotation. The tool chain is completely automated.

LusSy is currently able to prove properties on small platforms. Its components are reusable to build compositional verification tools, or static code analyzers using techniques other than model-checking that can scale up more efficiently.

We present the theoretical principles for each step of the transformation, as well as our implementation. The results are given for small examples, and for a medium size case-study called EASY. Experimenting with LusSy allowed us to compare the various tools we used as provers, and to evaluate the effects of the optimizations we implemented.

[2] Matthieu Moy, Florence Maraninchi, and Laurent Maillet-Contoz. Pinapa: An extraction tool for SystemC descriptions of systems-on-a-chip. In EMSOFT, pages 317--324, September 2005. 25/88 = 28% accepted as regular papers, Rank A CORE 2014. [ bib | .pdf ]
SystemC is becoming a de-facto standard for the description of complex systems-on-a-chip. It enables system-level descriptions of SoCs: the same language is used for the description of the architecture, software and hardware parts. A tool like pinapa is compulsory to work on realistic SoCs designs for anything else than simulation: it is able to extract both architecture and behavior information from SystemC code, with very few limitations. pinapa can be used as a front-end for various analysis tools, ranging from “superlint” to model-checking. It is open source and available from http://greensocs.sourceforge.net/pinapa/. There exists no equivalent tool for SystemC up to now.

[3] Matthieu Moy, Florence Maraninchi, and Laurent Maillet-Contoz. LusSy: A toolbox for the analysis of systems-on-a-chip at the transactional level. In International Conference on Application of Concurrency to System Design, pages 26--35, June 2005. Acceptance rate: 23/45 = 51%. [ bib | .pdf ]
We describe a toolbox for the analysis of Systems-on-a-chip described in SystemC at the transactional level. The tools are able to extract information from SystemC code, and to build a set of parallel automata that capture the semantics of a SystemC design, including the transaction-level specific constructs. As far as we know, this provides the first executable formal semantics of SystemC. Being implemented as a traditional compiler front-end, it is able to deal with general SystemC designs. The intermediate representation is now connected to existing formal verification tools via appropriate encodings. The toolbox is open and other tools will be used in the future.

[4] Matthieu Moy. Chapter 5.9, formal verification. In Frank Ghenassia, editor, Transaction-Level Modeling with SystemC. TLM Concepts and Applications for Embedded Systems, pages 190--206. Springer, 2005. [ bib | http ]
[5] Matthieu Moy. Pinapa: Pinapa Is Not a Parser. Published as Free Software (LGPL License), 2005. [ bib | http ]

This file was generated by bibtex2html 1.91.