Skip to main content

Automatic Formal Synthesis of Hardware from Higher Order Logic

Gordon, Mike, Iyoda, Juliano, Owens, Scott, Slind, Konrad (2006) Automatic Formal Synthesis of Hardware from Higher Order Logic. Electronic Notes in Theoretical Computer Science, 145 . pp. 27-43. ISSN 1571-0661. (doi:10.1016/j.entcs.2005.10.003) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:31916)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.
Official URL:
http://dx.doi.org/10.1016/j.entcs.2005.10.003

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.

Item Type: Article
DOI/Identification number: 10.1016/j.entcs.2005.10.003
Additional information: Proceedings of the 5th International Workshop on Automated Verification of Critical Systems (AVoCS 2005)
Uncontrolled keywords: Theorem proving; compiling; hardware synthesis
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Scott Owens
Date Deposited: 15 Nov 2013 12:07 UTC
Last Modified: 16 Nov 2021 10:09 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/31916 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.