That could be a killer combination for specific functional verification goals. For instance look at recent SNPS’s webinar on MVRC & Formality @ http://bit.ly/9oupo9
Other ideas I have on using Formal equiv checker in functional verification are to automate Gate Level debug, debugging X’s, porting RTL TB’s to GLS etc. Need a good API + formal tool for all those ideas though…
Signing off!
www.cvcblr.com