作者：Mark Handover；Abdelouahab Ayari
簡(jiǎn)介

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

調(diào)試提出了另一個(gè)次要的但常常同樣具有挑戰(zhàn)性的問(wèn)題。原因是，雖然采用定向或約束隨機(jī)方法通過(guò)動(dòng)態(tài)測(cè)試檢查連通性肯定能發(fā)現(xiàn)一些連通性錯(cuò)誤，但問(wèn)題只會(huì)表現(xiàn)為被測(cè)模塊內(nèi)部的功能性問(wèn)題，而不一定能幫助查明問(wèn)題連接。使用斷言可以在源頭捕獲設(shè)計(jì)錯(cuò)誤，從而減輕調(diào)試問(wèn)題。但是，所需的檢查量仍然可能令人瞠目。

為應(yīng)對(duì)此類挑戰(zhàn)，形式驗(yàn)證為我們提供了一種快速、詳盡且支持高效調(diào)試的解決方案。傳統(tǒng)上，芯片級(jí)形式驗(yàn)證確實(shí)不可行。該方法通常以模塊級(jí)別為目標(biāo)，使?fàn)顟B(tài)空間的規(guī)模保持在適當(dāng)水平。但是，鑒于連通性檢查僅集中在布線上（與模塊級(jí)別的復(fù)雜度相比，布線一般是器件的簡(jiǎn)單部分），借助一些假設(shè)，狀態(tài)空間可以減小到可管理的規(guī)模。這種簡(jiǎn)化的性質(zhì)取決于所需檢查的類型。

本文首先會(huì)概述幾種類型的連通性檢查，然后詳細(xì)介紹一種新型半自動(dòng)驗(yàn)證流程（包括代碼）。已有一些 Mentor Graphics 使用該流程來(lái)簡(jiǎn)化連通性檢查。該流程基于一個(gè)腳本環(huán)境，圍繞該環(huán)境提供了充足的信息以方便用戶開(kāi)始實(shí)施新的驗(yàn)證方法。

點(diǎn)對(duì)點(diǎn)連通性檢查的類型

直接點(diǎn)對(duì)點(diǎn)檢查

連通性檢查的最簡(jiǎn)單形式是點(diǎn)對(duì)點(diǎn)檢查 —— 端口 A 是否連接到端口 B？這是就同一層次結(jié)構(gòu)而言的。

例如，如果一個(gè)設(shè)計(jì)有八個(gè)模塊，所有模塊都位于頂層，那么驗(yàn)證只需要檢查這八個(gè)模塊與頂層之間的連接。

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

跨層次結(jié)構(gòu)的直接點(diǎn)對(duì)點(diǎn)檢查

這在本質(zhì)上與簡(jiǎn)單檢查方法相似，不過(guò)檢查的是位于一個(gè)層次結(jié)構(gòu)中一個(gè)模塊上的端口是否在物理上正確連接到位于另一層次結(jié)構(gòu)中的一個(gè)模塊，或者位于信號(hào)源的單個(gè)端口是否連接到多個(gè)端點(diǎn)。

以對(duì)存儲(chǔ)器的寫(xiě)使能為例。它可能起源于單個(gè)頂層輸入管腳，但可以連接到跨許多不同層次位置的許多存儲(chǔ)器實(shí)例。

現(xiàn)在涉及層次結(jié)構(gòu)，因此無(wú)法將上方的模塊實(shí)例統(tǒng)一進(jìn)行黑盒化處理。黑盒化處理應(yīng)該在最高層級(jí)上執(zhí)行，但只能用于那些不在寫(xiě)使能路徑上或可能影響寫(xiě)使能連通性的邏輯路徑上的模塊。盡管更具挑戰(zhàn)性并需要一些設(shè)計(jì)知識(shí)，但這種更具選擇性的黑盒方法仍然可以顯著簡(jiǎn)化狀態(tài)空間。

其他類型的檢查

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

我們來(lái)看幾個(gè)例子。

條件點(diǎn)對(duì)點(diǎn)檢查

兩點(diǎn)之間的連接可能取決于系統(tǒng)中的其他行為或另一個(gè)信號(hào)的狀態(tài)。例如，當(dāng)驗(yàn)證管腳多路復(fù)用時(shí)，所選的 IO 路徑將取決于控制信號(hào)的值。令情況變得復(fù)雜的是，信號(hào)的目的地可能是一個(gè)相反值，執(zhí)行檢查時(shí)可能還需要考慮這一點(diǎn)。

