高機率高密度狀態追蹤

Abstract

有限狀態機(FSM)的狀態追蹤不論在硬體或軟體的驗證上都是一項有用的技術，但長久以來卻為因二元圖形表示法(BDD nodes representation)花費太多記憶體所困擾。高密度式狀態追蹤(High Density approach)雖然可以稍微的解決這個問題，但是對於設計較複雜的系統的驗證上還是有其極限。 在這篇論文中，我們提出一個高機率高密度式有限狀態機狀態追蹤(High Probability High Density approach)的方式，且使用引導追蹤(hints)來幫助追蹤。我們同時使用了高機率和高密度的引導方式企圖讓所花費的記憶體盡量減少。當在目標狀態(target state)在使用高密度方式可以被計算到但所花費的記憶體卻遠超過我們能接受時，我們只保留高機率的狀態。因此，針對較複雜的電路設計上我們的方式能夠確定所有高機率的狀態都會被計算到。我們將兩種高機率和高密度的方式合併成高機率高密度式(HPHD)狀態追蹤。我們的實驗和之前傳統的方式(BFS search)還有Ravi(High Density)的方式相比較來證明我們有效率的解法。

State traversal is a useful technique in hardware and software verification but suffers from state or BDD explosion problem. Although the High Density(HD) approach alleviates this problem, it has its potential limit in verifying complex systems. In this paper, we propose High Probability High Density(HPHD) approach using hints to guide the exploration of the state space. The hints are not only controlled by the density of states in terms of BDD as HD does, but also the probability values of target states. When the target states satisfy the density requirement but their BDD representation is still larger than the affordable memory space, only the states with high probability values will be explored. Thus, in the case it is impossible to travel all states for a complex system, this approach ensures that all states with high probability values are visited; that is, the states will the most possibility to be used in execution will be verified. We show how to combine the high density approach and guided search technique to yield a HPHD state traversal. Comparing our results with previous approaches, our results demonstrate the effectiveness of this new approach.