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/