I remember sitting through presentations a few years ago on Innologic's symbolic simulation tools, and it struck me as a very useful semi-formal method for verifying logic.
I wanted to try it on NoC testing since the conditions for correct behavior are fairly easy to identify (i.e. don't lose/corrupt the data). Also I remember wasting a lot of time running simulations at Altera testing small design configurations to verify the tools, which would have been easier to do with formal techniques (and possibly more convincing).
Is anyone using symbolic simulation tools, and how well do they work?