CFP last date
22 April 2024
Reseach Article

Encoding SystemC Models in Formal Synchronous Formalism

by Riadh Hocine, Hamoudi Kalla
International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 34 - Number 3
Year of Publication: 2011
Authors: Riadh Hocine, Hamoudi Kalla
10.5120/4080-5876

Riadh Hocine, Hamoudi Kalla . Encoding SystemC Models in Formal Synchronous Formalism. International Journal of Computer Applications. 34, 3 ( November 2011), 26-32. DOI=10.5120/4080-5876

@article{ 10.5120/4080-5876,
author = { Riadh Hocine, Hamoudi Kalla },
title = { Encoding SystemC Models in Formal Synchronous Formalism },
journal = { International Journal of Computer Applications },
issue_date = { November 2011 },
volume = { 34 },
number = { 3 },
month = { November },
year = { 2011 },
issn = { 0975-8887 },
pages = { 26-32 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume34/number3/4080-5876/ },
doi = { 10.5120/4080-5876 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-06T20:20:09.653555+05:30
%A Riadh Hocine
%A Hamoudi Kalla
%T Encoding SystemC Models in Formal Synchronous Formalism
%J International Journal of Computer Applications
%@ 0975-8887
%V 34
%N 3
%P 26-32
%D 2011
%I Foundation of Computer Science (FCS), NY, USA
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.

References
  1. 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.
  2. IEEE Std 1666-2005. IEEE Standard SystemCLangauge Reference Manual, 2005.
  3. Marquet K., Moy M. and JeannetB. "Efficient Encoding of SystemC/TML in Promela". DATICS-IMECS03, Hong-Kong 2011.
  4. 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.
  5. Snyder W.2006.SystemPerl - APerl Library for SystemC. http://www.veripool.com/systemperl.html.
  6. E.D.G.C. Front-End. Edison Design Group C++ Front-End. Website:http://edg.com/cpp.html, 2006.
  7. 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).
  8. 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).
  9. 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).
  10. 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.
  11. 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.
  12. 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.
  13. Marchand H. and Rutten E. 2002. SIGNAL and SIGALI User’s Manual. Research Report IRISA/INRIA-Rennes, France.
  14. 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).
  15. 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.
  16. 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.
  17. 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).
  18. 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).
Index Terms

Computer Science
Information Sciences

Keywords

SystemC SIGNAL Pointers Analysis Static Single Assignment Functional and Compositional Correctness