Geometry of Synthesis II: From Games to Delay-Insensitive Circuits

This paper extends previous work on the compilation of higher-order imperative languages into digital circuits [Ghica, D.R., Geometry of Synthesis: a structured approach to VLSI design, in: POPL, 2007, pp. 363–375.]. We introduce concurrency, an essential feature in the context of hardware compilation and we re-use an existing game model to simplify correctness proofs. The target designs we compile to are asynchronous event-logic circuits, which naturally match the asynchronous game model of the language.