形式驗證

形式驗證是為了驗證RTL代碼與門級網表之間的邏輯等價性。

在綜合的流程中通常會插入掃描鏈，這樣綜合出的結果的邏輯關系可能會與RTL代碼的等效邏輯不一致；在版圖流程中，通常會做時鍾樹綜合，將會在網表中插入BUFF和反向器，這就可能會造成邏輯的不等價。如果在這兩種情況下，都采用重新進行一番驗證的方式來驗證門級網表的正確性，那么將會帶來大量的時間消耗，項目流程會被拉長，這對於IC設計來說是不能承受的高成本，

因此，采用邏輯等價性驗證的方式來驗證綜合之后、版圖導出的門級網表是否與經過驗證的RTL代碼的邏輯功能完全等價。這樣就使得綜合之后的門級網表在節省時間的前提下，得到完全的功能驗證。

形式驗證流程主要是在綜合插入掃描鏈之后，版圖時鍾樹綜合之后進行。