Investigation On Operational Semantics And Algebraic Laws Of An Event-driven System-level Simulator

Nowadays, SoC (Systems-on-a-Chip) systems have been used more and more widely. One SoC system may consist of different function modules, including hardware components and software components. To achieve high performance with low cost, hardware/software co-design methodologies are adopted. Usually, the first step of hardware/software co-design is to describe the system behaviors using a system-level description language. SystemC is such a language based on C++. SystemC has been used on system modeling and hardware/software co-design, widely. Recently, SystemC 2.1 has been approved as an IEEE standard (IEEE 1666) for system level chip design.As a system-level description language, SystemC possesses some new and interesting programming features, including delayed event notifications, event notification cancelation, event notification overriding and delta-cycle. These programming features usually make programmers confused. It is also mandatory to provide a strict, precise and unambiguous understanding of SystemC for development of simulators, synthesizers and verifiers. User manuals written by natural languages always contain subtle ambiguities. This thesis presents an operational semantics of a kernel subset language of SystemC, using structural operational semantics. Based on the operational semantics, bi-simulation is defined to check the equivalence of two programs. A prototype of the simulator is implemented using Prolog, which helps check the correctness of the presented operational semantics. Finally, a set of algebraic laws of SystemC are presented, which can be verified via bi-simulation on operational semantics model. To the best knowledge of the author, there are few publications about the research on the algebraic laws of SystemC.Operational semantics and algebraic laws are very useful in practice. Operational semantics is also the base for furture work on synthesis and verification. Algebraic laws can be applied in design optimization and program transformation, with correctness guaranteed.