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

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

0 引言

芯片驗(yàn)證方向經(jīng)過(guò)多年的探索和積累已經(jīng)有一套較為完備的驗(yàn)證體系[1]。其中，simulation 驗(yàn)證和formal 驗(yàn)證是兩大常用的驗(yàn)證方法。從對(duì)測(cè)試點(diǎn)的覆蓋程度上來(lái)說(shuō)，兩者的區(qū)別在于simulation 著眼于測(cè)試空間中的單個(gè)點(diǎn)，而formal 驗(yàn)證可以完全覆蓋輸入空間，從而能在約束條件下有效證明設(shè)計(jì)的準(zhǔn)確度[2]，formal 驗(yàn)證方法能在短時(shí)間內(nèi)遍歷所有可能的激勵(lì)，從而大大提高驗(yàn)證效率[3]，因此近年來(lái)formal 驗(yàn)證方法得到了越來(lái)越多的關(guān)注。

formal 驗(yàn)證工具大體可以分為兩類[4]，一類是MFV(Mainstream Formal Verification)，其具有成熟的功能，能實(shí)現(xiàn)高度自動(dòng)化驗(yàn)證。另一類是FPV(Formal Property Verification)，需要手動(dòng)開(kāi)發(fā)驗(yàn)證環(huán)境，編寫(xiě)property[5]。對(duì)于邏輯較為復(fù)雜、難以調(diào)用工具自帶模型的模塊更傾向于選擇FPV 工具來(lái)進(jìn)行驗(yàn)證。

保序模塊用于確保處理器內(nèi)部讀、寫(xiě)訪問(wèn)嚴(yán)格按照既定的順序處理，其與時(shí)序控制以及流水線控制密切相關(guān)，設(shè)計(jì)規(guī)模較大，邏輯復(fù)雜度較高，采用formal fpv 工具，本文按照驗(yàn)證對(duì)象介紹、Design Review、驗(yàn)證環(huán)境搭建、驗(yàn)證模型編寫(xiě)、JasperGold debug 的流程來(lái)展開(kāi)介紹。

1 驗(yàn)證對(duì)象簡(jiǎn)介

保序模塊是我司某存儲(chǔ)器系統(tǒng)中用于保證讀、寫(xiě)訪問(wèn)順序的模塊，基本框圖如圖1 所示，主要包括B 指令譯碼、B 數(shù)據(jù)寫(xiě)訪問(wèn)緩存、B 數(shù)據(jù)保序、B 數(shù)據(jù)提前返回、A 數(shù)據(jù)保序、A 數(shù)據(jù)提前返回、重讀等功能。

圖1 保序模塊基本框圖

保序模塊會(huì)對(duì)輸入的B 指令進(jìn)行譯碼，譯碼后的B數(shù)據(jù)寫(xiě)訪問(wèn)會(huì)經(jīng)過(guò)28 級(jí)流水buffer 緩存，在流水線上會(huì)對(duì)B 數(shù)據(jù)寫(xiě)請(qǐng)求地址相關(guān)的訪問(wèn)進(jìn)行保序處理，同時(shí)會(huì)判斷B 數(shù)據(jù)讀與B 數(shù)據(jù)寫(xiě)是否提前返回，以及重讀指示信號(hào)是否產(chǎn)生。對(duì)于A 數(shù)據(jù)訪問(wèn)來(lái)說(shuō)，A 數(shù)據(jù)寫(xiě)訪問(wèn)也會(huì)經(jīng)過(guò)28 級(jí)流水buffer 緩存，在流水線上會(huì)對(duì)A 數(shù)據(jù)訪問(wèn)進(jìn)行保序處理，也會(huì)判斷A 數(shù)據(jù)寫(xiě)數(shù)據(jù)是否提前返回。

其中，地址相關(guān)的保序需滿足：讀寫(xiě)同拍發(fā)生，認(rèn)為讀操作期望讀取舊值；先寫(xiě)后讀場(chǎng)景，認(rèn)為讀操作期望讀取寫(xiě)入后的新值。

