This talk from the 32c3 just two weeks ago looks at exactly that problem. They have "chicken bits" (not sure if that's the technical term :)) which can turn off certain features, and they can patch microcode.

https://media.ccc.de/v/32c3-7171-when_hardware_must_just_wor...

  Software design and testing is hard, but what happens when each bug fix can cost months of delay and millions of dollars? In this talk we’ll take a behind-the-scenes look at the challenges in the design of a very complex, yet critical piece of hardware: the modern x86 CPU.

Killbits is the one I've heard most commonly - as the talk says, most modern processors have a bunch because it's impossible to test every possible edge case a priori.

(Good recent examples include the AMD lockup bug that Matt Dillon found, and the nasty counter-example of the Intel Quark segfault bug, which can't be worked around so easily because the Quark doesn't have killbits. "Oops.")

>most modern processors have a bunch because it's impossible to test every possible edge case a priori.

Only with the sort of engineering most current CPU manufacturers use.

It's possible to have formally verified hardware; it's just expensive with current tech. Tools are improving, though. I suspect the next cutting edge will be the unification of functional-language-to-hardware compilers like Clash or Lambda-CCC with fully dependent languages like Agda or Idris, where you can statically verify arbitrary properties though the type system.

I've just written an Idris programm that determined "your mothers phone number", hows that for arbitrary facts? (tip of the hat to xkcd.)

Great video. Very informative. Thanks.

It's also able to load microcode patches very early on in the machine bring-up process. Microcode can be anywhere as simple as a single hardware enable bit "turn on this hardware unit" or as complex as "this instruction should be decoded as this sequence of microops."

It's hard to know exactly what's wrong without more internal, never-to-see-the-light-of-day Intel information, but it's possible the patch is as simple as tweaking the decoding, or disabling an optimization. It's doubtful a fix like this would require disabling an entire instruction set or hardware unit (like the TSX fix required; those are fairly rare bugs, even for Intel).

Specifically, given that it happens to be a bug that only happens with FMA3 disabled and hyperthreading enabled, it's probably some kind of hardware scheduling deadlock, and the patch could be as simple as "when the decoder sees this sequence of instructions, add some strategically placed NOPs to avoid the deadlock."