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

Abstract

In this paper 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 will be discussed. It will be 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 that will be discussed is a carry-bypass ALU based on the Mead & Conway ALU. A general scheme will be presented to verify layout instances of these modules with respect to their behavioral specification.