保序模塊的formal fpv 驗證

趙亞雪，植 玉，梁其鋒，石義軍

(深圳市中興微電子技術有限公司，廣東 深圳 518054)

0 引言

芯片驗證方向經過多年的探索和積累已經有一套較為完備的驗證體系[1]。其中，simulation 驗證和formal 驗證是兩大常用的驗證方法。從對測試點的覆蓋程度上來說，兩者的區別在于simulation 著眼于測試空間中的單個點，而formal 驗證可以完全覆蓋輸入空間，從而能在約束條件下有效證明設計的準確度[2]，formal 驗證方法能在短時間內遍歷所有可能的激勵，從而大大提高驗證效率[3]，因此近年來formal 驗證方法得到了越來越多的關注。

formal 驗證工具大體可以分為兩類[4]，一類是MFV(Mainstream Formal Verification)，其具有成熟的功能，能實現高度自動化驗證。另一類是FPV(Formal Property Verification)，需要手動開發驗證環境，編寫property[5]。對于邏輯較為復雜、難以調用工具自帶模型的模塊更傾向于選擇FPV 工具來進行驗證。

保序模塊用于確保處理器內部讀、寫訪問嚴格按照既定的順序處理，其與時序控制以及流水線控制密切相關，設計規模較大，邏輯復雜度較高，采用formal fpv 工具，本文按照驗證對象介紹、Design Review、驗證環境搭建、驗證模型編寫、JasperGold debug 的流程來展開介紹。

1 驗證對象簡介

保序模塊是我司某存儲器系統中用于保證讀、寫訪問順序的模塊，基本框圖如圖1 所示，主要包括B 指令譯碼、B 數據寫訪問緩存、B 數據保序、B 數據提前返回、A 數據保序、A 數據提前返回、重讀等功能。

圖1 保序模塊基本框圖

保序模塊會對輸入的B 指令進行譯碼，譯碼后的B數據寫訪問會經過28 級流水buffer 緩存，在流水線上會對B 數據寫請求地址相關的訪問進行保序處理，同時會判斷B 數據讀與B 數據寫是否提前返回，以及重讀指示信號是否產生。對于A 數據訪問來說，A 數據寫訪問也會經過28 級流水buffer 緩存，在流水線上會對A 數據訪問進行保序處理，也會判斷A 數據寫數據是否提前返回。

其中，地址相關的保序需滿足：讀寫同拍發生，認為讀操作期望讀取舊值；先寫后讀場景，認為讀操作期望讀取寫入后的新值。

2 Design Review

常用的formal sign-off flow 可以分為兩種情況。

一種是傳統formal sign-off flow，如圖2 所示，特點是所有的斷言都需要被證明。對于這種sign-off flow，理想的RTL 代碼行數應在1 500～3 000 范圍內。在傳統Formal sign-off flow 中工具根據手動編寫的斷言自動提取生成coverage，不需要再編寫cover，保序模塊驗證正是采用這種傳統的方法。

圖2 傳統formal sign-off flow

另一種是新型formal sign-off flow，如圖3 所示，特點是允許有證不出來的斷言，也就是說允許有處于undetermined 的斷言，對于證不出來的斷言需要手動編寫function cover，對這種sign-off flow 來說，理想的RTL 代碼行數應在3 000～5 000 范圍內。

圖3 新型formal sign-off flow

通過Design Review 可以梳理出fpv 驗證的大框架。保序模塊涉及流水數較多有29 級，且前級流水的信號會對后級流水信號的變化產生影響，從input-output 信號通路角度來考慮，將保序模塊拆分成6 條通路，分別對每條通路使用formal fpv 進行驗證。

3 驗證環境搭建

保序模塊驗證平臺由三部分組成，分別是rtl_dmss、signoff、sva，其中rtl_dmss 用來存放設計RTL 代碼，signoff用來存放filelist、tcl 腳本以及編譯仿真過程中產生的臨時文件，sva 用來存放驗證模型、驗證平臺的環境文件。

在驗證平臺環境中首先定義了模塊端口上的所有信號，然后將待測設計DUV 與驗證模型連接起來作為激勵入口，驗證平臺結構如圖4 所示。

圖4 驗證平臺結構

在沒有外部約束的情況下，formal 會窮舉整個輸入空間，所以為了避免出現不符合設計需求的場景，需要在驗證模型中添加相應的約束。驗證輸出和待測設計輸出的比對工作則放到了驗證模型的assertion 部分，在assertion 部分會進行一致性比對和時序檢查。

4 驗證模型編寫

由于保序模塊涉及29 級流水且邏輯較為復雜，fpv工具自帶的模型并不適合保序模塊，需要手動搭建各條通路的驗證模型。保序模塊的驗證模型包括模塊功能模型、激勵約束和斷言三部分。

4.1 功能模型編寫

功能模型用來模擬被測對象的功能，通過將功能模型的輸出結果與待測對象的輸出進行比對、檢查，可以得知待測對象功能的正確性。功能模型使用Verilog 語言來編寫而不是SystemVerilog，這是因為功能模型一定要可綜合，而SystemVerilog 有些語法不可綜合。對于保序模塊來說，功能模型以cycle 為單位進行建模，描述了模塊處于29 級流水的工作情況。

4.2 激勵約束編寫

