設計芯片是一個復雜的過程。它從定義架構要求開始，然后是微架構開發，然后是 RTL 設計和功能驗證。然后綜合設計得到網表，交給后端團隊進行后端流程。在后端流程中，網表在各個階段經歷各種變化，無論是在識別錯誤??后對設計執行的工程變更單 （ECO），還是為時序收斂而修改單元。簡而言之，該設計在進入最終流片階段之前會進行多次更改。

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

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

圖 1一個典型的 Conformal LEC 流程包括一個設置模式和一個 LEC 模式。

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

黑盒規格

閱讀圖書館和設計

設計約束規范

建模指令規范

切換到 LEC 模式

LEC 模式包括：

映射過程

比較過程

一、黑匣子規格

在典型的設計中，會有模擬塊、存儲器和數字塊。內存和模擬塊由不同的團隊提供，在運行 LEC 時它們將被視為黑盒。如果設計中存在 IP，則 IP 驗證由 IP 提供商執行，用戶無需花費時間驗證 IP。因此，即使 IP 也可以作為黑盒包含在內。

可以使用命令指定黑盒，如下圖 2中的第 25 行所示。這必須在讀取設計文件/庫之前完成，以確保只讀取 I/O 端口而不是整個設計。這樣做會大大減少運行時間，并且在我們在大型設計上運行 LEC 時會有很大幫助。當一個模塊被指定為黑盒時，Conformal 工具將驗證連接——黑盒的輸入和輸出——但它不會驗證黑盒內部的邏輯。

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

2. 閱讀VHDL/Verilog 設計和庫

除了 Verilog 和 VHDL 支持讀取設計文件外，Conformal 工具還支持讀取 Verilog 標準仿真庫和 Liberty 格式庫。該信息通過使用如下圖 3中第 37 行和第 40 行所示的命令提供給工具。搜索路徑和文件列表也可以使用適當的命令輸入到工具中。

圖 3上面顯示的命令用于讀取設計文件。

讀入設計后，Conformal 中內置的硬件描述語言 （HDL） 規則檢查插件可用于檢查 lint 錯誤和警告。這些錯誤和警告可以根據嚴重程度進行報告，并且可以添加豁免。使用以下命令報告黃金和修訂設計中的錯誤和警告消息：

報告規則檢查 -design -error -warning -golden -verbose 》 rpt.rule.golden

報告規則檢查 -design -error -warning -revised -verbose 》 rpt.rule.revised

3.設計約束規范

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

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

添加引腳約束 0 scan_enable-revised

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

4.建模指令規范

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

設置展平模型-gated_clock

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

5.切換到LEC模式

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

設置系統模式 lec

6. 映射過程

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

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

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

7.比較過程

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

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

添加比較點-所有比較

圖 6所示的 LEC 日志摘要是非等效的黃金和修訂設計。

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

Deekshith Krishnegowda 是 Marvell Technology 圣克拉拉辦事處的 IC 設計工程師。