Formality 和 Modelsim

小弟最近在学习IC设计的基本流程，感觉做IC设计真心不简单啊，使用的软件好多啊！最近有些问题不是很明白，所以想求助各位大神指点，问题是这样：

在进行DC综合之后，我们需要对DC综合之后的结果进行功能验证和时序验证，其中时序验证一般使用的是Prime Time，这个没有疑问；功能验证的目的是为了保证综合前的RTL代码和综合后的网表的逻辑功能是一致的，但是网上提到在进行功能验证的时候，有的说是使用Formality，有的说使用Modelsim，使用Formality的原因是说对门级网表进行动态仿真使用的时间太长。

我想问的是这两个有什么很大的区别吗?在进行功能仿真的时候到底是使用哪一个呢?还是两个都要使用?还有这两个软件验证后的结果是等效的吗?

formality是形式验证，区别于“仿真”
仿真是在时域计算并出波形，比如用modelsim，vcs等等

我特别想知道的是这两个软件的验证结果是不是等效的?即 对于同一个综合后的结果只需要进行其中的一个就行了?

完全是两码事的东西。一个是功能仿真，一个是等效验证。功能仿真更多的是检查你的代码写错了没，等效验证侧重检查工具的综合有没有错误。