- 學位論文
閘級模擬中有效率尋找真實未知値之具支配性模版
An Efficient Method to Find Dominating Real X Patterns in Gate-Level Simulation
摘要
未初始化的暫存器或斷電的區塊可能使我們的設計存在未知值(Xs)。 由於閘級邏輯模擬中的X悲觀問題，這樣的Xs無法正確處理。 為了消除錯誤的X，目前的演算法重複地調用SAT求解器來檢查X是否為錯誤的。 SAT求解器嘗試找單一個解，即使輸入布爾函數相同，SAT求解器也將完全重新執行。 在本文中，提出了一種找到真實X的支配性模版的方法。利用二元決策圖，我們可以有效地找到一個很好的模版。 找到模版後，我們可以在用SAT求解器之前檢查模版。如果模式匹配成功，我們可以確認X是真實的，而不需要調用SAT求解器。實驗結果表明，該方法可以在短時間內找到足夠好的解決方案。
並列摘要
Unknown values(Xs) may exist in a design due to uninitialized registers or blocks that are powered down. Due to X-pessimism in gate-level logic simulation, such Xs cannot be handled correctly. To eliminate false X, current algorithm repeatedly calls the SAT solver to check if the X is false or not. SAT solvers try to find a single solution and even if the input Boolean function is the same, the SAT solver will be completely re-executed. In this paper, a method to find the dominating real X patterns is presented. Taking use of Binary Decision Diagrams (BDDs), we can find good patterns efficiently. After finding the patterns, we can check the patterns before calling the SAT solver. If a pattern match successfully, we can confirm X is real without calling the SAT solver. Experimental results show that the proposed method can find enough good patterns in a short time.