Using higher order logic and functional languages to synthesize correct hardware

Shiu Kai Chin, Edward P. Stabler, Kevin J. Greene

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Higher-order logic (HOL), the HOL proof checker, and the functional language SCHEME have been used to describe and verify several hardware synthesis functions, including one which synthesizes Pezaris-like array multipliers. The synthesis functions are shown to be equivalence preserving transformations. The synthesis functions produce functional forms corresponding to gate level interconnection lists. Proofs of theorems relating the synthesized functional forms to functional specifications are developed within HOL. Unlike simulation-based methods, which require exhaustive case analysis for each implementation, these theorems assert the corrections of all implementations produced by the synthesis functions. The combination of machine executable synthesis functions and correctness theorems are additional features which would logically extend CAD systems for design synthesis and design verification.

Original languageEnglish (US)
Title of host publicationInt Conf on Comput Lang 1988 Proc
PublisherIEEE Computer Society
Pages396-403
Number of pages8
ISBN (Print)0818608749
StatePublished - Dec 1 1988

Publication series

NameInt Conf on Comput Lang 1988 Proc

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Using higher order logic and functional languages to synthesize correct hardware'. Together they form a unique fingerprint.

Cite this