你是否會遇到以下問題：bug可能比較微妙，不直觀，無法手動推斷；或者在被觀察到之前就被激活很久了，傳統的模擬設計需要花很長時間自動；驗證工作量隨著設計復雜性的增加而增加，人工推理和手動編寫屬性不再可行，等等。目前驗證CPU的主流方法，如HW Testbench,

Universal Verification Methodology (UVM),

SW Testbench, Property Checking,

這些現有方法具有范圍受限、仿真較慢、long bug traces、需要手動編寫test的特點。

那么，如何可靠、快速、自動地驗證處理器硬件，并且生成bug trace？

NO.1

形式化驗證的開展基于形式化規范和自動推理。其中形式化規范是指通過形式化語言將DUV和待證明的屬性建模成形式化模型，自動推理是指通過嚴格的數學方法來推導DUV和待證明屬性規范之間的邏輯關系，通常是證明DUV的形式化模型能滿足所有形式化屬性規范。

形式化驗證的基本步驟：

系統建模：把系統轉換為能被模型檢測工具所接受的形式。這是模型檢測的首要步驟，構建系統模型時為了提高驗證過程的效率及可行性需要將和要驗證的屬性無關的細節抽象掉，僅保留與此相關的細節，這是一個比較簡單但通常會比較繁瑣的過程。

形式化規范：在對模型進行驗證之前以邏輯公式的形式給出待驗證的屬性。命題時態邏輯能夠表達出系統的行為如何隨著時間而發生變化，因而通常被用來描述規范。一條規范只是描述了系統某一個屬性，一組規范是否覆蓋了系統需要滿足的所有屬性一直是個開放問題。規范開發的人力投入也是長期困擾形式驗證的問題。

形式化驗證：模型檢測工具對輸入的模型的狀態空間進行搜索來確定輸入的規范是否為真，為真表示模型滿足規范；為假則表示模型不滿足規范，此時會給出一個反例來說明規范為假的原因。

NO.2

QED（快速錯誤檢測）是一種識別錯誤的方法（主要在處理器中，但也可用于其他組件），它將一組原始測試轉換為QED檢查。這涉及到將寄存器文件分成兩部分，其中一半用于原始指令，另一半用于重復的指令序列，原始序列和復制序列都以相同的順序執行相同的指令，但它們是交錯的，在原始指令序列和復制指令序列完成后，寄存器文件的兩部分應該匹配。

根據經驗，與傳統技術相比，這種方法可以將bug trace的長度減少多達6個數量級。

Bounded Model Checking（BMC）用于驗證有限狀態模型的正確性。它通過遍歷有限長度的路徑來檢查模型是否滿足給定的性質。

SQED基于BMC進行符號運算搜索所有指令序列組合。這為我們提供了一種無需編寫測試就可以驗證處理器的方法，也不需要提供任何手寫屬性，只依賴于SQED檢查。是對傳統的形式驗證方法的突破。

NO.3

基于SQED的指令集形式驗證具有如下特點

全自動驗證：Symbolic Instructions + Self-Consistency Checking，不需要開發屬性集。

高覆蓋率：BMC工具搜索給定深度的所有指令序列。

最簡bug復現：BMC工具自動生成從復位狀態到bug site的最短路徑。

借助AveMC高性能形式驗證平臺，AveMC/SQED組合為芯片設計指令集驗證提供了全新的驗證解決方案。

NO.4

AveMC在開源RISC-V上的SQED驗證過程: 給定RISC-V核的RTL實現和ISA SPEC，從ISA SPEC中自動解析生成QED Module（一個新的RTL），將原有的RISC-V核和QED Module連接起來。這里AveMC就可以直接進行驗證了。

指令集形式驗證是芯片設計驗證中的新興方向，在RISCV和AI/ML硬件加速芯片的驗證中得到越來越廣泛的應用。SQED是指令集形式驗證領域的新興工具，它通過完全自測試的特性解決了驗證屬性開發的低效和覆蓋率問題。在上海阿卡思微電子技術有限公司形式驗證平臺AveMC上，SQED得到了成功的實現。與開源形式驗證工具相比，AveMC/SQED不僅提升了驗證速度，還能發現其他工具無法發現的bug。

上海阿卡思微電子技術有限公司由硅谷回國的資深電子設計自動化(EDA)專家于2020年在上海張江高科技園區設立，旗下子公司成都奧卡思微電科技有限公司于2018年在成都高新區創立，公司聚集國際知名EDA公司和芯片設計公司具有多年研發經驗的尖端人才，基于形式化方法為邏輯芯片設計和工控軟件等提供驗證工具及咨詢服務，憑借在形式化方法領域深厚的技術積累及深入的產品實踐，公司已推出系列商用性能優異的驗證工具，服務于復雜芯片設計及通用設計流程，獲得多個標桿客戶的采購使用。在研產品及應用包括高階等價驗證、功能安全等，覆蓋數字信息、智能硬件、航空航天、人工智能等行業需求。公司將最新的EDA技術與本土用戶需求相結合，服務于中國集成電路自主可控設計；將產品開發與數字產業趨勢相結合，服務于中國技術創新與技術趕超；將技術推廣與產品優化相結合，服務于海內外需求市場。致力于成為國內領先的形式化技術開發與服務商。

審核編輯：湯梓紅