一種基于靜態(tài)形式驗(yàn)證的I/O復(fù)用電路高效驗(yàn)證方法

北京智芯微電子科技有限公司 段麗瑩 胡 毅 郝 燚 甘 杰 馮文楠 唐曉柯

隨著系統(tǒng)級(jí)芯片（System on Chip，SoC）中輸入/輸出（I/O）接口數(shù)量和復(fù)用功能的不斷增加，I/O復(fù)用電路的驗(yàn)證變得越來越復(fù)雜，并且需要耗費(fèi)大量時(shí)間。本文針對(duì)I/O復(fù)用電路的特點(diǎn)，提出一種基于靜態(tài)形式驗(yàn)證的高效驗(yàn)證方法，在驗(yàn)證早期對(duì)I/O復(fù)用進(jìn)行了復(fù)用功能驗(yàn)證和連接性驗(yàn)證，同時(shí)也進(jìn)行了翻轉(zhuǎn)覆蓋率收集。與傳統(tǒng)基于動(dòng)態(tài)驗(yàn)證的方法相比，本方法可以將驗(yàn)證時(shí)間縮短一半以上，顯著提升了設(shè)計(jì)質(zhì)量和開發(fā)效率。

芯片驗(yàn)證是芯片開發(fā)流程中必不可少的環(huán)節(jié)，芯片驗(yàn)證的目標(biāo)是全面，快速，簡單并高效。隨著芯片設(shè)計(jì)技術(shù)和制造工藝技術(shù)的發(fā)展，主流系統(tǒng)級(jí)芯片（System on Chip，SoC）的集成度不斷增加，使芯片具有越來越復(fù)雜的功能；同時(shí)，芯片面積和物理邊界在不斷減小。在這種環(huán)境下，芯片的輸入/輸出（I/O）接口面臨著功能需求增加與面積限制的矛盾。為解決這一問題，現(xiàn)今的SoC中普遍采用了I/O復(fù)用技術(shù)。傳統(tǒng)方法使用系統(tǒng)級(jí)仿真驗(yàn)證來驗(yàn)證I/O復(fù)用功能，需要在系統(tǒng)級(jí)別編寫場景測(cè)試?yán)╟ase），然后可以配合進(jìn)行相關(guān)的斷言驗(yàn)證。然而隨著SoC復(fù)雜度的提升，I/O接口的數(shù)量和復(fù)用功能也都隨之增加，從芯片級(jí)別對(duì)I/O復(fù)用進(jìn)行驗(yàn)證需要編寫復(fù)雜的測(cè)試?yán)M合并且花費(fèi)大量時(shí)間。如何實(shí)現(xiàn)I/O復(fù)用電路的高效驗(yàn)證成為了芯片驗(yàn)證工作中的一個(gè)重大挑戰(zhàn)。

靜態(tài)形式化驗(yàn)證（formal）方法是通過形式數(shù)學(xué)方法來證明斷言或?qū)傩?，以確保RTL代碼的正確性。屬性驗(yàn)證（formal property verification，F(xiàn)PV）是一種典型的靜態(tài)形式驗(yàn)證方法，已經(jīng)被證明是設(shè)計(jì)驗(yàn)證簽收（signoff）的一種可信賴的方案。但是，隨著設(shè)計(jì)逐漸變復(fù)雜，設(shè)計(jì)的容量和復(fù)雜度都會(huì)對(duì)使用形式化驗(yàn)證方法帶來制限，如果沒有任何人工抽取方法是無法實(shí)現(xiàn)全覆蓋的驗(yàn)證。本文提出了使用靜態(tài)驗(yàn)證工具VC Formal CC來完成I/O復(fù)用的單體和SoC級(jí)別的驗(yàn)證，無需搭建新的驗(yàn)證平臺(tái)，也不需要編寫專門的驗(yàn)證case。同時(shí)VC Formal CC可以產(chǎn)生覆蓋率數(shù)據(jù)，并合并到芯片級(jí)的覆蓋率數(shù)據(jù)中，有效提高了I/O復(fù)用電路驗(yàn)證的效率和完備性。

1 基于靜態(tài)形式化驗(yàn)證的連接性檢查

