Call for Paper - July 2022 Edition
IJCA solicits original research papers for the July 2022 Edition. Last date of manuscript submission is June 20, 2022. Read More

Encoding SystemC Models in Formal Synchronous Formalism

International Journal of Computer Applications
© 2011 by IJCA Journal
Volume 34 - Number 3
Year of Publication: 2011
Riadh Hocine
Hamoudi Kalla

Riadh Hocine and Hamoudi Kalla. Article: Encoding SystemC Models in Formal Synchronous Formalism. International Journal of Computer Applications 34(3):26-32, November 2011. Full text available. BibTeX

	author = {Riadh Hocine and Hamoudi Kalla},
	title = {Article: Encoding SystemC Models in Formal Synchronous Formalism},
	journal = {International Journal of Computer Applications},
	year = {2011},
	volume = {34},
	number = {3},
	pages = {26-32},
	month = {November},
	note = {Full text available}


The size and thus the complexity of many systems, that use an intellectual property component (IP), have reached a level where design validation with mere testing and simulation does not deliver the required quality any more. Obtaining a formal model from a non-formal one is a complex and error prone task. A logical step is therefore to try to generate automatically a formal description from an existing non-formal system model, thus making this step faster and more reliable. In this paper, we describe a methodology to automaticallygenerate formal synchronous models from existing non-formalsystem level design descriptions that integrates smoothly intoexisting co-design flows. We exemplify the approach with thepopular system design language SystemC and the flexible andexpressive synchronous dataflow formalism SIGNAL.SystemC is a HDL which allows for modeling systems in behavioral level, it is a set of library routines and macros implemented in C++, it is a good language for input of design flow for the systems which requires verification, but it is not a formal language.


  • Séméria L.and Ghosh A. 2000. Methodology for Hardware/Software Co-verification in C/C++.In Proceedings of the 2000 Asia and South Pacific Design Automation Conference(ASP-DAC)pp 405-408 (24-28 Jun. 2000),Yokohama, Japan.
  • IEEE Std 1666-2005. IEEE Standard SystemCLangauge Reference Manual, 2005.
  • Marquet K., Moy M. and JeannetB. "Efficient Encoding of SystemC/TML in Promela". DATICS-IMECS03, Hong-Kong 2011.
  • Habibi A. and Tahar S. "On the Transformation of SystemC to AsmL Using Abstract Interpretation". Electronic Notes in Theoretical Computer Science (ENTSC) vol. 131, pp. 39-49, 2005 in press.
  • Snyder W.2006.SystemPerl - APerl Library for SystemC.
  • E.D.G.C. Front-End. Edison Design Group C++ Front-End. Website:, 2006.
  • Doucet F., Shukla S., and Gupta R.2003. Introspection in System-Level Language Frameworks: Meta-level vs.Integrated.In Proceedings of 2003 Design, Automation and Test in Europe Conference (DATE)vol. 1, pp. 382–387,(2003).
  • Eibl C. J., Albrecht C., and R. Hagenau.2005. gSysC: A Graphical Front End for SystemC. In Proceedings of 19th European Conference on Modelingand Simulation (ECMS), Riga, Latvia (Jun. 2005).
  • Große D., Drechsler R, Linhard L. and Angst G.2003. Efficient Automatic Visualization of SystemC Designs.In Proceedings of the Forum on Specification and Design Languages (FDL), Frankfurt, Germany (Sep. 2003).
  • Gajski, D.D., Wu A.C.-H., Chaiyakul V., Mori S., Nukiyama T. and Bricaud P. 2000. Essential Issues for IP Reuse. In Proceedings of the 2000 Asia and South Pacific Design Automation Conference (ASP-DAC)pp. 37-42 (25-28 Jan. 2000). Yokohama, Japan.
  • Martin G. 1998. Design Methodologies for System Level IP. In Proceedings of the 1998 Design, Automation and Test in Europe Conference(DATE)pp. 286-189 (23-26 Feb. 1998), Paris France.
  • Potop-Butucaru D., De Simone R. andTalpin J.-P."The Synchronous Hypothesis and Polychronous Languages". Embedded Systems Design and Verification, pp 6-16-6-27, CRC press 2009.
  • Marchand H. and Rutten E. 2002. SIGNAL and SIGALI User’s Manual. Research Report IRISA/INRIA-Rennes, France.
  • Novello D. 2003. Tree SSA - A New High-Level Optimization Framework for the GNU Compiler Collection. In Proceeding of the Nord/USENIX Users Conference (Feb. 2003).
  • Kalla H., TalpinJ.-P., Berner D. and BesnardL. 2006. Automated Translation of C/C++ Models into a Synchronous Formalism. In Proceedings of the 13th Annual IEEE International Symposium and Workshop on Engineering of Computer Based Systems (ECBS)vol. 9 pp. 436 (27-30 Mar. 2006). Postdam, Germany.
  • Séméria L. 2001. Applying Pointer Analysis to the Synthesis of Hardware from C. Doctoral thesis, Department of Electrical Engineering of Stanford University, USA.
  • SémériaL. and De Micheli G. "Encoding of Pointers for Hardware Synthesis". IEEE Transactions on Very Large Scale Integration (VLSI) Systems - System Level Design. Vol 9 Issues 6 (Jan. 2001).
  • Séméria L. and De MicheliG.1998. SpC: Synthesis of Pointers in C Application of Pointer Analysis to the Behavioral Synthesis from C. In Proceedings of the 1998 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)pp. 340-346 (8-12 Nov. 1998).