Automatic Formal Synthesis of Hardware from Higher Order Logic

A compiler that automatically translates recursive function definitions in higher order logic to clocked synchronous hardware is described. Compilation is by mechanised proof in the HOL4 system, and generates a correctness theorem for each function that is compiled. Logic formulas representing circuits are synthesised in a form suitable for direct translation to Verilog HDL for simulation and input to standard design automation tools. The compilation scripts are open and can be safely modified: synthesised circuits are correct-by-construction. The synthesisable subset of higher order logic can be extended using additional proof-based tools that transform definitions into the subset. Key words: Theorem proving, compiling, hardware synthesis

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Slind
• Keywords: Additional Proof-based Tools, Design Automation Tools, ENTCS 2006, Recursive Function Definitions