simulation 方法通過接口平臺產生transaction，再把transaction 傳輸給參考模型和待測設計，而formal 驗證方法會對約束后的激勵進行遍歷，也就是說formal 驗證平臺的激勵來自約束條件，如圖5 所示，激勵約束可以分為legal 和illegal 兩種。

圖5 輸入激勵約束

工具會對所有輸入信號進行全隨機遍歷，通過編寫激勵約束能保證輸入信號滿足待測設計的需求，而不會出現超出設計需求的場景。

值得注意的是，在編寫激勵約束時不要過約束，否則驗證的完整性就會大打折扣。對于保序模塊來說，調試初期可能存在過約束的場景，調試過程中再逐漸放開約束，保證驗證的完整性和正確性。為了避免造成混亂，建議添加注釋將過約束和正常約束加以區別，同時出于規范化考慮，可以給激勵約束的名稱添加“ASM_”前綴。

對保序模塊的配置地址進行約束時，雖然配置地址可以是隨機的，但在一次仿真中各個cycle 的配置地址需要保持不變，所以也需要對配置地址加以約束。

4.3 斷言編寫

為了檢查待測設計的準確性，需要把功能模型輸出與待測設計輸出進行比較，通過斷言來檢查兩者是否匹配。斷言檢查流程如圖6 所示，當斷言的所有狀態都被分析證實后該條斷言判斷為proved。

圖6 斷言檢查流程

formal fpv 斷言編寫的原則之一是簡單化。對于bit位較多的信號可以按一定的規則對信號進行拆分，例如在保序模塊中檢查輸出讀地址的正確性，由于讀地址信號有32×8 bit，包含8 個通道每個通道32 bit 地址，可以使用循環把讀地址拆分成8 份，編寫斷言來檢查每一份讀地址的正確性。

出于規范化考慮，可以給斷言的名稱添加“AST_”前綴。為了避免斷言調試出錯，在復位信號有效時需要disable掉該斷言，在保序模塊中寫作“disable iff(！core_sync_rst_n)”。

完備性是保序模塊驗證的重要衡量指標之一，通過給每條斷言添加注釋能方便地找出該條斷言對應設計的哪些功能點，便于了解設計各個功能點是否都有斷言覆蓋。

5 JasperGold debug

5.1 JasperGold 工具介紹

運行tcl 腳本啟動JasperGold 軟件的UI 界面，可以看到各條斷言的仿真結果，如圖7 所示。

圖7 斷言仿真結果

JasperGold 的配置、編譯和仿真都是通過tcl 命令來實現的，可以查閱相關命令的使用說明，如圖8 所示。

圖8 JasperGold 命令集

各條斷言仿真結果可能有prove、unreachable、undetermined 三種情況。圖7 中assert 前打綠勾表示斷言驗證通過，打叉表示該斷言出現反例，可以雙擊查看波形進一步分析。打勾和感嘆號表示斷言的前提條件無法滿足，需要檢查約束條件是否過約束，debug 分析是驗證模型問題還是待測設計問題。

當斷言出現反例時，雙擊失敗的斷言可以打開對應的波形，波形能精準定位到出現反例的時刻，如圖9 所示，深灰表示觸發斷言，淺灰色表示斷言違例。

圖9 反例斷言仿真波形

5.2 debug 結果分析

在驗證保序模塊驗過程中發現了一些設計的缺陷，對這些缺陷加以整理匯總，主要有以下幾類。

第一類缺陷是待測設計中某些信號定義錯誤，這類屬于比較直觀的缺陷。在斷言檢查時發現驗證輸出的B數據讀地址與待測設計輸出的B 數據讀地址不一致。定位問題發現是設計信號出現了位寬越界，養成良好的編碼習慣能大大減少這種情況的出現。

第二類缺陷是待測設計某些通道的信號處理出錯。保序模塊讀訪問包含8 個通道，斷言檢查時發現輸出的地址有效指示信號出錯。通過前向追溯問題發現待測設計某一通道的位寬處理出錯，該缺陷在更上一層次的系統驗證中沒有檢查出來。這就要求在編寫斷言時，當遇到復雜的信號時可以將其拆分成多組，分別檢查每組信號的時序，能迅速、精準地定位問題從而提高驗證效率。

第三類缺陷是待測設計中循環處理出錯。保序模塊內信號的處理均受流水線控制，采用循環方法模擬流水線處理，在此過程中一些信號的賦值出錯。通過斷言檢查發現驗證輸出與待測設計輸出不一致，定位到寫訪問使能信號計算出錯，進一步向前推算發現問題的源頭是循環處理出錯。對于這種問題鏈路過長的情況，如果從輸出信號開始定位驗證難度較大，可以通過添加輔助邏輯來縮短問題鏈路，從而降低問題難度。

6 結論

基于formal fpv 的驗證方法在保序模塊驗證中有著很不錯的效果，驗證共發現8 單故障，其中一單故障發現了系統級驗證遺漏的問題。formal fpv 驗證能實現輸入激勵的全范圍遍歷，這給驗證工作提供了極大的便利。但是，formal fpv 驗證很大程度上依賴于斷言編寫的質量，且復雜的模塊需要手動編寫驗證功能模型。

綜合來看，對于設計相對簡單的模塊采用formal fpv驗證能提高驗證效率，加快驗證收斂速度。