Correctness proofs of parameterized hardware modules in the Cathedral-II synthesis environment

The correctness of parameterised hardware module generators is examined. These modules are the basic building blocks for the Cathedral II silicon compiler and therefore their correctness is vital. The proof of their functional correctness by means of the Boyer-Moore theorem prover is discussed. It is shown that later modifications made to the module generators can be proven correct very easily, starting from the proofs of the original module. The specific module generator discussed is a carry-bypass ALU based on the Mead & Conway ALU. A general scheme is presented to verify layout instances of these modules with respect to their behavioral specification