“在未來(lái)五年內(nèi)仿真將逐漸被淘汰，僅用于子系統(tǒng)和系統(tǒng)級(jí)驗(yàn)證。與此同時(shí)，形式化驗(yàn)證方法已經(jīng)開(kāi)始處理一些系統(tǒng)級(jí)任務(wù)。隨著技術(shù)發(fā)展，更多Formal相關(guān)的商業(yè)標(biāo)準(zhǔn)化會(huì)推出。”

Intelfellow

M. V. Achutha Kiran Kumar

隨著Formal技術(shù)的發(fā)展，業(yè)內(nèi)已經(jīng)有不少公司有專門的形式化驗(yàn)證團(tuán)隊(duì)，也培養(yǎng)了一批熱愛(ài)Formal，愿意來(lái)鉆研這門技術(shù)的EDA人。

仿真方法學(xué)是動(dòng)態(tài)驗(yàn)證的一種，是一個(gè)“你想到哪里才能驗(yàn)到哪里”的驗(yàn)證方式，本質(zhì)上在不斷做加法。你需要先讓自己盡可能多地想到各種場(chǎng)景、耗費(fèi)大量時(shí)間搭建測(cè)試環(huán)境，再試圖“碰出BUG”，但是這種方式更擅長(zhǎng)發(fā)現(xiàn)設(shè)計(jì)“這里有BUG”，但卻很難回答“那里沒(méi)有BUG”的問(wèn)題。

這方面形式化驗(yàn)證工具有很大的優(yōu)勢(shì)。

形式化驗(yàn)證則被稱為靜態(tài)驗(yàn)證，是一種基于嚴(yán)格的數(shù)學(xué)與算法的驗(yàn)證方法學(xué)。用戶利用SVA斷言描述清楚需要證明的設(shè)計(jì)規(guī)格，通過(guò)編譯RTL和基于SVA的斷言語(yǔ)言，建立Formal模型，然后不斷做減法，發(fā)現(xiàn)不符合模型的“反例”。

顯而易見(jiàn)的一個(gè)優(yōu)勢(shì)是，形式化驗(yàn)證工具能夠通過(guò)建立數(shù)學(xué)模型，實(shí)現(xiàn)更敏捷的反向驗(yàn)證，以類似數(shù)學(xué)定理證明的方式，通過(guò)對(duì)所有可能的激勵(lì)空間進(jìn)行遍歷，保證邏輯沒(méi)有死角，實(shí)現(xiàn)驗(yàn)證的完備化、自動(dòng)化。

傳統(tǒng)的仿真工具，在進(jìn)入具體發(fā)現(xiàn)bug階段前，往往需要很長(zhǎng)時(shí)間為UVM搭建一個(gè)完備的驗(yàn)證平臺(tái)（testbench）；而在調(diào)試（Debug）階段，當(dāng)出現(xiàn)UVM error，需要問(wèn)題定位時(shí)，仿真工具一般需要從UVM繁雜的log到rtl再到waveform、信號(hào)級(jí)別，這也是一個(gè)很長(zhǎng)的回溯曲線。形式化驗(yàn)證在這兩個(gè)方面，則可以節(jié)省很多時(shí)間，尤其是通過(guò)直接提供反例波形，可以精準(zhǔn)直指相關(guān)信號(hào)進(jìn)行問(wèn)題定位。

早期大家可能會(huì)擔(dān)心，覺(jué)得Formal工具是不是有使用門檻，這種擔(dān)心來(lái)源于形式化驗(yàn)證工具使用過(guò)程中，需要基于對(duì)設(shè)計(jì)的全面理解，才能正確構(gòu)建驗(yàn)證模型的斷言和約束。

一方面，形式化驗(yàn)證對(duì)驗(yàn)證工程師而言，確實(shí)能夠大大的減輕焦慮，芯華章2021年推出GalaxFV，并且在項(xiàng)目的打磨中，持續(xù)不斷地在豐富應(yīng)用級(jí)斷言庫(kù)，并對(duì)其參數(shù)化、提高可配置性，讓GalaxFV更加容易使用。

另外，隨著設(shè)計(jì)規(guī)模增加，工具更加的自動(dòng)化、智能化，理解設(shè)計(jì)會(huì)成為工程師的一大優(yōu)勢(shì)！用好Formal工具，項(xiàng)目將不再需要靠堆人、堆license、堆時(shí)間來(lái)提高驗(yàn)證質(zhì)量。