2 Design Review

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

一種是傳統(tǒng)formal sign-off flow，如圖2 所示，特點(diǎn)是所有的斷言都需要被證明。對(duì)于這種sign-off flow，理想的RTL 代碼行數(shù)應(yīng)在1 500～3 000 范圍內(nèi)。在傳統(tǒng)Formal sign-off flow 中工具根據(jù)手動(dòng)編寫(xiě)的斷言自動(dòng)提取生成coverage，不需要再編寫(xiě)cover，保序模塊驗(yàn)證正是采用這種傳統(tǒng)的方法。

圖2 傳統(tǒng)formal sign-off flow

另一種是新型formal sign-off flow，如圖3 所示，特點(diǎn)是允許有證不出來(lái)的斷言，也就是說(shuō)允許有處于undetermined 的斷言，對(duì)于證不出來(lái)的斷言需要手動(dòng)編寫(xiě)function cover，對(duì)這種sign-off flow 來(lái)說(shuō)，理想的RTL 代碼行數(shù)應(yīng)在3 000～5 000 范圍內(nèi)。

圖3 新型formal sign-off flow

通過(guò)Design Review 可以梳理出fpv 驗(yàn)證的大框架。保序模塊涉及流水?dāng)?shù)較多有29 級(jí)，且前級(jí)流水的信號(hào)會(huì)對(duì)后級(jí)流水信號(hào)的變化產(chǎn)生影響，從input-output 信號(hào)通路角度來(lái)考慮，將保序模塊拆分成6 條通路，分別對(duì)每條通路使用formal fpv 進(jìn)行驗(yàn)證。

3 驗(yàn)證環(huán)境搭建

保序模塊驗(yàn)證平臺(tái)由三部分組成，分別是rtl_dmss、signoff、sva，其中rtl_dmss 用來(lái)存放設(shè)計(jì)RTL 代碼，signoff用來(lái)存放filelist、tcl 腳本以及編譯仿真過(guò)程中產(chǎn)生的臨時(shí)文件，sva 用來(lái)存放驗(yàn)證模型、驗(yàn)證平臺(tái)的環(huán)境文件。

在驗(yàn)證平臺(tái)環(huán)境中首先定義了模塊端口上的所有信號(hào)，然后將待測(cè)設(shè)計(jì)DUV 與驗(yàn)證模型連接起來(lái)作為激勵(lì)入口，驗(yàn)證平臺(tái)結(jié)構(gòu)如圖4 所示。

圖4 驗(yàn)證平臺(tái)結(jié)構(gòu)

在沒(méi)有外部約束的情況下，formal 會(huì)窮舉整個(gè)輸入空間，所以為了避免出現(xiàn)不符合設(shè)計(jì)需求的場(chǎng)景，需要在驗(yàn)證模型中添加相應(yīng)的約束。驗(yàn)證輸出和待測(cè)設(shè)計(jì)輸出的比對(duì)工作則放到了驗(yàn)證模型的assertion 部分，在assertion 部分會(huì)進(jìn)行一致性比對(duì)和時(shí)序檢查。

4 驗(yàn)證模型編寫(xiě)

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

4.1 功能模型編寫(xiě)

功能模型用來(lái)模擬被測(cè)對(duì)象的功能，通過(guò)將功能模型的輸出結(jié)果與待測(cè)對(duì)象的輸出進(jìn)行比對(duì)、檢查，可以得知待測(cè)對(duì)象功能的正確性。功能模型使用Verilog 語(yǔ)言來(lái)編寫(xiě)而不是SystemVerilog，這是因?yàn)楣δ苣Ｐ鸵欢ㄒ删C合，而SystemVerilog 有些語(yǔ)法不可綜合。對(duì)于保序模塊來(lái)說(shuō)，功能模型以cycle 為單位進(jìn)行建模，描述了模塊處于29 級(jí)流水的工作情況。

