使用形式驗(yàn)證技術(shù)作為片上系統(tǒng) （SoC） 設(shè)計(jì)的主流技術(shù)，終于成為消除驗(yàn)證差距的公認(rèn)方法。最近的一項(xiàng)調(diào)查表明，26% 的芯片設(shè)計(jì)項(xiàng)目現(xiàn)在使用基于斷言的正式驗(yàn)證 （ABV）。然而，這種經(jīng)典模擬的替代方法的承諾需要很多年才能開(kāi)花結(jié)果，而且仍然只有高級(jí)驗(yàn)證環(huán)境才能包含它。為什么會(huì)這樣？到目前為止，我們可以從它的使用中學(xué)到什么，以便將其提供給整個(gè) SoC 工程社區(qū)？

SoC 塊驗(yàn)證碰壁

自問(wèn)世以來(lái)，SoC 設(shè)備一直是開(kāi)發(fā)團(tuán)隊(duì)的驗(yàn)證噩夢(mèng)。雖然現(xiàn)在驗(yàn)證完整的 SoC 最好留給仿真和快速原型設(shè)計(jì)系統(tǒng)來(lái)完成，但即使是這些設(shè)備上的較大塊也已經(jīng)超出了純仿真環(huán)境。

仿真、更快的模擬器、關(guān)鍵測(cè)試的驗(yàn)證知識(shí)產(chǎn)權(quán) （VIP） 以及通用驗(yàn)證方法 （UVM） 的出現(xiàn)都有助于緩解這種情況。盡管如此，驗(yàn)證要求仍超過(guò)了基于模擬的環(huán)境中的可用處理時(shí)間。

形式驗(yàn)證通過(guò)使用針對(duì)特定需求的自動(dòng)化“應(yīng)用程序”有助于改進(jìn)塊驗(yàn)證，否則需要大量的模擬工作。檢查標(biāo)準(zhǔn)通信協(xié)議的正確操作、確保關(guān)鍵連接和寄存器操作、分析域重置時(shí)的正確啟動(dòng)序列以及許多其他任務(wù)現(xiàn)在都由這些解決方案處理。

然而，我們才剛剛開(kāi)始挖掘形式驗(yàn)證的真正威力。它的許多使用問(wèn)題已被消除，使我們處于可能是全新驗(yàn)證時(shí)代的最前沿，因?yàn)樵摷夹g(shù)已部署用于核心驗(yàn)證。

形式驗(yàn)證：如果這么好，今天在哪里？

首先，快速回顧一下形式驗(yàn)證技術(shù)，為什么它有可能創(chuàng)造這種根本性轉(zhuǎn)變，以及今天是什么阻止了它。

硬件仿真的工作原理是通過(guò)一系列有意義的狀態(tài)循環(huán)一個(gè)硬件描述語(yǔ)言 （HDL） 代碼塊來(lái)演示其操作。此狀態(tài)序列由輸入激勵(lì)（設(shè)備輸入上的一組事件的 HDL 描述）驅(qū)動(dòng)，旨在探索正確的狀態(tài)以識(shí)別操作問(wèn)題。

這種方法引出了一個(gè)問(wèn)題：如果我們知道代碼塊可以進(jìn)入的所有狀態(tài)以及狀態(tài)間轉(zhuǎn)換，那么我們不能簡(jiǎn)單地詢問(wèn)有關(guān)代碼操作的問(wèn)題以確保其正確嗎？這將避免必須編寫(xiě)許多行刺激來(lái)嘗試使代碼塊進(jìn)入正確的信息承載狀態(tài)。這是形式驗(yàn)證工具使用的方法。

這種基本方法可以轉(zhuǎn)變?yōu)樵S多有用的應(yīng)用程序。例如，如果可以根據(jù)設(shè)計(jì)代碼的一個(gè)方面和要檢查的驗(yàn)證場(chǎng)景自動(dòng)創(chuàng)建要問(wèn)的問(wèn)題，則可以創(chuàng)建用于驗(yàn)證目的的自動(dòng)化應(yīng)用程序。這將不需要用戶編寫(xiě)問(wèn)題。如果正式工具可以用最少的輸入演示特定的狀態(tài)序列（例如狀態(tài)機(jī)操作），那么設(shè)計(jì)工程師就可以理解他或她的代碼如何執(zhí)行，從而揭示可能的錯(cuò)誤。