有延遲的點(diǎn)對(duì)點(diǎn)

某些情況下需要點(diǎn)對(duì)點(diǎn)連接，但傳播可能要花費(fèi)若干周期，而不是立即發(fā)生。因此，這就需要完善點(diǎn)對(duì)點(diǎn)檢查。

無(wú)延遲的點(diǎn)對(duì)點(diǎn)

這類似于前面所述的簡(jiǎn)單點(diǎn)對(duì)點(diǎn)檢查，但有一個(gè)重大區(qū)別：用戶要求檢查明確驗(yàn)證不僅 A 連接到 B，而且路徑上沒(méi)有時(shí)序邏輯。

構(gòu)造檢查

鑒于需要?jiǎng)?chuàng)建大量檢查才能全面檢查器件連通性情況，用戶如何創(chuàng)建所需的斷言？

一種常見(jiàn)方法是使用格式特別編制的電子表格，其中詳細(xì)說(shuō)明了應(yīng)連接的各個(gè)點(diǎn)、涉及的路徑延遲、反轉(zhuǎn)、條件等。然后，工具或腳本解析電子表格并將其轉(zhuǎn)換為斷言語(yǔ)言，例如 SystemVerilog 斷言 (SVA) 或?qū)傩哉f(shuō)明語(yǔ)言 (PSL)。圖 1 顯示了一個(gè)帶有一些連通性信息的電子表格描述范例。

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

圖 1

我們來(lái)瀏覽一下該電子表格。我們指定了兩種檢查類型：“cond” 指條件連接，“connect” 指無(wú)條件的直接連接。這將允許我們?cè)趧?chuàng)建檢查器期間創(chuàng)建不同斷言類型。“輸入1” 和 “輸入2” 字段詳細(xì)列出了設(shè)計(jì)中要進(jìn)行連通性檢查的起點(diǎn)和終點(diǎn)。“條件” 列用于詳細(xì)說(shuō)明需要設(shè)置什么信號(hào)才允許點(diǎn)對(duì)點(diǎn)連接為真。“connect”檢查沒(méi)有條件，檢查將是直接、無(wú)條件的。最后，所有延遲字段都是 0，表示所有連接都沒(méi)有延遲。

一旦電子表格格式固定并填充內(nèi)容，便可使用適當(dāng)?shù)墓ぞ呋蚰_本來(lái)解析電子表格和創(chuàng)建斷言，而斷言將作為目標(biāo)送入形式化工具。一種方法是使用通用屬性模板，然后在單獨(dú)的檢查器描述中添加每個(gè)屬性實(shí)例的連通性信息。這樣就可以將其綁定（使用 SystemVerilog 的 bind 結(jié)構(gòu)體）到設(shè)計(jì)的頂層。

圖 2 顯示了兩個(gè)通用屬性模板。

圖 2

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

此模板文件可以包含許多獨(dú)特類型的連通性檢查，一旦明確便無(wú)需用戶編輯。該文件不包含任何設(shè)計(jì)信息，因而與項(xiàng)目無(wú)關(guān)，可以重復(fù)使用。

從電子表格自動(dòng)創(chuàng)建的源就是檢查器詳細(xì)信息，其中包含模板文件中不同檢查的實(shí)例，并添加了適當(dāng)?shù)男盘?hào)名稱。一個(gè)例子如圖 3 所示。

圖 3

其他注意事項(xiàng)

時(shí)鐘

設(shè)計(jì)不可避免地包含多個(gè)時(shí)鐘。通過(guò)形式驗(yàn)證，未定義的時(shí)鐘會(huì)產(chǎn)生與這些時(shí)鐘明確相關(guān)的設(shè)計(jì)邏輯和任何斷言的抽象。來(lái)自抽象域的信號(hào)成為形式驗(yàn)證控制點(diǎn)，這可能會(huì)導(dǎo)致意外激發(fā)。

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

連通性檢查常常不驗(yàn)證時(shí)鐘邏輯，因此定義時(shí)鐘貌似是不必要的任務(wù)。然而，為檢查連通性而創(chuàng)建的斷言會(huì)使用時(shí)鐘。

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

不過(guò)，鑒于難以識(shí)別路徑上的時(shí)序邏輯，這可能不是一個(gè)容易執(zhí)行的簡(jiǎn)化操作。

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

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

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

