Abstract

The problem of synthesis of gate-level descriptions of digital circuits from behavioural specifications written in higher-level programming languages (hardware compilation) has been studied for a long time, yet a definitive solution has not been forthcoming. In this talk I will describe a new technique based on recent advances in programming language theory: affine type systems, monoidal categories and game semantics. We argue that one of the major obstacles in the way of a useful and mature hardware compiler is the lack of a well defined function interface model, i.e. a canonical way in which functions can communicate with their arguments. We will show how digital circuits exhibit an inherent structure which is a model of affine higher-order type systems. Game semantics can provide interpretations for common language constants which are concretely representable in this setting, for both synchronous and asynchronous digital circuits. The key issue of sharing of resources and the additional structure required will also be addressed using game-semantic techniques. We illustrate these theoretical considerations with a prototype compiler from Syntactic Control of Interference (an affine dialect of Idealised Algol) into digital circuits.