Formal and executable contracts for transaction-level modeling in SystemC

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Formal and executable contracts for transaction-level modeling in SystemC

Full text

Pdf (553 KB)

Source

International Conference on Compilers, Architecture and Synthesis for Embedded Systems archive
Proceedings of the seventh ACM international conference on Embedded software table of contents

Grenoble, France

SESSION: Models and components table of contents

Pages 97-106

Year of Publication: 2009

ISBN:978-1-60558-627-4

Authors

Tayeb Bouhadiba	VERIMAG/Grenoble INP, Grenoble, France
Florence Maraninchi	VERIMAG/Grenoble INP, Grenoble, France
Giovanni Funchal	VERIMAG/STMicroelectronics, Grenoble, France

Sponsors

ACM: Association for Computing Machinery
SIGBED: ACM Special Interest Group on Embedded Systems
SIGMICRO: ACM Special Interest Group on Microarchitectural Research and Processing
SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 16, Downloads (12 Months): 17, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1629335.1629349 What is a DOI?

ABSTRACT

Transaction-Level Modeling (TLM) for systems-on-a-chip (SoCs) has become a standard in the industry, using SystemC. With SystemC/TLM, it is possible to develop an executable virtual prototype of a hardware platform, so that software developers can start writing code long before the actual chip is available. A hardware model in SystemC/TLM can be very abstract, compared to the detailed RTL model. It is clearly component-based, with guidelines defining how components should be designed for use in any TLM context. However, these guidelines are quite informal for the moment. In this paper, we establish a structural correspondence between functional SystemC/TLM models and a formal component-model for embedded systems called 42, for which we have defined a notion of control contract, and an execution mode for systems made of components' contracts. This is a way of formalizing the principles of functional SystemC/TLM. Moreover, it allows the combined use of SystemC/TLM components with 42 components. Demonstrating that such a combined use is possible is key to the adoption of formal components' definitions in the community of TLM users.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	T. Bouhadiba and F. Maraninchi. Contract-based coordination of hardware components for the development of embedded software. In COORDINATION'09, Lisbon, Portugal, June 2009.
	2	J. Buck, S. Ha, E. Lee, and D. Messerschmitt. Ptolemy: a framework for simulating and prototyping heterogeneous systems. International Journal of Computer Simulation, 4:155--182, April 1994.
	3	The Spirit Consortium. IP-XACT 1.4 specification. www.spiritconsortium.org/releases/1.4.
	4	J. Cornet, F. Maraninchi, and L. Maillet-Contoz. A method for the efficient development of timed and untimed transaction-level models of systems-on-chip. In DATE, Munich, Germany, Mar. 2008.
	5	F. Ghenassia. Transaction Level Modeling With SystemC: TLM Concepts And Applications for Embedded Systems. Springer-Verlag, 2005.
	6	P. Herber, J. Fellmuth, and S. Glesner. Model checking SystemC designs using timed automata. In CODES/ISSS '08, pages 131--136, New York, NY, USA, 2008. ACM.
	7	G. J. Holzmann. The model checker spin. IEEE Transactions on Software Engineering, 23(5):279--295,May 1997.
	8	K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1{2):134--152, Oct. 1997.
	9	F. Maraninchi and T. Bouhadiba. 42: Programmable models of computation for a component-based approach to heterogeneous embedded systems. In ACM GPCE, Salzburg, Austria, Oct. 2007.
	10	F. Maraninchi, M. Moy, C. Helmstetter, J. Cornet, C. Traulsen, and L. Maillet-Contoz. SystemC/TLM semantics for heterogeneous system-on-chip validation. In NEWCAS/TAISA, Montreal, Canada, June 2008.
	11	K. L. Mcmillan. The SMV system, Nov. 06 1992.
	12	M. Moy, F. Maraninchi, and L. Maillet-Contoz. The extraction tool for SystemC descriptions of systems-on-a-chip. In EMSOFT, New-York, USA, Sept. 2005.
	13	M. Moy, F. Maraninchi, and L. Maillet-Contoz. LusSy: an open tool for the analysis of systems-on-a-chip at the transaction level. Design Automation for Embedded Systems, 10(2--3), Sept. 2006.
	14	B. Niemann and C. Haubelt. Formalizing TLM with communicating state machines. In Forum on specification & Design Languages (FDL), pages 285--293, 2006.
	15	Open SystemC Initiative. IEEE 1666 Standard: SystemC Language Reference Manual, 2005. http://www.systemc.org/.
	16	O. Ponsini and W. Serwe. A schedulerless semantics of TLM models written in SystemC via translation into LOTOS. In 15th international symposium on formal methods, pages 278--293, 2008.