A succinct and efficient implementation of a 232 BDD package - Details

Author：

Lv, Guanfeng (Lv, Guanfeng.) | Chen, Yao (Chen, Yao.) | Feng, Yachao (Feng, Yachao.) | Chen, Qingliang (Chen, Qingliang.) | Su, Kaile (Su, Kaile.)

Indexed by：

EI Scopus

Abstract：

As　a　data　structure　for　representing　and　manipulating　Boolean　functions,　BDDs　(Binary　Decision　Diagrams)　are　commonly　used　in　many　fields　such　as　model-checking,　system　verification　and　so　on.　For　saving　space　and　improving　operation　speed,　all　the　existing　packages　limit　the　number　of　variables　to　216.　However,　such　a　limitation　also　restrains　its　applicability.　In　this　paper,　we　present　TiniBDD,　an　efficient　implementation　of　a　232　BDD　package　incorporating　sub-allocation　of　memory　and　lightweight　Garbage　Collection　as　well　as　a　new　operator　named　as　Satisfiable　Assignment　Operator.　Compared　with　the　well-known　CUDD　which　is　one　of　the　best　216　BDD　packages　that　can　be　attained　publicly,　the　experiments　show　TiniBDD　has　comparable　performance.　©　2012　IEEE.

Keyword：

Binary decision diagrams Boolean functions Model checking

Author Community：

[ 1 ] [Lv, Guanfeng]School of Computer Science and Technology, Beijing University of Technology, Beijing, China
[ 2 ] [Chen, Yao]School of Computer Science and Technology, Beijing University of Technology, Beijing, China
[ 3 ] [Feng, Yachao]School of Computer Science and Technology, Beijing University of Technology, Beijing, China
[ 4 ] [Chen, Qingliang]Department of Computer Science, Jinan University, Guangzhou, China
[ 5 ] [Su, Kaile]School of Information Science and Technology, Peking University, Beijing, China