當(dāng)工程師自己提出問(wèn)題時(shí)，形式驗(yàn)證的真正威力才得以發(fā)揮。這需要使用斷言編寫(xiě)問(wèn)題或?qū)傩裕⒃诜Q為基于斷言的驗(yàn)證或 ABV 的過(guò)程中應(yīng)用于設(shè)計(jì)。

當(dāng)然，這種高級(jí)描述掩蓋了 ABV 的問(wèn)題，包括存儲(chǔ)這么多信息的工具的容量和性能要求已經(jīng)通過(guò)最新技術(shù)得到解決。

兩個(gè)問(wèn)題仍然是 ABV 廣泛使用的障礙：

斷言的創(chuàng)作，通常使用 SystemVerilog 標(biāo)準(zhǔn)語(yǔ)法，可能很復(fù)雜且難以可視化

對(duì)驗(yàn)證進(jìn)度或覆蓋率的理解很難與其他驗(yàn)證方法的理解和對(duì)比

盡管在這兩個(gè)方面都取得了進(jìn)步，但還需要更多的努力來(lái)降低學(xué)習(xí)曲線，從而使 ABV 得以普遍擴(kuò)散。

ABV 應(yīng)用程序

在驗(yàn)證過(guò)程中應(yīng)用 ABV 有兩種常用方法。首先是檢查特定的極端案例類型的問(wèn)題，這些問(wèn)題通常需要花費(fèi)大量精力來(lái)構(gòu)建模擬測(cè)試平臺(tái)來(lái)分析問(wèn)題。第二個(gè)是對(duì)塊進(jìn)行更一般的檢查，無(wú)論是結(jié)合模擬還是獨(dú)立檢查。

形式驗(yàn)證的第一個(gè)使用模型很有價(jià)值，可以在驗(yàn)證計(jì)劃中減少合理的百分比。第二個(gè)模型有可能改變特征驗(yàn)證過(guò)程，節(jié)省大量時(shí)間和資源支出，同時(shí)增加發(fā)現(xiàn)設(shè)計(jì)中每個(gè)錯(cuò)誤的整體潛力。已經(jīng)有一些行業(yè)部門(mén)在第二種模式中廣泛使用 ABV。其中包括汽車和航空電子產(chǎn)品，其中高質(zhì)量和可靠性是一個(gè)因素。

在組合仿真-形式驗(yàn)證流程中，如圖 1 所示，通常使用仿真進(jìn)行一般操作分析并“感受”設(shè)計(jì)的行為和性能。此外，還有一些功能更適合模擬，例如數(shù)學(xué)數(shù)據(jù)處理或信號(hào)處理。然而，形式驗(yàn)證非常適合控制或數(shù)據(jù)傳輸種類的功能，如有限狀態(tài)機(jī)、數(shù)據(jù)通信和協(xié)議檢查。此外，確保某些類型的驗(yàn)證場(chǎng)景，例如安全檢查（例如，某項(xiàng)活動(dòng)是否會(huì)發(fā)生），也是該技術(shù)的最佳選擇。這些代碼和場(chǎng)景示例通常需要很高比例的驗(yàn)證資源。

斷言創(chuàng)作改進(jìn)

與 UVM 推動(dòng)模擬測(cè)試臺(tái)創(chuàng)建的分層方法相同，新技術(shù)正在出現(xiàn)，將抽象引入斷言創(chuàng)作。這些抽象通過(guò)掩蓋斷言細(xì)節(jié)來(lái)降低復(fù)雜性，同時(shí)允許工程師考慮驗(yàn)證任務(wù)而不是斷言的個(gè)別特征。

