序列特定目標識別和正規證明在系統層級設計中的錯誤路徑生成

Abstract

隨着系統晶片的複雜性呈指數級增長，且製作先進製程晶片的成本逐步提高，考量到上市時間和ECO所需的資金壓力，驗證程序已成為晶片設計流程中不可或缺的要素。在眾多主流的驗證方法中，基於模擬的約束隨機驗證方法通過對系統行為進行隨機模擬，以提升驗證的可靠性。這些方法以代碼覆蓋率、分支覆蓋率、狀態機覆蓋率以及功能覆蓋率等指標來衡量設計的可靠性。然而，這些指標僅關注於錯誤發生的特定狀態，而忽略了可能導致系統錯誤的訊號傳播，這最終構成了潛在風險。要識別潛在錯誤，需要對各種情況進行模擬。因此，在本研究中，我們將正規驗證方法和模擬驗證方法相結合，以找出可能導致錯誤的各種狀態。同時，也克服了正規驗證在處理大型設計方面的局限性。最終，我們在一個複雜設計中應用了這一方法，成功地發現了兩個潛在系統錯誤。這些錯誤無法單獨通過模擬驗證或正規驗證方法發現，但通過我們的方法得以揭示。

The verification process has become an essential component in the chip design workflow due to the exponential growth in the complexity of system chips and the gradual increase in manufacturing costs for advanced process chips. Simulationbased constrained random verification is a widely used technique in the field of verification. This method improves the dependability of the verification process by subjecting the system behavior to random simulations. These methodologies utilize many metrics, including code coverage, branch coverage, state machine coverage, and functional coverage[1][2], to assess the reliability of a design. Nevertheless, the aforementioned measures primarily concentrate on individual states where faults are observed, disregarding the transmission of signals that could potentially result in system mistakes, thereby presenting possible hazards. In order to detect hidden flaws, it is necessary for simulations to encompass arange of scenarios. Therefore, this study aims to integrate formal verification approaches with simulation-based verification methods in order to detect various states that have the potential to result in mistakes. In the final analysis, we implement this methodology to an intricate design and effectively discover two potential system flaws. These mistakes are not easily detected using standalone simulation-based or formal verification approaches, but our approach is able to uncover them.