作者：Mark Handover；Abdelouahab Ayari
簡介

連通性檢查涉及驗證器件布線。它相當于問這樣一個問題：“設計元素是否被正確裝配？” 更準確地說，它是在驗證設計中的邏輯模塊之間的連接是否正確，例如：模塊 B1 上的輸出 A 是否正確連接到模塊 B2 上的輸入 A''。這常常是很困難的驗證任務。設計包含數以千計的導線，這些導線的正確性可能都需要檢查，因此要檢查的連接數量是一個問題。

調試提出了另一個次要的但常常同樣具有挑戰性的問題。原因是，雖然采用定向或約束隨機方法通過動態測試檢查連通性肯定能發現一些連通性錯誤，但問題只會表現為被測模塊內部的功能性問題，而不一定能幫助查明問題連接。使用斷言可以在源頭捕獲設計錯誤，從而減輕調試問題。但是，所需的檢查量仍然可能令人瞠目。

為應對此類挑戰，形式驗證為我們提供了一種快速、詳盡且支持高效調試的解決方案。傳統上，芯片級形式驗證確實不可行。該方法通常以模塊級別為目標，使狀態空間的規模保持在適當水平。但是，鑒于連通性檢查僅集中在布線上（與模塊級別的復雜度相比，布線一般是器件的簡單部分），借助一些假設，狀態空間可以減小到可管理的規模。這種簡化的性質取決于所需檢查的類型。

本文首先會概述幾種類型的連通性檢查，然后詳細介紹一種新型半自動驗證流程（包括代碼）。已有一些 Mentor Graphics 使用該流程來簡化連通性檢查。該流程基于一個腳本環境，圍繞該環境提供了充足的信息以方便用戶開始實施新的驗證方法。

點對點連通性檢查的類型

直接點對點檢查

連通性檢查的最簡單形式是點對點檢查 —— 端口 A 是否連接到端口 B？這是就同一層次結構而言的。

例如，如果一個設計有八個模塊，所有模塊都位于頂層，那么驗證只需要檢查這八個模塊與頂層之間的連接。

在這種情況下，我們只需把八個子模塊進行黑盒化處理，而不必對整個器件進行建模。檢查不依賴于模塊內容，因此無需讀取這些模塊的 HDL。

跨層次結構的直接點對點檢查

這在本質上與簡單檢查方法相似，不過檢查的是位于一個層次結構中一個模塊上的端口是否在物理上正確連接到位于另一層次結構中的一個模塊，或者位于信號源的單個端口是否連接到多個端點。

以對存儲器的寫使能為例。它可能起源于單個頂層輸入管腳，但可以連接到跨許多不同層次位置的許多存儲器實例。

現在涉及層次結構，因此無法將上方的模塊實例統一進行黑盒化處理。黑盒化處理應該在最高層級上執行，但只能用于那些不在寫使能路徑上或可能影響寫使能連通性的邏輯路徑上的模塊。盡管更具挑戰性并需要一些設計知識，但這種更具選擇性的黑盒方法仍然可以顯著簡化狀態空間。

其他類型的檢查

驗證器件的模塊間連通性可能需要進行多種類型的檢查。到目前為止，我們僅考慮了點對點檢查，即所有條件下 A = B，層級可以相同或不同。許多連接都是這種性質的，但也可能需要其他類型的檢查。

我們來看幾個例子。

條件點對點檢查

兩點之間的連接可能取決于系統中的其他行為或另一個信號的狀態。例如，當驗證管腳多路復用時，所選的 IO 路徑將取決于控制信號的值。令情況變得復雜的是，信號的目的地可能是一個相反值，執行檢查時可能還需要考慮這一點。

有延遲的點對點

某些情況下需要點對點連接，但傳播可能要花費若干周期，而不是立即發生。因此，這就需要完善點對點檢查。

無延遲的點對點

這類似于前面所述的簡單點對點檢查，但有一個重大區別：用戶要求檢查明確驗證不僅 A 連接到 B，而且路徑上沒有時序邏輯。

構造檢查

