Proof producing synthesis of arithmetic and cryptographic hardware
Konrad L. Slind, Scott Owens, Juliano Iyoda, Mike Gordon · Formal Aspects of Computing · 2007
Abstract A compiler from a synthesisable subset of higher order logic to clocked synchronous hardware is described. It is being used to create coprocessors for cryptographic and arithmetic applications. The compiler automatically translates a functionfdefined in higher order logic (typically using recursion) into a device that computesfvia a four-phase handshake circuit. Compilation is by fully automatic proof in the HOL4 system, and generates a correctness theorem for each compiled function. Synthesised circuits can be directly translated to Verilog, and then input to design automation tools. A fully-expansive ‘LCF methodology’ allows users to safely modify and extend the compiler’s theorem proving scripts to add optimisations or to enlarge the synthesisable subset of higher order logic.