Verifiable and executable theories of design for synthesizing correct hardware

Shiu Kai Chin, Kevin J. Greene

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

Abstract

Formally verified hardware synthesis functions have been developed and implemented using high-order logic, automatic theorem provers, and declarative languages. The synthesis functions, which take the form of equivalence-preserving transformations, enable implementations to be related to their specifications in a formally verified manner. As shown by the theory of design for array multipliers, verified synthesis functions produce implementations which are correct by construction, thus avoiding the exponential growth in effort inherent in simulation-based and Boolean comparison-based verification. Theories of design with their verified synthesis functions and correctness theorems represent additional features which would logically extend computer-aided design systems for design synthesis and design verification.

Original languageEnglish (US)
Title of host publication1988 IEEE Int Conf Comput Des VLSI Comput Process ICCD 88 Proc
PublisherIEEE Computer Society
Pages604-610
Number of pages7
ISBN (Print)0818608722
StatePublished - Dec 1 1988

Publication series

Name1988 IEEE Int Conf Comput Des VLSI Comput Process ICCD 88 Proc

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Verifiable and executable theories of design for synthesizing correct hardware'. Together they form a unique fingerprint.

  • Cite this

    Chin, S. K., & Greene, K. J. (1988). Verifiable and executable theories of design for synthesizing correct hardware. In 1988 IEEE Int Conf Comput Des VLSI Comput Process ICCD 88 Proc (pp. 604-610). (1988 IEEE Int Conf Comput Des VLSI Comput Process ICCD 88 Proc). IEEE Computer Society.