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.