Formal verification is being used by virtually every big name in chip design. That said, this is the first I've read of someone starting by parsing the ISA specification. It has been talked about but some people (myself included) were not sure if it would be reasonable in practice.

It feels like most of the recent architecture grad students that I know have gone into formal verification in industry.

Formal verification of software is basically never done, but I was under the impression that chip vendors relied pretty heavily on both exhaustive state testing and formal verification.

Exhaustive state testing is intractable for any modern design. Some combination of constrained random verification and directed testing is used.

http://chipdesignmag.com/display.php?articleId=4913

I wouldn't be so sure to call it intractable. It is pretty hard and time consuming, but not impossible by any stretch of imagination.

Critical parts are hopefully exhaustively tested. Say, memory protection and security.

That said, formal methods are better. ISA-Verifier is a pretty small tool though, nowhere near as strong as Isabelle model used for seL4 for example.

Intel has been doing it for years, and it's suggested they by far have the best hardware verification systems there are. They certainly learned from the FDIV bug.

One of the engineers who works on verification of floating point stuff at Intel has written an excellent book on automated formal reasoning tools: http://www.cl.cam.ac.uk/~jrh13/