Proceedings of the 15th international symposium on System Synthesis (ISSS '02)
The Formal Execution Semantics of SpecC
Kyoto, Japan
October 02-October 04
ISBN: 1-58113-576-9
We present a rigorous but transparent semantics definition of the SpecC language that covers the execution of SpecC behaviors and their interaction with the kernel process. The semantics include wait, waitfor, par, and try statements as they are introduced in SpecC. We present our definition in form of distributed Abstract State Machine (ASM) rules strictly following the lines of the SpecC Language Reference Manual [4]. We mainly see our formal semantics in three application areas. First, it is a concise, unambiguous description for documentation and standardization. Second, it applies as a high--level, pseudo code--oriented specification for the implementation of a SpecC simulator. Finally, it is a first step for SpecC synthesis in order to identify similar concepts with other languages like VHDL and SystemC for the definition of common patterns and language subsets.
Index Terms:
ASMs, SpecC, formal specifications, simulation
Citation:
Rainer D?mer, Andreas Gerstlauer, Wolfgang Mueller, "The Formal Execution Semantics of SpecC," isss, pp.150-155, Proceedings of the 15th international symposium on System Synthesis (ISSS '02), 2002