The design complexity of current microprocessor systems is such that practically every system released to the market incorporates latent bugs. Manufacturers and design houses alike strive to validate and verify their designs as much as possible during system development, and then attempt to contain the impact of escaped bugs through publicly available errata reports. Some escaped bugs are innocuous, and can be easily overcome through a BIOS or OS update, but still others are potentially dangerous to the users of the system, or they might compromise its security and adversely affect its performance.
This project focuses on developing integrated hardware and software solutions to guarantee that a processor chip operates correctly, even if its design is flawed. The key idea driving this research is to create two modes of operation for the processor: a complex high-performance mode to be used when executing within the portion of the system that has been verified at design time, and a simple low-performance mode guaranteed to be correct under all execution scenarios. By carefully selecting the appropriate mode of operation at runtime, it is possible to always execute correctly: in high-performance when the operation is one that has been verified at design-time or in low performance otherwise. In addition, because of the extreme simplicity of the low-performance mode, it is possible to guarantee that this mode of operation always provides correct results but at a performance price. Related research has shown that, in practice, the low-performance mode intervenes only in very rare occasions, making its performance impact negligible overall. The research challenges to be undertaken in this project include devising low-cost mechanisms to select execution between fast and correct mode, developing the simple mode of operation in such a way that can be fully verified, and developing techniques to efficiently encode the correct states of operation.
