Comment by bsder
9 years ago
Formal verification of a decode unit simply will never happen. The complexity is far too high.
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.
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?