cudd.ps

主要进行大规模的电路综合

(diagrams,)g(the)448 3640 y(v)n(ariables)h(may)e(shift)h(in)f(the)g
(order)l(,)i(b)n(ut)f(the)o(y)f(retain)h(their)g(indices.)47
b(The)28 b(package)j(k)o(eeps)448 3752 y(track)d(of)e(the)h(v)n
(ariable)h(permutation)h(\(and)e(its)g(in)l(v)o(erse\).)40
b(The)26 b(application)j(is)e(not)g(af)n(fected)448 3865
y(by)d(v)n(ariable)h(reordering,)h(e)o(xcept)f(in)e(the)h(follo)n(wing)
h(cases.)585 4053 y Fn(\017)46 b Fp(If)17 b(the)i(application)i(uses)e
(generators)i(\()p Fo(Cudd)p 2104 4053 28 4 v 34 w(F)-10
b(or)m(eac)o(hCube)20 b Fp(and)e Fo(Cudd)p 2985 4053
V 34 w(F)-10 b(or)m(eac)o(hNode)676 4166 y Fp(\))27 b(and)h(reordering)
j(is)c(enabled,)k(then)d(it)f(must)h(tak)o(e)h(care)f(not)g(to)g(call)g
(an)o(y)g(operation)676 4279 y(that)g(may)g(create)i(ne)n(w)e(nodes)h
(\(and)g(hence)h(possibly)g(trigger)g(reordering\).)46
b(This)28 b(is)676 4392 y(because)g(the)f(cubes)h(\(i.e.,)e(paths\))i
(and)f(nodes)h(of)e(a)g(diagram)i(change)g(as)f(a)f(result)h(of)676
4505 y(reordering.)585 4692 y Fn(\017)46 b Fp(If)26 b(the)h
(application)j(uses)d Fo(Cudd)p 1712 4692 V 34 w(bddConstr)o(ain)j
Fp(and)d(reordering)i(tak)o(es)f(place,)h(then)676 4805
y(the)23 b(property)j(of)e Fo(Cudd)p 1440 4805 V 33 w(bddConstr)o(ain)j
Fp(of)c(being)i(an)e(image)h(restrictor)i(is)e(lost.)1920
5225 y(6)p eop
%%Page: 7 7
7 6 bop 589 573 a Fp(The)27 b(CUDD)f(package)j(relies)g(on)e(garbage)i
(collection)h(to)e(reclaim)g(the)g(memory)f(used)448
686 y(by)35 b(diagrams)i(that)e(are)h(no)f(longer)h(in)f(use.)64
b(The)34 b(scheme)i(emplo)o(yed)h(for)e(garbage)i(col-)448
799 y(lection)32 b(is)d(based)i(on)f(k)o(eeping)h(a)e(reference)j
(count)f(for)f(each)g(node.)48 b(The)29 b(references)k(that)448
912 y(are)26 b(counted)i(are)e(both)h(the)f(internal)h(references)i
(\(references)f(from)e(other)h(nodes\))g(and)f(e)o(x-)448
1024 y(ternal)37 b(references)h(\(typically)g(references)g(from)d(the)g
(calling)i(en)l(vironment\).)68 b(When)35 b(an)448 1137
y(application)25 b(creates)f(a)d(ne)n(w)g(BDD,)f(ADD,)f(or)j(ZDD,)d(it)
j(must)f(increase)j(its)e(reference)i(count)448 1250
y(e)o(xplicitly)-6 b(,)41 b(through)d(a)e(call)g(to)g
Fo(Cudd)p 1712 1250 28 4 v 33 w(Ref)p Fp(.)65 b(Similarly)-6
b(,)40 b(when)c(a)f(diagram)i(is)f(no)g(longer)448 1363
y(needed,)28 b(the)e(application)i(must)e(call)g Fo(Cudd)p
1877 1363 V 34 w(Recur)o(siveDer)m(ef)41 b Fp(\(for)26
b(BDDs)e(and)i(ADDs\))e(or)448 1476 y Fo(Cudd)p 649 1476
V 34 w(Recur)o(siveDer)m(efZdd)29 b Fp(\(for)24 b(ZDDs\))e(to)h
(\223rec)o(ycle\224)j(the)e(nodes)h(of)e(the)h(diagram.)589
1589 y(T)-6 b(erminal)37 b(nodes)h(carry)g(a)e(v)n(alue.)69
b(This)36 b(is)h(especially)i(important)g(for)d(ADDs.)67
b(By)448 1702 y(def)o(ault,)29 b(the)f(v)n(alue)f(is)g(a)f(double.)41
b(T)-7 b(o)25 b(change)k(to)d(something)j(dif)n(ferent)g(\(e.g.,)e(an)g
(inte)o(ger\),)448 1815 y(the)21 b(package)i(must)d(be)h(modi\002ed)g
(and)g(recompiled.)30 b(Support)21 b(for)g(this)g(process)i(is)d
(currently)448 1928 y(v)o(ery)k(rudimentary)-6 b(.)448
2174 y Fq(3.2.2)92 b(The)22 b(Manager)448 2348 y Fp(All)27
b(nodes)i(used)g(in)f(BDDs,)f(ADDs,)g(and)h(ZDDs)e(are)i(k)o(ept)g(in)g
(special)h(hash)g(tables)g(called)448 2461 y(the)36 b
Fo(unique)i(tables)p Fp(.)66 b(Speci\002cally)-6 b(,)40
b(BDDs)35 b(and)h(ADDs)e(share)j(the)f(same)f(unique)j(table,)448
2574 y(whereas)24 b(ZDDs)d(ha)n(v)o(e)j(their)f(o)n(wn)f(table.)30
b(As)22 b(the)h(name)f(implies,)i(the)f(main)g(purpose)h(of)f(the)448
2687 y(unique)i(table)e(is)g(to)f(guarantee)k(that)d(each)g(node)h(is)e
(unique;)j(that)e(is,)g(there)g(is)g(no)g(other)g(node)448
2800 y(labeled)h(by)e(the)h(same)f(v)n(ariable)i(and)e(with)g(the)g
(same)h(children.)30 b(This)22 b(uniqueness)j(property)448
2912 y(mak)o(es)34 b(decision)i(diagrams)f(canonical.)61
b(The)33 b(unique)i(tables)f(and)g(some)g(auxiliary)i(data)448
3025 y(structures)e(mak)o(e)d(up)g(the)g(DdManager)h(\(manager)h(for)e
(short\).)52 b(Though)32 b(the)f(application)448 3138
y(that)c(uses)h(only)f(the)g(e)o(xported)h(functions)h(needs)f(not)f
(be)f(concerned)j(with)e(most)f(details)i(of)448 3251
y(the)20 b(manager)l(,)h(it)e(has)h(to)f(deal)h(with)f(the)h(manager)g
(in)g(the)f(follo)n(wing)i(sense.)28 b(The)19 b(application)448
3364 y(must)28 b(initialize)h(the)f(manager)h(by)e(calling)i(an)e
(appropriate)k(function.)42 b(\(See)27 b(Section)h(3.3.\))448
3477 y(Subsequently)-6 b(,)25 b(it)c(must)h(pass)g(a)f(pointer)j(to)d
(the)h(manager)h(to)e(all)h(the)f(functions)j(that)f(operate)448
3590 y(on)h(decision)i(diagrams.)589 3703 y(W)l(ith)k(the)g(e)o
(xception)i(of)d(a)g(fe)n(w)g(statistical)j(counters,)h(there)d(are)g
(no)f(global)i(v)n(ariables)448 3816 y(in)f(the)g(CUDD)d(package.)50
b(Therefore,)32 b(it)e(is)f(quite)i(possible)h(to)d(ha)n(v)o(e)i
(multiple)g(managers)448 3929 y(simultaneously)h(acti)n(v)o(e)d(in)f
(the)g(same)g(application.)2140 3896 y Ff(1)2223 3929
y Fp(It)g(is)g(the)g(pointers)i(to)e(the)h(managers)448
4042 y(that)24 b(tell)g(the)g(functions)i(on)e(what)f(data)h(the)o(y)g
(should)i(operate.)448 4287 y Fq(3.2.3)92 b(Cache)448
4462 y Fp(Ef)n(\002cient)23 b(recursi)n(v)o(e)i(manipulation)h(of)e
(decision)h(diagrams)f(requires)i(the)d(use)h(of)f(a)f(table)i(to)448
4575 y(store)i(computed)g(results.)34 b(This)24 b(table)i(is)e(called)i
(here)g(the)e Fo(cac)o(he)i Fp(because)g(it)f(is)f(ef)n(fecti)n(v)o
(ely)448 4688 y(handled)g(lik)o(e)f(a)e(cache)i(of)f(v)n(ariable)i(b)n
(ut)e(limited)h(capacity)-6 b(.)30 b(The)22 b(CUDD)d(package)24
b(starts)f(by)p 448 4749 1196 4 v 550 4810 a Fe(1)583
4837 y Fd(The)18 b(global)h(statistical)e(counters)i(are)f(used)h
(locally;)g(hence)g(the)o(y)f(are)h(compatible)g(with)e(the)i(use)f(of)
g(multi-)448 4929 y(ple)h(managers.)1920 5225 y Fp(7)p
eop
%%Page: 8 8
8 7 bop 448 573 a Fp(def)o(ault)31 b(with)e(a)g(small)g(cache,)i(and)f
(increases)h(its)e(size)h(until)g(either)g(no)f(further)i(bene\002t)e
(is)448 686 y(achie)n(v)o(ed,)c(or)f(a)f(limit)g(size)h(is)f(reached.)
31 b(The)23 b(user)h(can)g(in\003uence)h(this)f(polic)o(y)g(by)g
(choosing)448 799 y(initial)h(and)f(limit)g(v)n(alues)g(for)g(the)g
(cache)h(size.)589 912 y(T)-7 b(oo)22 b(small)g(a)f(cache)i(will)e
(cause)i(frequent)h(o)o(v)o(erwriting)f(of)f(useful)h(results.)30
b(T)-7 b(oo)21 b(lar)n(ge)i(a)448 1024 y(cache)h(will)d(cause)j(o)o(v)o
(erhead,)g(because)g(the)e(whole)h(cache)g(is)f(scanned)i(e)n(v)o(ery)f
(time)f(garbage)448 1137 y(collection)27 b(tak)o(es)f(place.)32
b(The)24 b(optimal)h(parameters)i(depend)f(on)e(the)h(speci\002c)g
(application.)448 1250 y(The)e(def)o(ault)j(parameters)f(w)o(ork)f
(reasonably)i(well)e(for)f(a)g(lar)n(ge)i(spectrum)g(of)f
(applications.)589 1363 y(The)32 b(cache)h(of)f(the)h(CUDD)d(package)k
(is)e(used)h(by)f(most)g(recursi)n(v)o(e)i(functions)h(of)d(the)448
1476 y(package,)26 b(and)e(can)f(be)h(used)g(by)g(user)n(-supplied)k
(functions)e(as)d(well.)29 b(\(See)23 b(Section)h(4.4.\))448
1722 y Fh(3.3)99 b(Initializing)24 b(and)i(Shutting)g(Do)o(wn)f(a)g
(DdManager)448 1896 y Fp(T)-7 b(o)27 b(use)g(the)h(functions)i(in)d
(the)h(CUDD)d(package,)30 b(one)e(has)g(\002rst)f(to)g(initialize)j
(the)d(package)448 2009 y(itself)e(by)e(calling)j Fo(Cudd)p
1238 2009 28 4 v 33 w(Init)p Fp(.)k(This)23 b(function)j(tak)o(es)e
(four)g(parameters:)585 2177 y Fn(\017)46 b Fp(numV)-10
b(ars:)28 b(It)21 b(is)h(the)f(initial)i(number)f(of)g(v)n(ariables)h
(for)f(BDDs)e(and)i(ADDs.)k(If)21 b(the)h(to-)676 2290
y(tal)e(number)i(of)f(v)n(ariables)h(needed)h(by)d(the)h(application)j
(is)d(kno)n(wn,)g(then)g(it)g(is)f(slightly)676 2403
y(more)h(ef)n(\002cient)h(to)f(create)i(a)e(manager)i(with)e(that)h
(number)g(of)f(v)n(ariables.)30 b(If)22 b(the)f(num-)676
2516 y(ber)g(is)g(unkno)n(wn,)i(it)e(can)h(be)f(set)g(to)g(0,)h(or)f
(to)g(an)o(y)g(other)i(lo)n(wer)e(bound)h(on)g(the)f(number)676
2629 y(of)28 b(v)n(ariables.)47 b(Requesting)31 b(more)e(v)n(ariables)i
(than)f(are)f(actually)i(needed)f(is)f(not)g(in-)676
2742 y(correct,)24 b(b)n(ut)g(is)g(not)g(ef)n(\002cient.)585
2922 y Fn(\017)46 b Fp(numV)-10 b(arsZ:)27 b(It)h(is)f(the)h(initial)h
(number)f(of)g(v)n(ariables)i(for)d(ZDDs.)40 b(See)27
b(Sections)h(3.9)676 3035 y(and)c(3.11)f(for)h(a)f(discussion)k(of)c
(the)h(v)n(alue)g(of)g(this)g(ar)n(gument.)585 3215 y
Fn(\017)46 b Fp(numSlots:)c(Determines)31 b(the)f(initial)h(size)f(of)g
(each)h(subtable)h(of)d(the)h(unique)i(table.)676 3328
y(There)c(is)g(a)f(subtable)j(for)f(each)f(v)n(ariable.)44
b(The)28 b(size)g(of)g(each)h(subtable)h(is)e(dynami-)676
3440 y(cally)e(adjusted)i(to)e(re\003ect)g(the)g(number)h(of)f(nodes.)
37 b(It)25 b(is)h(normally)h(O.K.)d(to)i(use)g(the)676
3553 y(def)o(ault)f(v)n(alue)f(for)g(this)g(parameter)l(,)h(which)f(is)
g(CUDD)p 2448 3553 V 31 w(UNIQ)o(UE)p 2828 3553 V 31
w(SLO)l(TS.)585 3733 y Fn(\017)46 b Fp(cacheSize:)39
b(It)28 b(is)g(the)g(initial)h(size)g(\(number)g(of)f(entries\))h(of)f
(the)h(cache.)43 b(Its)28 b(def)o(ault)676 3846 y(v)n(alue)c(is)f(CUDD)
p 1240 3846 V 32 w(CA)l(CHE)p 1578 3846 V 31 w(SLO)l(TS.)585
4026 y Fn(\017)46 b Fp(maxMemory:)29 b(It)23 b(is)g(the)h(tar)n(get)g
(v)n(alue)g(for)f(the)h(maximum)f(memory)g(occupation)j(\(in)676
4139 y(bytes\).)k(The)23 b(package)i(uses)g(this)f(v)n(alue)g(to)f
(decide)i(tw)o(o)f(parameters.)785 4319 y Fq(\226)46
b Fp(the)29 b(maximum)f(size)i(to)e(which)i(the)f(cache)h(will)e(gro)n
(w)-6 b(,)30 b(re)o(gardless)g(of)f(the)g(hit)876 4432
y(rate)24 b(or)f(the)h(size)g(of)f(the)h(unique)h(table.)785
4571 y Fq(\226)46 b Fp(the)19 b(maximum)g(size)h(to)f(which)h(gro)n
(wth)f(of)g(the)h(unique)h(table)f(will)f(be)g(preferred)876
4683 y(to)k(garbage)i(collection.)676 4863 y(If)j(maxMemory)h(is)g(set)
g(to)f(0,)h(CUDD)e(tries)i(to)g(guess)g(a)f(good)i(v)n(alue)g(based)f
(on)g(the)676 4976 y(a)n(v)n(ailable)c(memory)-6 b(.)1920
5225 y(8)p eop
%%Page: 9 9
9 8 bop 448 573 a Fp(A)23 b(typical)i(call)f(to)f Fo(Cudd)p
1255 573 28 4 v 34 w(Init)j Fp(may)d(look)h(lik)o(e)g(this:)557
760 y Fg(manager)52 b(=)i(Cudd_Init\(0,0,)o(CUD)o(D_)o(UN)o(IQ)o(UE)o
(_SL)o(OT)o(S,)o(CU)o(DD)o(_CA)o(CH)o(E_)o(SL)o(OT)o(S,0)o(\);)448
948 y Fp(T)-7 b(o)34 b(reclaim)i(all)f(the)g(memory)g(associated)j
(with)d(a)f(manager)l(,)39 b(an)c(application)j(must)d(call)448
1061 y Fo(Cudd)p 649 1061 V 34 w(Quit)p Fp(.)29 b(This)23
b(is)g(normally)i(done)g(before)g(e)o(xiting.)448 1310
y Fh(3.4)99 b(Setting)26 b(P)o(arameters)448 1484 y Fp(The)i(package)j
(pro)o(vides)f(se)n(v)o(eral)g(functions)h(to)d(set)h(the)g(parameters)
h(that)f(control)i(v)n(arious)448 1597 y(functions.)g(F)o(or)22
b(instance,)j(the)e(package)i(has)f(an)f(automatic)h(w)o(ay)f(of)g
(determining)i(whether)448 1710 y(a)f(lar)n(ger)i(unique)f(table)g(w)o
(ould)g(mak)o(e)f(the)g(application)k(run)c(f)o(aster)-5
b(.)32 b(In)24 b(that)g(case,)h(the)f(pack-)448 1823
y(age)19 b(enters)h(a)e(\223f)o(ast)i(gro)n(wth\224)f(mode)g(in)g
(which)g(resizing)i(of)d(the)h(unique)h(subtables)i(is)c(f)o(a)n(v)n
(ored)448 1936 y(o)o(v)o(er)25 b(garbage)h(collection.)36
b(When)25 b(the)g(unique)h(table)g(reaches)g(a)f(gi)n(v)o(en)g(size,)h
(ho)n(we)n(v)o(er)l(,)f(the)448 2049 y(package)d(returns)e(to)g(the)f
(normal)h(\223slo)n(w)f(gro)n(wth\224)i(mode,)f(e)n(v)o(en)f(though)i
(the)e(conditions)k(that)448 2162 y(caused)k(the)f(transition)i(to)d(f)
o(ast)h(gro)n(wth)f(still)h(pre)n(v)n(ail.)35 b(The)25
b(limit)g(size)h(for)f(f)o(ast)h(gro)n(wth)g(can)448
2275 y(be)k(read)h(by)f Fo(Cudd)p 1070 2275 V 33 w(ReadLooseUpT)-8
b(o)31 b Fp(and)g(changed)h(by)e Fo(Cudd)p 2544 2275
V 33 w(SetLooseUpT)-8 b(o)p Fp(.)49 b(Similar)448 2388
y(pairs)25 b(of)e(functions)j(e)o(xist)e(for)g(se)n(v)o(eral)h(other)f
(parameters.)31 b(See)23 b(also)h(Section)h(4.8.)448
2637 y Fh(3.5)99 b(Constant)26 b(Functions)448 2811 y
Fp(The)18 b(CUDD)e(P)o(ackage)j(de\002nes)g(se)n(v)o(eral)h(constant)g
(functions.)30 b(These)18 b(functions)j(are)e(created)448
2924 y(when)24 b(the)g(manager)g(is)g(initialized,)i(and)e(are)g
(accessible)i(through)f(the)f(manager)h(itself.)448 3170
y Fq(3.5.1)92 b(One,)22 b(Logic)i(Zer)n(o,)g(and)e(Arithmetic)i(Zer)n
(o)448 3344 y Fp(The)36 b(constant)i(1)d(\(returned)j(by)e
Fo(Cudd)p 1738 3344 V 34 w(ReadOne)p Fp(\))g(is)g(common)g(to)g(BDDs,)h
(ADDs,)g(and)448 3457 y(ZDDs.)42 b(Ho)n(we)n(v)o(er)l(,)29
b(its)f(meaning)i(is)e(dif)n(ferent)i(for)f(ADDs)d(and)j(BDDs,)f(on)g
(the)h(one)g(hand,)448 3570 y(and)c(ZDDs,)f(on)g(the)h(other)h(hand.)33
b(The)25 b(diagram)g(consisting)j(of)d(the)g(constant)h(1)f(node)g
(only)448 3683 y(represents)33 b(the)d(constant)i(1)e(function)i(for)e
(ADDs)f(and)h(BDDs.)46 b(F)o(or)29 b(ZDDs,)h(its)g(meaning)448
3796 y(depends)i(on)d(the)g(number)i(of)e(v)n(ariables:)42
b(It)29 b(is)g(the)h(conjunction)j(of)c(the)g(complements)i(of)448
3909 y(all)j(v)n(ariables.)63 b(Con)l(v)o(ersely)-6 b(,)38
b(the)d(representation)j(of)c(the)g(constant)i(1)e(function)i(depends)
448 4022 y(on)28 b(the)g(number)h(of)e(v)n(ariables.)44
b(The)27 b(constant)j(1)d(function)j(of)e Fo(n)f Fp(v)n(ariables)j(is)d
(returned)j(by)448 4135 y Fo(Cudd)p 649 4135 V 34 w(ReadZddOne)p
Fp(.)589 4248 y(The)f(constant)j(0)c(is)h(common)h(to)f(ADDs)f(and)h
(ZDDs,)g(b)n(ut)h(not)f(to)g(BDDs.)44 b(The)29 b(BDD)448
4360 y(logic)21 b(0)f(is)g Fq(not)g Fp(associated)i(with)e(the)h
(constant)h(0)e(function:)29 b(It)20 b(is)g(obtained)i(by)f(complemen-)
448 4473 y(tation)26 b(\()p Fo(Cudd)p 910 4473 V 34 w(Not)r
Fp(\))e(of)h(the)g(constant)i(1.)32 b(\(It)24 b(is)h(also)g(returned)i
(by)e Fo(Cudd)p 2795 4473 V 33 w(ReadLo)o(gicZer)l(o)p
Fp(.\))448 4586 y(All)e(other)i(constants)h(are)e(speci\002c)g(to)f
(ADDs.)1920 5225 y(9)p eop
%%Page: 10 10
10 9 bop 448 573 a Fq(3.5.2)92 b(Pr)n(ede\002ned)22 b(Constants)448
747 y Fp(Besides)34 b(0)e(\(returned)j(by)d Fo(Cudd)p
1528 747 28 4 v 34 w(ReadZer)l(o)p Fp(\))h(and)g(1,)h(the)f(follo)n
(wing)h(constant)h(functions)448 860 y(are)24 b(created)h(at)f