4.2 激勵(lì)約束編寫(xiě)

simulation 方法通過(guò)接口平臺(tái)產(chǎn)生transaction，再把transaction 傳輸給參考模型和待測(cè)設(shè)計(jì)，而formal 驗(yàn)證方法會(huì)對(duì)約束后的激勵(lì)進(jìn)行遍歷，也就是說(shuō)formal 驗(yàn)證平臺(tái)的激勵(lì)來(lái)自約束條件，如圖5 所示，激勵(lì)約束可以分為legal 和illegal 兩種。

圖5 輸入激勵(lì)約束

工具會(huì)對(duì)所有輸入信號(hào)進(jìn)行全隨機(jī)遍歷，通過(guò)編寫(xiě)激勵(lì)約束能保證輸入信號(hào)滿足待測(cè)設(shè)計(jì)的需求，而不會(huì)出現(xiàn)超出設(shè)計(jì)需求的場(chǎng)景。

值得注意的是，在編寫(xiě)激勵(lì)約束時(shí)不要過(guò)約束，否則驗(yàn)證的完整性就會(huì)大打折扣。對(duì)于保序模塊來(lái)說(shuō)，調(diào)試初期可能存在過(guò)約束的場(chǎng)景，調(diào)試過(guò)程中再逐漸放開(kāi)約束，保證驗(yàn)證的完整性和正確性。為了避免造成混亂，建議添加注釋將過(guò)約束和正常約束加以區(qū)別，同時(shí)出于規(guī)范化考慮，可以給激勵(lì)約束的名稱添加“ASM_”前綴。

對(duì)保序模塊的配置地址進(jìn)行約束時(shí)，雖然配置地址可以是隨機(jī)的，但在一次仿真中各個(gè)cycle 的配置地址需要保持不變，所以也需要對(duì)配置地址加以約束。

4.3 斷言編寫(xiě)

為了檢查待測(cè)設(shè)計(jì)的準(zhǔn)確性，需要把功能模型輸出與待測(cè)設(shè)計(jì)輸出進(jìn)行比較，通過(guò)斷言來(lái)檢查兩者是否匹配。斷言檢查流程如圖6 所示，當(dāng)斷言的所有狀態(tài)都被分析證實(shí)后該條斷言判斷為proved。

圖6 斷言檢查流程

formal fpv 斷言編寫(xiě)的原則之一是簡(jiǎn)單化。對(duì)于bit位較多的信號(hào)可以按一定的規(guī)則對(duì)信號(hào)進(jìn)行拆分，例如在保序模塊中檢查輸出讀地址的正確性，由于讀地址信號(hào)有32×8 bit，包含8 個(gè)通道每個(gè)通道32 bit 地址，可以使用循環(huán)把讀地址拆分成8 份，編寫(xiě)斷言來(lái)檢查每一份讀地址的正確性。

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

完備性是保序模塊驗(yàn)證的重要衡量指標(biāo)之一，通過(guò)給每條斷言添加注釋能方便地找出該條斷言對(duì)應(yīng)設(shè)計(jì)的哪些功能點(diǎn)，便于了解設(shè)計(jì)各個(gè)功能點(diǎn)是否都有斷言覆蓋。

5 JasperGold debug

5.1 JasperGold 工具介紹

運(yùn)行tcl 腳本啟動(dòng)JasperGold 軟件的UI 界面，可以看到各條斷言的仿真結(jié)果，如圖7 所示。

圖7 斷言仿真結(jié)果

JasperGold 的配置、編譯和仿真都是通過(guò)tcl 命令來(lái)實(shí)現(xiàn)的，可以查閱相關(guān)命令的使用說(shuō)明，如圖8 所示。

圖8 JasperGold 命令集

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

當(dāng)斷言出現(xiàn)反例時(shí)，雙擊失敗的斷言可以打開(kāi)對(duì)應(yīng)的波形，波形能精準(zhǔn)定位到出現(xiàn)反例的時(shí)刻，如圖9 所示，深灰表示觸發(fā)斷言，淺灰色表示斷言違例。

