Formal support for untimed SystemC specifications: Application to high-level synthesis

SystemC lacks a well defined formal semantics for abstract specification, specifically for untimed models. This paper tackles this problem by providing the fundamentals of a framework which enables the analysis of any untimed SystemC specification under a formal meta-model. Then, the conditions for the SystemC specification to correspond with its formal meta-model are defined. As an application example, the use of the framework for high-level synthesis verification is shown.