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

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

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

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