Formal vs Simulation

Hi

I am writing a paper looking at "myths" in functional verification. By "myth" I mean the types of things which people take as accepted truth even though there may not be much evidence to back them up. So, will formal replace simulation?

My opinion here is that this is a definite no. Currently, I think some companies are applying both formal and simulation at the block level. But the number applying JUST formal would be extremely small (if any?). However, some functional verif is much better performed by formal and so it does replace the need to perform some of the simulation - although it is hard to realise what simulations you can drop if you prove a given property

At chip level - it is mainly simulation (although there may be some special proofs - clock domain crossing, tri-state bus driving)

My use of formal tools also suggests that formal and simulation are actually starting to converge! Formal tools use simulation to get to interesting start states. Simulation can use formal to try to prove properties about particular simulation states

Any opinons or good paper references are VERY welcome

Regards

Mike Bartley