鑒于需要創建大量檢查才能全面檢查器件連通性情況，用戶如何創建所需的斷言？

一種常見方法是使用格式特別編制的電子表格，其中詳細說明了應連接的各個點、涉及的路徑延遲、反轉、條件等。然后，工具或腳本解析電子表格并將其轉換為斷言語言，例如 SystemVerilog 斷言 (SVA) 或屬性說明語言 (PSL)。圖 1 顯示了一個帶有一些連通性信息的電子表格描述范例。

連通性信息（電子表格描述）

圖 1

我們來瀏覽一下該電子表格。我們指定了兩種檢查類型：“cond” 指條件連接，“connect” 指無條件的直接連接。這將允許我們在創建檢查器期間創建不同斷言類型。“輸入1” 和 “輸入2” 字段詳細列出了設計中要進行連通性檢查的起點和終點。“條件” 列用于詳細說明需要設置什么信號才允許點對點連接為真。“connect”檢查沒有條件，檢查將是直接、無條件的。最后，所有延遲字段都是 0，表示所有連接都沒有延遲。

一旦電子表格格式固定并填充內容，便可使用適當的工具或腳本來解析電子表格和創建斷言，而斷言將作為目標送入形式化工具。一種方法是使用通用屬性模板，然后在單獨的檢查器描述中添加每個屬性實例的連通性信息。這樣就可以將其綁定（使用 SystemVerilog 的 bind 結構體）到設計的頂層。

圖 2 顯示了兩個通用屬性模板。

圖 2

屬性 cond_p 支持條件檢查，而 connect_p 支持直接無條件檢查。

此模板文件可以包含許多獨特類型的連通性檢查，一旦明確便無需用戶編輯。該文件不包含任何設計信息，因而與項目無關，可以重復使用。

從電子表格自動創建的源就是檢查器詳細信息，其中包含模板文件中不同檢查的實例，并添加了適當的信號名稱。一個例子如圖 3 所示。

圖 3

其他注意事項

時鐘

設計不可避免地包含多個時鐘。通過形式驗證，未定義的時鐘會產生與這些時鐘明確相關的設計邏輯和任何斷言的抽象。來自抽象域的信號成為形式驗證控制點，這可能會導致意外激發。

為了避免工具執行任何抽象，必須定義所有時鐘。但是，某些設計有很多 10s 的時鐘，所以這可能很麻煩。

連通性檢查常常不驗證時鐘邏輯，因此定義時鐘貌似是不必要的任務。然而，為檢查連通性而創建的斷言會使用時鐘。

理論上講，用戶只需定義那些與斷言相關的時鐘，以及那些影響斷言所檢查路徑上的時序邏輯的時鐘。

不過，鑒于難以識別路徑上的時序邏輯，這可能不是一個容易執行的簡化操作。

實踐中，顯式指定和定義設計中的所有時鐘可能會更容易。由于連通性檢查通常不檢查設計的時序行為，或者至多檢查連接是否存在延遲（或沒有延遲），因此一般可以給所有時鐘指定同一頻率。這就大大簡化了用戶為形式工具定義時鐘信息的任務。

分階段測試被測器件可能有多種工作模式，這些模式可能會影響可激活的連通性路徑或設計邏輯。測試應確保每種有效模式都得到測試，同時還要充分利用所有設計最小化（即黑盒化處理）的機會 —— 針對具體模式進行配置時可能會有這種機會。

用戶還應注意所執行測試的方面，并相應地對測試進行分組以便支持分階段方法，這樣測試環境的設置會更簡單。例如，如果存儲器連接測試屬于一組必須進行的連通性檢查，并且所有存儲器僅存在于少數幾個子模塊中，則除這些子模塊外的所有設計都可以進行黑盒化處理。這種特定的最小化對于連通性檢查的另一個方面（例如檢查 IP 接口或網橋連接）可能是不可行的。其他測試方面可能需要不同的最小化策略，因此可以在測試策略的第二階段中定義，并在第三階段和第四階段中進一步定義設置策略。