在芯片設(shè)計(jì)的驗(yàn)證中，連接驗(yàn)證是最基本的驗(yàn)證內(nèi)容。連接可以通過形式化驗(yàn)證方法完成完全的驗(yàn)證，但是需要執(zhí)行FPV設(shè)計(jì)人員將SoC分成不同的子系統(tǒng)，手動(dòng)將不進(jìn)行驗(yàn)證的模塊黑盒化，并使用常量和假設(shè)來約束設(shè)計(jì)。因此，驗(yàn)證過程需要消耗大量的人力和時(shí)間。

連接性檢查（Connectivity Check，CC）應(yīng)用是在形式化驗(yàn)證的基礎(chǔ)上建立的。與FPV相比，CC是一個(gè)自動(dòng)check的工具，可以實(shí)現(xiàn)高效的驗(yàn)證工作。CC通過讀取CSV表格自動(dòng)提取設(shè)計(jì)并分析連接檢查的需求。然后自動(dòng)產(chǎn)生連接檢查需要的斷言和假定。因此理想化來說，CC執(zhí)行屬性檢查，但是并不需要用戶再建立檢查器（checker）。該工具會(huì)幫助時(shí)鐘產(chǎn)生，重置（reset）產(chǎn)生和斷言產(chǎn)生。CC工具在設(shè)計(jì)提取方面具有強(qiáng)大的功能，能夠解決龐大的SoC編譯的問題。

靜態(tài)驗(yàn)證工具VC Formal CC的目標(biāo)應(yīng)用包括結(jié)構(gòu)檢查和功能檢查兩方面。結(jié)構(gòu)檢查是檢查從源到目標(biāo)是否有一個(gè)結(jié)構(gòu)連接/路徑。功能檢查是檢查設(shè)計(jì)中的兩個(gè)信號(hào)是否具有同樣的值，注意是在特定的條件，比如數(shù)據(jù)選擇器（multiplexer，MUX）邏輯。雖然傳統(tǒng)方法中使用動(dòng)態(tài)仿真也可以進(jìn)行功能檢查，但是它不能進(jìn)行結(jié)構(gòu)檢查。

連接性檢查有組合邏輯和時(shí)序邏輯兩種應(yīng)用場景。在組合邏輯的應(yīng)用中可以驗(yàn)證SoC I/O連接，模塊引腳復(fù)用/解復(fù)用，可配置多路復(fù)用，模塊的連接和常值檢查，在子模塊間的直接連接等內(nèi)容。在時(shí)序邏輯的應(yīng)用中，VC Formal CC可以支持檢查待延遲的路徑，比如在源-目的路徑上有觸發(fā)器（FlipFlop），和使能（enbale）路徑上有觸發(fā)器的路徑。在本工作中CC工具的使用主要是完成組合邏輯中的I/O復(fù)用進(jìn)行的驗(yàn)證。

2 IO復(fù)用的電路特征以及驗(yàn)證目標(biāo)

對(duì)于目前的SoC的焊盤（PAD）來說，大多數(shù)PAD屬于通用I/O（genneral Purpose I/O，GPIO）。常見的GPIO型PAD單元均為雙向I/O，除了輸入/輸出數(shù)據(jù)使能，還包括上下拉使能，驅(qū)動(dòng)能力使能等。為了實(shí)現(xiàn)高集成度和盡可能小的芯片面積，有限的I/O就通過PINMUX模塊和寄存器的不同配置來實(shí)現(xiàn)GPIO的復(fù)用。PAD的復(fù)用從功能角度具有以下兩個(gè)特點(diǎn)：

（1）I/O復(fù)用情況復(fù)雜

實(shí)際上，SoC的每一個(gè)PAD在大部分的工作時(shí)間內(nèi)都屬于自己主要服務(wù)的模塊，這是其最基本的屬性。但除此之外，它們還承擔(dān)著轉(zhuǎn)接到其他模塊并協(xié)助傳輸數(shù)據(jù)的任務(wù)。當(dāng)I/O被切換到其它功能時(shí)，功能控制的選擇、輸入輸出方向控制邏輯等都是通過相關(guān)寄存器的配置來實(shí)現(xiàn)。

（2）工作模式的不同

在SoC的開發(fā)中，還會(huì)加入可測(cè)性設(shè)計(jì)模塊（Design For Test，DFT）。因此，I/O復(fù)用的電路也要把測(cè)試功能考慮進(jìn)去。

