SHF:Small:Designing Architectures to be Formally Verifiable

点击翻译按钮获取中文摘要

Computer systems are exceedingly complicated, and a major challenge isverifying that they are correct in all situations. Hardware industryaccordingly spends more effort on verification than it does on actualdesign, yet functional design bugs still exist in today's computersystems, including shipped processor chips from major vendors. Thisproject seeks to overcome this verification challenge through averification-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 compatiblewith 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.