詳細信息：實施更高效流程的工具

某些 Mentor Graphics 客戶使用的方法（比如上面的例子）一般遵循一套通用步驟：首先，聲明檢查器的一個實例。然后，在適當的字段中添加適當的信號名稱。使用 Questa Formal，此方法適用于 Verilog、VHDL、混合語言設計和混合語言層次結構。本文是我們努力讓其他工程團隊能夠以最少的工作使用類似驗證流程的一部分。在我們的方法中，我們定義了連通性規范電子表格的格式，并且編寫了一個腳本來創建SVA 或 PSL 檢查器。我們還創建了一組屬性模板，以便支持多種類型的連通性檢查。該半自動化流程的詳細信息（包括代碼）說明如下。

為了能夠更好地部署這種連通性檢查方法，我們基于腳本的新環境允許自動創建各種所需文件。我們開發了一個 Perl 腳本 GenConn.pl，利用它來解析連通性信息的文本文件，創建 SVA 或 PSL 檢查器，還可以創建 Questa Formal 的 makefile。為此需要定義連通性數據的格式，然后作為制表符分隔值 (TSV) 或逗號分隔值 (CSV) 的文件提供給腳本。

利用形式驗證檢查 SoC 連通性的正確性

目前，腳本可以支持和創建七種類型的連通性檢查：

■ 點對點，有或無延遲

■ 條件點對點，有或無延遲

■ 互斥信號

■ 接高電平的信號

■ 接低電平的信號

要創建這些類型的檢查器，用戶需要填充連通性規范文件。該文件的格式詳見圖 4。

連通性規范

圖 4

“檢查器關鍵字” 表示用戶希望推斷的檢查類型，“信號 ...” 和 “條件信號” 條目是指向要檢查連通性的設計信號或端口的層次路徑。“延遲值” 是時序延遲周期數，須為整數。

例如，假設我們要檢查信號 top.en 到 top.u1.u2.enable 的連通性，并且該路徑上應有兩個周期的時序延遲。

圖 5 顯示了規范文件中該條目的樣子。請注意，對于互斥檢查器，雖然表中顯示了四個連接，但實際上可以指定任意數量的連接。

圖 5

除連通性信息外，規范文件還應包括被測設計的名稱、時鐘的名稱以及檢查器將使用的復位。無論高電平有效還是低電平有效，都需要提供復位感測。這些信息應按照如下格式指定：

■ Design

■ Clock <檢查器時鐘名稱>

■ Reset <檢查器復位名稱>

■ Reset_sense <低或高>

連通性規范文件需要以 TSV 或 CSV 格式傳遞給腳本。完整 TSV 格式連通性規范文件的例子如圖 6 所示。

圖 6

一旦以正確格式描述了完整的連通性規范，便可將其傳遞給腳本以創建檢查器。

該腳本可以接受多個參數，如圖 7 所示。

圖 7

默認情況下，預期輸入格式為 TSV，檢查器輸出文件（名為 “checkers.sv”）將采用 SVA 格式。不過，用戶可以通過指定適當的選項來更改默認行為。

腳本會自動創建輸出連通性規范文件。它是 TSV 或 CSV 規范輸入的副本，但每個條目都包括所創建檢查器的名稱。該文件的默認名稱為 checker_conn_spec，可使用 -s 開關予以覆蓋；擴展名為 .tsv 或 .csv，具體取決于輸入文件的格式。

輸出文件 checkers.sv 包含用于構建檢查器的所有必要信息。為了簡化使用，先前說明的 “屬性模板” 已經固定，并由腳本自動創建。檢查器模板本身、檢查器實例化和綁定信息都包含在一個檢查器文件中。圖 8（注意下一頁仍有代碼）顯示了 SVA 風格 checkers.sv 文件輸出的例子。

圖 8

選擇生成的 makefile 允許用戶編譯所創建的 SVA 或 PSL 檢查器文件以用于 Questa Formal，然后運行形式分析。

該 makefile 名為 Makefile _ ConnCheck。它有三個條目：

