解決SystemC正規驗證中之排程選擇數量爆炸之問題

Abstract

由於SystemC排程器容許在排程上的不確定性，SystemC的正規驗證被迫使處理在設計驗證上的可擴展性問題。這個可擴展性問題來自於探索所有可能的排程選擇，以確保能完整的捕捉到所有設計中可能的行為。為了能解決在探索排程選擇過程中造成的記憶體容量爆炸問題，我們在我們以符號模擬為基礎進行設計驗證的架構上，首先提出了符號偏序規約的技術來減少對等價的排程選擇的探索。除此之外，對於那些不能以偏序規約化簡的排程選擇，我們嘗試將這些排程選擇上的執行路徑(以及其相關的狀態)合併為較少的執行路徑以避免驗證引擎在執行路徑數量上的爆炸。實驗結果顯示，藉由結合這兩種技術，我們的驗證引擎在可擴展性上達到了巨大的提升。

Due to the non-determinism of the SystemC scheduler, formal SystemC verification must deal with a scalability issue. The issue stems from enumerating all scheduling alternatives such that all design behaviors can be captured assuredly. To conquer the scheduling alternative explosion problem under our symbolic simulation based verification scheme, we first adopt symbolic partial order reduction to reduce the equivalent scheduling alternatives for exploration. Moreover, for those scheduling alternatives that cannot be reduced by partial order reduction, we merge their execution paths (and also states) into fewer ones to prevent the number of paths from explosion. The experimental results show that we achieve a tremendous scalability improvement by combining these two techniques together.