A “Hardware Compiler” Semantics for Handel-C

We present a denotational semantics for the hardware compilation language Handel-C that maps language constructs to a set of equations, which describe the structure of the resulting hardware. This semantics is then shown to be useful for validating various algebraic laws which should hold for Handel-C programs, as well as exposing a key principle which governs how such hardware should be operated.