■ compile _ checkers：編譯 SVA 或 PSL

■ compile _ formal _ model：運行 CSL 流程以構建形式模型

■ run _ formal：運行 Questa Formal “證明” 流程

還有一個 run_all 條目，它允許依次執行所有三個步驟。為了運行 makefile 中的所有步驟，用戶需要執行：

make –f Makefile _ ConnCheck run _ all

運行形式編譯和證明步驟的結果分別放在目錄 “results/csl” 和 “results/prove” 中。

Makefile _ ConnCheck 文件具有成功編譯和運行 Questa Formal 所需的基本條目，但它更多地是作為模板提供，用戶在使用之前很可能需要進行編輯。

例如，makefile 沒有引用形式驗證的控制文件（用于定義時鐘、設置約束等），因此可能需要創建和指定該文件。

還有一個附加腳本 GenDoc.pl。此腳本的作用是將形式結果注釋到 checker _ conn _ spec 文件上，該文件是自動生成并加注了檢查器名稱的連通性規范。GenDoc 腳本應在獲得形式 “證明” 結果后運行。

該腳本可以接受多個參數，如圖 9 所示。

圖 9

默認輸入和輸出文件名為：

■ 連通性規范輸入文件名：checker _ conn _ spec.tsv

■ 連通性規范輸出文件：conn _ spec _ results（后綴取決于輸入文件格式）

■ 證明報告文件名：results/prove/0in _ prove.rpt

所有這些默認值都可以使用適當的開關予以覆蓋。

在 “證明” 形式運行之后，生成的輸出文件會詳細說明每個連通性規范條目以及檢查器名稱和狀態，如圖 10

所示。

圖 10

下一頁上的圖 11 給出了可用于運行完整連通性檢查流程的命令示例，圖 12 顯示了整個流程。

圖 11

圖 12

其他應用

連通性檢查在許多應用中都很有價值。下面介紹幾個例子。

焊盤環檢查

復雜器件具有多種配置，SoC 中的 IO 不可避免地會涉及復雜的多路復用焊盤。必須驗證所有配置下的焊盤環，檢查每種模式下是否都存在正確連接。利用形式技術檢查這種連通性會窮盡所有可能性，發現極端情況并帶來自動化功能，而仿真技術常常無法做到這一點。

存儲器 BIST 檢查

設計常常會包含由內建自測試 (BIST) 邏輯測試的存儲器，其中 BIST 邏輯是在 RTL 階段插入。可能是許多存儲器（常常位于不同層級）連接到單個主 BIST 控制器。

來自 BIST 控制器的控制信號連接到各種存儲器或存儲器控制器，這些連接可以是共用的。例如，來自 BIST控制器的 write _ enable 可以連接到許多存儲器上的 write _ enable 管腳。

形式連通性檢查是一種有效替代方法，用戶無需編寫動態測試來檢查存儲器 BIST 連接并在每次更改 RTL時重新運行測試。

此外，形式檢查還能確保這些存儲器／MBIST 連接上沒有放置時序邏輯，這常常是一個設計要求。

JTAG 檢查

與 MBIST 檢查類似，設計人員可以在設計中添加 JTAG 電路，這常常也在 RTL 階段進行。JTAG 的潛在用途包括：創建對設計的測試訪問，啟動全掃描檢查，或控制 MBIST 電路。

JTAG 邏輯具有固定的規范和多種標準工作模式。連通性檢查可用來確保所有正確的設計元素（例如 MBIST控制器）都連接到預期的 JTAG 控制寄存器。

在某些 JTAG 模式下，邊界掃描寄存器形成一條長鏈。該鏈的長度由設計團隊確定。在連通性規范中將長度指定為延遲周期數，連通性檢查便可確保在特定模式下該鏈的長度是正確的。

結語

本文提供的信息當然是很粗略的。詳細記錄哪怕是最基本的 SoC 驗證流程，也很容易寫上數十頁甚至更多。然而，盡管簡短，但應該還是有充足的材料來供用戶開始制定流程，以實現更有效的連通性檢查。

編輯：hfy