Compiling Joy Into Silicon: a Formally Verified Compiler forDelay-Insensitive Circuits

Abstract

Manually designing delay-insensitive electronic circuits has proven to be difficult in practice. As an alternative, we designed and implemented a compiler that automatically produces such circuits. The source language for the compiler is a language called "Joy", which is a simple but complete parallel language with a syntax similar to that of many procedural languages. The compiler's output is a netlist suitable for input into standard place-and-route tools. In this paper, we present the highlights of the compilation algorithm, and the proof of correctness for it. This is among the first formally verified algorithms for compiling a general language into circuits.