Can we really do without the support of formal methods in the verification of large designs?

From the IC industry´s standpoint, the incubation of formal methods for deployment in EDA verification flows has been very long and is still occurring. Formal methods applied at functional verification have interpreted different roles and finally have federated with simulation for the purpose of achieving coverage closure. Commercially available IP´s and custom IP´s have very often been exposed to sneaky bugs. Having correct IP´s is not enough for verifying the correctness of the whole system. Formal methods have to extend their effectiveness by including the so called transactional level models (TLM) in their analysis, that abstract the mechanisms that SoC blocks use to communicate and synchronize among themselves. Two major problems have to be faced: the first is that TLM includes a range of abstraction levels and the second is that a mapping between TLM assertions and RTL assertions should be provided and formally proven.