As a system-level modelling language, SystemC possesses several novel features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. We have explored the denotational semantics [15] for SystemC using Unifying Theories of Programming (abbreviated as UTP) [6], where algebraic laws can be achieved based on the denotational model. In this paper, we consider the inverse work; i.e., generating the denotational semantics from algebraic semantics for SystemC. A complete set of algebraic laws is explored. The concept of head normal from is applied in supporting the calculation. We also explore the simulation of algebraic laws and head normal form. Based on this, the mechanical derivation of denotational semantics from algebraic semantics is also studied.
展开▼
