一種基于靜態形式驗證的I/O復用電路高效驗證方法

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

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

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

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

1 基于靜態形式化驗證的連接性檢查

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

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

靜態驗證工具VC Formal CC的目標應用包括結構檢查和功能檢查兩方面。結構檢查是檢查從源到目標是否有一個結構連接/路徑。功能檢查是檢查設計中的兩個信號是否具有同樣的值，注意是在特定的條件，比如數據選擇器（multiplexer，MUX）邏輯。雖然傳統方法中使用動態仿真也可以進行功能檢查，但是它不能進行結構檢查。

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

2 IO復用的電路特征以及驗證目標

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

（1）I/O復用情況復雜

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

（2）工作模式的不同

在SoC的開發中，還會加入可測性設計模塊（Design For Test，DFT）。因此，I/O復用的電路也要把測試功能考慮進去。

圖1 IO復用在系統級的驗證對象

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

簡單來說，I/O復用實際上是利用一個巨大的MUX實現的。針對IO復用的結構，如果使用常規的驗證方法，從搭建驗證環境到驗證case的完成，工作量很大，并且工時較長。而這種情況對于連接性檢查工具CC check來說，正是它的優勢所在。通過使用CC check，不需要搭建專門的驗證環境，只需要提取驗證要點，配置驗證參數，驗證工具可以自動生成測試向量，并進行驗證。由此可以大幅提高I/O模塊的驗證效率，縮短產品開發周期。由于CC check使用的是靜態的數學理論實現測試向量的生成，極大地提高了驗證的完備性。

本工作的目標是在芯片級別驗證從各IP模塊經過PINMUX到IO PAD的驗證。圖1是系統級I/O復用驗證對象示意圖。其中灰色部分在連接性驗證中都是黑盒化，藍色部分是驗證的對象。

3 VC Fomral CC在I/O復用中的驗證流程

在進行連接性檢查之前，雖然使用測試case對IO復用進行了部分功能的驗證，但是對整個I/O復用的全部功能來說，這些驗證是不充分的，因此使用CC check對剩余的連接性進行驗證。在連接性檢查完成后，使用VC Formal CC產生的覆蓋率數據可以合并到芯片的覆蓋率數據中，完善SoC系統的連接性驗證。

使用VC Formal CC驗證I/O復用的流程如下：

（1）首先要根據I/O復用的設計spec抽取生成CC check需要的CSV表格

項目開始前需要準備一個CSV表格，它是VC Foraml CC用來連接驗證的輸入格式。這個表格就是一個CC測試計劃，如圖2所示，它包括源信號，目的信號，使能條件，復位，不同的延遲設置等。

圖3 CC check建立流程

（2）準備和運行TCL文件

在RTL和Formal流程中都是用的是工具命令語言（tool command language，TCL）。整個CC check流程建立中的設置如圖3所示。其中，定義復位信息可以支持多復位設置，打開自動黑盒子功能可以在連接驗證目標的基礎上對設計進行提取。通過使用命令Check_fv，在產生斷言后，會自動的執行check_fv和保存CC check的結果。

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

圖4 IO復用驗證中部分黑盒化list

圖5 使用Verdi GUI界面進行debug

（3）查看結果，debug，和鎖定bug

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

“check_fv”命令能夠自動執行這些斷言檢查，在進行了第一個檢查后，會發現有一些斷言失敗。我們查找了原因，一些是因為CSV文件中連接定義不正確，其余的是真正的RTL中的連接bug。

圖6 IO復用驗證的結果

圖7 IO驗證toggle結果

圖8 未toggle的信號調查

表1 本次驗證工作結果總結

表2 傳統驗證方法和本方法的對比

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

4 驗證結果

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

使用VC Formal CC容易地驗證連接性，并且實現toggle的覆蓋目標。研發人員可以在設計早期發現IO復用的連接錯誤。由于免去了搭建chip級驗證環境和編寫驗證case，assertion的工作，大大提升了驗證工作的效率，節省了產品開發時間。表1是對本次驗證工作結果的總結。表2是使用傳統驗證方法和使用VC Formal CC工作量的比較。

總結：靜態形式驗證作為芯片signoff的重要方法已經被應用到先進SoC芯片的驗證流程中，VC Formal CC更是簡化了Formal執行者的工作量，可以節省大量的人工，并且在連接性的結構性檢查中具有很大的優勢。本文使用VC Fomral CC實現了IO復用的驗證，在設計初期，不需要搭建驗證環境，不需要編寫驗證case，就可以對IO復用功能進行驗證，進而可以提前發現設計缺陷，縮短驗證時間。