TY - GEN
T1 - The geometry of synthesis how to make hardware out of software
AU - Ghica, Dan R.
PY - 2012/1/1
Y1 - 2012/1/1
N2 - High-level synthesis or “hardware compilation” is a behavioural synthesis method in which circuits are specified using conventional programming languages. Such languages are generally recognised as more accessible than hardware description languages, and it is expected that their use would significantly increase design productivity. The Geometry of Synthesis is a new hardware compilation technique which achieves this goal in a semantic-directed fashion, by noting that functional programming languages and diagrammatic descriptions of hardware share a common mathematical structure, and by using the game-semantic model of the programming language to reduce all computational effects to signal-like message passing. As a consequence, this technique has mature support for higher-order functions [1], local (assignable) state [2], concurrency [3] and (affine) recursion [4]. Moreover, the compiler can support features such as separate compilation, libraries and a foreign-function interface [5]. The programming language of GoS, Verity, is an “Algol-like” language [6] extended with concurrency features [7]. The interplay between the call-by-name function mechanism and local effects, an approach specific to Algol, is the key ingredient which makes it possible for a large class of programs in this language to have finitely representable semantic models which can be synthesised as stand-alone static circuits. The compiler is available as an open-source download.
AB - High-level synthesis or “hardware compilation” is a behavioural synthesis method in which circuits are specified using conventional programming languages. Such languages are generally recognised as more accessible than hardware description languages, and it is expected that their use would significantly increase design productivity. The Geometry of Synthesis is a new hardware compilation technique which achieves this goal in a semantic-directed fashion, by noting that functional programming languages and diagrammatic descriptions of hardware share a common mathematical structure, and by using the game-semantic model of the programming language to reduce all computational effects to signal-like message passing. As a consequence, this technique has mature support for higher-order functions [1], local (assignable) state [2], concurrency [3] and (affine) recursion [4]. Moreover, the compiler can support features such as separate compilation, libraries and a foreign-function interface [5]. The programming language of GoS, Verity, is an “Algol-like” language [6] extended with concurrency features [7]. The interplay between the call-by-name function mechanism and local effects, an approach specific to Algol, is the key ingredient which makes it possible for a large class of programs in this language to have finitely representable semantic models which can be synthesised as stand-alone static circuits. The compiler is available as an open-source download.
UR - http://www.scopus.com/inward/record.url?scp=85025452640&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:85025452640
SN - 9783642311123
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 23
EP - 24
BT - Mathematics of Program Construction - 11th International Conference, MPC 2012, Proceedings
A2 - Gibbons, Jeremy
A2 - Nogueira, Pablo
PB - Springer Verlag
T2 - 11th International Conference on Mathematics of Program Construction, MPC 2012
Y2 - 25 June 2012 through 27 June 2012
ER -