圖1 IO復(fù)用在系統(tǒng)級(jí)的驗(yàn)證對(duì)象

圖2 VCForaml CC需要的CSV文件格式和TCL命令

簡單來說，I/O復(fù)用實(shí)際上是利用一個(gè)巨大的MUX實(shí)現(xiàn)的。針對(duì)IO復(fù)用的結(jié)構(gòu)，如果使用常規(guī)的驗(yàn)證方法，從搭建驗(yàn)證環(huán)境到驗(yàn)證case的完成，工作量很大，并且工時(shí)較長。而這種情況對(duì)于連接性檢查工具CC check來說，正是它的優(yōu)勢(shì)所在。通過使用CC check，不需要搭建專門的驗(yàn)證環(huán)境，只需要提取驗(yàn)證要點(diǎn)，配置驗(yàn)證參數(shù)，驗(yàn)證工具可以自動(dòng)生成測(cè)試向量，并進(jìn)行驗(yàn)證。由此可以大幅提高I/O模塊的驗(yàn)證效率，縮短產(chǎn)品開發(fā)周期。由于CC check使用的是靜態(tài)的數(shù)學(xué)理論實(shí)現(xiàn)測(cè)試向量的生成，極大地提高了驗(yàn)證的完備性。

本工作的目標(biāo)是在芯片級(jí)別驗(yàn)證從各IP模塊經(jīng)過PINMUX到IO PAD的驗(yàn)證。圖1是系統(tǒng)級(jí)I/O復(fù)用驗(yàn)證對(duì)象示意圖。其中灰色部分在連接性驗(yàn)證中都是黑盒化，藍(lán)色部分是驗(yàn)證的對(duì)象。

3 VC Fomral CC在I/O復(fù)用中的驗(yàn)證流程

在進(jìn)行連接性檢查之前，雖然使用測(cè)試case對(duì)IO復(fù)用進(jìn)行了部分功能的驗(yàn)證，但是對(duì)整個(gè)I/O復(fù)用的全部功能來說，這些驗(yàn)證是不充分的，因此使用CC check對(duì)剩余的連接性進(jìn)行驗(yàn)證。在連接性檢查完成后，使用VC Formal CC產(chǎn)生的覆蓋率數(shù)據(jù)可以合并到芯片的覆蓋率數(shù)據(jù)中，完善SoC系統(tǒng)的連接性驗(yàn)證。

使用VC Formal CC驗(yàn)證I/O復(fù)用的流程如下：

（1）首先要根據(jù)I/O復(fù)用的設(shè)計(jì)spec抽取生成CC check需要的CSV表格

項(xiàng)目開始前需要準(zhǔn)備一個(gè)CSV表格，它是VC Foraml CC用來連接驗(yàn)證的輸入格式。這個(gè)表格就是一個(gè)CC測(cè)試計(jì)劃，如圖2所示，它包括源信號(hào)，目的信號(hào)，使能條件，復(fù)位，不同的延遲設(shè)置等。

圖3 CC check建立流程

（2）準(zhǔn)備和運(yùn)行TCL文件

在RTL和Formal流程中都是用的是工具命令語言（tool command language，TCL）。整個(gè)CC check流程建立中的設(shè)置如圖3所示。其中，定義復(fù)位信息可以支持多復(fù)位設(shè)置，打開自動(dòng)黑盒子功能可以在連接驗(yàn)證目標(biāo)的基礎(chǔ)上對(duì)設(shè)計(jì)進(jìn)行提取。通過使用命令Check_fv，在產(chǎn)生斷言后，會(huì)自動(dòng)的執(zhí)行check_fv和保存CC check的結(jié)果。

由于本SoC中的I/O復(fù)用模塊完全由組合邏輯構(gòu)成，所以在腳本中沒有對(duì)時(shí)鐘和進(jìn)行設(shè)置。在進(jìn)行SoC中的I/O復(fù)用部分的驗(yàn)證時(shí)，我們可以把不關(guān)心的連接驗(yàn)證的設(shè)計(jì)部分進(jìn)行黑盒化處理，這樣可以進(jìn)一步減少VC fomal CC工具分析對(duì)象的數(shù)量，在滿足驗(yàn)證完備性的前提下節(jié)省仿真時(shí)間。VC Formal CC中提供了自動(dòng)識(shí)別黑盒化的命令。圖4是本I/O復(fù)用驗(yàn)證中的部分黑盒化的list示意圖。

