A Denotational Semantics for Handel-C

We present a denotational semantics for a fully functional subset of the Handel-C hardware compilation language [1], based on the concept of typed assertion traces. We motivate the choice of semantic domains by illustrating the complexities of the behaviour of the language, paying particular attention to the prialt (priority-alternation) construct l-C. We then define the typed assertion traces over an abstract notion of actions, which we then instantiate as state-transformers. The denotational semantics is then given and some examples are discussed. As is fitting given those honoured at the Festschrift of which this paper is a part, we show how the work of both Dines Bj¨orner and Zhou Chaochen act as inspiration, from the past, into the future for this research work.

• Type: Conference
• Year: 2007
• Where: BIRTHDAY
• Authors: Andrew Butterfield
• Keywords: Applied Computing, BIRTHDAY 2007, Denotational Semantics, Handel-C Hardware Compilation, Typed Assertion Traces