例如，OneSpin 解決方案的 Operational Assertions 是一個(gè) SystemVerilog 庫(kù)，它允許正式測(cè)試以類似事務(wù)時(shí)序圖的方式表示，與驗(yàn)證工程師廣泛認(rèn)可的高級(jí) UVM 序列不同。Breker Verification Systems 的基于圖形的測(cè)試序列，現(xiàn)在由 Accellera Portable Stimulus 標(biāo)準(zhǔn)委員會(huì)考慮，是另一種抽象形式，也可以應(yīng)用于斷言創(chuàng)作。

這些技術(shù)在簡(jiǎn)化形式測(cè)試應(yīng)用的同時(shí)，具有提供可識(shí)別且更自然的輸入方案的優(yōu)勢(shì)，允許工程師通過(guò)消除一些形式驗(yàn)證之謎來(lái)與正在進(jìn)行的驗(yàn)證過(guò)程相關(guān)聯(lián)。

常見(jiàn)的覆蓋模型

簡(jiǎn)化斷言只是難題的一部分。該過(guò)程的另一端是整理來(lái)自各種來(lái)源的覆蓋率信息，以了解總體驗(yàn)證進(jìn)度，無(wú)論使用何種工具。模擬過(guò)程仍然主要集中在一種或另一種代碼覆蓋上，并包含一些功能覆蓋。形式驗(yàn)證覆蓋側(cè)重于斷言（所謂的“斷言覆蓋”），無(wú)論它們是否被執(zhí)行，它們是通過(guò)還是失敗，或者確實(shí)它們通過(guò)一個(gè)警告（例如，有界證明，例如“代碼在一定數(shù)量的時(shí)鐘周期內(nèi)通過(guò)”）。該信息可以反饋給驗(yàn)證計(jì)劃系統(tǒng)以提供一些有用的數(shù)據(jù)。

然而，測(cè)量正式的覆蓋率，確定由特定斷言測(cè)試的實(shí)際代碼，是領(lǐng)先的形式驗(yàn)證供應(yīng)商感興趣的領(lǐng)域。已經(jīng)提出了在精度和所需執(zhí)行資源方面都不同的方案。關(guān)鍵是能夠?qū)⑦@些正式模型與模擬模型進(jìn)行比較，以提供綜合的、有意義的覆蓋率評(píng)估。Accellera 統(tǒng)一覆蓋互操作性標(biāo)準(zhǔn) （UCIS） 委員會(huì)專注于這一目標(biāo)，并提出了可以將兩者進(jìn)行比較的方法。在這方面需要做更多的工作，但很明顯，一些形式驗(yàn)證供應(yīng)商擁有允許計(jì)算合理的進(jìn)度度量的解決方案。

模擬風(fēng)格調(diào)試

以對(duì)以仿真為中心的工程師有意義的方式調(diào)試形式驗(yàn)證代碼，在很大程度上已被許多形式驗(yàn)證供應(yīng)商解決。大多數(shù)工具可以在斷言失敗的情況下輸出“見(jiàn)證”。也就是說(shuō)，導(dǎo)致斷言失敗的仿真波形形式的一系列事件。事實(shí)上，包括 OneSpin 在內(nèi)的一些供應(yīng)商可以輸出模擬測(cè)試，允許在模擬器中重現(xiàn)故障以供進(jìn)一步研究。

破解主流ABV代碼

很明顯，ABV 的使用開(kāi)始成為主流。ARM 和 Oracle 都宣布了 ABV 在其環(huán)境中的全部功能，并指出它現(xiàn)在在他們的項(xiàng)目中被大量使用。

解決 Assertion Authoring、Collated Coverage 和 Simulation-centric Debug 這三條腿的問(wèn)題，并將其與對(duì)形式驗(yàn)證擅長(zhǎng)的設(shè)計(jì)領(lǐng)域和場(chǎng)景的清晰理解相結(jié)合，將推動(dòng)這種方法成為 SoC 驗(yàn)證的主流。一旦發(fā)生這種情況，將對(duì)未來(lái)的設(shè)計(jì)質(zhì)量和開(kāi)發(fā)進(jìn)度產(chǎn)生巨大影響。

審核編輯：郭婷