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

實現覆蓋率收斂

為什么這么難？

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

形式驗證如何加速

覆蓋率收斂

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

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

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

VCS+VC Formal

集成的優勢

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

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

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

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

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

SoC驗證時間

節約40%-80%

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

總結

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

??

??