Encoding SystemC Models in Formal Synchronous Formalism

Print
 
Download Full Text
International Journal of Computer Applications
© 2011 by IJCA Journal
Volume 34 - Number 3
Year of Publication: 2011
Authors:
Riadh Hocine
Hamoudi Kalla
10.5120/4080-5876

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

@article{key:article,
	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}
}

Abstract

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.

Reference

  • 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. http://www.veripool.com/systemperl.html.
  • E.D.G.C. Front-End. Edison Design Group C++ Front-End. Website:http://edg.com/cpp.html, 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).