A Denotational Semantics for Handel-C - Formal Methods and Hybrid Real-Time Systems - page 45

A Denotational Semantics for Handel-C

Andrew Butterfield

Trinity College Dublin
[e-mail]

Abstract. 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.

1 Introduction

This paper describes a denotational semantics for Handel-C which gives a pro-
gram a meaning as a set of “Typed Assertion Traces”.
Handel-C 1 [1] is a language originally developed by the Hardware Compila-
tion Group at Oxford University Computing Laboratory, and now marketed by
Celoxica Ltd. It is a hybrid of CSP [2] and C, designed to target hardware
implementations, specifically field-programmable gate arrays (FPGAs) [3]. The
language has sequential and parallel constructs and global variable assignment
and channel communication. The language targets synchronous hardware with
multiple clock domains. All assignments and channel communication events take
one clock cycle. All expression and conditional evaluations, as well as priority
resolutions are deemed to be instantaneous, effectively being completed before
the current clock-cycle ends.
We see the final semantics of Handel-C as having four components: types;
priorities; synchronous cores; and the asynchronous environment. A detailed
description of these and their motivation is given in [4]. Here we simply stress that
this paper is primarily concerned with the semantics of the synchronous cores,
incorporating priorities. The topics of typing and the external asynchronous
interface are beyond the scope of this paper.
We first introduce the language, then describe prior and related work in this
area, before motivating and describing the domains used for our denotational
semantics.

1 Handel-C is the registered trademark of Celoxica Ltd ( www.celoxica.com ).