Name
Abstract | ||
|---|---|---|
A compiler from a synthesisable subset of higher order logic to clocked synchronous hardware is described. It is being used to create coprocessors for cryptographic and arithmetic applications. The compiler automatically translates a function f defined in higher order logic (typically using recursion) into a device that computes f via a four-phase handshake circuit. Compilation is by fully automatic proof in the HOL4 system, and generates a correctness theorem for each compiled function. Synthesised circuits can be directly translated to Verilog, and then input to design automation tools. A fully-expansive ‘LCF methodology’ allows users to safely modify and extend the compiler’s theorem proving scripts to add optimisations or to enlarge the synthesisable subset of higher order logic. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/s00165-007-0028-5 | Formal Asp. Comput. |
Keywords | Field | DocType |
compiling,lcf methodology,synthesised circuit,high assurance,automatic proof,cryptographic hardware,cryptography,automation tool,clocked synchronous hardware,theorem proving,hardware synthesis,synthesisable subset,hol4 system,correctness theorem,arithmetic application,higher order logic,design automation,clock synchronization | Programming language,Computer science,Correctness,Automated theorem proving,Arithmetic,Theoretical computer science,Compiler,Electronic design automation,Verilog,Computer programming,Higher-order logic,Recursion | Journal |
Volume | Issue | ISSN |
19 | 3 | 1433-299X |
Citations | PageRank | References |
10 | 0.99 | 16 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Konrad Slind | 1 | 577 | 55.90 |
| Scott Owens | 2 | 23 | 2.65 |
| Juliano Iyoda | 3 | 61 | 9.21 |
| Mike Gordon | 4 | 23 | 2.07 |