Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types

This paper focuses on the important, but tricky, problem of determiningprovably correct program properties automatically from program source. Wedescribe a novel approach to constructing correct low-level programs. By usingmodern, full-spectrum dependent types, we are able to give an explicit and checkablelink between the low-level program and its high-level meaning. Our approachclosely links programming and theorem proving in that a type correct program is aconstructive proof that the program meets its specification. It goes beyond typicalmodel-checking approaches, that are commonly used to check formal propertiesof low-level programs, by building proofs over abstractions of properties. In thisway, we avoid the state-space explosion problem that bedevils model-checkingsolutions. We are also able to consider properties over potentially infinite domainsand determine properties for potentially infinite programs. We illustrateour approach by implementing a carry-ripple adder for binary numbers.