圖4 IO復(fù)用驗(yàn)證中部分黑盒化list

圖5 使用Verdi GUI界面進(jìn)行debug

（3）查看結(jié)果，debug，和鎖定bug

在編譯了RTL和CSV之后，VC Formal工具會(huì)為每個(gè)定義在CSV文件中的連接驗(yàn)證生成斷言，在CSV文件中描述了n個(gè)連接檢查，就有n個(gè)斷言產(chǎn)生。

“check_fv”命令能夠自動(dòng)執(zhí)行這些斷言檢查，在進(jìn)行了第一個(gè)檢查后，會(huì)發(fā)現(xiàn)有一些斷言失敗。我們查找了原因，一些是因?yàn)镃SV文件中連接定義不正確，其余的是真正的RTL中的連接bug。

圖6 IO復(fù)用驗(yàn)證的結(jié)果

圖7 IO驗(yàn)證toggle結(jié)果

圖8 未toggle的信號(hào)調(diào)查

表1 本次驗(yàn)證工作結(jié)果總結(jié)

表2 傳統(tǒng)驗(yàn)證方法和本方法的對(duì)比

Debug的方法有兩種，一種debug方法是使用命令行。在命令行中使用analyze_root_cause和report_root_cause兩個(gè)命令，命令行會(huì)報(bào)出連接錯(cuò)誤的原因。通過顯示的描述可以查找斷言fail的原因。另一種是使用VC Fomral CC的圖形用戶界面（Graphical User Interface，GUI），使用GUI可以同時(shí)觀測(cè)電路和波形，更加快速和便利。這種圖形化界面使得debug更直觀和便捷。圖5是一個(gè)fail的實(shí)例。通過GUI可以看到缺少一個(gè)enable的控制點(diǎn)（紅圈部分）。這種屬于CSV中enable定義不全。

4 驗(yàn)證結(jié)果

圖6是本次IO復(fù)用CC Check驗(yàn)證的最后結(jié)果。CSV中定義的所有的驗(yàn)證項(xiàng)目全部pass。我們還可以把收集的覆蓋率數(shù)據(jù)與SoC的仿真覆蓋率數(shù)據(jù)合并在一起。通過GUI就可以直接的看到翻轉(zhuǎn)（toggle）結(jié)果。圖7是本工作中針對(duì)IO復(fù)用的CC check的覆蓋率結(jié)果，結(jié)果顯示有16個(gè)信號(hào)沒有toggle。除此之外，其他信號(hào)全部都實(shí)現(xiàn)了toggle。圖8是未toggle信號(hào)的列表，經(jīng)過調(diào)查這些信號(hào)在IP內(nèi)是被固定為常值的。

使用VC Formal CC容易地驗(yàn)證連接性，并且實(shí)現(xiàn)toggle的覆蓋目標(biāo)。研發(fā)人員可以在設(shè)計(jì)早期發(fā)現(xiàn)IO復(fù)用的連接錯(cuò)誤。由于免去了搭建chip級(jí)驗(yàn)證環(huán)境和編寫驗(yàn)證case，assertion的工作，大大提升了驗(yàn)證工作的效率，節(jié)省了產(chǎn)品開發(fā)時(shí)間。表1是對(duì)本次驗(yàn)證工作結(jié)果的總結(jié)。表2是使用傳統(tǒng)驗(yàn)證方法和使用VC Formal CC工作量的比較。

總結(jié)：靜態(tài)形式驗(yàn)證作為芯片signoff的重要方法已經(jīng)被應(yīng)用到先進(jìn)SoC芯片的驗(yàn)證流程中，VC Formal CC更是簡化了Formal執(zhí)行者的工作量，可以節(jié)省大量的人工，并且在連接性的結(jié)構(gòu)性檢查中具有很大的優(yōu)勢(shì)。本文使用VC Fomral CC實(shí)現(xiàn)了IO復(fù)用的驗(yàn)證，在設(shè)計(jì)初期，不需要搭建驗(yàn)證環(huán)境，不需要編寫驗(yàn)證case，就可以對(duì)IO復(fù)用功能進(jìn)行驗(yàn)證，進(jìn)而可以提前發(fā)現(xiàn)設(shè)計(jì)缺陷，縮短驗(yàn)證時(shí)間。