Proof producing synthesis of arithmetic and cryptographic hardware
The work
| Authors | Konrad L. Slind; Scott Owens; Juliano Iyoda; Mike Gordon |
|---|---|
| Editors | |
| Type | article |
| Year | 2007 |
| Citekey | slind2007proof |
Where it appeared
| Published in | Formal Aspects of Computing |
|---|---|
| Publisher | Springer Science+Business Media |
| Volume | 19 |
| Issue | 3 |
| Pages | 343--362 |
Identifiers
| DOI | 10.1007/s00165-007-0028-5 |
|---|---|
| OpenAlex | W1989107966 |
Access
| Landing page | https://doi.org/10.1007/s00165-007-0028-5 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1007/s00165-007-0028-5 |
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
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 functionfdefined in higher order logic (typically using recursion) into a device that computesfvia 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.
Cite it as
@article{slind2007proof,
title = {Proof producing synthesis of arithmetic and cryptographic hardware},
author = {Konrad L. Slind and Scott Owens and Juliano Iyoda and Mike Gordon},
year = {2007},
journal = {Formal Aspects of Computing},
publisher = {Springer Science+Business Media},
volume = {19},
number = {3},
pages = {343--362},
doi = {10.1007/s00165-007-0028-5},
}
This record lives at https://refs.drheap.org/slind2007proof/ and will keep doing so.