0.前言：

前段時間很多朋友在微信群里討論Formal驗證的視頻資料問題，今天整理好了，分享給大家。

1.什么是形式驗證（Formal Verification）

在計算機硬件（特別是集成電路）和軟件系統(tǒng)的設(shè)計過程中，形式驗證的含義是根據(jù)某個或某些形式規(guī)范或?qū)傩裕褂脭?shù)學的方法證明其正確性或非正確性。形式驗證是一個系統(tǒng)性的過程，將使用數(shù)學推理來驗證設(shè)計意圖（指標）在實現(xiàn)(RTL)中是否得以貫徹。

由于仿真對于超大規(guī)模設(shè)計來說太耗費時間，形式驗證（Formal Verification）就出現(xiàn)了。FV的主要思想是通過使用形式證明的方式來驗證一個設(shè)計的功能是否正確。FV主要靠工具自己來完成，無需開發(fā)測試向量（斷言還是需要寫的），這比功能仿真的時間要少很多。

2.分享的Formal Verification視頻資料

關(guān)注微信公眾號《芯片驗證日記》，后臺回復”formal”，可得本文所有formal視頻資料對應(yīng)的百度鏈接，目錄如下圖所示。

2.1 《Formal_Coverage》的內(nèi)容，如下圖所示：

2.2 《Synopsys_VC-Formal_apps講解》的內(nèi)容，如下圖所示：

2.3 《動態(tài)系統(tǒng)的形式化分析與控制-上海交通大學殷翔》的內(nèi)容，如下圖所示：

2.4《邏輯與形式化方法-龍星計劃》的內(nèi)容，如下圖所示：

3.聲明

本文所有的視頻資料都是來自B站公開的視頻，如有侵權(quán)請后臺聯(lián)系作者刪除。

最后，收集整理資料非常費時，如果覺得對您有幫助，麻煩點個在看，或者賞個雞腿也行。謝謝！

審核編輯黃宇