「三種高手技巧」– 防止 CDC 路徑上發生突波惡夢

形式驗證突波偵測的優點

我們解釋了各種類型 CDC 路徑中的突波問題。然後，我們會概述形式驗證型自動化突波檢測方法2。這種方法利用結構化 CDC 分析、表示式分析和形式驗證方法，來清除並證明設計中真正的突波。為了處理執行時間更長、更複雜的設計，我們將以前的方法分解為更靈活、階層架構化、多階段和多重處理的流程。我們將說明流程的各個階段，以及實現並行處理的方式。

透過階層 (hierarchical) 架構的多階段和多重處理，使用者能比以前更高效地執行邏輯閘層級 CDC 和突波分析。藉著將 RTL 指令和 waiver 轉換為邏輯閘層級的指令和豁免，已經在 RTL 層級執行的艱巨工作可以得到重複利用，而無需重複執行。

這種多階段、邏輯閘層級 CDC 和突波分析方法有許多優點：

高品質的結果 用於突波驗證的形式驗證型方法產生的假錯較少，結果的品質更高（數千條路徑只有幾個突波），從而顯著減少了除錯和分類的工作量。

易於除錯 此工具使用表示式分析和形式驗證方法，可以確定導致突波情境的確切路徑，並可以精確指出可能產生突波的收斂點。

能夠處理大型 SoC 可以使用階層架構方法 (hierarchical)，首先完成對 IP 區塊的 CDC 和突波分析。IP 區塊隨後將顯示為灰色框，以便在頂層進行分析。

快速改進 多階段邏輯閘層級 CDC 和突波分析過程支持增量式改進，大幅縮短周轉時間，並消除單一過程中的 故障。

多重處理 由於突波分析可以在多個伺服器上並行執行，因此可以更有效地使用伺服器和記憶體。