Skip to main content
PRL Project

Using Nuprl for the Verification and Synthesis of Hardware

by Miriam Leeser

Philosophical Transactions of the Royal Society London

The Nuprl proof development system, based on constructive type theory, has a sophisticated proof editor and user interface which facilitates the development of proofs and specifications. We present our experience using Nuprl for hardware verification and synthesis. We have verified floating point hardware and are extending this work to reasoning about the IEEE floating point specification. In addition we are using Nuprl to reason about software for synthesizing hardware designs at several different levels. We present two efforts in this area. In the first, we prove a system that synthesizes CMOS circuits from boolean equations. The second system, PBS, minimizes large sets of boolean formulae by using the weak division algorithm.

bibTex ref: Lee92

cite link