電子設計界在其設計項目中采用云計算策略的速度很慢，這主要是由于對IP安全的擔憂。一種新興的方法可以改變這種不情愿，并允許更多的設計人員利用云作為計算平臺進行驗證。這種方法對于利用嵌入式處理器子系統和其他來自不同來源的IP的嵌入式設計具有特別的好處。

形式化驗證技術正在成為越來越多驗證解決方案的基礎，也是緩解云安全問題的關鍵。該技術能夠將驗證問題分解為多個抽象的數學問題，并將其傳輸到云中進行解決，并刪除所有設計細節，從而確保設計安全性。形式驗證過程通過提取要分析的特定狀態并與所需屬性進行比較來實現此目的。設計細節將保留并在本地重新應用于云操作的結果。此過程消除了將 IP 移出辦公室的需要。

由此產生的解決方案利用一系列基于云的服務器來提供廣泛的驗證功能，提供易于采用和使用、按需性能權衡以及按使用付費的業務模式。這對于基于IP的嵌入式設計尤其重要，其中IP由可能不擁有正式技術所有權的第三方使用。

通過云獲取驗證軟件

云計算驗證軟件使用“客戶端工具”，即在本地主機上運行并充當云引擎前端的組件，從設計代碼創建數學證明問題集以傳輸到云。客戶端工具包括“linting”功能（一種在硬件描述語言 （HDL） 代碼中查找設計錯誤的方法），并管理與云解決方案的通信。它還允許在本地主機上執行云處理結果的任何所需調試。

傳統上，驗證軟件被授權在本地主機上運行，并且從設計輸入到結果調試的整個操作都是使用單個產品完成的。對于云方案，客戶端工具使用戶體驗相同，就好像整個產品在本地運行一樣，為云使用模型提供了透明的感覺。

實際應用

轉型的按使用付費業務模式、對無限數量的計算引擎的訪問以及按需驗證應用程序的結合提供了一些有趣的新優勢。

例如，該軟件非常適合希望以最小的學習曲線和設置過程在其現有的基于仿真的驗證流程中添加強大的正式設計檢查的新用戶。

在最基本的云驗證過程中，設計寄存器傳輸級別 （RTL） 代碼由隨附的 lint 功能在本地進行檢查。然后，使用斷言綜合自動為設計的許多方面創建強大的測試。自動化測試包括一系列致命的設計錯誤檢查、仿真和綜合之間的潛在不匹配問題、寄存器和信令初始化和切換問題、代碼和有限狀態機 （FSM） 覆蓋范圍以及許多其他故障場景。通過在云中提供這種機制，新用戶可以采取“嘗試和觀察”的態度，而無需耗時的評估過程，快速測試他們的設計，沒有痛苦的學習曲線，并體驗正式技術，不像更傳統的方法，必須完成完整的工具許可和安裝過程，通常由供應商的工程師訪問現場， 通常與供應商的銷售努力相結合。

高級用戶也可以獲得相當大的好處。形式驗證本質上是一個并行的過程，數學證明問題并行運行。云解決方案提供無限數量的計算服務器，因此，可以在多個計算機之間執行驗證運行，以提供最佳的并行執行。即使成本保持不變 - 在單個服務器上花費10小時的成本與在10臺服務器上花費1小時的成本相同。在軟件許可方法中，必須預先購買足夠的許可證才能涵蓋完整的并行使用，通常對可能一起運行的操作數量設置了很小的上限。因此，在大多數驗證安裝中，并行操作通常受到多重限制。

該解決方案還支持按需使用特定目的，例如IP集成或驗證服務提供商的一種手段，這些服務提供商需要在外國環境中工作時訪問這些工具。在每種情況下，都可以利用該軟件，而無需最終客戶預先購買它，這是在沒有利用正式解決方案的第三方參與時的理想選擇。

嵌入式設計的云優勢

嵌入式設計有一些特定問題，可以通過基于云的基于應用程序的驗證來緩解。嵌入式設計的本質是，IP將從各種來源得到利用。此 IP 將應用一系列驗證指標，并可能使用復雜的接口進行互連（圖 2）。

圖 2：形式驗證可以為利用來自不同來源的IP的嵌入式設計提供嚴格的集成測試環境。

正如一家領先的半導體公司在最近的設計自動化會議上所討論的那樣，形式驗證可以在這種情況下發揮巨大的作用，以提供嚴格的集成測試環境。斷言用于指定接口以及要在 IP 和平臺之間傳遞的預期信息。鑒于知識產權的可重用性以及確保其在外國環境中正確相互聯系的重要性，這種對斷言的投資被認為是值得的。當然，如果這種互連是通過標準總線協議（例如ARM的AHB標準），則可以使用一組標準的協議斷言來確保其有效性。以這種方式使用斷言已被證明可以提高質量并減少集成時間，因為鑒于IP的可重用性，如果經過充分測試，則可以在隨后進行更多投資，并且將消除重寫斷言的需要。

這與云有什么關系？IP 創建者可以利用正式環境中的斷言來測試 IP 接口，例如，確保 IP 使用者應用的通信協議符合指定。但是，這并不意味著IP消費者可以使用正式技術。在這種情況下，消費者不太可能想要購買工具并忍受漫長的評估過程。云允許利用IP集成分析，而無需IP消費者不必要的工具所有權的費用和開銷，只需按使用付費訪問這些IP檢查的云解決方案即可節省高達95%的成本。

當然，如果使用其他適合嵌入式設計的正式靜態檢查，情況也是如此。例如，協議分析、寄存器檢查和其他片上系統 （SoC） 樣式分析在云中可用，在設計過程中可能需要少量應用程序。這對于嵌入式設計團隊來說是理想的選擇，他們可能希望快速創建一個硬件平臺來利用仿真器或虛擬模型，并檢查它是否正確實現，而無需采用復雜的驗證過程，以便他們可以繼續進行軟件設計。

預算范圍內的驗證

云解決方案最重要的優勢之一是業務模型及其對工具預算和嵌入式設計器控制的影響。例如，傳統的電子設計自動化（EDA）工具許可通常需要前期投資，無論是基于時間的許可證還是永久許可證。這要求購買者對工具資源需求有很好的了解，特別是很難使用任何驗證解決方案進行估計，因為使用模型將取決于編碼質量、復雜性和其他難以預測的因素。無論應用領域如何，這通常都是正確的，并且隨著潛在的項目規模和團隊結構而變得更加復雜。

在大多數驗證方案中，隨著更多代碼的完成并簽入設計數據庫，工具使用量會越來越大。隨著RTL編碼接近完成，對形式驗證軟件的需求將非常廣泛，有時對于通信和多媒體平臺等復雜設計，需求將達到平均四到五倍，并且隨著設計的合成和硅布局而下降。這種驗證膨脹的程度部分取決于代碼質量、實現的覆蓋率和其他指標。因此，將在整個設計流程中使用一定比例的可預測許可證。在膨脹期間，將應用一些不可預測的許可證數量。

云計算解決方案支持一種組合業務模型，其中某些許可證可以預先購買，而其他許可證可以使用按使用付費方案按需應用。設計團隊控制其資源需求，充分利用驗證過程的可變組件所需的資源，并消除冗余許可證。該模型還允許更大的財務控制，將一些工具費用負擔從資本預算轉移到更合適的運營或項目資金來源。

審核編輯：郭婷