Use of BDDs for Verification

Use of BDDs for Verification

0

X1

X2

X2

X3

X3

1

0

1

1

f = X1.X2 + X3

f1 = 1

f2 = X3

f3 = X2' X3 + X2

m In general: fv = Xv' flow + Xv fhigh

Ô Shannon decomposition of f at Xv

low child

high child

V1

V2

V3

Previous slide

Next slide

Back to the first slide

View Graphic Version