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

Edwin Brady, James McKinna, Kevin Hammond

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationProceedings of the Eighth Symposium on Trends in Functional Programming, TFP 2007, New York City, New York, USA, April 2-4. 2007.
Pages159-176
Number of pages18
DOIs
Publication statusPublished - 2007

Fingerprint

Dive into the research topics of 'Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types'. Together they form a unique fingerprint.

Cite this