Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types.
Edwin C. Brady, James McKinna, Kevin L Hammond · 2007
Abstract: This paper focuses on the important, but tricky, problem of determining provably correct program properties automatically from program source. We describe a novel approach to constructing correct low-level programs. By using modern, full-spectrum dependent types, we are able to give an explicit and checkable link between the low-level program and its high-level meaning. Our approach closely links programming and theorem proving in that a type correct program is a constructive proof that the program meets its specification. It goes beyond typical model-checking approaches, that are commonly used to check formal properties of low-level programs, by building proofs over abstractions of properties. In this way, we avoid the state-space explosion problem that bedevils model-checking solutions. We are also able to consider properties over potentially infinite domains and determine properties for potentially infinite programs. We illustrate our approach by implementing a carry-ripple adder for binary numbers.