詳細(xì)信息：實(shí)施更高效流程的工具

某些 Mentor Graphics 客戶使用的方法（比如上面的例子）一般遵循一套通用步驟：首先，聲明檢查器的一個(gè)實(shí)例。然后，在適當(dāng)?shù)淖侄沃刑砑舆m當(dāng)?shù)男盘?hào)名稱。使用 Questa Formal，此方法適用于 Verilog、VHDL、混合語(yǔ)言設(shè)計(jì)和混合語(yǔ)言層次結(jié)構(gòu)。本文是我們努力讓其他工程團(tuán)隊(duì)能夠以最少的工作使用類似驗(yàn)證流程的一部分。在我們的方法中，我們定義了連通性規(guī)范電子表格的格式，并且編寫(xiě)了一個(gè)腳本來(lái)創(chuàng)建SVA 或 PSL 檢查器。我們還創(chuàng)建了一組屬性模板，以便支持多種類型的連通性檢查。該半自動(dòng)化流程的詳細(xì)信息（包括代碼）說(shuō)明如下。

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

利用形式驗(yàn)證檢查 SoC 連通性的正確性

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

■ 點(diǎn)對(duì)點(diǎn)，有或無(wú)延遲

■ 條件點(diǎn)對(duì)點(diǎn)，有或無(wú)延遲

■ 互斥信號(hào)

■ 接高電平的信號(hào)

■ 接低電平的信號(hào)

要?jiǎng)?chuàng)建這些類型的檢查器，用戶需要填充連通性規(guī)范文件。該文件的格式詳見(jiàn)圖 4。

連通性規(guī)范

圖 4

“檢查器關(guān)鍵字” 表示用戶希望推斷的檢查類型，“信號(hào) ...” 和 “條件信號(hào)” 條目是指向要檢查連通性的設(shè)計(jì)信號(hào)或端口的層次路徑。“延遲值” 是時(shí)序延遲周期數(shù)，須為整數(shù)。

例如，假設(shè)我們要檢查信號(hào) top.en 到 top.u1.u2.enable 的連通性，并且該路徑上應(yīng)有兩個(gè)周期的時(shí)序延遲。

圖 5 顯示了規(guī)范文件中該條目的樣子。請(qǐng)注意，對(duì)于互斥檢查器，雖然表中顯示了四個(gè)連接，但實(shí)際上可以指定任意數(shù)量的連接。

圖 5

除連通性信息外，規(guī)范文件還應(yīng)包括被測(cè)設(shè)計(jì)的名稱、時(shí)鐘的名稱以及檢查器將使用的復(fù)位。無(wú)論高電平有效還是低電平有效，都需要提供復(fù)位感測(cè)。這些信息應(yīng)按照如下格式指定：

■ Design

■ Clock <檢查器時(shí)鐘名稱>

■ Reset <檢查器復(fù)位名稱>

■ Reset_sense <低或高>

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

圖 6

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

該腳本可以接受多個(gè)參數(shù)，如圖 7 所示。

圖 7

默認(rèn)情況下，預(yù)期輸入格式為 TSV，檢查器輸出文件（名為 “checkers.sv”）將采用 SVA 格式。不過(guò)，用戶可以通過(guò)指定適當(dāng)?shù)倪x項(xiàng)來(lái)更改默認(rèn)行為。

腳本會(huì)自動(dòng)創(chuàng)建輸出連通性規(guī)范文件。它是 TSV 或 CSV 規(guī)范輸入的副本，但每個(gè)條目都包括所創(chuàng)建檢查器的名稱。該文件的默認(rèn)名稱為 checker_conn_spec，可使用 -s 開(kāi)關(guān)予以覆蓋；擴(kuò)展名為 .tsv 或 .csv，具體取決于輸入文件的格式。

輸出文件 checkers.sv 包含用于構(gòu)建檢查器的所有必要信息。為了簡(jiǎn)化使用，先前說(shuō)明的 “屬性模板” 已經(jīng)固定，并由腳本自動(dòng)創(chuàng)建。檢查器模板本身、檢查器實(shí)例化和綁定信息都包含在一個(gè)檢查器文件中。圖 8（注意下一頁(yè)仍有代碼）顯示了 SVA 風(fēng)格 checkers.sv 文件輸出的例子。

圖 8

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

該 makefile 名為 Makefile _ ConnCheck。它有三個(gè)條目：

