### 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 language | English (US) |
---|---|

Title of host publication | 1988 IEEE Int Conf Comput Des VLSI Comput Process ICCD 88 Proc |

Publisher | IEEE Computer Society |

Pages | 604-610 |

Number of pages | 7 |

ISBN (Print) | 0818608722 |

State | Published - Dec 1 1988 |

### Publication series

Name | 1988 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

*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.