芯片設(shè)計(jì)之邏輯等價(jià)檢查 (LEC)

設(shè)計(jì)芯片是一個(gè)復(fù)雜的過程。它從定義架構(gòu)要求開始，然后是微架構(gòu)開發(fā)，然后是 RTL 設(shè)計(jì)和功能驗(yàn)證。然后綜合設(shè)計(jì)得到網(wǎng)表，交給后端團(tuán)隊(duì)進(jìn)行后端流程。在后端流程中，網(wǎng)表在各個(gè)階段經(jīng)歷各種變化，無論是在識(shí)別錯(cuò)誤??后對(duì)設(shè)計(jì)執(zhí)行的工程變更單 （ECO），還是為時(shí)序收斂而修改單元。簡(jiǎn)而言之，該設(shè)計(jì)在進(jìn)入最終流片階段之前會(huì)進(jìn)行多次更改。

為了在更改后驗(yàn)證設(shè)計(jì)，有必要通過提供測(cè)試用例來運(yùn)行仿真，但由于設(shè)計(jì)的復(fù)雜性（復(fù)雜的設(shè)計(jì)需要更多的運(yùn)行時(shí)間）以及設(shè)計(jì)更改的頻率，這通常是不可能的。在這種情況下，設(shè)計(jì)要經(jīng)過邏輯等效檢查 （LEC），其中工具通過注入隨機(jī)向量來驗(yàn)證設(shè)計(jì)。

業(yè)內(nèi)有許多工具可用于檢查邏輯等價(jià)性，但使用最廣泛的是Cadence的Conformal和 Synopsys 的Formality。除了 LEC，這些工具還可以用于執(zhí)行其他任務(wù)，例如 ECO。在本文中，我們將介紹 Conformal LEC 流程。

圖 1一個(gè)典型的 Conformal LEC 流程包括一個(gè)設(shè)置模式和一個(gè) LEC 模式。

一個(gè)典型的保形 LEC 平面運(yùn)行流程主要由一個(gè)設(shè)置階段和一個(gè) LEC 模式組成。設(shè)置模式包括以下步驟：

黑盒規(guī)格

閱讀圖書館和設(shè)計(jì)

設(shè)計(jì)約束規(guī)范

建模指令規(guī)范

切換到 LEC 模式

LEC 模式包括：

映射過程

比較過程

一、黑匣子規(guī)格

在典型的設(shè)計(jì)中，會(huì)有模擬塊、存儲(chǔ)器和數(shù)字塊。內(nèi)存和模擬塊由不同的團(tuán)隊(duì)提供，在運(yùn)行 LEC 時(shí)它們將被視為黑盒。如果設(shè)計(jì)中存在 IP，則 IP 驗(yàn)證由 IP 提供商執(zhí)行，用戶無需花費(fèi)時(shí)間驗(yàn)證 IP。因此，即使 IP 也可以作為黑盒包含在內(nèi)。

可以使用命令指定黑盒，如下圖 2中的第 25 行所示。這必須在讀取設(shè)計(jì)文件/庫(kù)之前完成，以確保只讀取 I/O 端口而不是整個(gè)設(shè)計(jì)。這樣做會(huì)大大減少運(yùn)行時(shí)間，并且在我們?cè)诖笮驮O(shè)計(jì)上運(yùn)行 LEC 時(shí)會(huì)有很大幫助。當(dāng)一個(gè)模塊被指定為黑盒時(shí)，Conformal 工具將驗(yàn)證連接——黑盒的輸入和輸出——但它不會(huì)驗(yàn)證黑盒內(nèi)部的邏輯。

圖 2可以使用此圖像中顯示的命令指定黑盒。

2. 閱讀VHDL/Verilog 設(shè)計(jì)和庫(kù)

除了 Verilog 和 VHDL 支持讀取設(shè)計(jì)文件外，Conformal 工具還支持讀取 Verilog 標(biāo)準(zhǔn)仿真庫(kù)和 Liberty 格式庫(kù)。該信息通過使用如下圖 3中第 37 行和第 40 行所示的命令提供給工具。搜索路徑和文件列表也可以使用適當(dāng)?shù)拿钶斎氲焦ぞ咧小?/p>

圖 3上面顯示的命令用于讀取設(shè)計(jì)文件。

讀入設(shè)計(jì)后，Conformal 中內(nèi)置的硬件描述語言 （HDL） 規(guī)則檢查插件可用于檢查 lint 錯(cuò)誤和警告。這些錯(cuò)誤和警告可以根據(jù)嚴(yán)重程度進(jìn)行報(bào)告，并且可以添加豁免。使用以下命令報(bào)告黃金和修訂設(shè)計(jì)中的錯(cuò)誤和警告消息：

報(bào)告規(guī)則檢查 -design -error -warning -golden -verbose 》 rpt.rule.golden

報(bào)告規(guī)則檢查 -design -error -warning -revised -verbose 》 rpt.rule.revised

3.設(shè)計(jì)約束規(guī)范

在設(shè)計(jì)中插入測(cè)試設(shè)計(jì) （DFT） 后，將添加某些端口/引腳用于調(diào)試目的。例如，scan_in、scan_out、scan_mode 和 scan_enable。在比較 RTL 與 DFT-RTL 設(shè)計(jì)時(shí)，由于這些額外的端口，設(shè)計(jì)將是非等效的。因此，有必要將設(shè)計(jì)置于黃金設(shè)計(jì)和修訂設(shè)計(jì)的通用功能模式中。這可以通過在設(shè)計(jì)中添加約束來實(shí)現(xiàn)。

