0.前言：

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

1.什么是形式驗(yàn)證（Formal Verification）

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

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

2.分享的Formal Verification視頻資料

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

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

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

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

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

3.聲明

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

最后，收集整理資料非常費(fèi)時(shí)，如果覺得對(duì)您有幫助，麻煩點(diǎn)個(gè)在看，或者賞個(gè)雞腿也行。謝謝！

審核編輯黃宇