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 of Handel-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 Bjorner and Zhou Chaochen act as inspiration, from the past, into the future for this research work.
展开▼
