Proof producing synthesis of arithmetic and cryptographic hardware
| Autor: | Scott Owens, Juliano Iyoda, Michael J. C. Gordon, Konrad Slind |
|---|---|
| Rok vydání: | 2007 |
| Předmět: |
Correctness
Recursion Computer science business.industry Programming language Computer programming computer.software_genre Higher-order logic Theoretical Computer Science Automated theorem proving Verilog Electronic design automation Compiler Arithmetic business computer Software computer.programming_language |
| Zdroj: | Formal Aspects of Computing. 19:343-362 |
| ISSN: | 1433-299X 0934-5043 |
| DOI: | 10.1007/s00165-007-0028-5 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink