skip to main content
10.1145/1629335.1629349acmconferencesArticle/Chapter ViewAbstractPublication PagesesweekConference Proceedingsconference-collections
research-article

Formal and executable contracts for transaction-level modeling in SystemC

Published:12 October 2009Publication History

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

  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. Google ScholarGoogle ScholarDigital LibraryDigital Library
  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.Google ScholarGoogle Scholar
  3. The Spirit Consortium. IP-XACT 1.4 specification. www.spiritconsortium.org/releases/1.4.Google ScholarGoogle Scholar
  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. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. F. Ghenassia. Transaction Level Modeling With SystemC: TLM Concepts And Applications for Embedded Systems. Springer-Verlag, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  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. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. G. J. Holzmann. The model checker spin. IEEE Transactions on Software Engineering, 23(5):279--295,May 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  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.Google ScholarGoogle Scholar
  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. Google ScholarGoogle ScholarDigital LibraryDigital Library
  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.Google ScholarGoogle ScholarCross RefCross Ref
  11. K. L. Mcmillan. The SMV system, Nov. 06 1992.Google ScholarGoogle Scholar
  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. Google ScholarGoogle ScholarDigital LibraryDigital Library
  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.Google ScholarGoogle Scholar
  14. B. Niemann and C. Haubelt. Formalizing TLM with communicating state machines. In Forum on specification&Design Languages (FDL), pages 285--293, 2006.Google ScholarGoogle Scholar
  15. Open SystemC Initiative. IEEE 1666 Standard: SystemC Language Reference Manual, 2005. http://www.systemc.org/.Google ScholarGoogle Scholar
  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. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Formal and executable contracts for transaction-level modeling in SystemC

            Recommendations

            Comments

            Login options

            Check if you have access through your login credentials or your institution to get full access on this article.

            Sign in
            • Published in

              cover image ACM Conferences
              EMSOFT '09: Proceedings of the seventh ACM international conference on Embedded software
              October 2009
              332 pages
              ISBN:9781605586274
              DOI:10.1145/1629335

              Copyright © 2009 ACM

              Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

              Publisher

              Association for Computing Machinery

              New York, NY, United States

              Publication History

              • Published: 12 October 2009

              Permissions

              Request permissions about this article.

              Request Permissions

              Check for updates

              Qualifiers

              • research-article

              Acceptance Rates

              EMSOFT '09 Paper Acceptance Rate33of106submissions,31%Overall Acceptance Rate60of203submissions,30%

              Upcoming Conference

              ESWEEK '24
              Twentieth Embedded Systems Week
              September 29 - October 4, 2024
              Raleigh , NC , USA

            PDF Format

            View or Download as a PDF file.

            PDF

            eReader

            View online with eReader.

            eReader