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

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

為什么這么難？

形式驗(yàn)證如何加速

覆蓋率收斂

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

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

VCS+VC Formal

集成的優(yōu)勢(shì)

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

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

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

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

SoC驗(yàn)證時(shí)間

節(jié)約40%-80%

總結(jié)

??