A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic

Higher order logic (HOL) is a modelling language suitable for specifying behaviour at many levels of abstraction. We describe a compiler from a `synthesizable subset' of HOL function definitions to correct-by-construction clocked synchronous hardware. The compiler works by theorem proving in the HOL4 system and goes through several phases, each deductively refining the specification to a more refined form, until a representation that corresponds to hardware is deduced. It also produces a proof that the generated hardware implements the HOL functions constituting the specification. Synthesized designs can be translated to Verilog HDL, simulated, and then input to standard design automation tools. Users can modify the theorem proving scripts that perform compilation. A simple example is adding rewrite for peephole optimisation, but all the theorem-proving infrastructure in HOL4 is available for tuning the compilation. Users can also extend the synthesisable subset. For example, the core system can only compile tail-recursions, but a `third-party' tool linRec is being developed to automatically generate tail recursive definitions to implement linear recursions, thereby extending the synthesizable subst of HOL to include linear recursion.

PDF