1+1>2：這兩個工具，治好驗證開發(fā)者的精神內(nèi)耗

實現(xiàn)覆蓋率收斂

為什么這么難？

形式驗證如何加速

覆蓋率收斂

• 新思科技專為分析未覆蓋點(diǎn)的可達(dá)性推出了一款VC Formal應(yīng)用，即Formal Coverage Analyzer（FCA）。該應(yīng)用可以生成總結(jié)性報告，指出相關(guān)覆蓋率目標(biāo)是否可以達(dá)到。這種分析通常稱為UNR（不可達(dá)性）。如果某個覆蓋率目標(biāo)無法達(dá)到，可能會導(dǎo)致兩種行為：如果設(shè)計人員在審核后確認(rèn)這符合預(yù)期，則可以將相關(guān)覆蓋率目標(biāo)從驗證計劃中移除，以便提高達(dá)成的覆蓋率百分比；如果這在預(yù)期之外，則通常表示這是一個設(shè)計漏洞或過約束，此時需要用戶采取行動來修復(fù)設(shè)計漏洞或放寬約束。

• 形式驗證發(fā)揮作用的另一種方式是覆蓋屬性。使用形式化技術(shù)驗證斷言時，工具將充分證明屬性的正確性或生成反例，而覆蓋屬性則與此不同，其目標(biāo)是讓形式化工具生成一條軌跡來顯示如何能達(dá)到該覆蓋點(diǎn)。該軌跡有助于創(chuàng)建新的仿真測試用例，以便打到難以覆蓋的覆蓋率目標(biāo)。

VCS+VC Formal

集成的優(yōu)勢

• 新思科技VCS解決方案與新思科技VC Formal解決方案共享一個通用編譯前端。統(tǒng)一的編譯確保VC Formal可以輕松地應(yīng)用于VCS驗證環(huán)境，并確保對設(shè)計語義和意圖的解釋一致。

• 新思科技的VC Formal FCA應(yīng)用可以在VCS shell內(nèi)原生調(diào)用，以進(jìn)行可達(dá)性分析來識別不可達(dá)目標(biāo)，從而創(chuàng)建一個排除文件并反饋給VCS環(huán)境，以此提高仿真覆蓋率。

• 新思科技VC Formal FPV應(yīng)用中運(yùn)行的覆蓋屬性可幫助創(chuàng)建更多的仿真測試用例，以覆蓋隨機(jī)仿真難以打到的點(diǎn)。

• 使用新思科技的VCS和VC Formal解決方案時，可以合并仿真和形式化覆蓋率數(shù)據(jù)庫。這樣一來，使用一種技術(shù)驗證的設(shè)計便無需使用另一種技術(shù)再次進(jìn)行驗證。這也大大加速了驗證收斂和簽核。

SoC驗證時間

節(jié)約40%-80%

總結(jié)

??