Automatic Formal Synthesis of Hardware from Higher Order Logic
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 synthesized 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: synthesized 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.
PDF