形式验证

形式验证是为了验证RTL代码与门级网表之间的逻辑等价性。

在综合的流程中通常会插入扫描链，这样综合出的结果的逻辑关系可能会与RTL代码的等效逻辑不一致；在版图流程中，通常会做时钟树综合，将会在网表中插入BUFF和反向器，这就可能会造成逻辑的不等价。如果在这两种情况下，都采用重新进行一番验证的方式来验证门级网表的正确性，那么将会带来大量的时间消耗，项目流程会被拉长，这对于IC设计来说是不能承受的高成本，

因此，采用逻辑等价性验证的方式来验证综合之后、版图导出的门级网表是否与经过验证的RTL代码的逻辑功能完全等价。这样就使得综合之后的门级网表在节省时间的前提下，得到完全的功能验证。

形式验证流程主要是在综合插入扫描链之后，版图时钟树综合之后进行。