Improving the efficiency of BDD-based operators by means of partitioning

被引：12

作者：

Cabodi, G ^{[1
]}

Camurati, P ^{[1
]}

Quer, S ^{[1
]}

机构：

[1] Politecn Torino, Dipartimento Automat & Informat, I-10129 Turin, Italy

来源：

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS | 1999年 / 18卷 / 05期

关键词：

binary decision diagrams (BDD's); finite state machines (FSM's); reachability analysis partitioning;

D O I：

10.1109/43.759068

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Binary decision diagrams (BDD's) are a state-of-the-art core technique for the symbolic representation and manipulation of Boolean functions, relations and finite sets. Many computer-aided design (CAD) applications resort to them, but size and time efficiency restrict their applicability to medium-small designs. We concentrate on complex operators used in symbolic manipulation. We analyze and optimize their performance by means of new dynamic partitioning strategies. We propose a novel quick algorithm for the estimation of cofactor size, and a technique to choose splitting variables according to their discrimination power, so that their cofactors may be optimized by different variable orderings (tending to the more flexible FBDD's), Furthermore, we analyze time efficiency and the impact of hashing/caching on BDD-based operators, We finally include an experimental observation of memory usage and running time for operators applied in symbolic manipulation.

引用

页码：545 / 556

页数：12

共 17 条

[1] Some heuristics for generating tree-like FBDD types [J].

Bern, J ;

Meinel, C ;

Slobodova, A .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 1996, 15 (01) :127-130

[2]

BRYANT RE, 1986, IEEE T COMPUT, V35, P677, DOI 10.1109/TC.1986.1676819

[3]

BRYANT RE, 1992, COMPUT SURV, V24, P293, DOI 10.1145/136035.136043

[4] SYMBOLIC MODEL CHECKING FOR SEQUENTIAL-CIRCUIT VERIFICATION [J].

BURCH, JR ;

CLARKE, EM ;

LONG, DE ;

MCMILLAN, KL ;

DILL, DL .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 1994, 13 (04) :401-424

[5] Verification and synthesis of counters based on Symbolic Techniques [J].

Cabodi, G ;

Camurati, P ;

Lavagno, L ;

Quer, S .

EUROPEAN DESIGN & TEST CONFERENCE - ED&TC 97, PROCEEDINGS, 1997, :176-181

[6]

Cabodi G, 1998, SOFTWARE PRACT EXPER, V28, P99, DOI 10.1002/(SICI)1097-024X(199801)28:1<99::AID-SPE143>3.0.CO

[7]

2-Y

[8]

CABODI G, 1996, P IEEE EURO DAC 96, P170

[9]

ENGLERT KJ, 1995, THESIS U FREIBURG FR

[10]

JAIN J, 1992, P BROWN MIT VLSI C, P210

← 1 2 →