BDD實現(xiàn)分析及其流化擴展.pdf

1、自從1986年R.E.Bryany等人提出了二叉決策圖(Binary Decision Diagrams)的概念以來，由于其空間和時間上表示和處理布爾函數(shù)的高效性，BDD被廣泛應用于大型數(shù)字系統(tǒng)設計中的邏輯功能驗證、綜合以及模型檢測等方面且日益受到重視。然而，傳統(tǒng)的BDD運算的實現(xiàn)主要基于哈希表技術，所以在處理大規(guī)模BDD運算時經常會遇到內存溢出問題。為了解決該問題有人提出如高效利用內存、基于廣度優(yōu)先實現(xiàn)BDD運算等方法，但由于BDD規(guī)

2、模過大或BDD有些層節(jié)點過多，內存溢出問題還是會出現(xiàn)。Shin-ichi Minato等人提出了基于流的BDD運算模型，可以從根本上解決這個問題。其主要思想是把BDD轉化為流，以流的形式作為運算輸入，內存只用作運算緩存而不用存儲整個BDD。v本文首先討論了一個經典BDD包(BuDDy)的具體實現(xiàn)，該包基于哈希表技術采用深度優(yōu)先算法實現(xiàn)簡約有序二叉決策圖(ROBDD)的運算。哈希表技術用于保證ROBDD的正則性。通過把哈希表和BDD節(jié)點存

3、儲表整合到同一個大的數(shù)組，提高了內存的利用率。運算過程中用動態(tài)規(guī)劃避免了重復BDD節(jié)點間運算，且可以比較低耗的完成自動垃圾回收。由于這些技術的應用，BuDDy在進行BDD運算時比其它BDD實現(xiàn)包的效率高，但由于其基于哈希表技術所以會遇到內存溢出問題。為此，本文在BuDDy的基礎上實現(xiàn)基于流的BDD運算，將其作為一個新的運算功能擴展到BuDDy包中。在本文的最后部分給出一個用擴展后的BuDDy包解決大規(guī)模BDD運算的實例，分析了流運算模型