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)

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. (Contact us about this Publication)
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: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Scott Owens
Date Deposited: 15 Nov 2013 12:07 UTC
Last Modified: 14 Jun 2019 14:08 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/31916 (The current URI for this page, for reference purposes)
  • Depositors only (login required):