圖9 反例斷言仿真波形

5.2 debug 結(jié)果分析

在驗(yàn)證保序模塊驗(yàn)過(guò)程中發(fā)現(xiàn)了一些設(shè)計(jì)的缺陷，對(duì)這些缺陷加以整理匯總，主要有以下幾類。

第一類缺陷是待測(cè)設(shè)計(jì)中某些信號(hào)定義錯(cuò)誤，這類屬于比較直觀的缺陷。在斷言檢查時(shí)發(fā)現(xiàn)驗(yàn)證輸出的B數(shù)據(jù)讀地址與待測(cè)設(shè)計(jì)輸出的B 數(shù)據(jù)讀地址不一致。定位問(wèn)題發(fā)現(xiàn)是設(shè)計(jì)信號(hào)出現(xiàn)了位寬越界，養(yǎng)成良好的編碼習(xí)慣能大大減少這種情況的出現(xiàn)。

第二類缺陷是待測(cè)設(shè)計(jì)某些通道的信號(hào)處理出錯(cuò)。保序模塊讀訪問(wèn)包含8 個(gè)通道，斷言檢查時(shí)發(fā)現(xiàn)輸出的地址有效指示信號(hào)出錯(cuò)。通過(guò)前向追溯問(wèn)題發(fā)現(xiàn)待測(cè)設(shè)計(jì)某一通道的位寬處理出錯(cuò)，該缺陷在更上一層次的系統(tǒng)驗(yàn)證中沒(méi)有檢查出來(lái)。這就要求在編寫(xiě)斷言時(shí)，當(dāng)遇到復(fù)雜的信號(hào)時(shí)可以將其拆分成多組，分別檢查每組信號(hào)的時(shí)序，能迅速、精準(zhǔn)地定位問(wèn)題從而提高驗(yàn)證效率。

第三類缺陷是待測(cè)設(shè)計(jì)中循環(huán)處理出錯(cuò)。保序模塊內(nèi)信號(hào)的處理均受流水線控制，采用循環(huán)方法模擬流水線處理，在此過(guò)程中一些信號(hào)的賦值出錯(cuò)。通過(guò)斷言檢查發(fā)現(xiàn)驗(yàn)證輸出與待測(cè)設(shè)計(jì)輸出不一致，定位到寫(xiě)訪問(wèn)使能信號(hào)計(jì)算出錯(cuò)，進(jìn)一步向前推算發(fā)現(xiàn)問(wèn)題的源頭是循環(huán)處理出錯(cuò)。對(duì)于這種問(wèn)題鏈路過(guò)長(zhǎng)的情況，如果從輸出信號(hào)開(kāi)始定位驗(yàn)證難度較大，可以通過(guò)添加輔助邏輯來(lái)縮短問(wèn)題鏈路，從而降低問(wèn)題難度。

6 結(jié)論

基于formal fpv 的驗(yàn)證方法在保序模塊驗(yàn)證中有著很不錯(cuò)的效果，驗(yàn)證共發(fā)現(xiàn)8 單故障，其中一單故障發(fā)現(xiàn)了系統(tǒng)級(jí)驗(yàn)證遺漏的問(wèn)題。formal fpv 驗(yàn)證能實(shí)現(xiàn)輸入激勵(lì)的全范圍遍歷，這給驗(yàn)證工作提供了極大的便利。但是，formal fpv 驗(yàn)證很大程度上依賴于斷言編寫(xiě)的質(zhì)量，且復(fù)雜的模塊需要手動(dòng)編寫(xiě)驗(yàn)證功能模型。

綜合來(lái)看，對(duì)于設(shè)計(jì)相對(duì)簡(jiǎn)單的模塊采用formal fpv驗(yàn)證能提高驗(yàn)證效率，加快驗(yàn)證收斂速度。