Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1016/j.entcs.2005.10.003 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
compiling,synthesised circuit,verilog hdl,automatic formal synthesis,theorem proving,logic formula,compilation script,clocked synchronous hardware,translates recursive function definition,hardware synthesis,synthesisable subset,hol4 system,higher order logic,additional proof-based tool,clock synchronization,design automation,computer programming | Logic synthesis,Programming language,Logic optimization,Computer science,Correctness,Theoretical computer science,Electronic design automation,Register-transfer level,Verilog,Logic family,Computer hardware,Higher-order logic | Journal |
Volume | ISSN | Citations |
145, | Electronic Notes in Theoretical Computer Science | 8 |
PageRank | References | Authors |
0.55 | 9 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mike Gordon | 1 | 23 | 2.07 |
| Juliano Iyoda | 2 | 61 | 9.21 |
| Scott Owens | 3 | 23 | 2.65 |
| Konrad Slind | 4 | 577 | 55.90 |