The ability to guarantee the functional correctness of digital integrated circuits and, in particular, complex microprocessors, is a key task in the production of secure and trusted systems. Unfortunately, this goal remains today an unfulfilled challenge, as even the most straightforward practical designs are released with latent bugs. Patching techniques can repair some of these escaped bugs, however, they often incur a performance overhead, and most importantly, they can only be deployed after an escaped bug has been exposed at the customer site. In this paper we present a novel approach to guaranteeing correct system operation by deploying a semantic guardian component. The semantic guardian is an additional control logic block which is included in the design, and can switch the microprocessor’s mode of operation from its normal, high-performance but error-prone mode, to a a secure, formally verified safe mode, guaranteing that the execution will be functionally correct. We exp...