仿真和形式驗證是當今SoC設計和驗證流程中使用的兩個關鍵驗證策略。它們各有所長，在查找邊界漏洞并最終實現(xiàn)驗證收斂和簽核方面相輔相成。 仿真和形式驗證通常由不同的團隊來完成，而他們各自都有一套簽核目標。由于形式驗證和仿真需要不同的專業(yè)知識和技能，兩個團隊通常不會密切合作。然而，仿真和形式驗證之間存在協(xié)同作用，它對整個驗證工作大有裨益，并能加速覆蓋率收斂。 在本文中，我們將通過研究仿真和形式驗證之間的技術聯(lián)系，探討如何幫助驗證和形式化團隊更好地合作，從而有效地結合這兩種技術來加速實現(xiàn)驗證簽核。

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

為什么這么難？

僅使用仿真來實現(xiàn)覆蓋率收斂是很難的。仿真所用的時間和測試運行的次數(shù)與已完成覆蓋率目標的百分比增長之間不呈線性關系。 如下圖所示，盡管隨著時間的推移，仿真運行次數(shù)不斷增加，但覆蓋曲線卻趨于平緩。這通常歸結于以下兩個因素：1) 那些覆蓋率目標在本質上就無法達到；2) 那些難以實現(xiàn)的覆蓋率目標可能需要手動創(chuàng)建測試用例，因為受約束的隨機仿真可能無法達到這些覆蓋率目標。在某些情況下，運行無數(shù)的仿真測試用例并不能產(chǎn)生最佳投資回報率，也無法實現(xiàn)覆蓋率收斂。

形式驗證如何加速

覆蓋率收斂

形式驗證可通過兩種方式加速仿真覆蓋率收斂：

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

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

VCS+VC Formal

集成的優(yōu)勢

雖然仿真和形式驗證之間的協(xié)同作用并不強求兩種技術一定要來自同一家EDA供應商，但如果這兩種解決方案擁有其他技術共性，則會有更多好處。 新思科技符合行業(yè)標準的VCS仿真器和新思科技的創(chuàng)新型VC Formal解決方案擁有很多有價值的聯(lián)系，能夠讓終端用戶從中獲益。

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

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

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

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

SoC驗證時間

節(jié)約40%-80%

在使用新思科技的VCS和VC Formal解決方案后，很多客戶發(fā)現(xiàn)驗證時間節(jié)省了40%到80%，同時也對實現(xiàn)驗證簽核更有信心。下表顯示了10種客戶設計以及形式化分析在減少驗證時間方面的影響。 為了幫助客戶最大限度地發(fā)揮形式化技術的優(yōu)勢，新思科技形式驗證服務團隊在世界各地提供專家支持，協(xié)助開展方法培訓、驗證審核和各種交鑰匙項目。

總結

憑借新思科技VCS與VC Formal解決方案的強大功能，形式化技術對于證明芯片設計的正確性有很大的幫助。通過使用形式化技術來增強仿真，開發(fā)者們可以加快覆蓋率收斂，從而實現(xiàn)更高質量的設計。新思科技的VC Formal解決方案、Verdi解決方案與VCS功能驗證解決方案互相緊密集成，能夠提供當今復雜SoC驗證所需的速度、容量和靈活性，并幫助開發(fā)者找出設計缺陷的根本原因。 更重要的是，開發(fā)者自己并不需要成為形式化專家，而只需利用這些解決方案就能取得成效。 新思科技芯片設計和驗證解決方案共享通用技術和一致的設計詮釋，能夠為驗證開發(fā)者提供無縫的用戶體驗并帶來更高的性能和生產(chǎn)力。新思科技產(chǎn)品“價值鏈”的持續(xù)創(chuàng)新能夠幫助企業(yè)高效地設計下一代變革性產(chǎn)品。此外，新思科技的VC Formal解決方案還可與驗證工具箱中的其他工具相互配合，助力開發(fā)者實現(xiàn)高質量的形式化簽核。

??

??