求Synopsys公司的ABV软件

最近，有大牛上传了Mentor的questa formal，请问小编及各位高人，synopsys公司有没有类似做基于断言的形式验证工具?Formality可以么?好像formality用于比对网表等后期等效性检查吧?
我是新手，麻烦各位好心人指点一下！

我也需要啊，formality目前也在用网表比对，可能其他功能还没用到。
Formality首先核对综合后的门级设计和综合前设计的RTL表达方式是否等效。随后当你对设计增加或者减少了一些逻辑功能(例如增加了扫描测试功能的线路,或者修改了时钟树线路)后,你可以再利用该工具进行核对。

谢谢！
谢谢指点！