例如，在下面的圖 4中，左側(cè)的觸發(fā)器是黃金設(shè)計(jì)中的常規(guī) D 觸發(fā)器，而右側(cè)的觸發(fā)器是掃描插入后修訂設(shè)計(jì)中的可掃描 D 觸發(fā)器。黃金設(shè)計(jì)中的 D 輸入是 D in的函數(shù)，而修訂設(shè)計(jì)中的 D 輸入是 D in、scan_in 和 scan_enable 的函數(shù)。因此，當(dāng)工具將向量傳遞給兩個(gè)觸發(fā)器時(shí)，它們將被標(biāo)記為不等價(jià)。但在功能模式下，scan_enable 將始終為零。因此，如果在 scan_enable 上添加約束以將其綁定到 1‘b0，則黃金設(shè)計(jì)和修訂設(shè)計(jì)在功能模式下將相等。

添加引腳約束 0 scan_enable-revised

圖 4這是掃描插入后黃金 DFF 與修訂后 DFF 的樣子。

4.建模指令規(guī)范

綜合后，綜合工具的網(wǎng)表輸出將進(jìn)行功率優(yōu)化。因此，黃金設(shè)計(jì)中的任何時(shí)鐘門控邏輯都將轉(zhuǎn)換為基于鎖存器的時(shí)鐘門控，如下面的圖 5所示。許多此類優(yōu)化將由不同的工具完成，有必要仔細(xì)審查它們并添加建模指令以匹配兩種設(shè)計(jì)。以下命令可用于為時(shí)鐘門控優(yōu)化添加建模指令：

設(shè)置展平模型-gated_clock

圖 5這是黃金 DFF 與修訂后 DFF 在功耗優(yōu)化后的樣子。

5.切換到LEC模式

添加所有設(shè)置約束和建模指令后，必須將工具切換到 LEC 模式以映射關(guān)鍵點(diǎn)和比較。這是通過使用以下命令完成的：

設(shè)置系統(tǒng)模式 lec

6. 映射過程

當(dāng)工具設(shè)置為 LEC 模式時(shí)，工具會(huì)自動(dòng)映射關(guān)鍵點(diǎn)，例如初級(jí)輸入 （PI）、初級(jí)輸出 （PO）、DFF、D 鎖存器、黑盒、Z 門和切割門。首先，該工具使用基于名稱的映射，然后是基于函數(shù)的映射。顧名思義，在基于名稱的映射中，工具映射基于黃金和修訂設(shè)計(jì)中的網(wǎng)絡(luò)/變量的名稱。在基于函數(shù)的映射中，該工具分析關(guān)鍵點(diǎn)的輸入邏輯錐并基于它進(jìn)行映射?；诿Q的映射比基于函數(shù)的映射需要更少的運(yùn)行時(shí)間，因此該工具會(huì)在切換到基于函數(shù)的映射之前嘗試使用基于名稱的映射來映射關(guān)鍵點(diǎn)。

必須映射所有關(guān)鍵點(diǎn)。但是第一次運(yùn)行 LEC 時(shí)，并不是所有的關(guān)鍵點(diǎn)都會(huì)被映射。這是因?yàn)?IC 設(shè)計(jì)過程中使用的不同工具進(jìn)行了優(yōu)化。例如，綜合工具根據(jù)設(shè)置將RTL中的寄存器/ dma_reg［0］［1］重命名為netlist中的/ dma_0_reg［1］?；诿Q的映射將無法匹配此關(guān)鍵點(diǎn)，而基于函數(shù)的映射可能會(huì)或可能無法匹配此關(guān)鍵點(diǎn)，這取決于邏輯錐的復(fù)雜性。在這些情況下，應(yīng)為工具提供重命名規(guī)則，以便映射這些關(guān)鍵點(diǎn)。以下重命名規(guī)則將解決上述未映射的關(guān)鍵點(diǎn)：

添加重命名規(guī)則 REG1 “%d_reg\［%d\］” “reg［@1］［@2］” -revised

7.比較過程

僅在映射的關(guān)鍵點(diǎn)上進(jìn)行比較。因此，如前所述，重要的是應(yīng)該映射所有關(guān)鍵點(diǎn)。該工具將嘗試通過將所有輸入組合傳遞給邏輯錐來證明等效性并檢查輸出行為。在比較過程之后，該工具會(huì)將關(guān)鍵點(diǎn)分類為等效點(diǎn)、反向等效點(diǎn)、非等效點(diǎn)和中止點(diǎn)。除等效關(guān)鍵點(diǎn)外的所有類別都應(yīng)調(diào)試。如果所有比較點(diǎn)都相同，那么我們可以得出結(jié)論，黃金和修改后的設(shè)計(jì)是匹配的。

在LEC模式下可以使用如下命令調(diào)用比較過程，比較后會(huì)顯示如圖6所示的信息：

添加比較點(diǎn)-所有比較

圖 6所示的 LEC 日志摘要是非等效的黃金和修訂設(shè)計(jì)。

如上所述，每次設(shè)計(jì)更改時(shí)運(yùn)行回歸和其他復(fù)雜模擬并不是驗(yàn)證設(shè)計(jì)的有效方式。在這種情況下使用 LEC 工具表明，可以用更少的運(yùn)行時(shí)間驗(yàn)證設(shè)計(jì)。按照上述步驟使用 Cadence Conformal 進(jìn)行 LEC 將簡(jiǎn)化整個(gè)過程并顯著減少調(diào)試時(shí)間。

Deekshith Krishnegowda 是 Marvell Technology 圣克拉拉辦事處的 IC 設(shè)計(jì)工程師。