Sciweavers

ENTCS
2006

Automatic Formal Synthesis of Hardware from Higher Order Logic

14 years 7 hour ago
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
Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Sl
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Slind
Comments (0)