Abstract
As a system-level modelling language, SystemC possesses several novel features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. It is challenging to formalise SystemC. In this paper, we study the denotational semantics for SystemC using Unifying Theories of Programming (abbreviated as UTP) [6]. Two trace variables are introduced, one is to record the state behaviours and another is to record the event behaviours. The timed model is formalised in a three-dimensional structure. A set of algebraic laws is explored, which can be proved via the achieved denotational semantics.
This work is partially supported by the National Basic Research Program of China (No. 2005CB321904), the National High Technology Research and Development Program of China (No. 2007AA010302), the National Natural Science Foundation of China (No. 90718004), Shanghai STCSM project (No. 06JC14022 and No. 067062017) and Shanghai Leading Academic Discipline Project (No. B412).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Brookes, S.D.: Full abstraction for a shared-variable parallel language. Information and Computation 127(2), 145–163 (1996)
Gawanmeh, A., Habibi, A., Tahar, S.: An executable operational semantics for SystemC using abstract state machines. Technical report, Department of Electrical and Computer Engineering, Concordia University Montreal (March 2004)
Habibi, A., Tahar, S.: SystemC fixpoint semantics. Technical report, Department of Electrical and Computer Engineering, Concordia University Montreal (January 2005)
He, J.: Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers. McGraw-Hill International Series in Software Engineering (1994)
Hoare, C.A.R., Hayes, I.J., He, J., Morgan, C., Roscoe, A.W., Sanders, J.W., Sorensen, I.H., Spivey, J.M., Sufrin, B.: Laws of programming. Communications of the ACM 38(8), 672–686 (1987)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)
IEEE. IEEE Standard Hardware Description Language based on the Verilog Hardware Description Language, vol. IEEE Standard 1364-2001. IEEE, Los Alamitos (2001)
Milner, R.: Communication and Mobile System: π-calculus. Cambridge University Press, Cambridge (1999)
Open SystemC Initiative (OSCI). Functional Specification for SystemC 2.0 (October 2001)
Open SystemC Initiative (OSCI). SystemC 2.0.1 Language Reference Manual (2003)
Peng, X., Zhu, H., He, J., Jin, N.: An operational semantics of an event-driven system-level simulator. In: Proc. SEW-30: The 30th IEEE/NASA Software Engineering Workshop, Columbia, Maryland, USA, April 2006, pp. 190–200. IEEE Computer Society Press, Los Alamitos (2006)
Ruf, J., Hoffmann, D.W., Gerlach, J., Kropf, T., Rosenstiel, W., Müller, W.: The simulation semantics of systemc. In: DATE ’01: Proceedings of the conference on Design, automation and test in Europe, Piscataway, NJ, USA, March 2001, pp. 64–70. IEEE Press, Los Alamitos (2001)
Zhu, H.: Linking the Semantics of a Multithreaded Discrete Event Simulation Language. PhD thesis, London South Bank University (February 2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhu, H., He, J., Peng, X., Jin, N. (2010). Denotational Approach to an Event-Driven System-Level Language. In: Butterfield, A. (eds) Unifying Theories of Programming. UTP 2008. Lecture Notes in Computer Science, vol 5713. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14521-6_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-14521-6_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14520-9
Online ISBN: 978-3-642-14521-6
eBook Packages: Computer ScienceComputer Science (R0)