There was an interesting question that was asked during the interview with Moshar from Broadcom
http://www.eetimes.com/news/design/showArticle.jhtml;jsessionid=MKCJBAP5HOPZKQSNDLPCKH0CJUNN2JVN?articleID=196902151
==================
EE Times: Are you using formal verification, and does it reduce the need for simulation and acceleration?
Moshar: We are using formal verification, but I don’t believe it is reducing the scope of the work we need to do. It will help you make sure that your IP is golden, but formal verification really does not apply at the SoC level. You have to go through all the traffic scenarios you need to cover.
===================
It would have been nice if a detailed answer was given ..From the question posed and reading the answer , it appears as if it is a limitation of Formal Verification. I think if you describe in terms of Formal properties using PSL , it would be still possible to formally verify the traffic between various cores on SOC..
I think it would be interesting to know on how companies operating in ESL space view this. As systemC and C based language design becoming popular and support TLM, it would interesting to see how one can extract information from these abstract models and verify the design intentions.
