Encoding SystemC Models in Formal Synchronous Formalism
Riadh Hocine, Hamoudi Kalla · 2011
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 automatically generate formal synchronous models from existing non-formal system level design descriptions that integrates smoothly into existing co-design flows. We exemplify the approach with the popular system design language SystemC and the flexible and expressive 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.