An operational semantics for Handel-C

We describe an operational semantics for the hardware compilation language Handel-C [10], which is a C-like language with channel communication and parallel constructs which compile down to mainly synchronously clocked hardware. The work in this paper builds on previous work describing the semantics of priority within Handel-C [9] and a denotational semantics for part of the language [8]. We describe a key subset of the language and show how a design decision for the real language, namely that default guards in prialt-statement executed in "zero-time", has consequences for the complexity of the operational semantics. We present the operational semantics, indicating clearly how it interfaces with the priority semantics of [9]. We then describe a notion of observational equivalence, and present an example illustrating how we handle the complexity of nested prialts in default guards.