■ compile _ checkers：編譯 SVA 或 PSL

■ compile _ formal _ model：運(yùn)行 CSL 流程以構(gòu)建形式模型

■ run _ formal：運(yùn)行 Questa Formal “證明” 流程

還有一個(gè) run_all 條目，它允許依次執(zhí)行所有三個(gè)步驟。為了運(yùn)行 makefile 中的所有步驟，用戶需要執(zhí)行：

make –f Makefile _ ConnCheck run _ all

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

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

例如，makefile 沒(méi)有引用形式驗(yàn)證的控制文件（用于定義時(shí)鐘、設(shè)置約束等），因此可能需要?jiǎng)?chuàng)建和指定該文件。

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

該腳本可以接受多個(gè)參數(shù)，如圖 9 所示。

圖 9

默認(rèn)輸入和輸出文件名為：

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

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

■ 證明報(bào)告文件名：results/prove/0in _ prove.rpt

所有這些默認(rèn)值都可以使用適當(dāng)?shù)拈_(kāi)關(guān)予以覆蓋。

在 “證明” 形式運(yùn)行之后，生成的輸出文件會(huì)詳細(xì)說(shuō)明每個(gè)連通性規(guī)范條目以及檢查器名稱和狀態(tài)，如圖 10

所示。

圖 10

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

圖 11

圖 12

其他應(yīng)用

連通性檢查在許多應(yīng)用中都很有價(jià)值。下面介紹幾個(gè)例子。

焊盤環(huán)檢查

復(fù)雜器件具有多種配置，SoC 中的 IO 不可避免地會(huì)涉及復(fù)雜的多路復(fù)用焊盤。必須驗(yàn)證所有配置下的焊盤環(huán)，檢查每種模式下是否都存在正確連接。利用形式技術(shù)檢查這種連通性會(huì)窮盡所有可能性，發(fā)現(xiàn)極端情況并帶來(lái)自動(dòng)化功能，而仿真技術(shù)常常無(wú)法做到這一點(diǎn)。

存儲(chǔ)器 BIST 檢查

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

來(lái)自 BIST 控制器的控制信號(hào)連接到各種存儲(chǔ)器或存儲(chǔ)器控制器，這些連接可以是共用的。例如，來(lái)自 BIST控制器的 write _ enable 可以連接到許多存儲(chǔ)器上的 write _ enable 管腳。

形式連通性檢查是一種有效替代方法，用戶無(wú)需編寫(xiě)動(dòng)態(tài)測(cè)試來(lái)檢查存儲(chǔ)器 BIST 連接并在每次更改 RTL時(shí)重新運(yùn)行測(cè)試。

此外，形式檢查還能確保這些存儲(chǔ)器／MBIST 連接上沒(méi)有放置時(shí)序邏輯，這常常是一個(gè)設(shè)計(jì)要求。

JTAG 檢查

與 MBIST 檢查類似，設(shè)計(jì)人員可以在設(shè)計(jì)中添加 JTAG 電路，這常常也在 RTL 階段進(jìn)行。JTAG 的潛在用途包括：創(chuàng)建對(duì)設(shè)計(jì)的測(cè)試訪問(wèn)，啟動(dòng)全掃描檢查，或控制 MBIST 電路。

JTAG 邏輯具有固定的規(guī)范和多種標(biāo)準(zhǔn)工作模式。連通性檢查可用來(lái)確保所有正確的設(shè)計(jì)元素（例如 MBIST控制器）都連接到預(yù)期的 JTAG 控制寄存器。

在某些 JTAG 模式下，邊界掃描寄存器形成一條長(zhǎng)鏈。該鏈的長(zhǎng)度由設(shè)計(jì)團(tuán)隊(duì)確定。在連通性規(guī)范中將長(zhǎng)度指定為延遲周期數(shù)，連通性檢查便可確保在特定模式下該鏈的長(zhǎng)度是正確的。

結(jié)語(yǔ)

本文提供的信息當(dāng)然是很粗略的。詳細(xì)記錄哪怕是最基本的 SoC 驗(yàn)證流程，也很容易寫(xiě)上數(shù)十頁(yè)甚至更多。然而，盡管簡(jiǎn)短，但應(yīng)該還是有充足的材料來(lái)供用戶開(kāi)始制定流程，以實(shí)現(xiàn)更有效的連通性檢查。

編輯：hfy