A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic
Mike Gordon, Juliano Iyoda, Scott Owens, Konrad L. Slind, William H. Gates · Kent Academic Repository (University of Kent) · 2005
(authors listed in alphabetical order) Abstract. Higher order logic (HOL) is a modelling language suitable for specifying behaviour at many levels of abstraction. We describe a compiler from a ‘synthesisable subset ’ of HOL function definitions to correctby-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 concrete 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. Synthesised 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 rewrites 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 synthesisable subset of HOL to include linear recursion. 1