Treffer: Semantic domains for Handel-C

Handel-C is a programming language which is a hybrid of CSP and C, designed to target hardware implementations, specifically field-programmable gate arrays (FPGAs). The language is C-like with CSP-like parallel constructs and channel communication added. All assignments and channel communication events take one clock cycle while all expression and conditional evaluations are deemed to be instantaneous. This report presents semantic domains required to give a denotational semantics of a simplified subset of the Handel-C language. We present the key domains and equations for a denotational semantics for Handel-C. The key contribution is that our semantics deals with a concurrent, deterministic language where events occur synchronously, in the presence of global shared variables. We exploit the finite and static nature of a Handel-C program s identifier space in order to define key concepts, such as world, change and choice. We have also demonstrated that our semantic domain is a c.p.o., with all our constructors shown to be monotonic, allowing us to assert the existence of fixpoints. General concurrency theories such as CSP and CSPP cater for a wider and more general range of circumstances than are found in Handel-C. By keeping our semantics separate and simpler, it is easier to ensure that it correctly captures the behaviour of the language. We view this work as leading towards a formal development methodology to allow the refinement of Handel-C programs from formal specifications. We hope to be able to integrate laws based on this semantics into the Circus refinement calculus framework. [Copyright &y& Elsevier]