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

Title of host publication | Int Conf on Comput Lang 1988 Proc |

Publisher | IEEE Computer Society |

Pages | 396-403 |

Number of pages | 8 |

ISBN (Print) | 0818608749 |

State | Published - Dec 1 1988 |

### Publication series

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

*Int Conf on Comput Lang 1988 Proc*(pp. 396-403). (Int Conf on Comput Lang 1988 Proc). IEEE Computer Society.