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

• 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).