Synthesis of Arithmetic Hardware Using Hardware Metafunctions

The objective of this work is the development of theorem-based design methods. Considering the large number of components which can be fabricated in VLSI circuits, proving that an implementation meets its functional specification will become increasingly difficult using simulation-based and Boolean comparison-based methods alone. Theorem-based design uses formal logic to create provably correct implementations. Past work has focused on using formal logic and post-hoc proof for design verification. Here, the focus is on hardware synthesis functions, called hardware metafunctions, which synthesize hardware in a provably correct manner. Designs produced using the metafunctions are correct-by-construction and are formally related to their specifications by simple substitution or rewriting of terms within the correctness theorem for each metafunction. Typically, the metafunctions are parametric and once proven correct validate an entire class of designs. Theorem-based design is practical when the metafunctions and their proofs of correctness are machine executable. This is accomplished using appropriate declarative languages with a strong formal basis and by developing the correctness proofs using automatic theorem provers. Here, the functional language SCHEME is used along with the Higher Order Logic (HOL) proof checker. An introduction to the use of higher order logic as a design language along with the verification of an adder array metafunction for an array multiplier is presented.