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

形式化驗(yàn)證技術(shù)正在成為越來(lái)越多驗(yàn)證解決方案的基礎(chǔ)，也是緩解云安全問(wèn)題的關(guān)鍵。該技術(shù)能夠?qū)Ⅱ?yàn)證問(wèn)題分解為多個(gè)抽象的數(shù)學(xué)問(wèn)題，并將其傳輸?shù)皆浦羞M(jìn)行解決，并刪除所有設(shè)計(jì)細(xì)節(jié)，從而確保設(shè)計(jì)安全性。形式驗(yàn)證過(guò)程通過(guò)提取要分析的特定狀態(tài)并與所需屬性進(jìn)行比較來(lái)實(shí)現(xiàn)此目的。設(shè)計(jì)細(xì)節(jié)將保留并在本地重新應(yīng)用于云操作的結(jié)果。此過(guò)程消除了將 IP 移出辦公室的需要。

由此產(chǎn)生的解決方案利用一系列基于云的服務(wù)器來(lái)提供廣泛的驗(yàn)證功能，提供易于采用和使用、按需性能權(quán)衡以及按使用付費(fèi)的業(yè)務(wù)模式。這對(duì)于基于IP的嵌入式設(shè)計(jì)尤其重要，其中IP由可能不擁有正式技術(shù)所有權(quán)的第三方使用。

通過(guò)云獲取驗(yàn)證軟件

云計(jì)算驗(yàn)證軟件使用“客戶端工具”，即在本地主機(jī)上運(yùn)行并充當(dāng)云引擎前端的組件，從設(shè)計(jì)代碼創(chuàng)建數(shù)學(xué)證明問(wèn)題集以傳輸?shù)皆啤？蛻舳斯ぞ甙ā發(fā)inting”功能（一種在硬件描述語(yǔ)言 （HDL） 代碼中查找設(shè)計(jì)錯(cuò)誤的方法），并管理與云解決方案的通信。它還允許在本地主機(jī)上執(zhí)行云處理結(jié)果的任何所需調(diào)試。

傳統(tǒng)上，驗(yàn)證軟件被授權(quán)在本地主機(jī)上運(yùn)行，并且從設(shè)計(jì)輸入到結(jié)果調(diào)試的整個(gè)操作都是使用單個(gè)產(chǎn)品完成的。對(duì)于云方案，客戶端工具使用戶體驗(yàn)相同，就好像整個(gè)產(chǎn)品在本地運(yùn)行一樣，為云使用模型提供了透明的感覺(jué)。

實(shí)際應(yīng)用

轉(zhuǎn)型的按使用付費(fèi)業(yè)務(wù)模式、對(duì)無(wú)限數(shù)量的計(jì)算引擎的訪問(wèn)以及按需驗(yàn)證應(yīng)用程序的結(jié)合提供了一些有趣的新優(yōu)勢(shì)。

例如，該軟件非常適合希望以最小的學(xué)習(xí)曲線和設(shè)置過(guò)程在其現(xiàn)有的基于仿真的驗(yàn)證流程中添加強(qiáng)大的正式設(shè)計(jì)檢查的新用戶。

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

高級(jí)用戶也可以獲得相當(dāng)大的好處。形式驗(yàn)證本質(zhì)上是一個(gè)并行的過(guò)程，數(shù)學(xué)證明問(wèn)題并行運(yùn)行。云解決方案提供無(wú)限數(shù)量的計(jì)算服務(wù)器，因此，可以在多個(gè)計(jì)算機(jī)之間執(zhí)行驗(yàn)證運(yùn)行，以提供最佳的并行執(zhí)行。即使成本保持不變 - 在單個(gè)服務(wù)器上花費(fèi)10小時(shí)的成本與在10臺(tái)服務(wù)器上花費(fèi)1小時(shí)的成本相同。在軟件許可方法中，必須預(yù)先購(gòu)買(mǎi)足夠的許可證才能涵蓋完整的并行使用，通常對(duì)可能一起運(yùn)行的操作數(shù)量設(shè)置了很小的上限。因此，在大多數(shù)驗(yàn)證安裝中，并行操作通常受到多重限制。

該解決方案還支持按需使用特定目的，例如IP集成或驗(yàn)證服務(wù)提供商的一種手段，這些服務(wù)提供商需要在外國(guó)環(huán)境中工作時(shí)訪問(wèn)這些工具。在每種情況下，都可以利用該軟件，而無(wú)需最終客戶預(yù)先購(gòu)買(mǎi)它，這是在沒(méi)有利用正式解決方案的第三方參與時(shí)的理想選擇。

嵌入式設(shè)計(jì)的云優(yōu)勢(shì)

嵌入式設(shè)計(jì)有一些特定問(wèn)題，可以通過(guò)基于云的基于應(yīng)用程序的驗(yàn)證來(lái)緩解。嵌入式設(shè)計(jì)的本質(zhì)是，IP將從各種來(lái)源得到利用。此 IP 將應(yīng)用一系列驗(yàn)證指標(biāo)，并可能使用復(fù)雜的接口進(jìn)行互連（圖 2）。

