cudd.ps

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

(initialization)j(time.)562 1048 y(1.)46 b(PlusIn\002nity)26
b(and)g(MinusIn\002nity:)34 b(On)25 b(computers)i(implementing)g(the)e
(IEEE)e(stan-)676 1161 y(dard)39 b(754)g(for)f(\003oating-point)k
(arithmetic,)h(these)d(tw)o(o)e(constants)j(are)d(set)h(to)f(the)676
1273 y(signed)19 b(in\002nities.)29 b(On)17 b(the)h(DEC)e(Alphas,)k
(the)e(option)i Fg(-ieee_with_no_i)o(ne)o(xa)o(ct)676
1386 y Fp(or)33 b Fg(-ieee_with_inexa)o(ct)26 b Fp(must)34
b(be)g(passed)h(to)f(the)g(DEC)e(compiler)j(to)f(get)676
1499 y(support)26 b(of)e(the)h(IEEE)d(standard.)34 b(\(The)24
b(compiler)i(still)f(produces)h(a)e(w)o(arning,)i(b)n(ut)f(it)676
1612 y(can)30 b(be)h(ignored.\))52 b(Compiling)32 b(with)e(those)i
(options)g(may)e(cause)i(substantial)i(per)n(-)676 1725
y(formance)39 b(de)o(gradation)j(on)c(the)g(Ev)n(olution)j(IV)c(CPUs.)
71 b(\(Especially)41 b(if)d(the)g(ap-)676 1838 y(plication)d(does)f
(use)f(the)g(in\002nities.\))58 b(The)33 b(problem)h(is)e(reportedly)k
(solv)o(ed)e(in)f(the)676 1951 y(Ev)n(olution)h(V)d(CPUs.)55
b(If)32 b Fg(gcc)e Fp(is)j(used)g(to)f(compile)i(CUDD)c(on)j(the)g
(Alphas,)i(the)676 2064 y(symbol)26 b Fg(HAVE)p 1193
2064 V 31 w(IEEE)p 1444 2064 V 31 w(754)d Fp(must)j(be)f(unde\002ned.)
37 b(\(See)25 b(the)h(Mak)o(e\002le)g(for)f(the)h(de-)676
2177 y(tails.\))39 b(The)26 b(v)n(alues)i(of)e(these)i(constants)h(are)
e(returned)i(by)d Fo(Cudd)p 2802 2177 V 34 w(ReadPlusIn\002nity)676
2290 y Fp(and)e Fo(Cudd)p 1031 2290 V 33 w(ReadMinusIn\002nity)p
Fp(.)562 2477 y(2.)46 b(Epsilon:)40 b(This)28 b(constant,)j(initially)g
(set)d(to)h(10)2188 2444 y Fc(\000)p Ff(12)2311 2477
y Fp(,)f(is)g(used)i(in)e(comparing)i(\003oating)676
2590 y(point)d(v)n(alues)g(for)f(equality)-6 b(.)39 b(Its)26
b(v)n(alue)h(is)f(returned)j(by)d Fo(Cudd)p 2688 2590
V 34 w(ReadEpsilon)p Fp(,)i(and)f(it)676 2703 y(can)h(be)g(modi\002ed)h
(by)g(calling)g Fo(Cudd)p 1887 2703 V 34 w(SetEpsilon)p
Fp(.)45 b(Unlik)o(e)29 b(the)g(other)g(constants,)j(it)676
2816 y(does)24 b(not)g(correspond)i(to)e(a)f(node.)448
3062 y Fq(3.5.3)92 b(Backgr)n(ound)448 3236 y Fp(The)22
b(background)k(v)n(alue)e(is)e(a)g(constant)j(typically)g(used)e(to)g
(represent)h(non-e)o(xisting)i(arcs)d(in)448 3349 y(graphs.)31
b(Consider)26 b(a)d(shortest)j(path)e(problem.)31 b(T)-7
b(w)o(o)22 b(nodes)j(that)g(are)f(not)g(connected)i(by)e(an)448
3462 y(arc)31 b(can)f(be)g(re)o(garded)i(as)e(being)h(joined)h(by)e(an)
g(arc)g(of)g(in\002nite)h(length.)50 b(In)30 b(shortest)j(path)448
3575 y(problems,)27 b(it)d(is)g(therefore)j(con)l(v)o(enient)h(to)d
(set)g(the)g(background)j(v)n(alue)d(to)g(PlusIn\002nity.)33
b(In)448 3688 y(netw)o(ork)26 b(\003o)n(w)e(problems,)i(on)f(the)g
(other)h(hand,)g(tw)o(o)e(nodes)i(not)g(connected)h(by)e(an)g(arc)g
(can)448 3801 y(be)j(re)o(garded)h(as)f(joined)h(by)f(an)g(arc)g(of)f
(0)h(capacity)-6 b(.)43 b(F)o(or)27 b(these)i(problems,)h(therefore,)h
(it)c(is)448 3914 y(more)i(con)l(v)o(enient)j(to)c(set)h(the)g
(background)j(v)n(alue)d(to)g(0.)43 b(In)29 b(general,)i(when)e
(representing)448 4027 y(sparse)c(matrices,)g(the)e(background)k(v)n
(alue)e(is)e(the)h(v)n(alue)g(that)g(is)g(assumed)h(implicitly)-6
b(.)589 4139 y(At)18 b(initialization,)k(the)d(background)i(v)n(alue)e
(is)f(set)g(to)g(0.)27 b(It)18 b(can)g(be)g(read)h(with)f
Fo(Cudd)p 3237 4139 V 34 w(ReadBac)n(kgr)l(ound)p Fp(,)448
4252 y(and)k(modi\002ed)f(with)f Fo(Cudd)p 1325 4252
V 34 w(SetBac)n(kgr)l(ound)p Fp(.)31 b(The)21 b(background)j(v)n(alue)d
(af)n(fects)h(procedures)448 4365 y(that)34 b(read)f(sparse)i
(matrices/graphs)h(\()p Fo(Cudd)p 1903 4365 V 34 w(addRead)h
Fp(and)c Fo(Cudd)p 2654 4365 V 34 w(addHarwell)p Fp(\),)k(proce-)448
4478 y(dures)31 b(that)f(print)g(out)f(sum-of-product)34
b(e)o(xpressions)e(for)d(ADDs)f(\()p Fo(Cudd)p 2855 4478
V 34 w(PrintMinterm)p Fp(\),)448 4591 y(generators)43
b(of)d(cubes)h(\()p Fo(Cudd)p 1458 4591 V 34 w(F)-10
b(or)m(eac)o(hCube)p Fp(\),)46 b(and)40 b(procedures)j(that)e(count)g
(minterms)448 4704 y(\()p Fo(Cudd)p 679 4704 V 34 w(CountMinterm)p
Fp(\).)1897 5225 y(10)p eop
%%Page: 11 11
11 10 bop 448 573 a Fq(3.5.4)92 b(New)22 b(Constants)448
747 y Fp(Ne)n(w)d(constant)k(can)d(be)h(created)h(by)e(calling)i
Fo(Cudd)p 2071 747 28 4 v 34 w(addConst)p Fp(.)29 b(This)21
b(function)h(will)e(retrie)n(v)o(e)448 860 y(the)31 b(ADD)e(for)i(the)g
(desired)h(constant,)i(if)d(it)f(already)i(e)o(xist,)h(or)e(it)f(will)g
(create)i(a)e(ne)n(w)g(one.)448 973 y(Ob)o(viously)-6
b(,)25 b(ne)n(w)e(constants)j(should)f(only)g(be)e(used)i(when)e
(manipulating)k(ADDs.)448 1220 y Fh(3.6)99 b(Cr)n(eating)26
b(V)-9 b(ariables)448 1394 y Fp(Decision)28 b(diagrams)g(are)e
(typically)j(created)f(by)e(combining)i(simpler)g(decision)g(diagrams.)
448 1507 y(The)22 b(simplest)h(decision)h(diagrams,)g(of)e(course,)h
(cannot)h(be)e(created)h(in)f(that)h(w)o(ay)-6 b(.)28
b(Constant)448 1620 y(functions)e(ha)n(v)o(e)e(been)g(discussed)h(in)e
(Section)h(3.5.)29 b(In)23 b(this)g(section)i(we)d(discuss)j(the)f
(simple)448 1733 y(v)n(ariable)i(functions,)f(also)g(kno)n(wn)e(as)h
Fo(pr)l(ojection)i(functions)p Fp(.)448 1976 y Fq(3.6.1)92
b(New)22 b(BDD)g(and)g(ADD)g(V)-8 b(ariables)448 2150
y Fp(The)27 b(projection)j(functions)g(are)e(distinct)h(for)f(BDDs)d
(and)j(ADDs.)39 b(A)26 b(projection)k(function)448 2263
y(for)24 b(BDDs)d(consists)k(of)e(an)h(internal)h(node)f(with)f(both)h
(outgoing)h(arcs)f(pointing)h(to)e(the)h(con-)448 2376
y(stant)h(1.)j(The)23 b Fo(else)h Fp(arc)g(is)f(complemented.)589
2489 y(An)e(ADD)e(projection)k(function,)h(on)d(the)g(other)h(hand,)g
(has)f(the)g Fo(else)h Fp(pointer)g(directed)h(to)448
2602 y(the)35 b(arithmetic)h(zero)f(function.)64 b(One)34
b(should)i(ne)n(v)o(er)f(mix)f(the)h(tw)o(o)f(types)h(of)f(v)n
(ariables.)448 2715 y(BDD)k(v)n(ariables)k(should)g(be)e(used)h(when)f
(manipulating)j(BDDs,)f(and)e(ADD)e(v)n(ariables)448
2828 y(should)c(be)e(used)h(when)f(manipulating)j(ADDs.)53
b(Three)33 b(functions)h(are)f(pro)o(vided)h(to)e(cre-)448
2941 y(ate)24 b(BDD)e(v)n(ariables:)585 3115 y Fn(\017)46
b Fo(Cudd)p 877 3115 V 33 w(bddIthV)-10 b(ar)r Fp(:)29
b(Returns)19 b(the)f(projection)j(function)g(with)d(inde)o(x)g
Fo(i)p Fp(.)27 b(If)18 b(the)g(function)676 3228 y(does)24
b(not)g(e)o(xist,)g(it)f(is)g(created.)585 3411 y Fn(\017)46
b Fo(Cudd)p 877 3411 V 33 w(bddNe)o(wV)-10 b(ar)r Fp(:)49
b(Returns)35 b(a)d(ne)n(w)h(projection)j(function,)i(whose)c(inde)o(x)g
(is)f(the)676 3524 y(lar)n(gest)25 b(inde)o(x)f(in)g(use)g(at)f(the)h
(time)f(of)h(the)g(call,)f(plus)i(1.)585 3706 y Fn(\017)46
b Fo(Cudd)p 877 3706 V 33 w(bddNe)o(wV)-10 b(arAtLe)o(vel)p
Fp(:)51 b(Similar)34 b(to)f Fo(Cudd)p 2284 3706 V 34
w(bddNe)o(wV)-10 b(ar)p Fp(.)60 b(In)34 b(addition)i(it)d(al-)676
3819 y(lo)n(ws)27 b(to)h(specify)i(the)e(position)i(in)e(the)g(v)n
(ariable)h(order)g(at)f(which)g(the)g(ne)n(w)g(v)n(ariable)676
3932 y(should)g(be)e(inserted.)40 b(By)25 b(contrast,)k
Fo(Cudd)p 2072 3932 V 34 w(bddNe)o(wV)-10 b(ar)29 b Fp(adds)e(the)f(ne)
n(w)g(v)n(ariable)i(at)676 4045 y(the)23 b(end)h(of)g(the)g(order)-5
b(.)448 4220 y(The)34 b(analogous)i(functions)g(for)e(ADDs)f(are)g
Fo(Cudd)p 2144 4220 V 34 w(addIthV)-10 b(ar)p Fp(,)38
b Fo(Cudd)p 2796 4220 V 34 w(addNe)o(wV)-10 b(ar)p Fp(,)36
b(and)448 4333 y Fo(Cudd)p 649 4333 V 34 w(addNe)o(wV)-10
b(arAtLe)o(vel)p Fp(.)448 4576 y Fq(3.6.2)92 b(New)22
b(ZDD)g(V)-8 b(ariables)448 4751 y Fp(Unlik)o(e)33 b(the)f(projection)i
(functions)g(of)e(BDDs)e(and)i(ADDs,)g(the)g(projection)i(functions)g
(of)448 4863 y(ZDDs)22 b(ha)n(v)o(e)i(diagrams)h(with)e
Fo(n)12 b Fl(+)g Fp(1)24 b(nodes,)g(where)g Fo(n)f Fp(is)g(the)h
(number)g(of)f(v)n(ariables.)31 b(There-)448 4976 y(fore)f(the)f(ZDDs)e
(of)h(the)h(projection)j(functions)f(change)g(when)d(ne)n(w)h(v)n
(ariables)h(are)f(added.)1897 5225 y(11)p eop
%%Page: 12 12
12 11 bop 448 573 a Fp(This)21 b(will)g(be)h(discussed)i(in)d(Section)h
(3.9.)28 b(Here)21 b(we)g(assume)h(that)g(the)g(number)g(of)f(v)n
(ariables)448 686 y(is)j(\002x)o(ed.)k(The)23 b(ZDD)f(of)h(the)h
Fo(i)p Fp(-th)g(projection)i(function)g(is)d(returned)j(by)e
Fo(Cudd)p 2959 686 28 4 v 33 w(zddIthV)-10 b(ar)p Fp(.)448
935 y Fh(3.7)99 b(Basic)25 b(BDD)h(Manipulation)448 1109
y Fp(Common)34 b(manipulations)j(of)d(BDDs)e(can)i(be)g(accomplished)j
(by)d(calling)h Fo(Cudd)p 3153 1109 V 34 w(bddIte)p Fp(.)448
1222 y(This)c(function)h(tak)o(es)g(three)f(BDDs,)45
b Fo(f)13 b Fp(,)31 b Fo(g)p Fp(,)g(and)g Fo(h)p Fp(,)h(as)e(ar)n
(guments)j(and)e(computes)46 b Fo(f)28 b Fn(\001)16 b
Fo(g)f Fl(+)462 1335 y Fo(f)500 1302 y Fc(0)536 1335
y Fn(\001)f Fo(h)p Fp(.)36 b(Lik)o(e)26 b(all)g(the)g(functions)i(that)
f(create)g(ne)n(w)e(BDDs)g(or)h(ADDs,)f Fo(Cudd)p 2899
1335 V 33 w(bddIte)j Fp(returns)448 1448 y(a)f(result)i(that)f(must)f
(be)h(e)o(xplicitly)i(referenced)g(by)d(the)h(caller)-5
b(.)42 b Fo(Cudd)p 2718 1448 V 33 w(bddIte)29 b Fp(can)f(be)f(used)448
1561 y(to)c(implement)i(all)e(tw)o(o-ar)n(gument)i(boolean)h
(functions.)31 b(Ho)n(we)n(v)o(er)l(,)22 b(the)i(package)h(also)f(pro-)
448 1674 y(vides)g Fo(Cudd)p 863 1674 V 33 w(bddAnd)i
Fp(as)c(well)g(as)g(the)h(other)g(tw)o(o-operand)i(boolean)f
(functions,)h(which)d(are)448 1787 y(slightly)32 b(more)f(ef)n
(\002cient)f(when)h(a)e(tw)o(o-operand)k(function)f(is)e(called)i(for)
-5 b(.)48 b(The)30 b(follo)n(wing)448 1900 y(fragment)25
b(of)f(code)g(illustrates)i(ho)n(w)d(to)h(b)n(uild)h(the)e(BDD)f(for)i
(the)g(function)39 b Fo(f)34 b Fl(=)20 b Fo(x)3087 1867
y Fc(0)3087 1926 y Ff(0)3124 1900 y Fo(x)3164 1867 y
Fc(0)3164 1926 y Ff(1)3202 1900 y Fo(x)3242 1867 y Fc(0)3242
1926 y Ff(2)3280 1900 y Fo(x)3320 1867 y Fc(0)3320 1926
y Ff(3)3357 1900 y Fp(.)885 2087 y Fg(DdManager)50 b(*manager;)885
2200 y(DdNode)h(*f,)j(*var,)e(*tmp;)885 2313 y(int)h(i;)885
2539 y(...)885 2765 y(f)h(=)g(Cudd_ReadOne\(m)o(ana)o(ge)o(r\))o(;)885
2878 y(Cudd_Ref\(f\);)885 2990 y(for)f(\(i)g(=)i(3;)e(i)h(>=)g(0;)g
(i--\))e({)1103 3103 y(var)h(=)h(Cudd_bddIthVar\()o(ma)o(na)o(ger)o(,i)
o(\);)1103 3216 y(tmp)f(=)h(Cudd_bddAnd\(man)o(ag)o(er)o(,Cu)o(dd)o(_N)
o(ot)o(\(v)o(ar\))o(,f)o(\);)1103 3329 y(Cudd_Ref\(tmp\);)1103
3442 y(Cudd_Recursive)o(Der)o(ef)o(\(m)o(an)o(ag)o(er,)o(f\))o(;)1103
3555 y(f)g(=)g(tmp;)885 3668 y(})448 3856 y Fp(This)24
b(e)o(xample)g(illustrates)i(the)e(follo)n(wing)h(points:)585
4043 y Fn(\017)46 b Fp(Intermediate)20 b(results)g(must)e(be)g
(\223referenced\224)k(and)c(\223dereferenced.)-6 b(\224)22
b(Ho)n(we)n(v)o(er)l(,)d Fg(var)676 4156 y Fp(is)35 b(a)g(projection)k
(function,)h(and)c(its)g(reference)i(count)f(is)e(al)o(w)o(ays)h
(greater)i(than)e(0.)676 4269 y(Therefore,)24 b(there)h(is)e(no)h(call)
g(to)f Fo(Cudd)p 1929 4269 V 34 w(Ref)p Fp(.)585 4457
y Fn(\017)46 b Fp(The)24 b(ne)n(w)g Fg(f)f Fp(must)i(be)f(assigned)j
(to)e(a)f(temporary)j(v)n(ariable)f(\()p Fg(tmp)d Fp(in)h(this)h(e)o
(xample\).)676 4570 y(If)c(the)g(result)i(of)e Fo(Cudd)p
1408 4570 V 34 w(bddAnd)k Fp(were)c(assigned)i(directly)h(to)d
Fg(f)p Fp(,)f(the)i(old)f Fg(f)f Fp(w)o(ould)i(be)676
4682 y(lost,)h(and)h(there)h(w)o(ould)f(be)f(no)h(w)o(ay)f(to)h(free)g
(its)f(nodes.)585 4870 y Fn(\017)46 b Fp(The)23 b(statement)i
Fg(f)54 b(=)g(tmp)21 b Fp(has)j(the)g(same)g(ef)n(fect)g(as:)1897
5225 y(12)p eop
%%Page: 13 13
13 12 bop 1330 573 a Fg(f)54 b(=)g(tmp;)1330 686 y(Cudd_Ref\(f\);)1330
799 y(Cudd_RecursiveD)o(er)o(ef)o(\(ma)o(na)o(ge)o(r,)o(tm)o(p\);)676
1024 y Fp(b)n(ut)27 b(is)f(more)h(ef)n(\002cient.)39
b(The)26 b(reference)j(is)d(\223passed\224)j(from)e Fg(tmp)d
Fp(to)j Fg(f)p Fp(,)f(and)h Fg(tmp)d Fp(is)676 1137 y(no)n(w)f(ready)h
(to)g(be)f(reutilized.)585 1324 y Fn(\017)46 b Fp(It)32
b(is)h(normally)i(more)e(ef)n(\002cient)g(to)g(b)n(uild)i(BDDs)c
(\223bottom-up.)-6 b(\224)35 b(This)e(is)g(why)f(the)676
1437 y(loop)22 b(goes)g(from)f(3)g(to)g(0.)28 b(Notice,)22
b(ho)n(we)n(v)o(er)l(,)g(that)g(after)g(v)n(ariable)h(reordering,)h
(higher)676 1550 y(inde)o(x)32 b(does)f(not)h(necessarily)i(mean)d
(\223closer)i(to)e(the)h(bottom.)-6 b(\224)31 b(Of)g(course,)j(in)d
(this)676 1663 y(simple)24 b(e)o(xample,)g(ef)n(\002cienc)o(y)g(is)g
(not)g(a)f(concern.)585 1851 y Fn(\017)46 b Fp(Had)31
b(we)g(w)o(anted)h(to)g(conjoin)i(the)e(v)n(ariables)h(in)f(a)f
(bottom-up)j(f)o(ashion)g(e)n(v)o(en)e(after)676 1963
y(reordering,)26 b(we)c(should)j(ha)n(v)o(e)f(used)g
Fo(Cudd)p 2074 1963 28 4 v 34 w(ReadIn)l(vP)-7 b(erm)p
Fp(.)30 b(One)23 b(has)g(to)h(be)f(careful,)676 2076
y(though,)28 b(to)e(\002x)f(the)i(order)g(of)f(conjunction)j(before)f
(entering)g(the)e(loop.)38 b(Otherwise,)676 2189 y(if)33
b(reordering)j(tak)o(es)e(place,)i(it)d(is)h(possible)h(to)e(use)h(one)
f(v)n(ariable)i(twice)f(and)g(skip)676 2302 y(another)25
b(v)n(ariable.)448 2551 y Fh(3.8)99 b(Basic)25 b(ADD)g(Manipulation)448
2726 y Fp(The)f(most)f(common)h(w)o(ay)g(to)f(manipulate)j(ADDs)c(is)i
(via)g Fo(Cudd)p 2521 2726 V 34 w(addApply)p Fp(.)31
b(This)23 b(function)448 2839 y(can)35 b(apply)g(a)e(wide)h(v)n(ariety)
h(of)f(operators)i(to)e(a)f(pair)h(of)g(ADDs.)58 b(Among)34
b(the)g(a)n(v)n(ailable)448 2951 y(operators)27 b(are)d(addition,)i
(multiplication,)h(di)n(vision,)f(minimum,)d(maximum,)h(and)g(boolean)
448 3064 y(operators)i(that)e(w)o(ork)g(on)g(ADDs)e(whose)i(lea)n(v)o
(es)g(are)g(restricted)i(to)e(0)f(and)h(1)f(\(0-1)h(ADDs\).)589
3177 y(The)g(follo)n(wing)h(fragment)g(of)f(code)h(illustrates)h(ho)n
(w)d(to)h(b)n(uild)h(the)f(ADD)e(for)i(the)g(func-)448
3290 y(tion)38 b Fo(f)c Fl(=)20 b Fp(5)p Fo(x)861 3304
y Ff(0)899 3290 y Fo(x)939 3304 y Ff(1)977 3290 y Fo(x)1017
3304 y Ff(2)1054 3290 y Fo(x)1094 3304 y Ff(3)1132 3290
y Fp(.)885 3478 y Fg(DdMan