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

由於SystemC排程器容許在排程上的不確定性，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.

並列關鍵字

SystemC ； formal verification ； scheduling alternatives ； partial order reduction ； symbolic simulation ； execution path merging

參考文獻

[3] P. Herber, J. Fellmuth, and S. Glesner, “Model Checking SystemC Designs Using Timed Automata,” In Proc. of CODES+ISSS, 2008

[4] J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “Uppaal — a Tool Suite for Automatic Verification of Real–Time Systems,” In Workshop on Verification and Control of Hybrid Systems, 1995.

[5] D. Grose, H. M. Le, and R. Drechsler, “Proving Transaction and System-level Properties of Untimed SystemC TLM Designs,” In Proc. of MEMOCODE, 2010.

[7] E. M. Clarke, D. Kroening, and F. Lerda, “A tool for checking ANSI-C programs,” In Proc. of TACAS, 2004.

[8] C.-N. Chou, Y.-S. Ho, C. Hsieh, and C.-Y. Huang, “Symbolic Model Checking on SystemC Desings,” In Proc. of DAC, 2012

國際替代計量

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

全文下載

主題瀏覽