[jfries]

Formal verification is alive and well in ASIC design land. I suppose it's especially suitable here because of the mix of late bugs being very expensive and that the designs are fundamentally restricted to not too many fancy tricks (for example, hardware can't be monkey patched in runtime).

But where I think formal really shines and saves a lot of time is in bring-up of new code. Using formal, it's possible to write a simple unit-test style test environment, and rely on the formal tool to insert all tricky stall conditions, etc. It's then possible to verify things that are normally tricky to both design for correctly, and also to test.