圖 2：形式驗(yàn)證可以為利用來(lái)自不同來(lái)源的IP的嵌入式設(shè)計(jì)提供嚴(yán)格的集成測(cè)試環(huán)境。

正如一家領(lǐng)先的半導(dǎo)體公司在最近的設(shè)計(jì)自動(dòng)化會(huì)議上所討論的那樣，形式驗(yàn)證可以在這種情況下發(fā)揮巨大的作用，以提供嚴(yán)格的集成測(cè)試環(huán)境。斷言用于指定接口以及要在 IP 和平臺(tái)之間傳遞的預(yù)期信息。鑒于知識(shí)產(chǎn)權(quán)的可重用性以及確保其在外國(guó)環(huán)境中正確相互聯(lián)系的重要性，這種對(duì)斷言的投資被認(rèn)為是值得的。當(dāng)然，如果這種互連是通過(guò)標(biāo)準(zhǔn)總線協(xié)議（例如ARM的AHB標(biāo)準(zhǔn)），則可以使用一組標(biāo)準(zhǔn)的協(xié)議斷言來(lái)確保其有效性。以這種方式使用斷言已被證明可以提高質(zhì)量并減少集成時(shí)間，因?yàn)殍b于IP的可重用性，如果經(jīng)過(guò)充分測(cè)試，則可以在隨后進(jìn)行更多投資，并且將消除重寫(xiě)斷言的需要。

這與云有什么關(guān)系？IP 創(chuàng)建者可以利用正式環(huán)境中的斷言來(lái)測(cè)試 IP 接口，例如，確保 IP 使用者應(yīng)用的通信協(xié)議符合指定。但是，這并不意味著IP消費(fèi)者可以使用正式技術(shù)。在這種情況下，消費(fèi)者不太可能想要購(gòu)買(mǎi)工具并忍受漫長(zhǎng)的評(píng)估過(guò)程。云允許利用IP集成分析，而無(wú)需IP消費(fèi)者不必要的工具所有權(quán)的費(fèi)用和開(kāi)銷，只需按使用付費(fèi)訪問(wèn)這些IP檢查的云解決方案即可節(jié)省高達(dá)95%的成本。

當(dāng)然，如果使用其他適合嵌入式設(shè)計(jì)的正式靜態(tài)檢查，情況也是如此。例如，協(xié)議分析、寄存器檢查和其他片上系統(tǒng) （SoC） 樣式分析在云中可用，在設(shè)計(jì)過(guò)程中可能需要少量應(yīng)用程序。這對(duì)于嵌入式設(shè)計(jì)團(tuán)隊(duì)來(lái)說(shuō)是理想的選擇，他們可能希望快速創(chuàng)建一個(gè)硬件平臺(tái)來(lái)利用仿真器或虛擬模型，并檢查它是否正確實(shí)現(xiàn)，而無(wú)需采用復(fù)雜的驗(yàn)證過(guò)程，以便他們可以繼續(xù)進(jìn)行軟件設(shè)計(jì)。

預(yù)算范圍內(nèi)的驗(yàn)證

云解決方案最重要的優(yōu)勢(shì)之一是業(yè)務(wù)模型及其對(duì)工具預(yù)算和嵌入式設(shè)計(jì)器控制的影響。例如，傳統(tǒng)的電子設(shè)計(jì)自動(dòng)化（EDA）工具許可通常需要前期投資，無(wú)論是基于時(shí)間的許可證還是永久許可證。這要求購(gòu)買(mǎi)者對(duì)工具資源需求有很好的了解，特別是很難使用任何驗(yàn)證解決方案進(jìn)行估計(jì)，因?yàn)槭褂媚Ｐ蛯⑷Q于編碼質(zhì)量、復(fù)雜性和其他難以預(yù)測(cè)的因素。無(wú)論應(yīng)用領(lǐng)域如何，這通常都是正確的，并且隨著潛在的項(xiàng)目規(guī)模和團(tuán)隊(duì)結(jié)構(gòu)而變得更加復(fù)雜。

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

云計(jì)算解決方案支持一種組合業(yè)務(wù)模型，其中某些許可證可以預(yù)先購(gòu)買(mǎi)，而其他許可證可以使用按使用付費(fèi)方案按需應(yīng)用。設(shè)計(jì)團(tuán)隊(duì)控制其資源需求，充分利用驗(yàn)證過(guò)程的可變組件所需的資源，并消除冗余許可證。該模型還允許更大的財(cái)務(wù)控制，將一些工具費(fèi)用負(fù)擔(dān)從資本預(yù)算轉(zhuǎn)移到更合適的運(yùn)營(yíng)或項(xiàng)目資金來(lái)源。

審核編輯：郭婷