The formal execution semantics of SpecC
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, pipe, and try statements as they are introduced in SpecC. We present our definition in form of distributed Abstract State Machine (ASM) rules reflecting the specification given in the SpecC Language Reference Manual . We mainly see our formal semantics in three application areas. First, it can be taken as a high-level, pseudo code-oriented specification for the implementation of a SpecC simulator which is outlined in a separate section. Second, it is a concise, unambiguous description for documentation and standardization. Finally, it is a first step for Spece synthesis in order to identify similar concepts with other languages like VHDL and SystemC for the definition of common patterns and language subsets.