Re:Intel Skylake/Kaby Lake processors: broken hyper-threading
by wyager on Monday June 26, 2017 @01:33AM
(#14634328)
That's the whole point of doing a provably correct transformation from a simpler model domain. Even complicated OOOE engines are fairly tractable if you don't try to implement them at an RTL level...
Perhaps we are imagining different formal verification methodologies. Can you tell me what kind of formal verification you're referring to?
Formally verifying something like a multiplier block is difficult but doable if you care. Formally verifying an FPU is probably at about the limit.
If you want formal verification, you would have to simplify a modern microprocessor a lot.