A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic
european symposium on programming(2005)
摘要
Higher order logic (HOL) is a modelling language suitable for specifying behaviour at many levels of abstraction. We describe a com- piler from a 'synthesisable subset' of HOL function denitions to correct- by-construction clocked synchronous hardware. The compiler works by theorem proving in the HOL4 system and goes through several phases, each deductively rening the specication to a more concrete form, until a representation that corresponds to hardware is deduced. It also pro- duces a proof that the generated hardware implements the HOL func- tions constituting the specication. Synthesised designs can be translated to Verilog HDL, simulated and then input to standard design automa- tion tools. Users can modify the theorem proving scripts that perform compilation. A simple example is adding rewrites for peephole optimi- sation, but all the theorem-proving infrastructure in HOL4 is available for tuning the compilation. Users can also extend the synthesisable sub- set. For example, the core system can only compile tail-recursions, but a 'third-party' tool linRec is being developed to automatically generate tail recursive denitions to implement linear recursions, thereby extend- ing the synthesisable subset of HOL to include linear recursion.
更多查看译文
关键词
computer programming,clock synchronization,front end,higher order logic,first order,register allocation,theorem proving
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络