Using higher order logic and functional languages to synthesize correct hardware

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.