SHF:Small:Designing Architectures to be Formally Verifiable

Duke University, Durham NC

Investigators

Abstract

Computer systems are exceedingly complicated, and a major challenge is verifying that they are correct in all situations. Hardware industry accordingly spends more effort on verification than it does on actual design, yet functional design bugs still exist in today's computer systems, including shipped processor chips from major vendors. This project seeks to overcome this verification challenge through a verification-aware design methodology. This project designs systems such that they can be verified with existing formal verification methodologies, rather than expecting arbitrary designs to be verifiable. Rather than design a system and then try to verify it, the proposed philosophy is to understand the capabilities of existing verification methodologies and then try to design the best possible systems that are compatible with these methodologies. In this work, the verification is performed with existing verification tools and the innovation is in the design. The broad impact of this work is the development of computer systems, or portions thereof, that are formally verified and thus provably correct in all cases.