Synthesis of arithmetic hardware using hardware metafunctions

The development of theorem-based design methods is considered. 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 proofs of correctness using automatic theorem provers. 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 along with the verification of an adder array metafunction for an array multiplier is presented